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    [from the cache]
©2003-2011 Jasper Spaans. Advertise on this site