[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.069 / U:19.032 seconds]
©2003-2018 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site