| Popis: |
Symbolic execution is an effective method to analyse an application's properties thoroughly, based on the idea of analysing every control flow path an application can take. Although symbolic execution has many different use cases, it suffers from two main challenges: the state space explosion problem and the computationally expensive solving of constraints collected along the paths. The primary goal of this thesis is to tackle both issues and improve the applicability of symbolic execution, i.e., allowing larger and more complex applications to be analysed by symbolic execution. This work will focus on C and C++ as languages for systems programming. Moreover, this work heavily builds on KLEE --- a symbolic execution engine based on the LLVM framework. We took on the challenge of managing the memory used by symbolic execution more efficiently. If an application is tested, symbolic execution tracks its memory. Due to the state space explosion problem, dynamic symbolic execution must handle many states simultaneously. Choosing the right granularity of tracked memory changes will positively impact symbolic execution's performance and memory utilisation. While constraint solving is one computationally expensive part of symbolic execution, incremental solving is an effective method for SMT and SAT solving to reuse existing solutions and speed up the solving process. Unfortunately, utilising this approach is less straightforward in symbolic execution as it hinders different optimisations and caching strategies used by symbolic execution. We introduce a technique that nevertheless helps to combine these methods efficiently. Furthermore, we researched how a multi-threaded symbolic execution engine can efficiently utilise process-local resources, avoiding inter-process communication. We mainly focus on the shared use of solver queries across threads by separating shared and common query constraints and re-using the latter results more efficiently across multiple queries. Besides the general challenges of symbolic execution, we found it difficult to evaluate the improvement we made along with this work. While partially caused by our learning process, we found that symbolic execution and its state-space explosion problem make it hard to compare contributions in this field and assess their impact. Therefore, we came up with Deterministic State-Space Exploration that improves this process. |
