User: Password:
|
|
Subscribe / Log in / New account

state of the art in formal proofs of kernels

state of the art in formal proofs of kernels

Posted Nov 20, 2012 13:33 UTC (Tue) by ebiederm (subscriber, #35028)
In reply to: state of the art in formal proofs of kernels by Cyberax
Parent article: Attacking hardened Linux systems with kernel JIT spraying

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.


(Log in to post comments)

state of the art in formal proofs of kernels

Posted Nov 20, 2012 19:14 UTC (Tue) by dlang (subscriber, #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.


Copyright © 2017, Eklektix, Inc.
Comments and public postings are copyrighted by their creators.
Linux is a registered trademark of Linus Torvalds