[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