your Windows® embedded community
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, AndroidOKL4 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.-basedGalois 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."
Background
OKL4's microkernel OS runs almost everything in userspace, and includes a thin hardware abstraction layer that can support Windows Mobile, Windows CE, Linux, Symbian, and/or other guest OSes. It also includes a minimal POSIX-compliant execution environment, enabling multiple applications and device drivers to run in separate, isolated partitions.
OKL4 provides for decreased BOM (bill of materials), as well as the separation of GPL and proprietary software code as required by companies' intellectual property policies, claims OK Labs.
Availability
OKL4 Verified is available for free download for non-commercial evaluation on embedded ARM11 or x86 platforms, here.