Document Open Access Logo

Toward Tool-Independent Summaries for Symbolic Execution (Artifact)

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



PDF
Thumbnail PDF

Artifact Description

DARTS.9.2.7.pdf
  • Filesize: 0.63 MB
  • 4 pages

Document Identifiers

Author Details

Frederico Ramos
  • Instituto Superior Técnico, University of Lisbon, Portugal
  • INESC-ID Lisbon, Portugal
Nuno Sabino
  • Instituto Superior Técnico, University of Lisbon, Portugal
  • Carnegie Mellon University, Pittsburgh, PA, USA
  • Institute of Telecommunications, Campus de Santiago, Aveiro, Portugal
Pedro Adão
  • Instituto Superior Técnico, University of Lisbon, Portugal
  • Institute of Telecommunications, Campus de Santiago, Aveiro, Portugal
David A. Naumann
  • Stevens Institute of Technology, Hoboken, NJ, USA
José Fragoso Santos
  • Instituto Superior Técnico, University of Lisbon, Portugal
  • INESC-ID Lisbon, Portugal

Acknowledgements

The authors were supported by Fundação para a Ciência e a Tecnologia (UIDB/50008/2020, Instituto de Telecomunicações, and UIDB/50021/2020, INESC-ID multi-annual funding, and PhD grant SFRH/BD/150692/2020), project DIVINA (CMU/TIC/0053/2021), the SmartRetail project (C6632206063-00466847) financed by IAPMEI, the European Commission under grant agreement number 830892 (SPARTA), and the NSF award CNS-1718713.

Cite AsGet BibTex

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)
https://doi.org/10.4230/DARTS.9.2.7

Artifact

Artifact Evaluation Policy

The artifact has been evaluated as described in the ECOOP 2023 Call for Artifacts and the ACM Artifact Review and Badging Policy

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.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software verification and validation
  • Security and privacy → Formal methods and theory of security
Keywords
  • Symbolic Execution
  • Runtime Modelling
  • Symbolic Summaries

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. R. David, S. Bardin, T. D. Ta, L. Mounier, J. Feist, M. Potet, and J. Marion. Binsec/se: A dynamic symbolic execution toolkit for binary-level analysis. In 2016 IEEE 23rd International Conference on Software Analysis, Evolution, and Reengineering (SANER), volume 1, pages 653-656, 2016. URL: https://doi.org/10.1109/SANER.2016.43.
  2. Mark Mossberg, Felipe Manzano, Eric Hennenfent, Alex Groce, Gustavo Grieco, Josselin Feist, Trent Brunson, and Artem Dinaburg. Manticore: A user-friendly symbolic execution framework for binaries and smart contracts. In 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 1186-1189, 2019. URL: https://doi.org/10.1109/ASE.2019.00133.
  3. Nuno Sabino. Automatic vulnerability detection: Using compressed execution traces to guide symbolic execution. Master’s thesis, Instituto Superior Técnico, November 2019. Google Scholar
  4. Salvatore Sanfilippo. Simple dynamic strings [online]. 2015. Accessed: 2023-06-19. URL: https://github.com/antirez/sds.
  5. Y. Shoshitaishvili, R. Wang, C. Salls, N. Stephens, M. Polino, A. Dutcher, J. Grosen, S. Feng, C. Hauser, C. Kruegel, and G. Vigna. SOK: (State of) The Art of War: Offensive Techniques in Binary Analysis. In 2016 IEEE Symposium on Security and Privacy (SP), pages 138-157, 2016. URL: https://doi.org/10.1109/SP.2016.17.
  6. Richard Wiedenhöft. C Hash map [online]. 2014. Accessed: 2023-06-19. URL: https://gist.github.com/Richard-W/9568649.
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