面向計算機并發程序的形式化驗證方法設計
摘 要：
計算機并發性程序形式化驗證一直是軟件安全領域的難題。軟件并發性漏洞難以被發現，一旦發生問題，會造成不可估量的安全問題。形式化驗證基于嚴格的數學推導基礎，采用語言、語義、推理證明三位一體方法，構建形式邏輯系統，以確保被驗證系統的安全性能。傳統的形式化驗證方法由于人工參與多、驗證工作量大、驗證效率低等不足，難以對計算機并發程序進行嚴謹高效的模型描述與驗證。研究了一種可雙向轉換的并發性程序形式化驗證方法，解決了人工抽象建模存在的工作量大且易出錯的問題，并且保證了源碼層與抽象層驗證的一致性，大幅提升了形式化驗證的效率。
內容目錄：
1 并發性驗證基本路線
2 并發性驗證方法設計
2.1 中間層規范生成模塊
2.2 自動化并發性驗證模塊設計
2.3 自動化功能性驗證模塊設計
2.4 集成模塊設計
3 實驗過程和結果
3.1 中間層規范生成
3.2 自動向上映射及并發屬性驗證
3.3 自動向下映射及功能性驗證
3.4 驗證結果分析
4 結 語
形式化驗證作為一種基于嚴格數學推理的計算機軟件安全性和可靠性保障技術，近年來已經取得了巨大的進展。但是，隨著計算機系統越來越復雜，提供的功能越來越強大，其蘊含的安全性問題也日益嚴峻，因此對形式化驗證方法提出了更高的要求。計算機并發技術在高效利用計算機資源的同時，可能存在對計算機軟件安全造成很大威脅的并發錯誤。利用形式化驗證找出軟件中的并發錯誤并排除其帶來的安全隱患成為形式化方法研究領域的一個重點方向。
基于形式化驗證并發錯誤的研究主要包含兩個方面：以定理證明為例的演繹推理方法和以模型檢測為例的建模和驗證方法。前者通常利用從系統生成的一組規則并進行推理證明，以驗證系統是否滿足指定的規則。而模型檢測是一種對有限狀態的并發軟件系統進行自動化驗證的技術，其實現方式是使用過程建模語言將需要驗證的軟件系統進行重新建模，將軟件系統內部的數據、行為和實體進行抽象，并在系統模型代碼中加入相應的并發性驗證代碼，最后輸入到模型檢查引擎中得出并發性驗證結果。
經過相關工作人員的大量研究，目前針對并發程序的形式化驗證工作已經有部分成效。在早期的研究中，Taylor給出并發狀態、并發歷史等相關概念，并且提出了一種基于并發歷史的并發錯誤分析方法。Foster 等人將定理證明這一形式化方法引入并發問題檢測中，通過對程序的形式化規約進行靜態分析以檢測并發性漏洞。Enans在工具 LCLint 中實現了靜態檢測方法，并通過內存標注來檢測并發錯誤。在并發性形式化驗證的早期研究中，檢測目標的規模一般較小，復雜度不高，驗證過程的自動化程度較低，難以驗證大型并發軟件。
在近年針對軟件并發性驗證的研究中，研究人員基于驗證對象提出了不同的框架和方法。例如，采用符號執行、進程代數分析以及模型檢測等方式和思路，對軟件的并發性進行了形式化驗證。相較于早期的研究，其在自動化程度上有了進一步的提升。Kaki 等人利用進程代數，提出了一種針對并發和分布式程序行為特性的驗證技術，這種技術使用進程代數對建模程序行為進行自動抽象，彌補了程序實現與其模型之間的典型差距。吳亞楠設計了一個動態數據競爭檢測工具，提出了一種分層過濾的方法，可以減少動態監視程序執行行為的高性能開銷，以實現高效檢測多線程程序的數據競爭和驗證有害競爭。Foster 等人提出了一種具有大或無限狀態空間的并行反應程序的代數驗證策略，并利用反應關系和克萊尼代數證明了該策略的可行性。進程代數分析和符號執行的引入使得并發系統定義的精確程度有了進一步的提高，但在驗證效率方面依然無法支持大型復雜軟件的并發性驗證工作。
隨著形式化方法中模型檢測技術的發展和完善，不斷有研究人員將其應用在并發性形式化驗證上。Guellati 等人 改進了自動狀態機的模型檢測算法，將基于時間計算樹邏輯（Time Computation Tree Logic，TCTL）模型檢查算法應用于持續動作定時自動機模型，對模型檢驗算法和可表達及驗證的性質范圍進行了改進和擴展，使得模型可以捕捉系統行為中真正的并發性。David 等人 研究了一套基于依賴保證的并發程序驗證框架（CSim2），可實現對并發系統進行自頂向下的組合驗證，通過使用模擬框架，在頂層上進行驗證的屬性被組合傳播到系統每個并發組件中的最低源碼層。
目前針對系統并發性形式化驗證的研究在許多層面已有突破，但仍存在一些難點和問題。首先，推理低效困難，普通驗證過程通常采用單一的源碼或者字節碼進行底層驗證，并發性驗證需要證明高層的安全屬性，如死鎖、可達性、無散度判別等。而源碼級別涉及太多的無意義變量與邏輯，導致驗證效率很差。其次，驗證系統存在模型間的語義鴻溝，功能驗證和行為驗證所用的方法不同，缺乏抽象端到源碼端的一致性證明。
針對計算機軟件并發性驗證的難點，本文提出了一種可雙向轉換的并發性形式化驗證方法，解決了普通抽象過程中建模驗證缺乏靈活性的問題，避免了對系統進行重復抽象建模，并且保證了源碼層與抽象層驗證的一致性。文章首先介紹了驗證方法的基本路線，路線分別從代碼功能正確性和行為功能正確性兩方面進行程序的驗證，以保證最終的驗證一致性。其次對框架的整體設計思路進行了詳盡的描述，方法根據輸入的源碼應用程序接口（Application Programming Interface，API）與功能需求文檔，通過模型規范提取器和形式化命題生成器抽取規范表示并輸入到中間映射層，自動向上映射 生 成 相 應 的 通 信 順 序 進 程（Communication Sequential Process，CSP）模型，向下映射生成相應的功能性規范。經過自動驗證器完成并發性驗證和功能性驗證。最后基于該并發性驗證方法進行應用案例分析。
1并發性驗證基本路線
以 CSP 過程建模為例的并發性形式化驗證方法使用模型檢查技術，通過系統抽象獲取整體模型，利用自動化驗證器完成并發性驗證。為保證系統整體的安全性，還需要對計算機軟件的功能正確性進行驗證，但是因為系統中存在模型間的語義鴻溝，無法保證并發性驗證模型和功能正確性驗證模型的一致性。如果交由人工編寫功能規范再進行復雜的一致性推理，則會嚴重影響驗證效率。為此，本文提出了一種可以保證源碼端和抽象端一致性的可雙向轉換的并發性驗證方法。方法路線如圖 1 所示。
圖 1 方法路線
基于輸入的源碼 API 及其用自然語言給出的功能規范，路線分為代碼端的功能正確性驗證和抽象端的行為并發性驗證。整體的驗證路線為首先根據提供的函數 API以及需求規范說明文檔進行規范提取，然后轉化為一種抽象度居中的中間層規范。這種中間層規范既可以自動向上映射為高層規范并輸入到并發性驗證模塊中進行并發屬性驗證，也可以自動向下映射為源碼層規范并輸入到功能性驗證模塊中進行功能正確性驗證，經過兩條路線驗證后，最終得到驗證結果。整體的驗證步驟如圖 2 所示。
圖2 驗證步驟
中間層規范是指對源碼規范與需求進行了適度抽象的形式化表示。一方面，中間層規范不僅完整地描述了底層程序功能，而且過濾了程序實現細節，使得程序安全驗證可同時映射高層與底層兩個方向，解決了高層抽象驗證與源碼級驗證之間存在的語義鴻溝，提供了高層屬性端到源碼端的一致性驗證。另一方面，生成中間層規范時可以一次性覆蓋所有源碼 API，從中間層規范自動向上映射出過程模型分析系統并發屬性，避免了對整個系統進行人工的重復建模，提高了系統靈活性。
2并發性驗證方法設計
可雙向轉換的并發性驗證方法設計架構整體可分為中間層規范生成模塊、自動化功能性驗證模塊、自動化并發性驗證模塊以及集成模塊。其中，中間層規范生成模塊主要用于將源碼 API信息與文檔功能需求整合并生成一種可以雙分支映射的中間層規范；自動化功能性驗證模塊主要通過自動向下映射機制使中間層規范轉化為源碼級驗證模型，再通過自動化功能性驗證工具進行功能性驗證，并得出功能正確性驗證結果；自動化并發性驗證模塊主要通過自動向上映射機制使中間層規范轉換為抽象過程模型，再通過自動化并發性驗證工具進行并發屬性驗證，得到并發性驗證結果；集成模塊根據并發屬性驗證與功能性驗證的結果，最終生成具有跨模型邏輯一致性的安全驗證結果。
2.1 中間層規范生成模塊
設計中間層規范模塊由形式化命題生成器、模型規范提取器和中間層規范生成器組成。模塊結構設計如圖 3 所示。
圖 3 中間層規范模塊結構設計
形式化命題生成器用于對輸入的源碼進行形式化表示，通過分析待驗證程序中所有的變量，將其作為所述中間層規范中的行為載體；確定待驗證程序中的主要狀態變遷依靠的函數，將其設置為功能元素；隱藏底層內存狀態，引入等價的抽象狀態用于表述底層完整功能邏輯，忽略函數變量具體的取值，只考慮相應的狀態變遷及變遷條件，并描述出函數具體內部邏輯。模型規范提取器根據提供的代碼流程以及相應的需求說明文檔，將文檔中關于代碼的邏輯限制轉化為便于進行形式化描述的模型規范。獲得的模型規范為一種抽象度居中的形式化描述，用于輸入到中間層規范生成器中。中間層規范生成器根據輸入的形式化命題與相應的模型規范，整合成為一種抽象度居中的中間層規范。從整體而言，中間層規范模塊一次性處理所有的 API，轉化為所述中間層規范。
將中間層規范輸入到自動化功能性驗證模塊與自動化并發性驗證模塊，即可進行自動化驗證和并發性驗證。
2.2 自動化并發性驗證模塊設計
自動化并發驗證模塊主要負責提供抽象端的并發性驗證，通過雙向轉換器將中間層規范自動向上映射為抽象層規范。其完成并發性驗證的具體步驟描述如下：
步驟 1：根據所述中間層規范表現出的狀態間邏輯關系進行抽象；
步驟 2：確定狀態間轉移條件，形成不同的抽象路徑，每條路徑包含相應的前置后置狀態；
步驟 3：對所述中間層規范進行分析，確定路徑相關性，將并發的路徑并列起來，生成相應的高層規范；
步驟 4：根據高層規范得到高層抽象狀態機，并參考系統的狀態遷移屬性，推理出狀態遷移合法性規則，編寫高層屬性規范；
步驟 5：依據所述高層抽象狀態機中的狀態、行為及邏輯信息，形成可用于并發推理的抽象過程模型，再根據所述高層規范與所述高層屬性規范，生成并插入并發安全屬性語句，最后進行并發屬性驗證。
2.3 自動化功能性驗證模塊設計
自動化功能性驗證模塊主要負責提供源碼級的功能正確性驗證，在生成可雙向映射的中間層規范后，經由雙向轉換器自動向下映射為源碼級規范，經過細節抽取、驗證函數生成、規范生成和最終驗證 4 個步驟完成功能性驗證。關鍵步驟描述如下：
步驟 1：根據所述中間層規范給出的函數調用關系，抽取函數實現邏輯以及函數內部變量的數據結構和傳遞條件；
步驟 2：根據所述數據結構和傳遞條件，分析函數應達到的安全標準，將其生成為一個源碼級形式化規范；
步驟 3：將生成的所述源碼級形式化規范插入到源碼中，形成源碼級驗證模型；
步驟 4：將轉換輸出的所述源碼級驗證模型進行功能性驗證。系統整體的工作流程圖如圖4所示。
圖 4 自動并發驗證工作流程
2.4 集成模塊設計
集成模塊由結果生成器組成。結果生成器根據中間層規范模塊中的并發屬性驗證與功能性驗證情況，生成具有跨模型邏輯一致性的安全驗證結果。
集合模塊整合了屬性并發性和功能正確性的驗證結果，最后生成一份源碼安全性報告。
3實驗過程和結果
本文以一個 C 語言實現的融資程序為案例，采用第二節所述的雙向并發性驗證方法對程序進行驗證：
案例程序主要的功能為控制融資金額，預先給定一個最低融資目標，當實際融資金額小于融資目標時，可以進行相應的融資操作；當融資金額大于或等于相應的融資目標時，更新融資狀態為關閉狀態。此案例涉及金融安全領域，對代碼安全性要求較高，因此需要采用形式化驗證方法使程序滿足相應的安全性需求。本文將對該程序生成抽象度居中的中間層規范，再進行雙向自動化映射以及驗證器驗證，最后根據結果分析說明本文所述方法的有效性。
3.1 中間層規范生成
步驟 1：首先對于案例程序來說，確定聲明中 goal 與 raised 為函數變量，在中間層規范中體現為實際的行為載體；再確定程序內部狀態變遷的主要邏輯依靠 invest 函數內部行為來實現，則將 invest 定義為中間層規范中的 FUNCTION元素。
步驟 2：函數內部邏輯為當融資金額小于目標時，進行融資操作；考慮到中間層規范既要隱藏底層具體繁雜的內存狀態，又要引入等價的抽象狀態用于表述底層完整功能邏輯，raised涉及兩種狀態，則將其聲明為一個 old(raised) 帶有時間性質的元素類型，當 old(raised)
步驟 3：根據上述操作，將程序中所有 API都整合為中間層規范；本例中 invest 整合出的中間層規范為：
3.2 自動向上映射及并發屬性驗證
步驟 1：根據中間層規范中表現出的狀態間邏輯關系進行抽象。
步驟 2：確定每個狀態之間的轉移條件，形成不同的抽象路徑，每條路徑包含相應的前置后置狀態。對于本例來說，中間層規范中的 invest函數抽象出的路徑為兩條，以第一條路徑為例，前 置 條 件 為 (raised
步驟 3：對完整的中間層規范進行分析，確定每一條路徑的相關性，將可并發產生的路徑并列起來；經過對所有路徑的分析，得到的 invest高層規范代碼為：
步驟 4：根據高層規范得到 invest 函數高層抽象狀態機，參考整個系統的狀態遷移屬性，推理出狀態遷移合法性規則，編寫高層屬性規范。在本例中，參考 invest 函數路徑，考慮到一旦募集成功，融資金額不能低于最低融資目標，則本例得到的高層屬性規范代碼為：
步驟 5：根據高層規范，生成相應的 CSP 模型代碼；根據相應的高層屬性規范及系統需求文檔給出的并發性要求，編寫相應的并發屬性判 斷 語 句， 如：#assert P() deadlock，#assert P() deterministic 等；并將判斷語句插入到 CSP 抽象過程模型代碼中，最后輸入到自動化并發驗證模塊進行系統并發模擬驗證，并得出并發性驗證結果。
3.3 自動向下映射及功能性驗證
步驟 1：根據中間層規范給出的函數調用關系，抽取具體的函數實現邏輯，以及函數內部變量的數據傳遞結構和傳遞條件。
步驟 2：根據具體的數據傳遞結構及條件，自動化分析函數模塊應該達到的安全標準，將其生成為一個單獨的驗證函數。在本例中，參考中間層規范中表述當 raised 舊值小于最低目標融資時，函數會進行融資操作，自動生成一條判斷函數語句：assert(raised == old_raised + value)。
步驟 3：將自動生成的單獨驗證函數插入到源碼中，形成最后輸出的源碼級規范，本例生成代碼為：
步驟 4：將生成的源碼級規范輸入到功能性驗證工具中，根據規范中單獨的驗證函數為功能性驗證工具調整參數，使其可以完全覆蓋函數本身的邏輯分支，并得出功能性驗證結果。
3.4 驗證結果分析
上述案例首先通過代碼邏輯信息及功能需求整合出了相應的中間層規范，描述了行為載體goal，raised，state 與功能元素 invest，close 之間的邏輯關系。一方面，通過自動向上映射生成了高層規范，根據 invest 元素的功能邏輯編寫了高層屬性規范，最終插入相應并發性斷言進行了自動化并發性驗證。另一方面，通過自動向下映射生成了相應的源碼級規范，根據 raised 行為載體的邏輯需求插入了功能性斷言并進行了自動化功能性驗證。
在本例中，自動化并發性驗證模塊與功能性驗證模塊給出的驗證結果均為正確，表示驗證過程中生成規范與斷言均得到了滿足，源碼層的功能性規范與抽象層的并發屬性規范通過了驗證。驗證結果表明，本例設計的形式化驗證方法成功證明了融資程序的源碼級實現與相應抽象層屬性之間的邏輯一致性。
在驗證流程中，一方面，通過中間層規范雙向映射的驗證方法，消除了高層抽象驗證與源碼級驗證的語義鴻溝。另一方面，生成中間層規范時一次性覆蓋了所有源碼 API，避免了對系統進行人工重復建模。在實際驗證流程中，雙向映射過程采用自動化工具完成，相較于傳統并發程序驗證采用的手動驗證方式，降低了人工參與度，提高了驗證效率。
４結 語
本文以 C 語言程序源碼的并發性驗證方法為研究對象，提出了一種可雙向轉換的并發性驗證方法，針對傳統并發性驗證建模缺乏靈活性的問題進行了改進，并在整個驗證過程中提供了從抽象端到源碼端的一致性保證。首先，根據可雙向轉換的并發驗證思路設計了驗證系統的框架；其次，根據整體驗證思路設計了一種中間層規范生成器，將提供的代碼及需求說明文檔轉化為中間層規范；最后，設計了一種自動化雙向轉換器，將中間層規范自動映射為高層規范與功能性規范并分別進行驗證。根據對融資程序的試驗驗證，證明了此雙向轉換并發性驗證方法的有效性及可用性。未來主要是在面向更復雜的驗證目標時能更好地提供效率保障，并且在實際的驗證工作中提高自動化程度，減少人工參與度。
引用格式：謝小賦 , 曾夢岐 , 龐飛 . 面向計算機并發程序的形式化驗證方法設計 [J]. 信息安全與通信保密 ,2022(3):54-62.
