A new efficient memory allocator for KLEE that supports cross-run and cross-path determinism as well as spatially and temporally distanced allocations.
Overview
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 discuss 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.
Artifact
The artifact page is available here.
Publications
-
KDAlloc: The KLEE Deterministic Allocator
Daniel Schemmel, Julian Büning, Frank Busse, Martin Nowack, Cristian Cadar
Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2023)
-
A Deterministic Memory Allocator for Dynamic Symbolic Execution
Daniel Schemmel, Julian Büning, Frank Busse, Martin Nowack, Cristian Cadar
36th European Conference on Object-Oriented Programming (ECOOP 2022)
Talks
-
KDAlloc: The KLEE Deterministic Allocator: Deterministic Memory Allocation during Symbolic Execution and Test Case Replay
Tool Talk @ ISSTA 2023
-
A Deterministic Memory Allocator for Dynamic Symbolic Execution
Talk @ ECOOP 2022
-
A Deterministic Memory Allocator for Dynamic Symbolic Execution
Talk @ KLEE 2022