lkml.org 
[lkml]   [1998]   [Sep]   [4]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
    /
    Date
    From
    SubjectRe: [OFFTOPIC] Re: Virtual Machines, JVM in kernel
    David Wragg wrote:
    > different type...). In general you can't prove that C programs don't
    > do dangerous things (hello Mr. Turing).

    That depends on the environment in which you run the C program.
    Userland Linux C programs can't generally do such nasty things as crash
    the kernel... if you trust the kernel :-)

    Anyway, you can prove that _some_ C programs don't do dangerous things.
    Or that they don't do _some_ dangerous things. Consider the threads
    about analysing the kernel source to see that non-interrupt-safe
    functions aren't called from interrupts, locks are not held by the wrong
    functions etc.

    > So I doubt that proof-carrying code would be useful for traditional
    > kernel programming.

    I doubt it too, for "traditional" kernel programming.

    Longer term, I hope to see proof-carrying code all over the place,
    without it being a big deal. I'd like to see code run in a cage until
    it has been verified safe -- then the verification can be seen as an
    optimisation of the cage/program combination.

    Verifying the cage is one of those interesting exercises in verifying a
    verifier ;-)

    -- Jamie

    -
    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.030 / U:60.136 seconds]
    ©2003-2016 Jasper Spaans. hosted at Digital OceanAdvertise on this site