Constraint Solving with Deep Learning for Symbolic Execution
This addresses a bottleneck in software analysis for developers and security researchers, though it is an incremental improvement over existing reuse techniques.
The paper tackles the high cost of constraint solving in symbolic execution by introducing DeepSolver, a deep learning-based approach that trains a neural network to classify path conditions for satisfiability, resulting in high accuracy and improved efficiency over state-of-the-art techniques.
Symbolic execution is a powerful systematic software analysis technique, but suffers from the high cost of constraint solving, which is the key supporting technology that affects the effectiveness of symbolic execution. Techniques like Green and GreenTrie reuse constraint solutions to speed up constraint solving for symbolic execution; however, these reuse techniques require syntactic/semantic equivalence or implication relationship between constraints. This paper introduces DeepSover, a novel approach to constraint solving with deep learning for symbolic execution. Our key insight is to utilize the collective knowledge of a set of constraint solutions to train a deep neural network, which is then used to classify path conditions for their satisfiability during symbolic execution. Experimental evaluation shows DeepSolver is highly accurate in classifying path conditions, is more efficient than state-of-the-art constraint solving and constraint solution reuse techniques, and can well support symbolic execution tasks.