近日，中国科学院软件研究所在支持编程语言中正则表达式非经典特性的字符串约束求解研究方面取得进展，提出了带权重的流字符串转换器的新自动机模型，对正则表达式的非经典特性进行形式建模，并根据该模型设计出新的字符串约束求解算法，研制出目前国际上第一个支持对编程语言中正则表达式非经典特性进行推理的字符串约束求解器OSTRICH，该成果被编程语言国际会议POPL 2022录用。
　　该成果历时两年，由软件所研究员张立军、吴志林带领的可信智能系统团队软件验证组，与德国凯泽斯劳滕工业大学Anthony W. Lin研究组、英国伦敦大学皇家霍洛威学院Matthew Hague研究组/伯贝克学院Taolue Chen研究组、瑞典乌普萨拉大学Philipp Ruemmer研究组合作完成。该成果是软件验证组成员在POPL上发表的与字符串约束求解相关的第三篇论文。
　　正则表达式是计算机科学的基本概念，但编程语言（如Javascript）中的正则表达式（简称Regex）与经典的正则表达式有较大区别：编程语言中的正则表达式一般采用算子的非经典语义（如贪婪/懒惰的Kleene star），且包含一些新的特性（如捕获组和引用）。字符串约束求解器是对操作字符串的程序进行自动分析与验证的基础，而由于对Regex进行形式建模颇有挑战性，已有字符串约束求解器（如Z3、CVC4）均不支持Regex中的非经典特性。
　　可信智能系统团队软件验证组针对该问题开展研究，提出了带权重的流字符串转换器的自动机模型（简称PSST）来对含有Regex的字符串函数的语义进行形式建模，并定义了相应的字符串约束理论。PSST使用权重来对正则表达式算子的贪婪/懒惰语义进行建模，同时使用字符串变量来对捕获组进行建模。同时，科研人员使用大量的实验验证了PSST语义与Javascript正则表达式实际语义的一致性。
　　研究进一步证明，PSST拥有良好的封闭性和算法性质，如正则保持性，即正则语言在PSST下的原象是正则的。科研团队利用PSST的良好算法性质设计了字符串约束求解算法，其主要思想是通过计算象和原象来传播正则约束。该团队定义的字符串约束理论一般来讲是不可判定的，但该团队证明了该算法对于直线子集是完备的。研究团队将该算法在软件验证组开发的OSTRICH字符串约束求解器中实现，并从开源的正则表达式库中生成了超过19万5千个测试用例来评估算法的性能。实验结果表明，算法在精度和效率方面均提升了已有的基于符号执行的方法。
　　该研究在字符串约束求解研究中具有重要意义，并为Web应用的高精度测试、分析、与验证，以及正则表达式的拒绝服务攻击漏洞的分析与检测奠定了理论基础。
　　论文链接