近日，中国科学院软件研究所（以下简称软件所）在支持编程语言中正则表达式非经典特性的字符串约束求解研究方面取得进展。

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

软件所可信智能系统团队软件验证组针对该问题进行了两年多的潜心研究，提出了带权重的流字符串转换器的自动机模型（简称为PSST）来对含有Regex的字符串函数的语义进行形式建模，并定义了相应的字符串约束理论。同时，该团队还证明了PSST拥有良好的封闭性和算法性质。该研究不仅在字符串约束求解研究中具有重要的意义，而且为Web应用的高精度测试、分析与验证，以及正则表达式的拒绝服务攻击漏洞的分析与检测奠定了理论基础。其研究成果被编程语言国际顶级会议POPL 2022录用。

（高子越 袁一雪）

相关论文信息：

http://arXiv:2111.04298