CSIRO or the Commonwealth Scientific and Industrial Research Organization’s Data61 now has proof of implementation correctness of the open-source seL4 microkernel for the RISC-V instruction-set architecture (ISA).
The RISC-V ISA is offered under open source licenses that come without any additional charges or fees. As per Data61, several organizations are building on processors that are based on the open RISC-V ISA, focusing on platforms right from embedded and cyberphysical systems to high-end servers.
The progress in Data61’s development implies the availability of seL4’s security enforcement to the RISC-V ecosystem.
Dr. Rafal Kolanski, Leader of the Proof Engineering Team at Data61’s Trustworthy Systems Research Group, mentions that the company is looking forward to transitioning the software industry away from ad hoc and untrustworthy practices to principled approaches based on the fundamentals and essentials of mathematics.
He adds, “Verification will become the default choice where safety or security is at stake, and the verification of seL4 on RISC-V architecture is an important milestone.”
More about Data61’s seL4
Data61 promotes seL4 as the world’s pilot OS (operating system) kernel that has witnessed mathematically surety to be secure. It is also represented as one of the fastest and most technically progressed OS microkernels in the world.
Technically, the kernel is a piece of software that operates on the core of a given computer system and ensures factors such as overall security, reliability, and safety.
Interestingly, seL4’s list of deployments extend from defense systems to autonomous air and ground vehicles with a definite aim of safeguarding them from cyber threats.
Originally verified for 32-bit Arm processors deployed in mobile devices, seL4 was later deployed for 64-bit Intel processors that dominate mainstream computing.