Fine-grain memory object representation in symbolic execution
File(s)
Accepted version
Author(s)
Nowack, Martin
Type
Conference Paper
Abstract
Dynamic Symbolic Execution (DSE) has seen risingpopularity as it allows to check applications for behaviours suchas error patterns automatically. One of its biggest challenges is thestate space explosion problem: DSE tries to evaluate all possibleexecution paths of an application. For every path, it needs torepresent the allocated memory and its accesses. Even thoughdifferent approaches have been proposed to mitigate the statespace explosion problem, DSE still needs to represent a multitudeof states in parallel to analyse them. If too many states arepresent, they cannot fit into memory, and DSE needs to terminatethem prematurely or store them on disc intermediately. Witha more efficient representation of allocated memory, DSE canhandle more states simultaneously, improving its performance.In this work, we introduce an enhanced, fine-grain and efficientrepresentation of memory that mimics the allocations of testedapplications. We tested GNU Coreutils using three differentsearch strategies with our implementation on top of the symbolicexecution engine KLEE. We achieve a significant reduction ofthe memory consumption of states by up to 99.06% (mean DFS:2%, BFS: 51%, Cov.: 49%), allowing to represent more states inmemory more efficiently. The total execution time is reduced byup to 97.81% (mean DFS: 9%, BFS: 7%, Cov.:4%)—a speedupof 49x in comparison to baseline KLEE.
Date Issued
2020-01-09
Date Acceptance
2019-09-17
Citation
2020, pp.1-12
Publisher
IEEE
Start Page
1
End Page
12
Copyright Statement
© 2020 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
Sponsor
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Identifier
https://ieeexplore.ieee.org/document/8952548
Grant Number
EP/N007166/1
EP/R011605/1
Source
34th IEEE/ACM International Conference on Automated Software Engineering (ASE 2019)
Subjects
Science & Technology
Technology
Automation & Control Systems
Computer Science, Software Engineering
Engineering, Electrical & Electronic
Computer Science
Engineering
symbolic execution
memory representation
Publication Status
Published
Start Date
2019-11-10
Finish Date
2019-11-15
Coverage Spatial
San Diego, CA, USA
Date Publish Online
2020-01-09