mCertiKOS Hypervisor

mCertiKOS is a fully verified hypervisor using CertiKOS framework.

• mCertiKOS hypervisor consists of 5500 lines of C and x86 assembly, and can boot a version of Linux as a guest.
• mCertiKOS hypervisor is divided into 40 layers.
• mCertiKOS runs on the Landshark UGV and the American-Built Car platforms.

Variants of mCertiKOS Kernels

We built 3 variants of mCertiKOS certified OS kernels.

• mCertiKOS-base: a certified traditional kernel.
• mCertiKOS-rz: support ring-0 certified process.
• mCertiKOS-emb: a certified embedded system.

Macro Benchmarks

Normalized macro benchmarks: Linux on KVM and CertiKOS, baseline is Linux on bare metal.

LMbench

Normalized macro benchmarks: Linux on KVM and CertiKOS, baseline is Linux on bare metal.

IPC Performance

The IPC performance between mCertiKOS-base and seL4 on x86.

---

Acknowledgements

This project is sponsored by NSF grants 1065451, 1521523, and 1319671, DARPA grants FA8750-16-2-0274 and FA8750-15-C-0082, DARPA CRASH grants FA8750-10-2-0254, and DARPA HACMS grants FA8750-12-2-0293. Any opinions, findings, and conclusions contained in this document are those of the authors and do not reflect the views of these agencies.