Formalizing a JVML verifier for initialization in a theorem prover

Yves Bertot

To appear at 13th Conference on Computer-Aided Verification (CAV01), Paris, France, 18-22 July 2001


Abstract

The byte-code verifier is advertised as a key component of the security and safety strategy for the Java language, making it possible to use and exchange Java programs without fearing too much damage due to erroneous programs or malignant program providers. As Java is likely to become one of the languages used to embed programs in all kinds of appliances or computer-based applications, it becomes important to verify that the claim of safety is justified. We worked on a type system proposed in \origpaper\ to enforce a discipline for object initialization in the Java Virtual Machine Language and implemented it in the Coq \cite{Coq} proof and specification language. We first produced mechanically checked proofs of the theorems in \origpaper\ and then we constructed an functional implementation of a byte-code verifier. We have a mechanical proof that this byte-code verifier only accepts programs that have a safe behavior with respect to initialization. Thanks to the extraction mechanism provided in Coq \cite{PaulinWerner93}, we obtain a program in CAML that can be directly executed on sample programs.


Server START Conference Manager
Update Time 28 Mar 2001 at 08:36:01
Maintainer www-cav01@lsv.ens-cachan.fr.
Start Conference Manager
Conference Systems