lkml.org 
[lkml]   [1998]   [Sep]   [4]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
SubjectRe: [OFFTOPIC] Re: Virtual Machines, JVM in kernel
Date
From
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

\
 
 \ /
  Last update: 2005-03-22 13:44    [W:0.049 / U:0.708 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site