The seL4 Foundation and RISC-V International are pleased to announce that Ryan Barry from UNSW Sydney has completed the proof that the seL4 microkernel on the RISC-V architecture enforces the key security property of integrity.
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).
The implication is that 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. Confidentiality is the next security property the Trustworthy Systems (TS) team at UNSW is working on for RISC-V.
Even without proof of confidentiality, seL4 already has the by far 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.
Stay tuned for more exciting news about seL4 on RISC-V!