Proving the soundness of a Java bytecode verifier specification in Isabelle/HOL

Abstract

Compiled Java programs may be downloaded from theWorld Wide Web and be executed on any host platform that implements the Java Virtual Machine (JVM). However, in general it is impossible to check the origin of the code and trust in its correctness. Therefore standard implementations of the JVM contain a bytecode verifier that statically checks several security constraints before execution of the code. We have formalized large parts of the JVM, covering the central parts of object orientation, within the theorem prover Isabelle/HOL. We have then formalized a specification for a Java bytecode verifier and formally proved its soundness. While a similar proof done with paper and pencil turned out to be incomplete, using a theorem prover like Isabelle/HOL guarantees a maximum amount of reliability.