License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2023.24
URN: urn:nbn:de:0030-drops-182171
URL: https://drops.dagstuhl.de/opus/volltexte/2023/18217/
Ramos, Frederico ;
Sabino, Nuno ;
Adão, Pedro ;
Naumann, David A. ;
Fragoso Santos, José
Toward Tool-Independent Summaries for Symbolic Execution
Abstract
We introduce a new symbolic reflection API for implementing tool-independent summaries for the symbolic execution of C programs. We formalise the proposed API as a symbolic semantics and extend two state-of-the-art symbolic execution tools with support for it. Using the proposed API, we implement 67 tool-independent symbolic summaries for a total of 26 libc functions. Furthermore, we present SumBoundVerify, a fully automatic summary validation tool for checking the bounded correctness of the symbolic summaries written using our symbolic reflection API. We use SumBoundVerify to validate 37 symbolic summaries taken from 3 state-of-the-art symbolic execution tools, angr, Binsec and Manticore, detecting a total of 24 buggy summaries.
BibTeX - Entry
@InProceedings{ramos_et_al:LIPIcs.ECOOP.2023.24,
author = {Ramos, Frederico and Sabino, Nuno and Ad\~{a}o, Pedro and Naumann, David A. and Fragoso Santos, Jos\'{e}},
title = {{Toward Tool-Independent Summaries for Symbolic Execution}},
booktitle = {37th European Conference on Object-Oriented Programming (ECOOP 2023)},
pages = {24:1--24:29},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-281-5},
ISSN = {1868-8969},
year = {2023},
volume = {263},
editor = {Ali, Karim and Salvaneschi, Guido},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18217},
URN = {urn:nbn:de:0030-drops-182171},
doi = {10.4230/LIPIcs.ECOOP.2023.24},
annote = {Keywords: Symbolic Execution, Runtime Modelling, Symbolic Summaries}
}
Keywords: |
|
Symbolic Execution, Runtime Modelling, Symbolic Summaries |
Collection: |
|
37th European Conference on Object-Oriented Programming (ECOOP 2023) |
Issue Date: |
|
2023 |
Date of publication: |
|
11.07.2023 |
Supplementary Material: |
|
Software (ECOOP 2023 Artifact Evaluation approved artifact): https://doi.org/10.4230/DARTS.9.2.7 |