Brains behind iOS’ secure microkernel start moving it to RISC-V
Last week, the Data61 division of Australia’s Commonwealth Scientific and Industrial Research Organisation (CSIRO) released the first RISC-V version of its seL4 microkernel.
Sel4 has been a long-term project dating back to when Data61 was still its own agency (NICTA, National ICT Australia), and built a “provably-secure” microkernel. It later spun out the project as Open Kernel Labs, and launched the open source version of seL4 in 2014.
As part of its RISC-V plans, the CSIRO has joined the RISC-V foundation, so as to have a seat at the table as the foundation develops the ISA specification of the processor architecture.
Vulture South spoke to Data61 chief research scientist for trustworthy systems, professor Gernot Heiser, about the seL4-on-RISC 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.
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.
As the Meltdown/Spectre speculative execution design flaws showed, hardware bugs can be catastrophically disruptive, hard to identify, and hard to fix.
While seL4 runs on ARM (its original platform) and since then Intel hardware (it’s still going through the formal verification process on Chipzilla devices), Heiser said porting the microkernel to an open hardware platform is a natural next step.
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 s that we ca 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,” he said.
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 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”.
In Apple phones, the microkernel forms the basis of the secure enclave that helps secure the device against unauthorised access.
Because it’s a microkernel, seL4 needs a lot of work to turn it into a functioning system: “you get a lot of services with the Linux kernel”, Heiser said, and those are created in userspace in an seL4 environment.
“There’s nothing stopping us for having complete user level services available, but that hasn’t happened yet,” 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”. ®
Sponsored:
Minds Mastering Machines – Call for papers now open
Article source: http://go.theregister.com/feed/www.theregister.co.uk/2018/04/23/csiros_data61_eyes_new_target_for_ultrasecure_kernel_riscv/