String Analysis via Automata Manipulation with Logic Circuit Representation
Autor: | Jie-Hong R. Jiang, Chun-Han Lin, Hung-En Wang, Fang Yu, Tzung-Lin Tsai |
---|---|
Rok vydání: | 2016 |
Předmět: |
Theoretical computer science
Finite-state machine Computer science String (computer science) 020207 software engineering 02 engineering and technology Data structure Automaton Nondeterministic algorithm 0202 electrical engineering electronic engineering information engineering Attack patterns 020201 artificial intelligence & image processing State (computer science) Logic optimization |
Zdroj: | Computer Aided Verification ISBN: 9783319415277 CAV (1) |
DOI: | 10.1007/978-3-319-41528-4_13 |
Popis: | Many severe security vulnerabilities in web applications can be attributed to string manipulation mistakes, which can often be avoided through formal string analysis. String analysis tools are indispensable and under active development. Prior string analysis methods are primarily automata-based or satisfiability-based. The two approaches exhibit distinct strengths and weaknesses. Specifically, existing automata-based methods have difficulty in generating counterexamples at system inputs to witness vulnerability, whereas satisfiability-based methods are inadequate to produce filters amenable for firmware or hardware implementation for real-time screening of malicious inputs to a system under protection. In this paper, we propose a new string analysis method based on a scalable logic circuit representation for (nondeterministic) finite automata to support various string and automata manipulation operations. It enables both counterexample generation and filter synthesis in string constraint solving. By using the new data structure, automata with large state spaces and/or alphabet sizes can be efficiently represented. Empirical studies on a large set of open source web applications and well-known attack patterns demonstrate the unique benefits of our method compared to prior string analysis tools. |
Databáze: | OpenAIRE |
Externí odkaz: |