String Analysis with Logic Circuit Representation: Implementation and Optimization

Web applications is popular in recent years, so web security becomes a severe issue. String manipulation mistakes can cause serious vulnerabilities and lead to malicious attacks from the Internet. To detect these vulnerabilities, string analysis tools are indispensable. Prior string analysis methods are primarily automata-based or satisfiability-based. The two approaches exhibit distinct strengths and weaknesses. Automata-based methods have difficulty generating counterexamples for system inputs, while satisfiability-based approaches are inadequate to produce filters for real-time screening of malicious inputs. We proposed a new string analysis method based on nondeterministic finite automata (NFA) operations to support string manipulations. It enables both counterexample generation and filter synthesis. In this thesis, we utilize logic circuit to represent nondeterministic finite automata and preform automata operations to support string analysis under and-inverter graph (AIG) data structure. We implement our tool, named SLOG, and evaluate it with string constraints generated from real web applications. This thesis also study ways to further optimize our circuit construction and improve the solver performance.