String Analysis with Logic Circuit Representation: Implementation and Optimization

網路應用程式近年來相當普及，所以網路安全成為了一個重要課題，字串操作的問題可能產生資安漏洞而導致惡意的網路攻擊，為了偵測這些漏洞，字串分析的工具是不可或缺的。目前，字串分析的方法主要分為兩種:基於自動機的方法與基於可滿足性的方法。而這兩種方法各有各的優缺點，基於自動機的方法難以產生輸入端的攻擊實例，而基於可滿足性的方法不適於產生及時過濾惡意輸入字串的過濾器。我們提出了一個利用非決定性有限自動機來支援字串操作的方法，同時可提供攻擊實例生成與過濾器的合成。在這篇論文中，我們以邏輯電路來表示非決定性有限自動機，藉由AIG的資料結構操作自動機來支援字串分析。我們實作出名為SLOG的程式，並利用實際的網路應用程式生成測資來進行實驗。這篇論文也探討了一些進一步優化電路結構及提升運算效能的方法。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