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