What is decidable about string constraints with the ReplaceAll function
What is decidable about string constraints with the ReplaceAll function
复制标题
DOI：
10.1145/3158091
复制
发表时间：
2017-11
影响因子：
--
通讯作者：
Taolue Chen;Yan Chen;M. Hague;Anthony W. Lin;Zhilin Wu
中科院分区：
文献类型：
--
作者：
Taolue Chen;Yan Chen;M. Hague;Anthony W. Lin;Zhilin Wu
具有串联的字符串理论被广泛认为是解决弦乐操纵程序的约束的基础。但是，该理论远远不足以表达许多在实践中也需要的弦约束。例如，使用常规约束（与正则表达式的模式匹配）和字符串固定函数（替换第一次出现或所有出现``模式''字符串''字符串常数/变量/正则表达式替换''字符串常数/变量）等。常规约束和字符串固定功能对于诸如对JavaScript（或更一般的HTML5应用程序）对跨站点脚本（XSS）漏洞的应用都至关重要，这激发了我们考虑更丰富的字符串约束。越来越多地认识到字符串替换功能（尤其是替换功能）的重要性，可以通过将函数纳入几个字符串约束求解器的输入语言中来见证。最近，显示出任何包含字符串替换函数的字符串理论（即使是最有限的版本，模式/替换字符串都是恒定字符串）都无法确定的，如果我们不施加某种直线（aka acyclicity）限制在公式上。尽管如此，直线限制仍然实际上是明智的，因为通常通过符号执行生成的字符串约束来满足此条件。在本文中，我们提供了首次对直线字符串约束的系统研究，并用字符串固定功能和常规约束作为基本操作。我们表明，可以决定了一大批此类约束（即，在模式中只允许常规的字符串或正则表达式）。我们注意到，即使在此限制下，字符串替换函数也足以表达串联操作员等等（例如，使用字符串变量的正则表达式扩展）。这为我们提供了最能表达的逻辑，其中包含相同伞下的串联，替换和规则约束。我们针对直线片段的决策程序遵循自动理论方法，并且是模块化的，从某种意义上说，弦乐替换术语被一个人删除以生成越来越多的定期约束，然后可以通过状态将其放电ART字符串约束求解器。我们还表明，在某种程度上，该片段是带有弦线和常规约束的直线片段的最大可决定子类。为此，我们显示了以下两个扩展的不确定性结果：（1）替换函数的模式参数中允许变量，（2）长度约束。
The theory of strings with concatenation has been widely argued as the basis of constraint solving for verifying string-manipulating programs. However, this theory is far from adequate for expressing many string constraints that are also needed in practice; for example, the use of regular constraints (pattern matching against a regular expression), and the string-replace function (replacing either the first occurrence or all occurrences of a ``pattern'' string constant/variable/regular expression by a ``replacement'' string constant/variable), among many others. Both regular constraints and the string-replace function are crucial for such applications as analysis of JavaScript (or more generally HTML5 applications) against cross-site scripting (XSS) vulnerabilities, which motivates us to consider a richer class of string constraints. The importance of the string-replace function (especially the replace-all facility) is increasingly recognised, which can be witnessed by the incorporation of the function in the input languages of several string constraint solvers. Recently, it was shown that any theory of strings containing the string-replace function (even the most restricted version where pattern/replacement strings are both constant strings) becomes undecidable if we do not impose some kind of straight-line (aka acyclicity) restriction on the formulas. Despite this, the straight-line restriction is still practically sensible since this condition is typically met by string constraints that are generated by symbolic execution. In this paper, we provide the first systematic study of straight-line string constraints with the string-replace function and the regular constraints as the basic operations. We show that a large class of such constraints (i.e. when only a constant string or a regular expression is permitted in the pattern) is decidable. We note that the string-replace function, even under this restriction, is sufficiently powerful for expressing the concatenation operator and much more (e.g. extensions of regular expressions with string variables). This gives us the most expressive decidable logic containing concatenation, replace, and regular constraints under the same umbrella. Our decision procedure for the straight-line fragment follows an automata-theoretic approach, and is modular in the sense that the string-replace terms are removed one by one to generate more and more regular constraints, which can then be discharged by the state-of-the-art string constraint solvers. We also show that this fragment is, in a way, a maximal decidable subclass of the straight-line fragment with string-replace and regular constraints. To this end, we show undecidability results for the following two extensions: (1) variables are permitted in the pattern parameter of the replace function, (2) length constraints are permitted.