MACE: Model-inference-Assisted Concolic Exploration for Protocol and Vulnerability Discovery

Published version: [PDF] [PS] [PS.BZ2] [VIEW]
Full version: [PDF] [PS] [PS.BZ2] [VIEW]

@inproceedings{usenix11mace,
  author = {Chia Yuan Cho and Domagoj Babi\'c and Pongsin Poosankam and 
    Kevin Zhijie Chen and Edward XueJun Wu and Dawn Song},
  title = {{MACE: Model-inference-Assisted Concolic Exploration for
    Protocol and Vulnerability Discovery}},
  booktitle = {Proceedings of the 20th USENIX Security Symposium}, 
  year = {2011},
  location = {San Francisco, CA, USA},
  month = {Aug},
}

Abstract: Program state-space exploration is central to software security, testing, and verification. In this paper, we propose a novel technique for state-space exploration of software that maintains an ongoing interaction with its environment. Our technique uses a combination of symbolic and concrete execution to build an abstract model of the analyzed application, in the form of a finite-state automaton, and uses the model to guide further state-space exploration. Through exploration, MACE further refines the abstract model. Using the abstract model as a scaffold, our technique wields more control over the search process. In particular: (1) shifting search to different parts of the search-space becomes easier, resulting in higher code coverage, and (2) the search is less likely to get stuck in small local state-subspaces (e.g., loops) irrelevant to the application's interaction with the environment. Preliminary experimental results show significant increases in the code coverage and exploration depth. Further, our approach found a number of new deep vulnerabilities.