基于自动机的字符串约束求解器OSTRICH

1. 成果简介

字符串操作程序往往具有高度的复杂性，其潜在缺陷可能导致严重的后果，注入攻击 (Injection) 即为其典型案例之一，已被列入 2021 年 OWASP 十大应用安全风险。近年来，为了自动识别包括注入攻击在内的程序缺陷，研究者们提出了一种名为符号执行的有效且日益普及的技术。该方法本质上是对程序的静态执行路径进行分析，将每条路径中的变量值抽象为定义在相应数据域上的约束公式。为判断这些约束的可满足性，符号执行工具需要依赖高效的约束求解器对其进行求解。需要注意的是，整数、数组和字符串数据类型广泛出现在此类程序中，因而，相关的约束求解器必须能够支持这几类数据类型与相关操作。主流的编程语言如 C++ 和 Java 等通常提供标准的字符串操作，包括字符串连接、replace (替换) 和 replaceAll (全局替换) 等。此外，Web 编程语言还普遍提供复杂的字符串操作如 htmlEscape 和 trim，用于净化恶意用户输入，这些操作通常可以方便地使用有限状态转换器 (finite transduer) 进行建模[9]。然而，除了上述仅涉及字符串数据类型的操作外，能够实现字符串与整数相互转换的操作如 length 和indexOf 等，以及能实现字符串与数组相互转换的操作如 match、split 和 join 等也在实际程序中频繁出现。有研究指出，在 18 个常见的 Web 应用中，length、indexOf、substring、split 及其变体占据了所有字符串操作调用的 80% 以上，其使用频率显著超过了其他字符串操作。整数与数组数据类型的引入进一步加剧了字符串约束的复杂性，也为求解器的理论研究与实际开发带来了新的挑战。

本课题组基于自动机模型设计了字符串约束求解算法，能够解决含整数和数组数据类型的字符串约束的可满足性问题。 具体来说，本课题组提出代价增强的有限自动机模型 (Cost-Enriched Finite Automata, CEFA)，定义代价增强的正则语言 (Cost-enriched Regular Language, CERL)，并基于 CERL的反向传播的思想设计了含有整数数据类型的字符串约束的直线子集的判定算法，该算法的主要思想是将字符串函数值域上的字符串变量相关的正则约束反向传播到字符串函数定义域上的字符串变量，同时用 CEFA 中的代价寄存器 (costregisters) 来保存字符串函数中的整数值，来达到消除字符串函数的目的。最终，约束的可满足性会被转化为 CEFAs 在线性整数算术公式约束下的非空性问题，该非空性问题是可判定的，求解复杂度为 PSPACE-complete。并且，本课题组将该方法扩展到包含字符串数组的约束求解和包含带计数操作的正则表达式的约束求解中，将整个算法实现在原型工具OSTRICH中。OSTRICH的架构如下图所示。

2. 技术先进性

该技术先进性主要体现在以下方面：

（1）提出代价增强的有限自动机模型 (Cost-Enriched Finite Automata, CEFA)，定义代价增强的正则语言 (Cost-enriched Regular Language, CERL)，并基于 CERL的反向传播的思想设计了含有整数数据类型的字符串约束的直线子集的判定算法。

（2）提出将字符串数组编码为字符串的创新性方案。

（3）用CEFA加速含有计数操作的正则表达式的字符串约束的求解。

（4）针对线性整数算术公式限定下的 CEFAs 的非空性问题求解进行了优化，主要包括基于代价寄存器的更新信息对自动机进行化简，以及基于 Parikh 像求解结果对可接受串的搜索过程进行剪枝。

3. 技术成熟度

该方法已经形成相应工具，在国际比赛SMT-COMP 2023中拿到字符串求解(QF_S)赛道的冠军，可推广使用。

4. 可应用领域

该技术可应用于自动定理证明、程序分析、程序验证和软件测试。

5. 联系人

胡登杭，hudh@ios.ac.cn，15810525156