[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
    Jamie Lokier <> writes:
    > Anyway, you can prove that _some_ C programs don't do dangerous things.
    > Or that they don't do _some_ dangerous things.

    Yes, but there are a lot of dangerous things that can be done in C. It
    would be a little annoying when your program, despite being quite
    safe, gets rejected by the automatic prover because it can't quite
    make it.

    > 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.

    Fine, I'm sure that much is achievable for realistic code. However, I
    suspect that it would be easy to write "unrealistic" code designed to
    fool the analyser.

    Any realistic automated program analysis has to attempt a "proof", but
    if that doesn't work in a reasonable amount of time, give up and make
    a safe assumption instead. For loading untrusted code into a kernel,
    the safe assumption would be that the code is dangerous, and so should
    not be admitted. So for this to be useful, it has to be shown that the
    some C programs that are accepted include quite a lot of realistic

    Dave Wragg

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