“The verified seL4 microkernel forms the basis of TRENTOS®, the secure operating system for MiG-V, a RISC-V processor with supply chain security. This unique combination of hardware and software security can protect critical IT systems from APTs,” said Sascha Kegreiß, CTO of HENSOLDT Cyber.   

 HENSOLDT Cyber increases the trustworthiness of this hardware and software combination by working with CSIRO’s Data61 to mathematically prove that the binary code of the seL4 microkernel is the correct translation of its source code. This reliability was achieved by mapping both the binary and source code into a common intermediate language, before verifying equivalence with automated theorem provers.  

Binary verification eliminates the need to trust the deployed compiler. Compilers can introduce faults or unintended behavior, which in turn can be exploited by attackers. These errors are not identifiable by formal verification of the source code; the process must therefore extend to the binary code to rule out faults in the deployed software. With binary verification, we have proof that everything guaranteed by the source code also applies to the binary code, since the automatic theorem provers have verified that they are indeed equivalent.  

RISC-V is the first 64-bit architecture for which binary verification of an operating system has been achieved. This makes seL4 the first fully formally verified core for a 64-bit processor. By combining an openly available and testable processor architecture with a formally verified operating system kernel, seL4 on RISC-V offers the most comprehensive security approach yet achieved by a processor. The process ensures that the program code written and proved correct by the seL4 community (organized in the seL4 Foundation) has been compiled error-free for the RISC-V architecture and is thus available as a verified binary.  

“This is an important step, it strengthens seL4’s position as defining the state of the art in secure operating systems “, said Prof. Gernot Heiser, Chairman of the seL4 Foundation.  

Dr Zoltan Kocsis, CSIRO Verification Engineer said: “Translation validation ties all of our verification efforts together. Bringing translation validation to a modern, 64-bit processor presented significant scalability challenges but, in the end, we were able to overcome them.”  

Trustworthiness is the core value at HENSOLDT Cyber, which manifests itself in our corporate vision “Secure IT instead of IT security”. Secure IT must be verifiably secure; for this, the binary verification of seL4 on RISC-V represents an important step. As HENSOLDT Cyber, we are constantly working with our partners to raise the individual components of its solutions to unprecedented levels of security, so that it can easily provide its customers with the resulting security features.  

For more information about HENSOLDT Cyber’s MiG-V