Genode Lab's Genode Operating System Framework
with Data61's seL4 Microkernel
running on physical ARM hardware.
This mission has led us to bringing together Genode and seL4 onto actual ARM hardware.
CTI would wish to thank Yevgeny Lavrov who led the effort to converge the two entities producing the results documented here. This advancement would not have been possible without his persistence and dedication.
Critical Technolgies Inc's high level mission is to be able to perform remote attestation of a system and to ensure secure boot of the hardware
and software on every power cycle. On x86 platforms this done via the Trusted Protection Module (TPM) using SABLE. However
this method does not translate to ARM based systems as no TPM chip is present. ARM's TrustZone, along with the seL4 Microkernel and Genode is CTI's answer to this
problem.
Using boards, such as the Raspberry Pi 3B and 3B+ and the
Xilinx Zynq UltraScale+ ZCU102 we hope to create enviroments in ARM that can be
equivalent to our work in the x86 world.
Created by Genode Lab's the Genode Framework is a high structured architecture for highly secure special-purpose operating systems. It's key feature is the sandboxing of every component with highly selected access rights and capabilities granting extremely high security across the entire system.
Created by Data61 the seL4 Microkernel is an open source kernel with end-to-end proof of implementation and security enforcement. It's strong capability based philosophy aligns well with Genode.
Various ARM boards were considered for this project. Ultimately it came down to
the boards that both seL4 and Genode supported. This narrowed down the selection to very few - but even still there was issues
getting both components to cooperate on the given hardware. However this was overcome on two boards.
The SABRE Lite
board from Boundry Devices and the Wandboard Quad from
Wandboard are the currently supported boards for this effort and are available at the links above.
