SAN FRANCISCO, May 5, 2021 – Today, the seL4 Foundation and RISC-V International announced that the verified seL4 microkernel on the RV64 architecture has been proved down to the executable code by CSIRO’s Data61, thanks to funding provided by HENSOLDT Cyber GmbH. This guarantees that the seL4 microkernel on RV64 will operate to specification even when built with an untrusted C compiler, GCC.
Within and across open collaboration communities it is essential to work together on areas of mutual interest. RISC-V and seL4 are pleased to announce their progress and their alliances as they join forces to enable stronger overall security, combining security-oriented architecture and operating system design.
“We are excited to be one of the first architectures with secure operating system kernels with such a strong formal verification story,” said Mark Himelstein, CTO of RISC-V International. “RISC-V is continuing to increase the security features that encompass the ISA and the secure seL4 kernel is a natural complement.”
“This is another milestone for seL4, which continues to define the state of the art in OS security,” added Prof Gernot Heiser, Chairman of the seL4 Foundation. “Stronger aligning the two open ecosystems makes a lot of sense.”
“The verified seL4 microkernel forms the core of TRENTOS, our secure operating system for our MiG-V chip, a RISC-V processor with supply chain security”, said Sascha Kegreiß, CTO of HENSOLDT Cyber GmbH. “This unique combination of hardware and software security can protect critical assets from advanced persistent cyber threats.”
“Translation validation ties all of our verification efforts together,” said Dr Zoltan Kocsis, CSIRO Verification Engineer. “Bringing translation validation to a modern, 64-bit processor presented significant scalability challenges but, in the end, we were able to overcome them.”
More on RISC-V Alliances can be found here: https://riscv.org/community/alliances/
###
About RISC-V International
RISC-V is a free and open ISA enabling a new era of processor innovation through open collaboration. Founded in 2015, RISC-V International is composed of more than 1,300 members building the first open, collaborative community of software and hardware innovators powering a new era of processor innovation. The RISC-V ISA delivers a new level of free, extensible software and hardware freedom on architecture, paving the way for the next 50 years of computing design and innovation.
RISC-V International, a non-profit organization controlled by its members, directs the future development and drives the adoption of the RISC-V ISA. Members of RISC-V International have access to and participate in the development of the RISC-V ISA specifications and related HW / SW ecosystem.
About the seL4 Foundation
The seL4 microkernel is the world’s first operating system kernel with a machine-checked correctness proof of its implementation, and has further proofs of security enforcement. In addition to its unique assurance, it features unbeaten performance. The source code of seL4, as well as all proofs, are open-source under the GPL V2 license.
The seL4 Foundation is a global, independent and neutral non-profit organization for funding and steering the future evolution of seL4. It is set up under the Linux Foundation, tasked with accelerating the development of seL4 and related technologies.