Document Open Access Logo

A Deterministic Memory Allocator for Dynamic Symbolic Execution

Authors Daniel Schemmel , Julian Büning , Frank Busse , Martin Nowack , Cristian Cadar

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2022.9.pdf
  • Filesize: 0.99 MB
  • 26 pages

Document Identifiers

Author Details

Daniel Schemmel
  • Imperial College London, UK
Julian Büning
  • RWTH Aachen University, Germany
Frank Busse
  • Imperial College London, UK
Martin Nowack
  • Imperial College London, UK
Cristian Cadar
  • Imperial College London, UK

Funding

This project has received funding from the European Research Council under the European Union’s Horizon 2020 research and innovation program (grant agreement no. 819141 and 966733).

Acknowledgements

We would like to thank Jordy Ruiz and the anonymous reviewers for their valuable feedback on the paper.

Cite AsGet BibTex

Daniel Schemmel, Julian Büning, Frank Busse, Martin Nowack, and Cristian Cadar. A Deterministic Memory Allocator for Dynamic Symbolic Execution. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 9:1-9:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ECOOP.2022.9

Abstract

Dynamic symbolic execution (DSE) has established itself as an effective testing and analysis technique. While the memory model in DSE has attracted significant attention, the memory allocator has been largely ignored, despite its significant influence on DSE. In this paper, we discuss the different ways in which the memory allocator can influence DSE and the main design principles that a memory allocator for DSE needs to follow: support for external calls, cross-run and cross-path determinism, spatially and temporally distanced allocations, and stability. We then present KDAlloc, a deterministic allocator for DSE that is guided by these six design principles. We implement KDAlloc in KLEE, a popular DSE engine, and first show that it is competitive with KLEE’s default allocator in terms of performance and memory overhead, and in fact significantly improves performance in several cases. We then highlight its benefits for use-after-free error detection and two distinct DSE-based techniques: MoKlee, a system for saving DSE runs to disk and later (partially) restoring them, and SymLive, a system for finding infinite-loop bugs.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software testing and debugging
Keywords
  • memory allocation
  • dynamic symbolic execution

Metrics

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

Supplementary Materials

References

  1. Andrew Baumann, Jonathan Appavoo, Orran Krieger, and Timothy Roscoe. A fork() in the road. In Proc. of the 17th Workshop on Hot Topics in Operating Systems (HotOS'19), May 2019. Google Scholar
  2. Emery D. Berger, Kathryn S. McKinley, Robert D. Blumofe, and Paul R. Wilson. Hoard: A scalable memory allocator for multithreaded applications. In Proc. of the 9th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS'00), November 2000. Google Scholar
  3. Emery D. Berger and Benjamin G. Zorn. DieHard: Probabilistic memory safety for unsafe languages. In Proc. of the Conference on Programing Language Design and Implementation (PLDI'06), June 2006. Google Scholar
  4. Peter Boonstoppel, Cristian Cadar, and Dawson Engler. RWset: Attacking path explosion in constraint-based test generation. In Proc. of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08), March-April 2008. Google Scholar
  5. Luca Borzacchiello, Emilio Coppa, Daniele Cono D'Elia, and Camil Demetrescu. Memory models in symbolic execution: key ideas and new thoughts. Software Testing, Verification and Reliability, 29(8), 2019. URL: https://doi.org/10.1002/stvr.1722.
  6. Jacob Burnim and Koushik Sen. Heuristics for scalable dynamic test generation. In Proc. of the 23rd IEEE International Conference on Automated Software Engineering (ASE'08), September 2008. Google Scholar
  7. Frank Busse, Martin Nowack, and Cristian Cadar. Running symbolic execution forever. In Proc. of the International Symposium on Software Testing and Analysis (ISSTA'20), July 2020. Google Scholar
  8. Cristian Cadar, Daniel Dunbar, and Dawson Engler. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proc. of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI'08), December 2008. Google Scholar
  9. Cristian Cadar and Dawson Engler. Execution generated test cases: How to make systems code crash itself. In Proc. of the 12th International SPIN Workshop on Model Checking of Software (SPIN'05), August 2005. URL: https://doi.org/10.1007/11537328_2.
  10. Cristian Cadar, Vijay Ganesh, Peter Pawlowski, David Dill, and Dawson Engler. EXE: Automatically Generating Inputs of Death. In Proc. of the 13th ACM Conference on Computer and Communications Security (CCS'06), October 2006. URL: https://doi.org/10.1145/1455518.1455522.
  11. Cristian Cadar and Koushik Sen. Symbolic Execution for Software Testing: Three Decades Later. Communications of the Association for Computing Machinery (CACM), 56(2):82-90, 2013. URL: https://doi.org/10.1145/2408776.2408795.
  12. Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In Proc. of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08), March-April 2008. Google Scholar
  13. Jason Evans. A scalable concurrent malloc(3) implementation for FreeBSD. In Proc. of the 2006 BSDCan Conference (BSDCan'06), May 2006. Google Scholar
  14. International Organization for Standardization. ISO/IEC 9899-1999: Programming Languages - C, December 1999. Google Scholar
  15. Vijay Ganesh and David L. Dill. A decision procedure for bit-vectors and arrays. In Proc. of the 19th International Conference on Computer-Aided Verification (CAV'07), July 2007. Google Scholar
  16. Timotej Kapus and Cristian Cadar. A segmented memory model for symbolic execution. In Proc. of the Joint Meeting of the European Software Engineering Conference and the ACM Symposium on the Foundations of Software Engineering (ESEC/FSE'19), August 2019. Google Scholar
  17. Doug Lea. A memory allocator. URL: http://gee.cs.oswego.edu/dl/html/malloc.html.
  18. Maged M. Michael. Scalable lock-free dynamic memory allocation. In Proc. of the Conference on Programing Language Design and Implementation (PLDI'04), June 2004. Google Scholar
  19. Nicholas Nethercote and Julian Seward. Valgrind: A program supervision framework. Electronic Notes in Theoretical Computer Science, 89(2), 2003. Google Scholar
  20. Martin Nowack. Fine-grain memory object representation in symbolic execution. In Proc. of the 34th IEEE International Conference on Automated Software Engineering (ASE'19), November 2019. Google Scholar
  21. Martin Nowack, Katja Tietze, and Christof Fetzer. Parallel symbolic execution: Merging in-flight requests. In Proc. of the Haifa Verification Conference (HVC'15), December 2015. Google Scholar
  22. Hristina Palikareva and Cristian Cadar. Multi-solver support in symbolic execution. In Proc. of the 25th International Conference on Computer-Aided Verification (CAV'13), July 2013. Google Scholar
  23. Feng Qin, Joseph Tucek, Jagadeesan Sundaresan, and Yuanyuan Zhou. Rx: treating bugs as allergies - a safe method to survive software failures. In Proc. of the 20th ACM Symposium on Operating Systems Principles (SOSP'05), October 2005. Google Scholar
  24. Anthony Romano and Dawson Engler. SymMMU: Symbolically executed runtime libraries for symbolic memory access. In Proc. of the 29th IEEE International Conference on Automated Software Engineering (ASE'14), September 2014. Google Scholar
  25. Mark E. Russinovich, David A. Solomon, and Alex Ionescu. Windowsregistered Internals, Part 2. Microsoft Press, 6th edition, September 2012. Google Scholar
  26. Daniel Schemmel, Julian Büning, Oscar Soria Dustmann, Thomas Noll, and Klaus Wehrle. Symbolic liveness analysis of real-world software. In Proc. of the 30th International Conference on Computer-Aided Verification (CAV'18), July 2018. Google Scholar
  27. Daniel Schemmel, Julian Büning, César Rodríguez, David Laprell, and Klaus Wehrle. Symbolic partial-order execution for testing multi-threaded programs. In Proc. of the 32nd International Conference on Computer-Aided Verification (CAV'20), July 2020. Google Scholar
  28. Konstantin Serebryany, Derek Bruening, Alexander Potapenko, and Dmitry Vyukov. AddressSanitizer: A fast address sanity checker. In Proc. of the 2012 USENIX Annual Technical Conference (USENIX ATC'12), June 2012. Google Scholar
  29. Julian Seward and Nicholas Nethercote. Using Valgrind to detect undefined value errors with bit-precision. In Proc. of the 2005 USENIX Annual Technical Conference (USENIX ATC'05), April 2005. Google Scholar
  30. Matthias Springer and Hidehiko Masuhara. DynaSOAr: A parallel memory allocator for object-oriented programming on GPUs with efficient memory access. In Proc. of the 33rd European Conference on Object-Oriented Programming (ECOOP'19), July 2019. Google Scholar
  31. David Trabish, Shachar Itzhaky, and Noam Rinetzky. Address-aware query caching for symbolic execution. In Proc. of the IEEE International Conference on Software Testing, Verification, and Validation (ICST'21), April 2021. Google Scholar
  32. David Trabish and Noam Rinetzky. Relocatable addressing model for symbolic execution. In Proc. of the International Symposium on Software Testing and Analysis (ISSTA'20), July 2020. Google Scholar
  33. Guowei Yang, Corina S. Păsăreanu, and Sarfraz Khurshid. Memoized symbolic execution. In Proc. of the International Symposium on Software Testing and Analysis (ISSTA'12), July 2012. Google Scholar
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact