seL4 Integrity Enforcement Proved for RISC-V

Great news: Ryan Barry from the Trustworthy Systems verification team has just completed the access-control proofs of seL4.

What does this mean?

In more detail: the proof shows that seL4 will only allow a thread to access an object or memory resource if the access is explicitly authorised by a capability. Specifically, user code cannot write to memory for which it does not hold a write capability (nor will the kernel perform such a write on the user’s behalf).

This establishes the critical integrity property: A process cannot overwrite another process’s memory without explicit authorisation. In other words: user processes on seL4 are strongly isolated and cannot interfere with each other.

But it means more. As the proof guarantees that there is no access to objects or memory resources unless explicitly authorised, it also implies availability of the memory resource: A process cannot interfere with another’s resource access.

The integrity proof does not talk about read accesses directly, but it does predict which user threads can at most have read access to which memory regions.  This is a very useful property, even if it stops short of the stronger notion of confidentiality (the third of the classical “CIA properties” of security). This is because preventing read access is not sufficient for preventing leakage of secrets.

Where does that leave us?

We had previously proved confidentiality (including freedom from covert storage channels) for the 32-bit Armv7 architecture. For RISC-V, this final security proof still needs to be done (and we’re working on it).

However, we already have by far the most comprehensive verification story of any OS for RISC-V, and really for any OS for a 64-bit architecture. Specifically, we now have for RISC-V:

• Proof of functional correctness, meaning that the C implementation is proved to conform to the specification and, as such, is free of bugs in a very strong sense;
• Proof of translation correctness, meaning that the binary code produced by the compiler and linker is correct. This extends functional correctness to the executable binary;
• And now proof of integrity and availability enforcement, or, more general, that the kernel enforces the access-control model. Because of the other proofs, we know that this property, proved about the formal specification of the kernel, applies to the actual kernel executable.

This degree of assurance is only surpassed by the proof chains of seL4 for Armv7. It means we are getting close to RISC-V becoming the best-supported architecture for seL4.

Where does this leave Arm?

When we did the original functional correctness proof of seL4 12 years ago, Armv7 didn’t even exist, we did it for Armv6 and later adapted to v7. 32-bit Arm was then the only architecture with a verified kernel. By now, of course, 32-bit processors are not exactly hot any more, the world of mobile devices which Arm dominates has long moved to 64-bit Armv8 processors. So there is now an OS with an unparalleled verification story for an obsolescent version of the architecture.

I would encourage Arm, as well as major users of Arm processors, to consider this situation, where they are effectively being overtaken by RISC-V.

We would love to talk to you about rectifying this. There are plenty of major players with a strong interest in security on Arm processors. Each of them alone (including Arm itself) could easily afford funding the verification of seL4 on AArch64, but if a handful of them get together, the cost to each becomes a fraction of their marketing budget.

Think about it!