The Commonwealth Scientific and Industrial Research Organisation’s (CSIRO) Data61 has completed the proof of implementation correctness of the open-source seL4 microkernel for the RISC-V instruction-set architecture (ISA).
Unlike most other ISA designs, the RISC-V ISA is provided under open source licences that do not require fees. According to Data61, many organisations are developing processors based on the open RISC-V ISA, targeting platforms ranging from embedded and cyberphysical systems to high-end servers.
Data61’s development means that seL4’s security enforcement is now available to the RISC-V ecosystem.
“We aim to shift the software industry away from ad-hoc, unreliable engineering practices, and towards principled approaches based on the fundamentals of mathematics,” leader of the proof engineering team of Data61’s Trustworthy Systems Research group Dr Rafal Kolanski said.
“Verification will become the default choice where safety or security are at stake and the verification of seL4 on RISC-V architecture is an important milestone.”
Data61 touts seL4 as the world’s first operating system (OS) kernel that has been mathematically proven to be secure and is the world’s fastest and most advanced OS microkernel.
The kernel is the piece of software that runs at the core of any computer system and is responsible for ensuring overall security, safety, and reliability. SeL4’s list of deployments range from defence systems to autonomous air and ground vehicles, with the overarching goal of safeguarding them from cyber threats.
SeL4 was originally verified for 32-bit Arm processors used in mobile devices, and later for 64-bit Intel processors that dominate mainstream computing.
The Linux Foundation announced in April it had partnered with Data61 to push forward with work on the security-first operating system kernel.
While seL4 is not related to Linux, seL4 can be used, in theory, as a foundation for Linux and other Unix related operating systems.
“This is a big step for seL4,” added Professor Gernot Heiser, chairman of the seL4 Foundation that is tasked with growing the seL4 ecosystem. “This proof makes seL4’s unrivalled security enforcement available to the fastest-growing hardware ecosystem, and now covers all major computer architectures.”
German security company Hensoldt Cyber previously invested in the RISC-V verification of seL4 to complement its own RISC-V processor that was designed to protect defence systems, smart factories, autonomous vehicles, and critical infrastructure from cyberattacks.
On Tuesday, Hensoldt CEO Marian Rachow said the company has funded the work underway by Data61 as it believes seL4, being open source and the most secure microkernel, and RISC-V as an open and secure processor architecture, could become the best foundation for secure systems.
“Open source for secure systems will be the core strategy of Hensoldt Cyber,” Rachow said. “Now it is important to make these technologies accessible to the broad market. Our TRENTOS-M SDK, based on the seL4 microkernel, is the first step towards a secure ecosystem.”
Meanwhile, Professor Krste Asanovic, chairman of the RISC-V Foundation said he was looking forward to seeing the adoption of seL4 in the global RISC-V community.
