Performance Impacts from the seL4 Hypervisor

Hypervisor technologies are often presented as offering a high degree of separation at the cost of performance. Is this too expensive for embedded systems? The cost of performance has been shrinking year after year as new advancements in virtualization technologies are baked into processors. When a hypervisor couples hardware assisted virtualization with device emulation, it makes current systems portable, future proof, and extends the life of legacy systems.

seL4 is a perfect fit for the high assurance embedded hypervisor space. The open source seL4 microkernel is the first formally verified microkernel built with security and performance in mind. The mathematical proof of seL4 provides unprecedented assurance at the lowest, most critical software level.

This paper investigates the overheads associated with using seL4 as a hypervisor on ARM and x86 platforms, providing synthetic and real-world benchmarking methodology and results.

Citation: J. Millwood, R. VanVossen, L. Elliott, “Performance Impacts from the seL4 Hypervisor”, In Proceedings of the Ground Vehicle Systems Engineering and Technology Symposium (GVSETS), NDIA, Novi, MI, Aug. 13-15, 2020.