Messages in this thread | | | Subject | Re: [OFFTOPIC] Re: Virtual Machines, JVM in kernel | Date | Fri, 04 Sep 1998 19:17:03 -0300 | From | "Brandon S. Allbery KF8NH" <> |
| |
In message <y7ryarzljh3.fsf@sytry.doc.ic.ac.uk>, David Wragg writes: +----- | "Brandon S. Allbery KF8NH" <allbery@kf8nh.apk.net> writes: | > "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. +--->8
True, but as you note below (and I noted in the quoted message) C isn't amenable.
| It's worse than that. In general, "Safe" execution of C programs | simply cannot be proved (for some useful definition of safe). And if +--->8
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). 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. So proof-carrying code isn't going to work here.
-- brandon s. allbery [os/2][linux][solaris][japh] allbery@kf8nh.apk.net system administrator [WAY too many hats] allbery@ece.cmu.edu electrical and computer engineering KF8NH carnegie mellon university
- 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
| |