DROPS

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}
}

Document

Artifact

DOI: 10.4230/DARTS.9.2.7

Toward Tool-Independent Summaries for Symbolic Execution (Artifact)

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

Published in: DARTS, Volume 9, Issue 2, Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract

The artifact contains the extended versions of the tools angr and AVD with support for the symbolic reflection API proposed in the paper. Additionally, the artifact contains the source code of SumBoundVerify, our novel tool for the bounded-verification of symbolic summaries for the C programming language. The artifact contains all the scripts and datasets required to obtain the results presented in the paper, including: a library of 67 symbolic summaries implemented using the proposed symbolic reflection API; two symbolic test suites designed to test two open source C libraries; and the source code of the third-party summaries that were validated checked with SumBoundVerify.

Cite as

Frederico Ramos, Nuno Sabino, Pedro Adão, David A. Naumann, and José Fragoso Santos. Toward Tool-Independent Summaries for Symbolic Execution (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 7:1-7:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{ramos_et_al:DARTS.9.2.7,
  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 (Artifact)}},
  pages =	{7:1--7:4},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2023},
  volume =	{9},
  number =	{2},
  editor =	{Ramos, Frederico and Sabino, Nuno and Ad\~{a}o, Pedro and Naumann, David A. and Fragoso Santos, Jos\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.7},
  URN =		{urn:nbn:de:0030-drops-182478},
  doi =		{10.4230/DARTS.9.2.7},
  annote =	{Keywords: Symbolic Execution, Runtime Modelling, Symbolic Summaries}
}

Search Results

Documents authored by Sabino, Nuno

Toward Tool-Independent Summaries for Symbolic Execution

Abstract

Cite as

Toward Tool-Independent Summaries for Symbolic Execution (Artifact)

Abstract

Cite as

Thanks for your feedback!

Could not send message