[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    [W:0.021 / U:0.240 seconds]
    ©2003-2017 Jasper Spaans. hosted at Digital OceanAdvertise on this site