近日，中國科學院軟件研究所在支持編程語言中正則表達式非經典特性的字符串約束求解研究方面取得進展，提出了帶權重的流字符串轉換器的新自動機模型，對正則表達式的非經典特性進行形式建模，并根據該模型設計了新的字符串約束求解算法，研制了國際上第一個支持對編程語言中正則表達式非經典特性進行推理的字符串約束求解器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應用的高精度測試、分析、與驗證，以及正則表達式的拒絕服務攻擊漏洞的分析與檢測奠定了理論基礎。

　　論文鏈接