Fine-Grain Memory Object Representation in Symbolic Execution
| Autor: | Martin Nowack |
|---|---|
| Přispěvatelé: | Engineering & Physical Science Research Council (EPSRC) |
| Rok vydání: | 2019 |
| Předmět: |
Technology
Science & Technology Speedup Computer science Engineering Electrical & Electronic 020207 software engineering 02 engineering and technology Parallel computing Computer Science Software Engineering Symbolic execution Execution time Reduction (complexity) Automation & Control Systems Engineering Memory management memory representation Computer Science Path (graph theory) 0202 electrical engineering electronic engineering information engineering State space Distributed File System Resource management (computing) symbolic execution |
| Zdroj: | ASE 34th IEEE/ACM International Conference on Automated Software Engineering (ASE 2019) |
| Popis: | Dynamic Symbolic Execution (DSE) has seen rising popularity as it allows to check applications for behaviours such as error patterns automatically. One of its biggest challenges is the state space explosion problem: DSE tries to evaluate all possible execution paths of an application. For every path, it needs to represent the allocated memory and its accesses. Even though different approaches have been proposed to mitigate the state space explosion problem, DSE still needs to represent a multitude of states in parallel to analyse them. If too many states are present, they cannot fit into memory, and DSE needs to terminate them prematurely or store them on disc intermediately. With a more efficient representation of allocated memory, DSE can handle more states simultaneously, improving its performance. In this work, we introduce an enhanced, fine-grain and efficient representation of memory that mimics the allocations of tested applications. We tested GNU Coreutils using three different search strategies with our implementation on top of the symbolic execution engine KLEE. We achieve a significant reduction of the memory consumption of states by up to 99.06% (mean DFS: 2%, BFS: 51%, Cov.: 49%), allowing to represent more states in memory more efficiently. The total execution time is reduced by up to 97.81% (mean DFS: 9%, BFS: 7%, Cov.:4%)---a speedup of 49x in comparison to baseline KLEE. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|