Department of Computer Science
COLLOQUIUM

Thursday, November 4, 2004
4:15pm
B17 Upson Hall

George Necula
UC Berkeley

The Open Verifier Framework for Constructing Code Verifiers

Widely-deployed virtual machines, such as the Java VM or Microsoft's Common Language Infrastructure, feature code verification algorithms that restrict drastically the format and the type system that can be used by the foreign code to be verified. We propose instead that virtual machines be designed with extensible verifiers, which allow the supplier of the foreign code to also supply an appropriate untrusted verifier. This scheme allows for maximum of flexibility in the choice of the type system and compilation techniques that can be used for generating the foreign code.

The proposed untrusted verifiers control virtually all aspects of the verification by carrying on a dialogue with the trusted infrastructure using a language designed both to correspond closely to common verification actions and to carry simple adequacy proofs for those actions. We describe our experience implementing in this unified setting proof-carrying code, typed assembly language, and data-flow or abstract interpretation based verifiers. We also describe our initial experience with using this framework in an undergraduate compiler course at UC Berkeley.