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)
