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