Toward Tool-Independent Summaries for Symbolic Execution

Autor:	Ramos, Frederico, Sabino, Nuno, Adão, Pedro, Naumann, David A., Fragoso Santos, José
Jazyk:	angličtina
Rok vydání:	2023
Předmět:	Symbolic Execution Software and its engineering → Software verification and validation Runtime Modelling Security and privacy → Formal methods and theory of security Symbolic Summaries
DOI:	10.4230/lipics.ecoop.2023.24
Popis:	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. LIPIcs, Vol. 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023), pages 24:1-24:29
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::5e08b78c28e260cd81df2ab8a3a71a8a Zobrazit plný text záznamu