[發明專利]一種基于共享不可行路徑池的代碼并行驗證方法和裝置

在審

• 申請號: 202010344638.2
• 申請日: 2020-04-27
• 公開（公告）號: CN111444112A
• 公開（公告）日: 2020-07-24
• 發明（設計）人: 卜磊;閭樂成;謝準一;郭育鯤;趙建華;李宣東
• 申請（專利權）人: 南京大學
• 主分類號: G06F11/36
• 分類號: G06F11/36;G06F8/41
• 代理公司: 江蘇銀創律師事務所 32242
• 代理人: 孫計良

本發明公開了一種基于共享不可行路徑池的代碼并行驗證方法和裝置。該方法分為初始化過程、找出潛在路徑過程和對潛在路徑分析過程。在初始化過程中，輸入的源程序和驗證目標被構建成相應的SAT約束編碼G。然后通過對不可行路徑池中路徑和SAT約束編碼G的SAT求解，得到其SAT解對應的路徑作為潛在路徑存入并行任務池。再以多線程并行方式對并行任務池各個潛在路徑進行SMT求解，若SMT無解，則抽取不可滿足的最小集合X對應的不可行程序路徑片段加入至不可行路徑池。由此通過迭代，最終得到驗證目標是否可達。為提高驗證效率，本發明還增加了對不可行路徑剪枝步驟。相比于現有技術，本發明大大提高代碼驗證效率。

技術領域

本發明涉及軟件安全領域，特別涉及通過模型驗證軟件代碼安全性的技術。

背景技術

隨著計算機技術的不斷發展，計算機軟件在人們的日常生活中扮演著越來越重要的角色。在此情況下，軟件的安全性和正確性保障已經成為當前至關重要的問題。

模型檢驗方法是新近所提出的用于檢驗軟件安全性的方法。該方法利用現代編譯器將代碼轉化為中間代碼，在中間代碼的基礎上建模進行約束抽取，并對約束求解得到驗證結果。模型檢驗方法由于易于自動化和提供反例而成為軟件安全領域的熱門。

在最初的模型檢驗方法中，將程序代碼作為一個整體，通過對整體代碼行為進行編碼求解以判斷代碼的安全性。但在實際應用的環境中，由于現實所使用的軟件規模通常都非常龐大，程序代碼作為一個整體進行建模，抽取約束，再進行約束求解驗證所需要耗費的資源非常龐大，耗時也非常長，因此很難實際應用。

為降低模型檢驗方法的復雜度，現有技術提出了面向路徑進行模型檢驗的方法，也就是每次模型檢驗單獨驗證一條執行路徑而非程序代碼整體。但這種面向路徑進行模型檢驗存在程序路徑數過于龐大的問題，也就是若程序路徑數目非常大，需要驗證的路徑也非常多，該方法進行約束求解驗證所需要耗費的資源同樣非常龐大，耗時非常長。

發明內容

本發明所要解決的問題：提高面向路徑進行模型檢驗的效率。

為解決上述問題，本發明采用的方案如下：

根據本發明的一種基于共享不可行路徑池的代碼并行驗證方法，包括如下步驟：

S1：獲取用戶輸入的源代碼和驗證目標，所述驗證目標為用戶所輸入的源代碼中指定位置在所指定的步數內是否可達；

S2：將用戶輸入的源代碼轉換成流程控制狀態圖，并初始化并行任務池T為空，共享不可行路徑池I為空以及所述并行任務池T的最大路徑數K；

S3：根據流程控制狀態圖和驗證目標構建SAT約束編碼G；

S4：將所述共享不可行路徑池I中的各個路徑片段取反編碼后與所述SAT約束編碼G輸入至SAT求解器進行求解；若SAT求解器有解，則將SAT求解器所求的解對應至程序路徑生成相應的潛在程序路徑加入至所述并行任務池T，并將該組解取反加入所述SAT約束編碼G以避免重復路徑；若SAT求解器無解，則說明用戶所輸入的源代碼指定位置在所指定的步數內不可達，結束代碼驗證；

S5：持續步驟S4直到所述并行任務池T中的潛在程序路徑數達到最大路徑數K；

S6：根據并行任務池T的最大路徑數K構建包含K個線程的線程組，然后將所述并行任務池T中的每個潛在程序路徑分別輸入至線程組的各個線程中，由對應的線程進行SMT求解；所述SMT求解包括如下步驟：

S61：根據所輸入的潛在程序路徑和所述流程控制狀態圖構建SMT約束編碼W；