✳flâneur — a map of the web's best reading

What the Proofs Assume | seL4

sel4.systems · 1,403 words · saved by 1 readers

With a proof in formal logic, it is important to understand what its basic assumptions are, because this is where fault can still occur. Our proof about the seL4 microkernel goes down to the level of the C code, and for some architectures even to the binary code. Assumptions are not limitations or problems. Being able to clearly state an exhaustive list of assumptions means that the work needed to fully trust a system is massively reduced from looking at many thousands of lines of code to a number of small, specific, and easy to understand pieces. They are the following: Note that we do not need to trust the compiler and linker any more on architectures that are supported by our binary verification. Their output is formally verified for seL4 by an automatic tool if the kernel is compiled with the correct compiler settings that can be configured in the build system. The reduced proof assumptions mean that we do not need to trust the compiler or linker, but there may still be faults rema

What the Proofs Assume | seL4 Verification What the Proofs Assume This page defines in high-level language what the seL4 proofs assume. It is aimed at an audience with a technical background, but does not assume any expertise in formal verification. The Assumptions With a proof in formal logic, it is important to understand what its basic assumptions are, because this is where fault can still occur. Our proof about the seL4 microkernel goes down to the level of the C code, and for some architectures even to the binary code. Assumptions are not limitations or problems. Being able to clearly sta

Explore this link on the map →

saved by

related reading