The assurance story for seL4 on RISC-V https://riscv.org/keeps building.
We first formally proved functional correctness: that the seL4 C code on RISC-V platforms behaves exactly as its specification says https://microkerneldude.wordpress.com/2020/06/09/sel4-is-verified-on-risc-v/. We then established binary correctness: that the machine code running on the processor behaves exactly as the C code, and by extension, as the specification says https://microkerneldude.wordpress.com/2021/05/05/sel4-on-risc-v-verified-to-binary-code/. We now have established the crucial integrity property for seL4 on RISC-V: that the specification, and by extension the kernel binary, prevents an application running on top from modifying data without authorisation. In seL4 speak: seL4 provably enforces capability-based access control.
“The integrity property is crucial for security: it is key to enforce the isolation of components running on top of the kernel”, says Gerwin Klein, seL4 verification expert and chair of the seL4 Foundation technical steering committee. “This is what allows critical components, like the network controller that has access to software-controlled brakes in a modern car, to securely run alongside untrusted software, like the entertainment system. With integrity proved, you know that an attack on or from a vulnerable untrusted part of the system cannot compromise the critical parts.”
Integrity had been proved in the original seL4 verification on the Arm32 architecture. It is now also established for RISC-V architecture, making it the only 64-bit architecture that has an OS with such a comprehensive verification and security story. We thank Ryan Barry https://trustworthy.systems/people/?cn=Ryan+Barry of Trustworthy Systems, main author of these proofs! We also gratefully acknowledge funding from the Australian Reseach Council https://www.arc.gov.au/ through grant DP190103743 which has enabled this work.
See Gernot's blog https://microkerneldude.wordpress.com/2021/08/04/sel4-integrity-enforcement-proved-for-risc-v/ for more details. The proof is available on GitHub https://github.com/seL4/l4v/tree/master/proof/access-control.
June