Messages in this thread | | | Subject | Re: [OFFTOPIC] Re: Virtual Machines, JVM in kernel | From | David Wragg <> | Date | 04 Sep 1998 20:18:48 +0000 |
| |
"Brandon S. Allbery KF8NH" <allbery@kf8nh.apk.net> writes: > In message <y7rvhn4zytr.fsf@sytry.doc.ic.ac.uk>, David Wragg writes: > +----- > | "Brandon S. Allbery KF8NH" <allbery@kf8nh.apk.net> writes: > | > Checking whether the proof is consistent wouldn't be, but how do you verify > | > the proof "goes with" the code? Including a digital signature prevents > | > spoofing, but doesn't promise that the code actually works as the proof > | > claims. > | > | These wouldn't be general proofs of just anything - they would > | naturally refer to the subject of the proof (i.e. the code), so that > | altering the code automatically invalidates the proof. > +--->8 > > That's the "spoofing" scenario, which as I implied above isn't > "interesting". The point where it falls apart is that a "proof" that some > piece of C code doesn't have any buffer overflows *cannot* be verified.
In comparison to generating a proof, verifying a proof is an easy problem to mechanize.
> Type validation is useful, but only when the types themselves prevent > invalid accesses. C types don't insure that you can't write past the limits > of the typed address range (scalar variable, structure, array, etc.), so it > doesn't accomplish anything useful in practice.
It's worse than that. In general, "Safe" execution of C programs simply cannot be proved (for some useful definition of safe). And if it was possible to prove the relevant properties for realistic programs (despite the "in general" disclaimer), I think compiler writers would have noticed it by now, giving that they've been looking at this kind of problem for a few decades.
For languages like Java, the type system doesn't just make it easy to prove the relevant properties - it actually constrains the language so that for well-typed programs the relevant properties hold (proving this last bit is tough in itself, but can be done, because the proof is done for the definition of a particular language, rather than "in general").
-- Dave Wragg
- To unsubscribe from this list: send the line "unsubscribe linux-kernel" in the body of a message to majordomo@vger.rutgers.edu Please read the FAQ at http://www.tux.org/lkml/faq.html
| |