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