Verification with Small and Short Worlds

Rohit Sinha, Cynthia Sturton, Petros Maniatis, Sanjit A. Seshia, and David Wagner. Verification with Small and Short Worlds. In Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD), October 2012.

Download

[pdf] 

Abstract

We consider the verification of safety properties in systems with large arrays and data structures. Such systems are common at the low levels of software stacks; examples are hypervisors and CPU emulators. The very large data structures in such systems (e.g., address-translation tables and other caches) make automated verification based on straightforward state-space exploration infeasible. We present S2W, a new abstraction-based model-checking methodology to facilitate automated verification of such systems. As a first step, inductive invariant checking is performed. If that fails, we compute an abstraction of the original system by precisely modeling only a subset of state variables while allowing the rest of the state to evolve arbitrarily at each step. This subset of the state constitutes a "small world" hypothesis, and is extracted from the property. Finally, we verify the safety property on the abstract model using bounded model checking. We ensure the verification is sound by first computing a bound on the reachability diameter of the abstract model. For this computation, we developed a set of heuristics that we term the "short world" approach. We present several case studies, including verification of the address translation logic in the Bochs x86 emulator, and verification of security properties of several hypervisor models.

BibTeX

@InProceedings{sinha-fmcad12,
  author = 	 {Rohit Sinha and Cynthia Sturton and Petros Maniatis and Sanjit A. Seshia and David Wagner},
  title = 	 {Verification with Small and Short Worlds},
  booktitle = {Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD)},
  month = {October},
  year = 	 {2012},
  abstract = {We consider the verification of safety properties in systems with large 
arrays and data structures. Such systems are common at the low levels of 
software stacks; examples are hypervisors and CPU emulators. The very 
large data structures in such systems (e.g., address-translation tables 
and other caches) make automated verification based on straightforward 
state-space exploration infeasible.  We present S2W, a new 
abstraction-based model-checking methodology to facilitate automated 
verification of such systems.  As a first step, inductive invariant 
checking is performed.  If that fails, we compute an abstraction of the 
original system by precisely modeling only a subset of state variables 
while allowing the rest of the state to evolve arbitrarily at each step. 
This subset of the state constitutes a "small world" hypothesis, and 
is extracted from the property.  Finally, we verify the safety property 
on the abstract model using bounded model checking.  We ensure the 
verification is sound by first computing a bound on the reachability 
diameter of the abstract model. For this computation, we developed a set 
of heuristics that we term the "short world" approach. 
We present several case studies, including verification of the address translation logic in the  
Bochs x86 emulator, and verification of security properties of several hypervisor models.},
}