Prototyping Proof Carrying Code
We introduce a generic framework for proof carrying code, developed
and mechanically verified in Isabelle/HOL. The framework defines and
proves sound a verification condition generator with minimal
assumptions on the underlying programming language, safety policy,
and safety logic. We demonstrate its usability for prototyping proof
carrying code systems by instantiating it to a simple assembly
language with procedures and a safety policy for arithmetic
overflow.
pdf
BibTeX:
@inproceedings{WildmoserNKN-TCS04,
author={Martin Wildmoser and Tobias Nipkow and Gerwin Klein and Sebastian Nanz},
title={Prototyping Proof Carrying Code},
booktitle={Exploring New Frontiers of Theoretical Informatics},
editor={J.-J. Levy and E. Mayer and J. Mitchell},
publisher={Kluwer},year=2004,pages={333-347}}