License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2022.9
URN: urn:nbn:de:0030-drops-162372
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16237/
Go to the corresponding LIPIcs Volume Portal

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

A Deterministic Memory Allocator for Dynamic Symbolic Execution

pdf-format:
LIPIcs-ECOOP-2022-9.pdf (1.0 MB)

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.

BibTeX - Entry

@InProceedings{schemmel_et_al:LIPIcs.ECOOP.2022.9,
  author =	{Schemmel, Daniel and B\"{u}ning, Julian and Busse, Frank and Nowack, Martin and Cadar, Cristian},
  title =	{{A Deterministic Memory Allocator for Dynamic Symbolic Execution}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{9:1--9:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16237},
  URN =		{urn:nbn:de:0030-drops-162372},
  doi =		{10.4230/LIPIcs.ECOOP.2022.9},
  annote =	{Keywords: memory allocation, dynamic symbolic execution}
}

Keywords: memory allocation, dynamic symbolic execution
Collection: 36th European Conference on Object-Oriented Programming (ECOOP 2022)
Issue Date: 2022
Date of publication: 23.06.2022
Supplementary Material: Software (ECOOP 2022 Artifact Evaluation approved artifact): https://doi.org/10.4230/DARTS.8.2.13

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI