Search Results

Documents authored by Schemmel, Daniel

Document
Artifact
DOI: 10.4230/DARTS.8.2.13
A Deterministic Memory Allocator for Dynamic Symbolic Execution (Artifact)

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

Published in: DARTS, Volume 8, Issue 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
KDAlloc is a deterministic memory allocator for Dynamic Symbolic Execution. This artifact provides the allocator itself, integrated into the KLEE symbolic execution engine and the evaluation thereof.
Cite as

Daniel Schemmel, Julian Büning, Frank Busse, Martin Nowack, and Cristian Cadar. A Deterministic Memory Allocator for Dynamic Symbolic Execution (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 13:1-13:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{schemmel_et_al:DARTS.8.2.13,
  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 (Artifact)}},
  pages =	{13:1--13:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Schemmel, Daniel and B\"{u}ning, Julian and Busse, Frank and Nowack, Martin and Cadar, Cristian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.2.13},
  URN =		{urn:nbn:de:0030-drops-162110},
  doi =		{10.4230/DARTS.8.2.13},
  annote =	{Keywords: memory allocation, dynamic symbolic execution}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.9
A Deterministic Memory Allocator for Dynamic Symbolic Execution

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

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

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.
Cite as

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)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.ECOOP.2022.9},
  URN =		{urn:nbn:de:0030-drops-162372},
  doi =		{10.4230/LIPIcs.ECOOP.2022.9},
  annote =	{Keywords: memory allocation, dynamic symbolic execution}
}
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 About DROPS Imprint Privacy Contact