
International Day of Families at HENSOLDT Cyber
International Day of Families at HENSOLDT Cyber Interview with Markus Wolf, Sascha Fedderwitz, Emilia Fries We asked some of our colleagues a few questions on
Simone Rudow, Head of Marketing & PR at HENSOLDT Cyber
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 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
International Day of Families at HENSOLDT Cyber Interview with Markus Wolf, Sascha Fedderwitz, Emilia Fries We asked some of our colleagues a few questions on
How to mitigate hardware attacks? Written by Maja Malenko, Hardware Researcher at HENSOLDT Cyber In the final blog post of our hardware security trilogy, we
Is Hardware Reverse Engineering a Real Threat? Written by Maja Malenko, Hardware Researcher at HENSOLDT Cyber Today we are continuing the story of hardware security
Hardware Security: HENSOLDT Cyber’s MITHRIL Project Written by Maja Malenko, Hardware Researcher at HENSOLDT Cyber Creating secure hardware is a challenging task, especially in times
Successful ISO 9001:2015 certification We are pleased to announce that after eight months of hard work, preparation, and intensive teamwork, HENSOLDT Cyber has certified its
Hello Secure World – How to build and run your first secure TRENTOS® system Building on our first video session in which we took a
LEGAL:
CONTACT US:
FOLLOW US ON:
HEADQUARTER POSTAL ADDRESS:
OUR OFFICE IS LOCATED HERE: