The first RISC-V port of the seL4 microkernel was last week released by the Data61 division of the Australian government's Commonwealth Scientific and Industrial Research Organisation (CSIRO).
seL4 is an open-source and highly secure version of the L4 microkernel that aims to be mathematically proven to be bug free, in that it works as expected as per its specifications. Meanwhile, RISC-V is an open-source instruction-set architecture, and is used as the blueprint for various open-source processor core designs – some of which are now shipping as real usable silicon, such as chips from SiFive and Greenwaves.
The first release of the port is a prototype: it is 64-bit-only, there is no floating-point math hardware support, and it runs only in the Spike CPU simulator. The effort was started by Hesham Almatary as a Google Summer of Code project for RISC-V system-on-chip designers lowRISC, and continued when Almatary joined CSIRO and next the University of New South Wales in Australia.
As part of its RISC-V efforts, CSIRO has joined the RISC-V Foundation, so as to have a seat at the table as the fledgling processor architecture takes shape.
Vulture South spoke to Data61 chief research scientist for trustworthy systems, Professor Gernot Heiser, about the seL4-on-RISC-V project.
“RISC-V has a lot of momentum behind it,” Heiser said, not just because the specification is open, but also because of the open reference implementations on offer. We note that Western Digital has also thrown its weight behind it, as has Nvidia and Google, as they search around for affordable customizable cores to glue their hardware together.
Researchers forge secure kernel from maths proofsREAD MORE
Its combination of “greenfield design on the back of experience” makes RISC-V a “very clean design,” he added.
As a platform for seL4, Heiser said, RISC-V is also an important alternative to the Intel and Arm architectures. For one thing, RISC-V is free and open-source technology for engineers to adopt and tweak as they need. Also, they do not suffer from the Meltdown-Spectre speculative execution design flaws, and even if they were affected, the blueprints are all there in the open to be fixed.
While seL4 runs on Arm-compatible processors, its original platform, and since then Intel hardware – it's still going through the formal verification process on Chipzilla's CPUs – Heiser said porting the open-source microkernel to an open hardware platform is a natural next step. It means if anyone suspects there is a backdoor or a vulnerability in the processor design, the hardware design code can be inspected, analyzed, and verified.
And it means the designs can be improved directly by their users, rather than waiting for folks at Intel or Arm to get round to it. That's why the CSIRO wants to be part of the RISC-V foundation: “Some of the instruction set has not been finalised at all … it's important to take part so that we can have a say, and make sure seL4 is properly supported.”
Even though modern chips are dizzyingly complex, the openness of RISC-V means it's “more feasible to scrutinise,” he said. “In principle, we can analyse what's in the microarchitecture, and see how that could lead to security holes."
If you don't have a complete model of a CPU, he said, “it's very difficult, if not impossible, to analyse the processor.” Even for RISC-V, he said, “a lot of research is required” to systematically explore an architecture for vulnerabilities.
seL4 and L4 adoption has been a long process, Heiser told Vulture South – “it took eight years to get deployed to Apple devices, but it's now shipping hundreds of millions a year.”
By that, the professor means the L4 microkernel running on the Secure Enclave security coprocessor [PDF, p7] Apple builds into its most recent iPhones and iPads. That kernel has been tweaked by Apple to meet its needs.
Because it's a microkernel, seL4 needs a lot of work and extra code to turn it into a functioning system. A microkernel tries to do as little as possible so that as little possible can go wrong. All the system services and drivers run isolated in a layer above the microkernel, and can be restarted if something breaks, or upgraded if bugs need patching, without taking out the entire device.
“You get a lot of services with the Linux kernel,” Heiser said, whereas those services run in user-space alongside applications in an seL4 environment.
“There's nothing stopping us for having complete user level services available, but that hasn't happened yet,” Prof Heiser said. “We're keen to build an open source ecosystem,” he told us, because building seL4 into a complete operating system is “beyond the scope of what we can do ourselves.” ®