Messages in this thread | | | Subject | Re: [OFFTOPIC] Re: Virtual Machines, JVM in kernel | From | David Wragg <> | Date | 04 Sep 1998 20:43:11 +0000 |
| |
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
| |