sel4 is implemented 3 times: in c, haskell and isabelle/HOL.
The implementation in isabelle is proven to satisfy various key high level security properties. All 3 implementations are proven to be semantically equivalent. The compiled assembly output from gcc is also proven to be semantically equivalent to the C implementation.
Having these implementation layers is helpful for the proof work since the highest level properties can be proven over a much simpler and highly abstracted implementation (in issabelle / HOL), and the layers make the chain of equivalence proofs down to assembly more tractable. Most of the proof work is done in isabelle with the final C <-> assembly proofs using a custom automated smt based proof engine implemented in python.
The trusted components are the various language semantics / import tools, as well as a few very low level pieces of actual OS code (mostly parts of the early boot sequence iirc).
> The multicore kernel uses a big-lock approach, which makes sense for tightly-coupled cores that share an L2 cache. It is not meant to scale to many cores,
The implementation in isabelle is proven to satisfy various key high level security properties. All 3 implementations are proven to be semantically equivalent. The compiled assembly output from gcc is also proven to be semantically equivalent to the C implementation.
Having these implementation layers is helpful for the proof work since the highest level properties can be proven over a much simpler and highly abstracted implementation (in issabelle / HOL), and the layers make the chain of equivalence proofs down to assembly more tractable. Most of the proof work is done in isabelle with the final C <-> assembly proofs using a custom automated smt based proof engine implemented in python.
The trusted components are the various language semantics / import tools, as well as a few very low level pieces of actual OS code (mostly parts of the early boot sequence iirc).