A DoD customer was interested in using seL4 as a hypervisor to provide robust security and isolation and they wanted to run on the latest ARMv8 platform, due to its performance and feature set. The hypervisor allows the customer to adapt legacy drivers and applications on operating systems that they are already using, while improving security with the formally proven seL4 microkernel. However, seL4’s VMM mode was not implemented on ARMv8 platforms.
The ARMv7 specification included extensions for hardware virtualization on 32-bit ARM platforms. However, whether or not it was included was implementation defined, which made it more difficult to know if any particular ARMv7 platform had virtualization support or not. ARMv8, a more recent specification, however was written with virtualization in mind, and all ARM platforms that support ARMv8 also support virtualization. This made ARMv8 a great fit for seL4 virtualization.
DornerWorks ported the existing ARMv7 virtualization support to an ARMv8 implementation. DornerWorks provided BSP layers for the Xilinx Zynq UltraScale+ MPSoC and the NXP i.MX8 platforms. DornerWorks was also responsible for a new GIC500 driver, virtual UART drivers, an SMMU driver, VCPU support, 2-stage translation support in the MMU driver, and a virtual channel implementation to allow VMs to communicate. DornerWorks also provided an example configuration of a VMM system for each platform.
Using seL4 VMM mode on an ARMv8 platform resulted in a prototype that showed the isolation benefits that the customer required on the platform they needed. DornerWorks has also open-sourced all of this work on Github.