Bytecode Analysis for Proof Carrying Code
Out of annotated programs proof carrying code systems construct and
prove verification conditions that guarantee a given safety policy. The
annotations may come from various program analyzers and must not
be trusted as they need to be verified. A generic verification condition
generator can be utilized such that a combination of annotations is
verified incrementally. New annotations may be verified by using
previously verified ones as trusted facts. We show how results from a
trusted type analyzer may be combined with untrusted interval analysis
to automatically verify that bytecode programs do not overflow. All
trusted components are formalized and verified in Isabelle/HOL.
pdf
BibTeX:
@inproceedings{WildmoserCN-Bytecode05,
author = {Martin Wildmoser and Amine Chaieb and Tobias Nipkow},
title = {Bytecode Analysis for Proof Carrying Code},
journal = {Proceedings of the 1st Workshop on Bytecode Semantics, Verification and Transformation},
series = {Electronic Notes in Computer Science},
year = 2005,
volume = 141,
number = 1,
pages = {19-34},
url = {\url{http://www4.in.tum.de/~wildmosm/publications/WildmoserCN-Bytecode05.pdf}}
}