Symbolic assertion mining for security validation

Alessandro Danese1,a, Valeria Bertacco1,b and Graziano Pravadelli2
1University of Verona, Italy
aalessandro.danese@univr.it
bgraziano.pravadelli@univr.it
2University of Michigan, Ann Arbor, MI, USA
valeria@umich.edu

ABSTRACT


This paper presents DOVE, a validation framework to identify points of vulnerability inside IP firmwares. The framework relies on the symbolic simulation of the firmware to search for corner cases in its computational paths that may hide vulnerabilities. Then, DOVE automatically mine a compact set of formal assertions representing these unlikely paths to guide the analysis of the verification engineers. Experimental results on two case studies show the effectiveness of the generated assertions in pinpointing actual vulnerabilities and its efficiency in terms of execution time.



Full Text (PDF)