Taufkirchen, Germany, May 5th 2021 – German cybersecurity company HENSOLDT Cyber in partnership with CSIRO, has 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 the 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. HENSOLDT Cyber is continually working with its 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: https://hensoldt-cyber.com/mig-v
About HENSOLDT Cyber
Founded in 2018, HENSOLDT Cyber GmbH is a German Corporate Start-up company based in Taufkirchen near Munich that develops embedded information technology products meeting the highest security requirements. These integrate a highly secure operating system with security hardened hardware, thus creating a secure IT instead of IT security for the global IT market. The company combines more than 50 years of experience in defense and security electronics of the HENSOLDT Group with academic world-class expertise in hardware and software development. HENSOLDT Cyber currently employs over 50 people at various locations.
Further information about the company can be found at www.hensoldt-cyber.com
Contact for press inquiries, pictures and article requests
Simone Rudow
Head of Marketing & PR
Tel.: +49 (0) 174 218 8102
simone.rudow@hensoldt-cyber.com
