Messages in this thread | | | Date | Sat, 5 Sep 1998 18:16:28 +0100 | From | Jamie Lokier <> | Subject | Re: [OFFTOPIC] Re: Virtual Machines, JVM in kernel |
| |
David Wragg wrote: | It's worse than that. In general, "Safe" execution of C programs | simply cannot be proved (for some useful definition of safe). And if
Brandon S. Allbery wrote: > Which is why I've been leery of the concept: given a chunk of C code with a > proof attached, the proof is untrustworthy (in point of fact, it *lies* if > it claims there are no buffer overflows, except in degenerate cases that > only use scalar values --- but the packet itself is not a scalar).
No, no you have it wrong, I'm quite sure. In general, most C programs are not safe. But if they were all safe we wouldn't need an associated proof.
*Some* C programs that operate on arrays are safe, and can be proven to be safe. I've given several examples already. The degenerate cases you mention are but the simplest.
Finding these proofs is generally very difficult, but in some cases it is not difficult. Verifying proofs is possible and is, in general, much more efficient than finding a proof. And when a proof is verified, it *is* trustworthy. Or you have screwed up your logic. But that means you wrote the verifier wrong.
Please note that a proof does not "claim" anything, much less "there are no buffer overflows". A proof is not a series of statements to be believed. It is a guide for the verification process to deduce statements about the code -- every statement deduced satisfies the verification logic. Summary: proofs are considered _untrustworthy_ by the verifier, so they cannot break it. Perhaps you are thinking of a certificate, which is what ActiveX uses.
> You can verify that the proof doesn't work, probably, which would be > good enough... except that (as noted) *no* purported proof will pass > this because the desired condition is not provable.
I disagree with you on this point, because there are programs _I_ can prove (to your satisfaction, I hope) use arrays and do not cause buffer overflows. I am confident proofs for a subset of these programs can be verified mechanically. But I can't prove it without an example ;-)
> So proof-carrying code isn't going to work here.
If you're right that no mechanically-verifiable proofs can be found to satisfy the safety requirements, you have a point. But my limited experience with theorem provers and formal semantics of programming languages suggests otherwise.
-- Jamie
- 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
| |