seL4 operating system protects critical systems on RISC-V architecture from cyber-attacks

Organisations around the world are developing processors based on the open RISC-V instruction-set architecture (ISA), targeting diverse platforms ranging from embedded and cyberphysical systems to high-end servers. Many will be built into safety- and security-critical systems. Now, these systems can be protected from cyber attacks by the world’s most secure operating system.
CSIRO’s Data61, the data and digital specialist arm of Australia’s national science agency, today announced the completion of the proof of implementation correctness of the open-source seL4 microkernel for the RISC-V ISA. The development means that seL4’s unprecedented security enforcement is now available to the global and rapidly-growing RISC-V ecosystem.
Dr Rafal Kolanski, Leader of the Proof Engineering Team of Data61’s Trustworthy Systems Research group said, “We aim to shift the software industry away from ad-hoc, unreliable engineering practices, and towards principled approaches based on the fundamentals of mathematics. Verification will become the default choice where safety or security are at stake and the verification of seL4 on the RISC-V architecture is an important milestone.”
seL4 was originally verified for 32-bit Arm processors used in ubiquitous in mobile devices, and later for 64-bit Intel processors that dominate mainstream computing. “This is a big step for seL4,” said 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 GmbH invested in the RISC-V verification of seL4 to complement their own, highly-secure RISC-V processor designed to protect defence systems, smart factories, autonomous vehicles, and critical infrastructure from cyber attacks.
Marian Rachow, Managing Director, HENDSOLDT Cyber said, “We funded this work because we believe that seL4, being open source and the most secure microkernel, and RISC-V as an open and secure processor architecture, are the best foundation for secure systems. Open source for secure systems will be the core strategy of HENSOLDT Cyber. 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.”
Data61 joined RISC-V International in 2018 to actively participate in the global collaboration on the open Arm architecture.
Krste Asanovic, Chairman of the RISC-V International Board of Directors said, “Advances in software and hardware standardization through global collaboration and consensus as well as open-source development and delivery of software and hardware design, have accelerated technical progress at an unprecedented global scale. We look forward to witnessing the adoption of seL4 in the global RISC-V community.”
News release contact
Sophia Aiano, Sling & Stone
0475 302 080
sophia@slingstone.com
About seL4
An Australian innovation, seL4 is the world’s first operating system (OS) kernel that is mathematically proved 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 growing list of deployments range from defence systems to autonomous air and ground vehicles, safeguarding them from cyber threats.
About CSIRO’s Data61
CSIRO’s Data61 is the data and digital specialist arm of Australia’s national science agency. We are solving Australia’s greatest data-driven challenges through innovative science and technology. We partner with government, industry and academia, through the D61+ Network, to conduct mission-driven research for the economic, societal and environmental benefit of the country. Our research expertise includes artificial intelligence and machine learning, robotics, cybersecurity, privacy preserving technologies, blockchain and analytics.