The OKL4 Microkernel and Microvisors have for a long time been trusted to run many high security and high reliability systems. Not to mention being deployed in over a billion mobile phones. OKL4 has become synonymous with secure and trusted systems.

The OKL4 Ironvisor is our latest and most secure Separation Kernel and Hypervisor to date. Based on the OKL4 Microvisor, it has a reduced API and supports highly locked down and constrained partitions.

Like the Microvisor, the Ironvisor supports mutual distrust, separation of concerns and multi-domain systems, including mixing of classified and unclassified systems in a single device. It supports any OS running on the ARM platform, including Linux, FreeBSD, QNX, various RTOSes, as well as supporting light-weight execution environments (LWEEs) allowing bare metal code to run in its own partition directly on top of the separation kernel.

The OKL4 Ironvisor gives you a flexible, minimal platform with a small trusted computing base (TCB) which lends itself to certification and verification. It is designed from the ground up for secure systems and features the OKL4 Capabilities, a mandatory access control (MAC) system, and strong and static resource isolation.

The kernel is specially hardened against attack by design, going as far as removing all code related inter-domain communication and dynamic management of resource partitioning. Partitioning is instead run once during system deployment and the configuration frozen into the system image. It is an attractive choice for those considering kernels such as seL4 but without the rich API requirements or cost in time and dollars required in re-verification of the deployed system. Its small API and code size (only 26KB on ARMv7ve) make it suitable for traditional certification approaches.

The OKL4 Ironvisor is currently being deployed in some of the most secure and hardened devices anywhere, and is available immediately for evaluation and licensing through Cog Systems.