OK Labs announced a partnership with security IT firm Galois to develop and commercialize ultra-secure communications, data processing, and control systems based on the OKL4 hypervisor. Initially designed for virtual cohabitation with Linux, Android, and embedded RTOSes on secure mobile and other embedded devices, the solutions will meet standards including EAL5-EAL7, says OK Labs.

In January, OK Labs (Open Kernel Labs) announced the availability of a verified, secure, "bug-free" OKL4 Verified microkernel" version of its OKL4 hypervisor. Developed in partnership with NICTA (National Information and Communications Technology Australia), as well as the University of New South Wales (UNSW) and other institutions, OKL4 Verified is designed for business-critical and mission-critical applications in mobile/wireless devices, according to the company.

Now, OK Labs and security-oriented "technology transition" firm Galois say they'll collaborate on specific commercial implementations of the technology. The solutions will span communications, data processing, and control applications, including "augmenting the security of systems in applications from software-defined radio to financial services, and medical and mobile/wireless devices," says OK Labs.

The jointly developed solutions will "support extremely high levels of assurance, correctness and risk management for government agencies and contractors, device OEMs, network operators, software developers and integrators." In addition, the technology will comply with evaluation, certification, and accreditation standards including Common Criteria EAL5-EAL7 and the emerging NIST SP 800-53 Risk Management Framework, says OK Labs.

Early targets include Linux, Android

OKL4 Verified offers both a secure execution environment for trusted applications on its own, or can act as a mobile/embedded virtualization platform, says the company. In the latter role, it is said to play host to a range of guest operating systems, "such as Linux and Android and traditional embedded real-time operating systems (RTOSes)."

Portland, Oreg.-based Galois touts customers including the "DoD, DoE, Intelligence, as well as the medical and aerospace communities." The company has developed and hosts a large number of open source libraries for the mathematically-oriented, "purely functional" Haskell programming language. Galois' many software offerings include the Haskell Lightweight Virtual Machine (HaLVM), a port of the GHC (Glasgow Haskell Compiler) runtime system to the Xen hypervisor, allowing programmers to create Haskell programs that run directly on Xen's 'bare metal' implementation, says the company.

Other Galois solutions include its SELinux-based Trusted Services Engine (TSE), a network-enabled software appliance based on web standards. "Copilot," meanwhile, is billed as a domain-specific, embedded stream language for generating hard real-time C code.

Among other security offerings, Galois offers "Cryptol," a domain-specific language (DSL) and tool suite that is touted for simplifying the specification of a cryptographic algorithm and then compiling the spec into the VHDL chip layout language.

Stated Laura McKinney, CEO, Galois, "Partnering with OK Labs lets Galois build assurance arguments on OKL4 Verified, enabling higher levels of assurance than previously possible, which increases customers' confidence in their most trusted systems."

Stated Carl Nerup, VP Business Development, OK Labs, "Our collaboration yields unique capabilities for building and deploying mission-critical applications that meet strict federal, military, and civilian agency requirements, and imbuing business-critical enterprise and mobile apps with comparable security and assurance."

Availability

OKL4 Verified is available for free download for non-commercial evaluation on embedded ARM11 or x86 platforms, here.

This article was originally published on LinuxDevices.com and has been donated to the open source community by QuinStreet Inc. Please visit LinuxToday.com for up-to-date news and articles about Linux and open source.