| Title: | A Symbolic Model Checking Approach to the Analysis of String and Length Constraints |
| Authors: | 郁方
Yu, Fang
Wang, Hung-En;Chen, Shih-Yu;Yu, Fang;Jiang, Jie-Hong R. |
| Contributors: | 資管系 |
| Keywords: | length constraint;string analysis;symbolic model checking |
| Date: | 2018-07 |
| Issue Date: | 2018-11-29 16:23:06 (UTC+8) |
| Abstract: | Strings with length constraints are prominent in software security analysis. Recent endeavors have made significant progress in developing constraint solvers for strings and integers. Most prior methods are based on deduction with inference rules or analysis using automata. The former may be inefficient when the constraints involve complex string manipulations such as language replacement; the latter may not be easily extended to handle length constraints and may be inadequate for counterexample generation due to approximation. Inspired by recent work on string analysis with logic circuit representation, we propose a new method for solving string with length constraints by an implicit representation of automata with length encoding. The length-encoded automata are of infinite states and can represent languages beyond regular expressions. By converting string and length constraints into a dependency graph of manipulations over length-encoded automata, a symbolic model checker for infinite state systems can be leveraged as an engine for the analysis of string and length constraints. Experiments show that our method has its unique capability of handling complex string and length constraints not solvable by existing methods. |
| Relation: | ASE 2018 Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering , Pages 623-633 , Montpellier, France — September 03 - 07, 2018 |
| Data Type: | conference |
| DOI 連結: | https://doi.org/10.1145/3238147.3238189 |
| Appears in Collections: | [資訊管理學系] 會議論文
|
