Skip to content

seL4 on RISC-V Verified to Binary Code

2021/05/05

… and seL4 and RISC-V Foundations form an alliance

In June 2020 we announced that the seL4 microkernel, the world’s first operating system (OS) kernel with a machine-checked proof of implementation correctness, has now also been verified for the RV64 architecture, making it the first formally verified OS for RISC-V. We are pleased to announce that this verification has now been extended to the executable binary, meaning that the machine code running on the processor is proved to be correct against the kernel’s specification. RISC-V is the first 64-bit architecture for which this has been achieved.

What does this mean?

The previously announced proof means that, according to the semantics of the C language in which seL4 is implemented, the kernel will always behave as specified. Among others this means that seL4 cannot be attacked with stack overflows, malformed inputs or other forms of code injection or control-flow hijacking – it is provably secure in a very strong sense. However, there is still the risk of security holes resulting from a buggy (or compromised) C compiler, or from the compiler and kernel developers interpreting the C semantics differently.

The newly completed binary verification completely removes these risks – it guarantees that properties we prove about the C code hold for the executable code, and thus that the executable kernel binary behaves as required by the kernel’s formal specification. 

More than porting to a different ISA

The binary verification toolchain. Dark blue arrows are proved.

While seL4’s implementation correctness proofs use interactive theorem proving, with hundreds of thousands of (mostly hand-written but machine-checked) lines of proof, the binary verification uses an automated tool chain (see the seL4 White Paper for details). The tool chain converts both the C code as well as the binary into an intermediate language that represents the control flow of the program. It then uses SMT solvers to prove equivalence of the two programs, one short code sequence at a time. 

SMT solvers prove properties by a very efficient exploration of the state space, using state compression techniques to make the problem tractable. We had previously built the binary-verification toolchain for the 32-bit Armv7 architecture. As the state space grows exponentially with the word size, taking the step to a 64-bit architecture requires overcoming significant scalability challenges – which the ingenuity of our team around Matt Brecknell and Zoltan Kocsis could overcome in the end.

Further implications

This work represents a significant step for both the RISC-V and seL4 ecosystems. No 64-bit architecture other than RISC-V presently has an OS with such a comprehensive verification and security story. And seL4 has with RISC-V the ideal base for driving further innovation in computer system security, especially for our work on the systematic prevention of information leakage through timing channels, based on the approach we call time protection. Stay tuned for more exciting results to come!

We are now formalising the link between the two ecosystems by announcing that RISC-V International and the seL4 Foundation are joining each other as Associate Members.

From → seL4

7 Comments
  1. Richard B permalink

    Is the compiler not proven because of the target? I had thought the CompCert compiler was formally verified? Out of my depth here, but interested in understanding

  2. CompCert is proved to generate correct code, but still has an unverified front-end that can lead to buggy code, see https://dl.acm.org/doi/pdf/10.1145/1993498.1993532. Moreover, it is much worse at optimising systems code than GCC, resulting in significant performance degradation for seL4. And industry just prefers using GCC. Having a translation validation toolchain avoids having to depend on a certifying compiler.

    • Richard B permalink

      Thank you, this has short-circuited my misunderstanding perfectly 🙂

  3. Note that CompCert has evolved significantly since this 2011 paper, in particular the front-end is now formally verified. See for example https://hal.inria.fr/hal-01399482
    That’s said, the current seL4 approach might be more suitable for other reasons.

    • Zach Lym permalink

      IIRC, commercial usage of CompCert requires a non-gratis license.

  4. Much props for the post with your permission I would share this post with my followers?

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

%d bloggers like this: