Brains behind seL4 secure microkernel begin RISC-V chip port

Unveil first code, join giants in industry-standards club

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 proofs


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.” ®

Similar topics

Broader topics

Narrower topics

Other stories you might like

  • RISC-V needs more than an open architecture to compete
    Arm shows us that even total domination doesn't always make stupid levels of money

    Opinion Interviews with chip company CEOs are invariably enlightening. On top of the usual market-related subjects of success and failure, revenues and competition, plans and pitfalls, the highly paid victim knows that there's a large audience of unusually competent critics eager for technical details. That's you.

    Take The Register's latest interview with RISC-V International CEO Calista Redmond. It moved smartly through the gears on Intel's recent Platinum Membership of the open ISA consortium ("they're not too worried about their x86 business"), the interest from autocratic regimes (roughly "there are no rules, if some come up we'll stick by them"), and what RISC-V's 2022 will look like. Laptops. Thousand-core AI chips. Google hyperscalers. Edge. The plan seems to be to do in five years what took Arm 20.

    RISC-V may not be an existential risk to Intel, but Arm had better watch it.

    Continue reading
  • RISC-V CEO seeks 'world domination' by winning over the likes of Intel
    We speak to the head of ISA's governing body on industry adoption, timelines, and more

    Interview The CEO of RISC-V's governing body says she wants to nothing less than "world domination" for the rising open-source processor technology, but to do that, the nonprofit needs buy-in from a variety of organizations, even those steeped in dominant, proprietary architectures, such as x86 giant Intel.

    In an interview this week with The Register, RISC-V International CEO Calista Redmond reckons the buy-in, which comes in the form of paid memberships, is needed to support ongoing development of the royalty-free CPU instruction set architecture to better compete with x86 and Arm ISAs.

    "We have to have a level of funding in order to operate and manage this special rodeo of ours," she says.

    Continue reading
  • GNU Compiler Collection adds support for China's LoongArch CPU family
    MIPS...ish is on the march in the Middle Kingdom

    Version 12.1 of the GNU Compiler Collection (GCC) was released this month, and among its many changes is support for China's LoongArch processor architecture.

    The announcement of the release is here; the LoongArch port was accepted as recently as March.

    China's Academy of Sciences developed a family of MIPS-compatible microprocessors in the early 2000s. In 2010 the tech was spun out into a company called Loongson Technology which today markets silicon under the brand "Godson". The company bills itself as working to develop technology that secures China and underpins its ability to innovate, a reflection of Beijing's belief that home-grown CPU architectures are critical to the nation's future.

    Continue reading

Biting the hand that feeds IT © 1998–2022