[發(fā)明專利]一種反例引導(dǎo)的稀疏空間流模型檢測方法及系統(tǒng)

在審

• 申請?zhí)枺?/td>: 202111316310.0
• 申請日: 2021-11-08
• 公開（公告）號: CN114047913A
• 公開（公告）日: 2022-02-15
• 發(fā)明（設(shè)計）人: 于銀菠;劉家佳;徐源琪
• 申請（專利權(quán)）人: 西北工業(yè)大學(xué)
• 主分類號: G06F8/35
• 分類號: G06F8/35;G06F8/41
• 代理公司: 西安通大專利代理有限責(zé)任公司 61200
• 代理人: 高博

1.一種反例引導(dǎo)的稀疏空間流模型檢測方法，其特征在于，包括

S1、將待驗證的C程序代碼編譯為LLVM中間代碼；

S2、將LLVM中間代碼轉(zhuǎn)換為待驗證程序的稀疏空間流模型；

S3、對稀疏空間流模型進行變量抽象，執(zhí)行顯性值分析的模型檢測算法檢測抽象處理的稀疏空間流模型中是否存在反例；

S4、對存在的反例進行可行性驗證，判斷反例路徑在原始模型是否有效；通過反例信息引導(dǎo)原始模型基于插值的抽象細化及路徑、上下文和字段敏感的強更新細化模型再次進行模型檢測，通過反例和反例路徑上是否存在弱更新判斷程序是否違反安全屬性。

2.根據(jù)權(quán)利要求1所述的反例引導(dǎo)的稀疏空間流模型檢測方法，其特征在于，將LLVM中間代碼轉(zhuǎn)換為待驗證程序的稀疏空間流模型具體為：

提取LLVM代碼的控制流自動機通過流和上下文都不敏感的Andersen指針分析算法獲取指向信息，利用弱更新函數(shù)μ(a)和a＝χ(a)描述不確定的指向關(guān)系，以過程間內(nèi)存SSA的形式描述包含所有top-level和address-taken指針變量的def-use鏈，對于指令load p，μ(a)表示指針p指向的每個變量a在指令中的可能被間接訪問；函數(shù)a＝χ(a)表示變量a的定義和使用；對于store*p＝i，a＝χ(a)表示指針p指向的每個變量a被重新定義和使用，得到稀疏值流圖通過組合控制流自動機和稀疏值流圖構(gòu)建稀疏空間流模型

3.根據(jù)權(quán)利要求2所述的反例引導(dǎo)的稀疏空間流模型檢測方法，其特征在于，控制流自動機如下：

稀疏值流圖如下：

稀疏空間流模型如下：

其中，L是程序位置集合；l₀為初始程序位置；E為控制流邊集合；S為程序中所有操作語句的集合；N代表指針變量的定義節(jié)點或者使用節(jié)點的集合；ε代表指針變量所有可能def-use鏈的集合。

4.根據(jù)權(quán)利要求1所述的反例引導(dǎo)的稀疏空間流模型檢測方法，其特征在于，對稀疏空間流模型進行變量抽象具體為：

從空的抽象精度開始，通過精度函數(shù)Π計算稀疏空間流模型中變量賦值語句的精度π，根據(jù)精度π跟蹤的變量v計算語句的顯性值抽象；將具象狀態(tài)s根據(jù)精度轉(zhuǎn)化為抽象狀態(tài)實現(xiàn)稀疏空間流模型的變量抽象。

5.根據(jù)權(quán)利要求4所述的反例引導(dǎo)的稀疏空間流模型檢測方法，其特征在于，具象狀態(tài)s為：

s：＝cs@l

其中，cs：表示給一個程序變量賦一個整數(shù)值，l∈L為一個程序位置；

抽象狀態(tài)為：

其中，as：T表示一個未知值；⊥表示無數(shù)值。

6.根據(jù)權(quán)利要求1所述的反例引導(dǎo)的稀疏空間流模型檢測方法，其特征在于，對存在的反例進行可行性驗證具體為：

定義一條路徑為一個由一系列操作語句和程序位置對組成的序列ρ，當(dāng)發(fā)現(xiàn)一條路徑ρ到達違反檢測性質(zhì)的錯誤位置時，在滿精度的情況分析反例路徑在原始模型有效性，當(dāng)約束序列不滿足時，對精度進行細化。

7.根據(jù)權(quán)利要求6所述的反例引導(dǎo)的稀疏空間流模型檢測方法，其特征在于，對精度進行細化具體為：

計算出ρ導(dǎo)致約束序列不可滿足的第一個節(jié)點，利用函數(shù)SeqInterpolant計算出插值序列I；在獲取插值序列I后，將對應(yīng)程序位置l_k的插值l_k所用的程序變量細化到以l_k為起點，沿著路徑ρ后向的所有位置的精度中，同時函數(shù)BackReachability在空間流模型找出插值l_k所用變量在程序位置l_k后向的def-use鏈，將l_k所用變量被指向的指針變量加入對應(yīng)位置的精度中，為模型抽象從值空間和地址空間兩個方面，迭代細化精度。