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