Asserting Bytecode Safety

13 years 11 months ago
Asserting Bytecode Safety
Abstract. We instantiate an Isabelle/HOL framework for proof carrying code to Jinja bytecode, a downsized variant of Java bytecode featuring objects, inheritance, method calls and exceptions. Bytecode annotated in a first order expression language can be certified not to produce arithmetic overflows. For this purpose we use a generic verification condition generator, which we have proven correct and relatively complete. 1 Proof Carrying Code In mobile code applications, e.g. applets, grid computing, dynamic drivers, or ubiquitous computing, safety is a primary concern. Proof carrying code (PCC) aims at certifying that low level code adheres to some safety policy, such as type safety [6], bounded array accesses [13], or limited memory consumption [4]. When such properties are checked statically sandbox mechanisms and error recovery become obsolete. In classical PCC a verification condition generator (VCG) reduces annotated machine code to proof obligations that guarantee safety. Pr...
Martin Wildmoser, Tobias Nipkow
Added 27 Jun 2010
Updated 27 Jun 2010
Type Conference
Year 2005
Where ESOP
Authors Martin Wildmoser, Tobias Nipkow
Comments (0)