Technische Universität München

Abstract |

The bytecode verifier is an important part of Java's security architecture. This thesis presents a fully formal, executable, and machine checked specification of a representative subset of the Java Virtual Machine and its bytecode verifier together with a proof that the bytecode verifier is safe.

The specification consists of an abstract framework for bytecode verification which is instantiated step by step with increasingly expressive type systems covering all of the interesting and complex properties of Java bytecode verification: classes, objects, inheritance, virtual methods, exception handling, constructors, object initialization, bytecode subroutines, and arrays.

The instantiation yields two executable verified bytecode verifiers: the iterative data flow algorithm of the standard Java platform and also a lightweight bytecode verifier for resource-constrained devices such as smart cards.

All specifications and proofs have been carried out in the interactive
theorem prover Isabelle/HOL. Large parts of the proofs are written in
the human-readable proof language Isabelle/Isar making it possible to
understand and reproduce the reasoning independently of the theorem
prover. All formal proofs in this thesis are machine checked and
generated directly from Isabelle sources.

Online Copy |

Available as [PDF], [pgp signature],
[bibtex]

BibTeX entry |

@phdthesis{Klein-PhD, author = {Gerwin Klein}, title = {Verified Java Bytecode Verification}, school = {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen}, year = {2003}, url = {\url{http://www4.in.tum.de/~kleing/diss/}}, }

Isabelle Sources |

Exceptions |
Object Initialization |
Subroutines |
Arrays | ||||

Proof document | [PDF] | Proof document | [PDF] | Proof document | [PDF] | Proof document | [PDF] |

Browsable theories | [html] | Browsable theories | [html] | Browsable theories | [html] | Browsable theories | [html] |

Sources | [tar.gz] | Sources | [tar.gz] | Sources | [tar.gz] | Sources | [tar.gz] |

Gerwin Klein | Last modified: Fri Feb 21 17:27:42 CET 2003 |