MACE: model-inference-assisted concolic exploration for protocol and vulnerability discovery

TLDR

Program state‑space exploration is central to software security, testing, and verification. The paper proposes a novel technique for state‑space exploration that maintains ongoing interaction with the environment. The technique combines symbolic and concrete execution to build a finite‑state automaton model that guides and refines exploration, giving more control over the search process. The approach yields higher code coverage and deeper exploration, reduces stalling in local loops, and discovers new deep vulnerabilities.

Abstract

Programstate-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.