Abstract:

Bytecode Verification by Model Checking

David Basin and Stefan Friedrich and Marek Gawkowski


Java bytecode verification is traditionally performed by using dataflow analysis. We investigate an alternative 
based on reducing bytecode verification to model checking. First, we analyze the complexity and scalability of 
this approach. We show experimentally that, despite an exponential worst-case time complexity, model checking
 type-correct bytecode using an explicit-state on-the-fly model checker is feasible in practice, and we give a 
theoretical account why this is the case. Second, we formalize our approach usingIsabelle/HOL and prove 
its correctness. In doing so we build on the formalization of the Java Virtual Machine and data flow 
analysis framework of Pusch and Nipkow and extend it to a more general framework for reasoning about 
model-checking based analysis. Overall,our work constitutes the first comprehensive investigation of the 
theory and practice of bytecode verification by model checking.