Data61 ports seL4 microkernel to RISC-V architecture

Data61 has released an initial version of the seL4 microkernel for the RISC-V architecture

The port is only in prototype stage and according to release notes “currently only supports running in 64-bit mode without FPU or multicore support on the Spike simulation platform.”

“There is no verification for this platform,” the release notes add.

The open source seL4 kernel was developed to be highly secure. It was the first general-purpose operating system kernel formally proved correct against its specification.

The microkernel was originally developed by NICTA, with custodianship passed on to Data61’s Trustworthy Systems Group after the NICTA-CSIRO merger. seL4 is owned by General Dynamics C4 Systems.

The CSIRO said today that it had joined the RISC-V Foundation and intends to participate in the ongoing development of the RISC-V open instruction set architecture.

“RISC-V, through its openness and greenfield design, provides an opportunity for re-thinking the hardware-software stack,” said Professor Gernot Heiser, chief research scientist for Data61’s Trustworthy Systems Group

“The open architecture, which is designed by leading architects and has strong industry support, is an ideal platform for our open-source seL4 system,” Heiser said in a statement.

“We anticipate the combination of seL4 and RISC-V to provide a compelling security solution for the next-generation Internet of Things and cyber-physical systems.”

“The seL4 microkernel is one of our flagship achievements that is being designed into safety- and security-critical systems around the world,” said Data61’s CEO Adrian Turner.

“Our involvement with the RISC-V Foundation will further increase the international impact of Data61’s research and development.”