Design and Implementation of a Parallel Symbolic Execution Engine Based on Multi-Threading

Symbolic execution, as an effective test generation technique, has been increasingly used for software testing and vulnerability discovery, etc. However, the number of execution paths in a program rises exponentially with the number of branches, and symbolic execution can hardly be performed efficiently on large-scale programs, leading to poor scalability. Considering that multi-processed parallel symbolic execution approaches not only suffer from high communication overhead, but also fail to use the existing constraint solving optimization techniqnes. To tackle the above problems, we devise a novel work-stealing algorithm that requires no centralized nodes. In addition, to exploit the existing constraint solving optimizations, we enable different worker nodes to share the constraint solving information so as to accelerate the solving process. Based on the above mechanisms, we implement our parallel engine PKLEE (parallel KLEE) on the top of KLEE and conduct the experimental evaluations on it. In the exhaustive execution path scenario, the average time consumed by KLEE is three to four times longer than that of PKLEE with 8 threads available, and the effective workload executed by PKLEE is on average three times higher than that of KLEE in the same period of time.