DARTS.9.2.7.pdf
- Filesize: 0.63 MB
- 4 pages
Document
Toward Tool-Independent Summaries for Symbolic Execution (Artifact)
Authors
Frederico Ramos 
,
Nuno Sabino ,
Pedro Adão ,
David A. Naumann ,
José Fragoso Santos
-
Part of:
Issue:
Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023)
Volume: DARTS, Volume 9 (ECOOP 2023)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-07-11
Artifact Description
Document Identifiers
Author Details
- Instituto Superior Técnico, University of Lisbon, Portugal
- INESC-ID Lisbon, Portugal
- Instituto Superior Técnico, University of Lisbon, Portugal
- Carnegie Mellon University, Pittsburgh, PA, USA
- Institute of Telecommunications, Campus de Santiago, Aveiro, Portugal
- Instituto Superior Técnico, University of Lisbon, Portugal
- Institute of Telecommunications, Campus de Santiago, Aveiro, 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
https://doi.org/10.4230/DARTS.9.2.7
Artifact
DARTS-9-2-7-artifact-2d124f1174690bd2451636860b4b804b.gz
(Filesize: 1.32 GB)
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)
0PDF Downloads
References
- 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.
- 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.
-
Nuno Sabino. Automatic vulnerability detection: Using compressed execution traces to guide symbolic execution. Master’s thesis, Instituto Superior Técnico, November 2019.
- Salvatore Sanfilippo. Simple dynamic strings [online]. 2015. Accessed: 2023-06-19. URL: https://github.com/antirez/sds.
- 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.
- Richard Wiedenhöft. C Hash map [online]. 2014. Accessed: 2023-06-19. URL: https://gist.github.com/Richard-W/9568649.