Symbolic Software Model Validation

Cynthia Sturton, Rohit Sinha, Thurston H.Y. Dang, Sakshi Jain, Michael McCoyd, Wei-Yang Tan, Petros Maniatis, Sanjit A. Seshia, and David Wagner. Symbolic Software Model Validation. In Proceedings of the 10th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), October 2013. To appear

Download

[pdf] 

Abstract

Modeling is the crucial first step in formal verification. Some models are constructed by humans from source code, while others are extracted automatically by tools. Regardless of how a model is constructed, verification is only as good as the model; therefore, it is essential to validate the model against the implementation it represents. In this paper we present two complementary approaches to software model validation. The first, data-centric model validation, checks that, for data structures relevant to the property being verified, all operations that update these data structures are captured in the model. The second, operation-centric model validation, checks that each operation being modeled is correctly simulated by the model. Both techniques are based on a combination of symbolic execution and satisfiability modulo theories (SMT) solving. We demonstrate the application of our methods on several case studies, including the address translation logic in the Bochs x86 emulator, the Berkeley Packet Filter, a TCAS benchmark suite, the FTP server from GNU Inetutils, and a component of the XMHF hypervisor.

BibTeX

@InProceedings{sturton-memocode13,
  author = 	 {Cynthia Sturton and Rohit Sinha and Thurston H.Y. Dang and Sakshi Jain and Michael McCoyd and Wei-Yang Tan and Petros Maniatis and Sanjit A. Seshia and David Wagner},
  title = 	 {Symbolic Software Model Validation}, 
  booktitle = 	 {Proceedings of the 10th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE)}, 
  month = {October},
  year = 	 {2013},
  note = {To appear},
  abstract = {Modeling is the crucial first step in formal verification. 
Some models are constructed by humans from source 
code, while others are extracted automatically by tools. Regardless of how a model is constructed, verification is only 
as good as the model; therefore, it is essential to validate the 
model against the implementation it represents. In this paper 
we present two complementary approaches to software model 
validation. The first, data-centric model validation, checks that, 
for data structures relevant to the property being verified, all 
operations that update these data structures are captured in the 
model. The second, operation-centric model validation, checks 
that each operation being modeled is correctly simulated by the 
model. Both techniques are based on a combination of symbolic 
execution and satisfiability modulo theories (SMT) solving. We 
demonstrate the application of our methods on several case 
studies, including the address translation logic in the Bochs 
x86 emulator, the Berkeley Packet Filter, a TCAS benchmark 
suite, the FTP server from GNU Inetutils, and a component of 
the XMHF hypervisor.},
}