A deterministic memory allocator for dynamic symbolic execution

File Description SizeFormat 
kdalloc.pdfFile embargoed until 01 January 10000710.36 kBAdobe PDF    Request a copy
Title: A deterministic memory allocator for dynamic symbolic execution
Authors: Schemmel, D
Büning, J
Busse, F
Nowack, M
Cadar, C
Item Type: Conference Paper
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.
Date of Acceptance: 13-May-2022
URI: http://hdl.handle.net/10044/1/97506
ISSN: 1868-8969
Publisher: Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
Journal / Book Title: LIPIcs : Leibniz International Proceedings in Informatics
Copyright Statement: This paper is embargoed until publication.
Sponsor/Funder: European Research Council (ERC)
Funder's Grant Number: 819141
Conference Name: 36th European Conference on Object-Oriented Programming (ECOOP 2022)
Publication Status: Accepted
Start Date: 2022-06-06
Finish Date: 2022-06-10
Conference Place: Berlin, Germany
Embargo Date: publication subject to indefinite embargo
Appears in Collections:Computing