Toward Tool-Independent Summaries for Symbolic Execution

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

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

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.

Original languageEnglish
Title of host publication37th European Conference on Object-Oriented Programming, ECOOP 2023
EditorsKarim Ali, Guido Salvaneschi
ISBN (Electronic)9783959772815
DOIs
StatePublished - Jul 2023
Event37th European Conference on Object-Oriented Programming, ECOOP 2023 - Seattle, United States
Duration: 17 Jul 202321 Jul 2023

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume263
ISSN (Print)1868-8969

Conference

Conference37th European Conference on Object-Oriented Programming, ECOOP 2023
Country/TerritoryUnited States
CitySeattle
Period17/07/2321/07/23

Keywords

  • Runtime Modelling
  • Symbolic Execution
  • Symbolic Summaries

Fingerprint

Dive into the research topics of 'Toward Tool-Independent Summaries for Symbolic Execution'. Together they form a unique fingerprint.

Cite this