學術產出-Proceedings

Article View/Open

Publication Export

Google ScholarTM

政大圖書館

Citation Infomation

題名 A Symbolic Model Checking Approach to the Analysis of String and Length Constraints
作者 郁方
Yu, Fang
Wang, Hung-En;Chen, Shih-Yu;Yu, Fang;Jiang, Jie-Hong R.
貢獻者 資管系
關鍵詞 length constraint; string analysis; symbolic model checking
日期 2018-07
上傳時間 29-Nov-2018 16:23:06 (UTC+8)
摘要 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.
關聯 ASE 2018 Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering , Pages 623-633 , Montpellier, France — September 03 - 07, 2018
資料類型 conference
DOI https://doi.org/10.1145/3238147.3238189
dc.contributor 資管系
dc.creator (作者) 郁方zh_TW
dc.creator (作者) Yu, Fangen_US
dc.creator (作者) Wang, Hung-En;Chen, Shih-Yu;Yu, Fang;Jiang, Jie-Hong R.en_US
dc.date (日期) 2018-07
dc.date.accessioned 29-Nov-2018 16:23:06 (UTC+8)-
dc.date.available 29-Nov-2018 16:23:06 (UTC+8)-
dc.date.issued (上傳時間) 29-Nov-2018 16:23:06 (UTC+8)-
dc.identifier.uri (URI) http://nccur.lib.nccu.edu.tw/handle/140.119/121164-
dc.description.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.en_US
dc.format.extent 1252244 bytes-
dc.format.mimetype application/pdf-
dc.relation (關聯) ASE 2018 Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering , Pages 623-633 , Montpellier, France — September 03 - 07, 2018
dc.subject (關鍵詞) length constraint; string analysis; symbolic model checkingen_US
dc.title (題名) A Symbolic Model Checking Approach to the Analysis of String and Length Constraintsen_US
dc.type (資料類型) conference
dc.identifier.doi (DOI) 10.1145/3238147.3238189
dc.doi.uri (DOI) https://doi.org/10.1145/3238147.3238189