Bytecode Analysis for Proof Carrying Code

Martin Wildmoser, Amine Chaieb, Tobias Nipkow

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.



  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{}}