[Novalug] OT question about a mathematician's proof of a program
Stuart Gathman
stuart@gathman.org
Wed Dec 4 18:45:18 EST 2013
On 11/17/2013 03:57 PM, Mark Smith wrote:
> that is a common joke that we hear all the time. it is necessary
> *because* it is not possible to mathematically prove a complex OS.
> BUT if it were possible to prove a kernel, then it would not be
> necessary.
>
A tiny subset of the Java virtual machine specification was proved
secure (basically Class + Object). That was groundbreaking, but of
course didn't prove the *implementation* of said JVM secure or the full
library. Most real world Java security problems come not through the
JVM, but through library addons that require privileged operations, but
don't properly sanity check their inputs.
More information about the Novalug
mailing list