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.
@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/entities/document/10.4230/LIPIcs.ECOOP.2023.24}, URN = {urn:nbn:de:0030-drops-182171}, doi = {10.4230/LIPIcs.ECOOP.2023.24}, annote = {Keywords: Symbolic Execution, Runtime Modelling, Symbolic Summaries} }
Feedback for Dagstuhl Publishing