Messages in this thread | | | Date | Fri, 4 Sep 1998 03:33:28 +0100 | From | Jamie Lokier <> | Subject | Re: [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
| |