| |||||||||||||
Annotating the kernel to prevent exploitsAnnotating the kernel to prevent exploitsPosted Nov 19, 2012 22:39 UTC (Mon) by vonbrand (subscriber, #4458)In reply to: Annotating the kernel to prevent exploits by ebiederm Parent article: Attacking hardened Linux systems with kernel JIT spraying
The seL4 is a microkernel, of which some 7500 lines of C code have been verified rigurously (assuming the compiler and the underlying machine are correct). That is many, many orders of magnitude away from even the most spartan Linux configuration.
(Log in to post comments)
state of the art in formal proofs of kernels Posted Nov 20, 2012 4:26 UTC (Tue) by pjm (subscriber, #2080) [Link] 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.
state of the art in formal proofs of kernels Posted Nov 20, 2012 11:45 UTC (Tue) by Cyberax (✭ supporter ✭, #52523) [Link]
There's research towards proving that compiler output is correct by using type-annotated assembly language. It might be actually possible to check whether high-level invariants are not mis-translated by the compiler.
The next frontier is to prove that hardware itself is correct :)
state of the art in formal proofs of kernels Posted Nov 20, 2012 13:33 UTC (Tue) by ebiederm (subscriber, #35028) [Link]
There is compcert a formally proven C compiler written in coq.
Hardware design developed formal method for their logic ALUs and FPUs a long time ago. Although that clearly has it's limits. Especially timing.
The next frontier is for program proofs to stop being news and instead partial program proofs increasing program reliability to the point where any program updates except for features become news.
How we go from proofs of concept to useful proof tools is a question I don't yet see answers to.
state of the art in formal proofs of kernels Posted Nov 20, 2012 19:14 UTC (Tue) by dlang (✭ supporter ✭, #313) [Link]
> ...increasing program reliability to the point where any program updates except for features become news.
Given that people don't even bother to define what acceptable input is, I don't expect this to ever happen.
Not to mention that this would require anticipating all possible internal state, another thing that is not going to happen.
And then you need to have someone think through what should happen in all these combinations of cases, and not have any logic errors in what the 'proofs' are trying to show.
> Hardware design developed formal method for their logic ALUs and FPUs a long time ago. Although that clearly has it's limits. Especially timing.
And when Timing issues dominate, the 'correctness' generated by such proofs is pretty meaningless.
Math is not reality, they sometimes have a resemblance to each other, but that's just a happy coincidence.
|
|||||||||||||