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.”
For more details on binary verification of seL4 on RISC-V see Gernot’s blog:
seL4 on RISC-V Verified to Binary Code (and seL4 and RISC-V Foundations form an
alliance).
