Ecole d'ingénieur et centre de recherche en Sciences du numérique

Systematic comparison of symbolic execution systems: Intermediate representation and its generation

Poeplau, Sebastian; Francillon, Aurélien

ACSAC 2019, Annual Computer Security Applications Conference, December 9-13, 2019, San Juan, Puerto Rico

Symbolic execution has become a popular technique for software testing and vulnerability detection. Most implementations transform the program under analysis to some intermediate representation (IR), which is then used as a basis for symbolic execution. There is a multitude of available IRs, and even more approaches to transform target programs into a respective IR. When developing a symbolic execution engine, one needs to choose an IR, but it is not clear which influence the IR generation process has on the resulting system. What are the respective benefits for symbolic execution of generating IR from source code versus lifting machine code? Does the distinction even matter? What is the impact of not using an IR, executing machine code directly?We feel that there is little scientific evidence backing the answers to those questions. Therefore, we first develop a methodology for systematic comparison of different approaches to symbolic execution; we then use it to evaluate the impact of the choice of IR and IR generation. We make our comparison framework available to the community for future research.

Document Doi Bibtex

Titre:Systematic comparison of symbolic execution systems: Intermediate representation and its generation
Mots Clés:symbolic execution, intermediate representation
Type:Conférence
Langue:English
Ville:San Juan
Pays:PORTO RICO
Date:
Département:Sécurité numérique
Eurecom ref:6000
Copyright: © ACM, 2019. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ACSAC 2019, Annual Computer Security Applications Conference, December 9-13, 2019, San Juan, Puerto Rico http://dx.doi.org/10.1145/3359789.3359796
Bibtex: @inproceedings{EURECOM+6000, doi = {http://dx.doi.org/10.1145/3359789.3359796}, year = {2019}, title = {{S}ystematic comparison of symbolic execution systems: {I}ntermediate representation and its generation}, author = {{P}oeplau, {S}ebastian and {F}rancillon, {A}ur{\'e}lien}, booktitle = {{ACSAC} 2019, {A}nnual {C}omputer {S}ecurity {A}pplications {C}onference, {D}ecember 9-13, 2019, {S}an {J}uan, {P}uerto {R}ico}, address = {{S}an {J}uan, {PORTO} {RICO}}, month = {12}, url = {http://www.eurecom.fr/publication/6000} }
Voir aussi: