Decision procedures for path feasibility of string-manipulating programs with complex operations
Decision procedures for path feasibility of string-manipulating programs with complex operations
复制标题
DOI：
10.1145/3290362
复制
发表时间：
2018-11
影响因子：
--
通讯作者：
Taolue Chen;M. Hague;A. Lin;Philipp Rümmer;Zhilin Wu
中科院分区：
文献类型：
--
作者：
Taolue Chen;M. Hague;A. Lin;Philipp Rümmer;Zhilin Wu
字符串操作程序中检查路径可行性的决策过程的设计和实现是一个重要的问题，例如字符串程序的符号执行和web应用程序中跨站点脚本（XSS）漏洞的自动检测。（符号）路径是作为赋值和断言的有限序列给出的（即没有循环），检查其可行性相当于确定是否存在产生成功执行的输入。现代编程语言（例如JavaScript， PHP和Python）支持许多复杂的字符串操作，并且字符串也经常在计算过程中以一些复杂的方式被隐式修改（例如通过一些自动转义机制）。本文给出了保证路径可行性可判定性的两个一般语义条件：(1)每个断言允许正则一元分解（即是一个有效可识别的关系），(2)每个赋值使用一个（可能是不确定的）函数，其反比关系保持正则性。我们展示了语义条件是表达性的，因为它们被大量的字符串操作所满足，包括连接、单向和双向有限状态传感器、替换所有函数（其中替换字符串可以包含变量）、字符串反向函数、正则表达式匹配和一些（受限制的）字母计数/长度函数。语义条件也严格包含现有的可判定弦理论（例如直线碎片和无循环逻辑）和大多数现有基准（例如大多数Kaluza的基准，以及所有SLOG的基准，Stranger的基准和SLOTH的基准）。我们的语义条件还产生了概念上简单的决策过程，以及字符串求解器的可扩展架构，因为用户可以通过简单地提供用于图像前计算的代码，轻松地将自己的字符串函数合并到求解器中，而无需担心求解器的其他部分。尽管如此，遗憾的是，语义条件过于笼统，无法提供快速和完整的决策过程。我们以复杂性结果的形式为这一点提供了强有力的理论证据。为了解决这个问题，我们提出两个解决方案。我们的主要解决方案是在条件(2)中只允许部分字符串函数（即禁止不确定性）。在实践中，这一限制条件在许多情况下都得到了满足，从而产生了在理论和实践中都有效的决策程序。无论何时仍然需要非确定性函数（例如字符串函数split），我们的第二个解决方案是提供一个语法片段，它提供了对非确定性函数的支持，以及像单向换向器、replaceall（用常量替换字符串）、字符串反转函数、连接和正则表达式匹配这样的操作。我们表明，该片段可以简化为利用IC3等快速模型检查算法的现有求解器SLOTH。我们在一个新的字符串求解器OSTRICH中提供了我们的决策过程的有效实现（假设我们上面的第一个解，即确定性部分字符串函数）。我们的实现提供了对连接、反向、功能换能器（FFT）和替换的内置支持，并提供了一个可扩展性框架，以支持更多的字符串功能。我们证明了我们的新解算器与其他竞争性解算器的有效性。
The design and implementation of decision procedures for checking path feasibility in string-manipulating programs is an important problem, with such applications as symbolic execution of programs with strings and automated detection of cross-site scripting (XSS) vulnerabilities in web applications. A (symbolic) path is given as a finite sequence of assignments and assertions (i.e. without loops), and checking its feasibility amounts to determining the existence of inputs that yield a successful execution. Modern programming languages (e.g. JavaScript, PHP, and Python) support many complex string operations, and strings are also often implicitly modified during a computation in some intricate fashion (e.g. by some autoescaping mechanisms). In this paper we provide two general semantic conditions which together ensure the decidability of path feasibility: (1) each assertion admits regular monadic decomposition (i.e. is an effectively recognisable relation), and (2) each assignment uses a (possibly nondeterministic) function whose inverse relation preserves regularity. We show that the semantic conditions are expressive since they are satisfied by a multitude of string operations including concatenation, one-way and two-way finite-state transducers, replaceall functions (where the replacement string could contain variables), string-reverse functions, regular-expression matching, and some (restricted) forms of letter-counting/length functions. The semantic conditions also strictly subsume existing decidable string theories (e.g. straight-line fragments, and acyclic logics), and most existing benchmarks (e.g. most of Kaluza’s, and all of SLOG’s, Stranger’s, and SLOTH’s benchmarks). Our semantic conditions also yield a conceptually simple decision procedure, as well as an extensible architecture of a string solver in that a user may easily incorporate his/her own string functions into the solver by simply providing code for the pre-image computation without worrying about other parts of the solver. Despite these, the semantic conditions are unfortunately too general to provide a fast and complete decision procedure. We provide strong theoretical evidence for this in the form of complexity results. To rectify this problem, we propose two solutions. Our main solution is to allow only partial string functions (i.e., prohibit nondeterminism) in condition (2). This restriction is satisfied in many cases in practice, and yields decision procedures that are effective in both theory and practice. Whenever nondeterministic functions are still needed (e.g. the string function split), our second solution is to provide a syntactic fragment that provides a support of nondeterministic functions, and operations like one-way transducers, replaceall (with constant replacement string), the string-reverse function, concatenation, and regular-expression matching. We show that this fragment can be reduced to an existing solver SLOTH that exploits fast model checking algorithms like IC3. We provide an efficient implementation of our decision procedure (assuming our first solution above, i.e., deterministic partial string functions) in a new string solver OSTRICH. Our implementation provides built-in support for concatenation, reverse, functional transducers (FFT), and replaceall and provides a framework for extensibility to support further string functions. We demonstrate the efficacy of our new solver against other competitive solvers.