Verified Bytecode Verifiers

Gerwin Klein and Tobias Nipkow

Abstract

Using the theorem prover Isabelle/HOL we have formalized and proved correct an executable bytecode verifier in the style of Kildall's algorithm for a significant subset of the Java Virtual Machine. First an abstract framework for proving correctness of data flow based type inference algorithms for assembly languages is formalized. It is shown that under certain conditions Kildall's algorithm yields a correct bytecode verifier. Then the framework is instantiated with our previous work about the JVM. Finally we demonstrate the flexibility of the framework by extending our previous JVM model and the executable bytecode verifier with object initialization.

Online Copy

Available as [PDF]

Isabelle Sources

The ÁJava bytecode verifier with object initialization:

Bibtex entry

@article{KleinN-TCS02,
  author={Gerwin Klein and Tobias Nipkow},
  title={Verified Bytecode Verifiers},
  journal={Theoretical Computer Science},
  year="2002",
  pages="583--626",
  volume={298},
  number={3},
  editor={F. Honsell and M. Miculan}
  url={\url{http://www4.in.tum.de/~kleing/papers/tcs02.html}}
}
Gerwin Klein
2005-01-30 14:04:48