With gcc being part of the trusted base for all but ARMv7-A, have there been efforts to compile seL4 with CompCert? If so, what are the results? If not, why not?
(Half expected this to be an FAQ, but didn’t find it.)
2 Likes
gcc is not part of the TCB, thanks to our binary verification toolchain, which proves that the compiler/linker output retains the semantics of the C code. This means our proofs extend to to the executable code.
We did years ago experiment with CompCert. It resulted in performance degradation. But furthermore, using CompCert would not give us a complete proof chain. It uses a different logic to our Isabelle proofs, and we cannot be certain that its assumptions on C semantics are the same as of our Isabelle proofs.
Gernot concisely summarised the situation, but yes I made the necessary changes to seL4 to compile with CompCert ~2012 0. We discovered some interesting things along the way, like bugs in unverified code (E.g. something I remember offhand was a 4096 byte structure that had to occupy a single page for correctness. Nothing was constraining this to be true, but GCC coincidentally aligned it to 4096 bytes for perf. This wasn’t exclusive to CompCert, as I found a few similar bugs when making changes to build with Clang too). Xavier Leroy and the CompCert team were very helpful in this effort and many of the changes to CompCert during that time were introduced to support seL4.
I haven’t closely followed how seL4 has evolved since then, but I imagine it wouldn’t be too much effort to make contemporary seL4 CompCert-compatible.
If
gcc is not part of the TCB
is indeed true for the architectures other than ARMv7-A, then I’d suggest to update the topic “Which code is verified?” where Gerwin stated
Note that while the ARM configuration has the full proof stack including functional correctness, security theorems, system initialiser, and binary verification, the other architectures so far only include functional correctness.
Matt’s post sounds more encouraging. Translations from top level theorems in either of Coq and Isabelle/HOL into axioms of the other should not pose fundamental logical problems. I’d like to understand better where the subtle differences in the interpretation of the C semantics between the two projects surface in the seL4 code base. I would expect more relevant differences in the machine models, where both projects may want to revisit their current ARMv8-A (and RISC-V and x86) models in light of Alastair Reid’s much more detailed model as it fed into the Sail project.
I would in fact expect the opposite :-), i.e.I don’t think that the machine models for ARM will actually have different semantics for the instructions that we use and will be fairly easy to use across theorem provers, but the semantics of C that CompCert uses is definitely different to the semantics of C that we use in seL4, and is not likely to translate that well between Coq and Isabelle, because even the standard library in Coq uses dependent types which Isabelle doesn’t support (no real fundamental problem for those, I’d hope, but nothing that would work straightforwardly).
There is also a philosophical difference in the sense that CompCert has to care about the C standard, because it is an actual C compiler, whereas we don’t have to care about the C standard much – only as a tool to get what we want. We only need GCC to translate this particular program the way we want. This leads to one fairly large difference in the memory model: CompCert is very close to what the C standard describes, whereas we are much more detailed than what the C standard allows, i.e. we fix implementation-defined behaviours (to GCC’s behaviour) and we even allow some things that are strictly speaking undefined behaviour in C, because C expects these things to be done by the runtime (standard library, which we implement) and the OS (which we implement). The main one is memory allocation, where the standard says what you can expect out of malloc, and can’t rely on anything outside that, where we of course implement malloc (Untyped caps and retype operation in the kernel) and memory regions that correspond to page tables etc. We’re careful about how we do that, as are other kernels, but ultimately we have to inspect or validate the binary to see if the compiler did the right thing for allocation (it would have to have a very powerful reasoning engine to realise that some of the memory we’re allocating has not in fact come out of malloc, so I’d count it as extremely unlikely that the compiler does anything fancy with it). I doubt that we could prove the preconditions of CompCert’s correctness theorem for the kernel (even though I do think it will translate it exactly the way we’d want and expect).
For the actual execution of C statements and expressions I’d not expect any difference, apart from the fact that CompCert supports more of the language (e.g. can take addresses of local variables), which makes the execution model richer and therefore harder to reason about (see e.g. the VST project on top of CompCert – it’s very sophisticated and cool, but way harder to use than our logic that restricts the language instead).