[lkml]   [1998]   [Sep]   [5]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
Messages in this thread
    SubjectRe: [OFFTOPIC] Re: Virtual Machines, JVM in kernel
    David Wragg wrote:
    | It's worse than that. In general, "Safe" execution of C programs
    | simply cannot be proved (for some useful definition of safe). And if

    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

    *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
    Please read the FAQ at

     \ /
      Last update: 2005-03-22 13:44    [W:0.020 / U:38.156 seconds]
    ©2003-2016 Jasper Spaans. hosted at Digital OceanAdvertise on this site