lkml.org 
[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
    From
    Date
    Jamie Lokier <lkd@tantalophile.demon.co.uk> 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
    programs.

    --
    Dave Wragg


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