近日，中国科学院软件研究所在支持编程语言中正则表达式非经典特性的字符串约束求解研究方面取得进展，提出了带权重的流字符串转换器的新自动机模型，对正则表达式的非经典特性进行形式建模，并根据该模型设计了新的字符串约束求解算法，研制了国际上第一个支持对编程语言中正则表达式非经典特性进行推理的字符串约束求解器OSTRICH，其研究成果被编程语言国际顶级会议POPL 2022录用。

　　该项成果研究历时两年，由软件所张立军研究员、吴志林研究员带领的可信智能系统团队软件验证组与德国凯泽斯劳腾工业大学Anthony W. Lin研究组、英国伦敦大学皇家霍洛威学院Matthew Hague研究组和伯贝克学院Taolue Chen研究组、瑞典乌普萨拉大学Philipp Ruemmer研究组合作完成。该项成果是软件验证组成员在POPL上发表的与字符串约束求解相关的第3篇论文。

　　正则表达式是计算机科学中的基本概念，但编程语言（比如Javascript）中的正则表达式（简称为Regex）与经典的正则表达式有很大区别：编程语言中的正则表达式一般采用算子的非经典语义（比如贪婪/懒惰的Kleene star），而且包含一些新的特性（比如捕获组和引用）。字符串约束求解器是对操作字符串的程序进行自动分析与验证的基础，但由于对Regex进行形式建模比较有挑战性，已有字符串约束求解器（比如Z3、CVC4）均不支持Regex中的非经典特性。

　　可信智能系统团队软件验证组针对该问题进行了两年多的潜心研究，提出了带权重的流字符串转换器的自动机模型（简称为PSST）来对含有Regex的字符串函数的语义进行形式建模，并定义了相应的字符串约束理论。PSST使用权重来对正则表达式算子的贪婪/懒惰语义进行建模，同时使用字符串变量来对捕获组进行建模。而且，我们使用大量的实验验证了PSST语义与Javascript正则表达式实际语义的一致性。

　　进一步地，该团队证明了PSST拥有良好的封闭性和算法性质，比如正则保持性，即正则语言在PSST下的原象是正则的。团队利用PSST的良好算法性质设计了字符串约束求解算法，其主要思想是通过计算象和原象来传播正则约束。虽然该团队定义的字符串约束理论一般来讲是不可判定的，但是团队证明了该算法对于直线子集是完备的。团队将该算法在软件验证组开发的OSTRICH字符串约束求解器中进行了实现，并且从开源的正则表达式库中生成了超过19万5千个测试用例来评估算法的性能。实验结果表明算法在精度和效率方面都极大提升了已有的基于符号执行的方法。

　　该研究不仅在字符串约束求解研究中具有重要的意义，而且也为Web应用的高精度测试、分析、与验证，以及正则表达式的拒绝服务攻击漏洞的分析与检测奠定了理论基础。

　　论文链接