Extended Trustworthiness through binary verification of seL4® microkernel on RISC-V® processor architecture

Simone Rudow, Head of Marketing & PR at HENSOLDT Cyber

German cybersecurity company HENSOLDT Cyber in partnership with CSIROhas announced the release of an automated tool for binary verification of the seL4 microkernel with respect to the 64-bit RISC-V processor architecture.

“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

READ MORE
Allgemein
Cyber2020

Formal Verification

Formal Verification By Dr. Jacob Boender, Formal Verification Engineer at HENSOLDT Cyber GmbH One of the specialties of HENSOLDT Cyber is *formal verification*. This may

Weiterlesen »

Be the first to hear about our products and innovations!

Share on facebook
Share on linkedin
Share on email

Leave a Reply

Your email address will not be published. Required fields are marked *