Verified Bytecode Verifiers
Gerwin Klein and Tobias Nipkow
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.
pdf
ps
ScienceDirect/Elsevier
BibTeX:
@article{KleinN-TCS,author={Gerwin Klein and Tobias Nipkow},
title={Verified Bytecode Verifiers},
journal=TCS,year=2003,volume=298,pages={583--626}}