state of the art in formal proofs of kernels
Posted Nov 20, 2012 4:26 UTC (Tue) by pjm
In reply to: Annotating the kernel to prevent exploits
Parent article: Attacking hardened Linux systems with kernel JIT spraying
Even then, so far they only claim to have proven [subject to questionable assumptions such as the compiler conforming to the formalization that they've written themselves] that their C implementation has the same behaviour (and hence same set of bugs) as their implementation in a higher-level language. They haven't claimed to have proven anything (else) about the behaviour of that higher-level-language implementation. So for example, even if the seL4 microkernel contained a JIT compiler, they wouldn't have proven anything about the output of that compiler (to which the kernel presumably passes control while in kernel mode).
OTOH, that program equivalence would certainly reduce the opportunities for exploits (e.g. by ruling out any buffer overflows that don't occur in the higher-level language), and at least it's a bit easier to prove properties of code in a higher-level language than a lower-level one. Mathematical proofs increase confidence, but there's always a gap between a mathematical model and the real world.
to post comments)