[lkml]   [1998]   [Sep]   [3]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
Messages in this thread
SubjectRe: [OFFTOPIC] Re: Virtual Machines, JVM in kernel
In message <>, David Wragg writes:
| "Brandon S. Allbery KF8NH" <> writes:
| > Checking whether the proof is consistent wouldn't be, but how do you verify
| > the proof "goes with" the code? Including a digital signature prevents
| > spoofing, but doesn't promise that the code actually works as the proof
| > claims.
| These wouldn't be general proofs of just anything - they would
| naturally refer to the subject of the proof (i.e. the code), so that
| altering the code automatically invalidates the proof.

That's the "spoofing" scenario, which as I implied above isn't
"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.

Type validation is useful, but only when the types themselves prevent
invalid accesses. C types don't insure that you can't write past the limits
of the typed address range (scalar variable, structure, array, etc.), so it
doesn't accomplish anything useful in practice.

brandon s. allbery [os/2][linux][solaris][japh]
system administrator [WAY too many hats]
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
Please read the FAQ at

 \ /
  Last update: 2005-03-22 13:44    [from the cache]
©2003-2014 Jasper Spaans. hosted at Digital Ocean