High Assurance Systems via the Open Source seL4 Microkernel and Open RISC-V Processor

The seL4 microkernel provides significant cybersecurity benefits, mainly due to its formal proof and the fact that it is open source software. The formal proof ensures that the microkernel behaves exactly as expected, which results in a much higher basis for security. An open source license provides seL4 users with a much less expensive solution and many eyes focused on the development. One limitation of the current hardware that seL4 runs on is that it is closed, which makes it much harder to validate proof assumptions for the hardware. RISC-V has an open ISA, which gets around this issue. With open source software and open hardware combined, developers know exactly what is in their system and makes it much easier to certify their solution. We want to make improvements to the ecosystem by productionizing seL4 on standard RISC-V processors, by expanding the development tools, by adding some key new features, and by planning on EAL6+ Common Criteria certification. Our work will be a significant step towards our ultimate goal of a proven software-hardware combination that provides end-to-end guarantees of trusted computing, provably avoiding classes of errors in software or hardware that traditionally been fixed via patch and pray methods.