seL4 is verified on RISC-V!

by Gernot Heiser, CSIRO/Data61 Sounds great! But what does it mean?

seL4

seL4 (pronounced ess-e-ell-four) is arguably the world’s most secure operating system (OS) kernel.  The OS kernel is the lowest level of software running on a computer system. It is the code that executes in privileged mode (S-mode in RISC-V; M-mode is reserved for microcode/firmware).  The kernel is ultimately responsible for the security of a computer system.  seL4 is a microkernel. The idea of a microkernel is to minimise the trusted computing base – the part of the system for which there is no Plan B if it fails. The Linux and Windows kernels consist of tens of millions of lines of code, and contain literally thousands (more likely tens of thousands) of bugs – a huge attack surface. A well-designed microkernel, such as seL4, has about ten thousand lines – inherently more trustworthy. What sets seL4 aside from all other OS kernels, including other microkernels, is its verification story. It was the world’s first OS kernel with a machine-checked, mathematical proof of the functional correctness of its C implementation (winning us a Hall of Fame Award as a result). This means that it is proved to be bug-free relative to a specification formulated in a mathematical logic. And by now it has proofs about further security properties (which show that the specification has the right properties) and functional correctness extending down to the binary code. And it has the most advanced support for hard real-time systems. And it is the world’s fastest microkernel. It’s best in class by any definition. We originally verified seL4 for 32-bit Arm processors. We then extended that to 64-bit x86 processors. And now to RISC-V RV64 processors. Which now covers all the important ISAs.

seL4 on RISC-V

But the combination of seL4 and RISC-V is special. RISC-V is an open instruction-set architecture (ISA). seL4 is an open-source OS microkernel. It’s a match made in heaven. Especially in terms of security.  When we verify seL4, we have to assume that the hardware operates correctly (i.e. as specified). That assumes that there is an unambiguous specification in the first place, which is not the case for all hardware. But even where there is such a specification, and it is formal (meaning ritten in a mathematical formalism that supports mathematical reasoning about its properties), how do we know that it actually captures the behaviour of the hardware? Reality is we can be pretty sure that it does not. Hardware is no different from software in that both have bugs. But having an open ISA has advantages that go beyond being free of royalties. One is that it allows having open-source hardware implementations. An example of this is the CV64 (formerly Ariane) core developed at ETH Zurich. With an open-source implementation, you see what you get, and can check for yourself whether it has security-critical bugs. This is what German company HENSOLDT Cyber GmbH did: they produced a chip, based on Ariane, with a strong supply-chain security story. And, to complement this with a secure OS, funded the verification of seL4 on RISC-V. [Disclaimer: I have an interest in HENSOLDT Cyber.] The most exciting aspect of an open ISA with open-source hardware implementations is the prospect of verifying the implementations. This sounds like a big ask that will be hard to realise. But the same was said about a verified OS kernel – until we did it. I know there are multiple groups working towards this goal, and sooner or later one of them will succeed. This will be a revolutionary step towards achieving real security, and I bet it’s only a few years away!

Hardware-software co-design for security

Open-source hardware with a verified, open-source OS is a great thing for security, but there is more. The combination of open ISA, open-source OS and open-source hardware enables innovation at the hardware-software interface that was previously reserved for hardware manufacturers (and thus happened at a snail’s pace). This is really important for security. We are all aware of Spectre attacks, which use side effects of speculative execution to steal secrets. What is less understood is that speculative execution on its own is not enough. Spectre needs a covert timing channel to get the information out. Without the covert timing channel there is no Spectre attack. Preventing these covert timing channels happens to be something we’ve been working on for a few years. We developed OS mechanisms for preventing them, but only to realise that they don’t quite work. Digging deeper, we found that this is because the hardware doesn’t give us the right mechanisms. In other words, most existing hardware is broken in terms of security! And the underlying cause is the ISA, which is our hardware-software contract. The ISA specifies functionality of the hardware, but intentionally abstracts away anything to do with time. But timing can be used to leak information, and the ISA does not provide the means for stopping this. As such, the ISA is insufficient for ensuring security, and must be improved. This would normally be hopeless endeavour: trying to convince hardware manufacturers to agree to a new contract that imposes additional restriction on what they can do. (Trust me, I’ve tried!) Or even provide the OS with an extra instruction it can use to defeat covert channels – as long as the house is not on fire, they are unlikely to listen. And the Spectre fire is apparently not burning hot enough yet. Open hardware changes this. It enables us to innovate without waiting for manufacturers. It enables us to control both sides of the fence. It enables true co-design, for the benefit of security. Partnering with the creators of Ariane at ETH Zurich, we did exactly that: We explored how we can amend the hardware-software contract just a bit to give the OS the right means to defeat covert channels. And we could demonstrate that it takes very little to be highly effective. The relevant working groups in the RISC-V Foundation are discussing these mechanisms right now. Stay tuned for RISC-V setting the benchmark in processor security, complementing the world’s most secure OS kernel – seL4.

What to know more?

The seL4 web site explains seL4, and has a whitepaper, written for non-experts, that explains seL4 and its verification story in detail.]]>