1 Search Results for "Ramos, Frederico"

Document
DOI: 10.4230/LIPIcs.ECOOP.2023.24
Toward Tool-Independent Summaries for Symbolic Execution

Authors: Frederico Ramos, Nuno Sabino, Pedro Adão, David A. Naumann, and José Fragoso Santos

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

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.
Cite as

Frederico Ramos, Nuno Sabino, Pedro Adão, David A. Naumann, and José Fragoso Santos. Toward Tool-Independent Summaries for Symbolic Execution. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 24:1-24:29, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@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}
}
  • Refine by Author
  • 1 Adão, Pedro
  • 1 Fragoso Santos, José
  • 1 Naumann, David A.
  • 1 Ramos, Frederico
  • 1 Sabino, Nuno

  • Refine by Classification
  • 1 Security and privacy → Formal methods and theory of security
  • 1 Software and its engineering → Software verification and validation

  • Refine by Keyword
  • 1 Runtime Modelling
  • 1 Symbolic Execution
  • 1 Symbolic Summaries

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2023

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact