TY - GEN
T1 - Toward Tool-Independent Summaries for Symbolic Execution
AU - Ramos, Frederico
AU - Sabino, Nuno
AU - Adão, Pedro
AU - Naumann, David A.
AU - Santos, José Fragoso
N1 - Publisher Copyright:
© Frederico Ramos, Nuno Sabino, Pedro Adão, David A. Naumann, and José Fragoso Santos;
PY - 2023/7
Y1 - 2023/7
N2 - 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.
AB - 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.
KW - Runtime Modelling
KW - Symbolic Execution
KW - Symbolic Summaries
UR - http://www.scopus.com/inward/record.url?scp=85168903154&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85168903154&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.ECOOP.2023.24
DO - 10.4230/LIPIcs.ECOOP.2023.24
M3 - Conference contribution
AN - SCOPUS:85168903154
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 37th European Conference on Object-Oriented Programming, ECOOP 2023
A2 - Ali, Karim
A2 - Salvaneschi, Guido
T2 - 37th European Conference on Object-Oriented Programming, ECOOP 2023
Y2 - 17 July 2023 through 21 July 2023
ER -