作者 |蔡雄上海控安可信軟件創新研究院研發工程師

版塊 |鑒源論壇 · 觀模

形式化方法是基于嚴格的數學基礎，通過采用數學邏輯證明來對計算機軟硬件系統進行建模、規約、分析、推理和驗證，是用于保證計算機軟硬件系統正確性以及安全性的一種重要方法。形式化方法是基于嚴格定義的數學概念和語言，其描述軟件及其性質的語言是無歧義的，構造和驗證方法是嚴格的。加上形式化方法在開發過程具備良好的可重復性，并且相應的模型軟件也具有比較強的可分析性和可驗證性，可以很好地支持抽象模型建立、系統精化、模型和證明重用，有效地提高和保障系統的可信性。

圖1驗證與分析框架

其中主要將驗證與分析框架劃分為三個部分：

（1）利用VCC做單元級別的函數驗證，基于軟件架構設計規范及軟件詳細設計規范等文檔，選取適用的審查、分析或測試等方法，驗證軟件單元設計和實施的正確性和一致性；

（2）利用CBMC做多個函數的集成驗證，集成驗證主要是針對軟件高層設計進行驗證，一般來說是對模塊和子系統為單位進行驗證，驗證每個函數調用其他函數時，調用者的規范能否滿足；

（3）利用PAT做系統驗證，確認整個系統是否滿足了軟件規格說明中的功能性和非功能性的各項需求，以及滿足的程度，系統驗證應能夠發現和找出因需求不正確、不完整或實現與需求之間的不一致而引起的失效，并識別在沒有文檔化時或被遺失的那些需求，驗證系統在運行時能否滿足要求的性質。

01

VCC

VCC(Verified C Compiler)是一個針對C語言程序的驗證工具。VCC提供了用于描述C語言函數的前置條件、后置條件、不變式等函數規約的接口。VCC是在原始C語言的基礎上進行撰寫函數約束對C代碼進行進一步的完善C語言更深層次的屬性。其對約束內容可以劃分為對一階邏輯表達式的約束和指針的約束。

為了驗證程序的正確性，VCC使用演繹驗證模式。它生成一定數量的數學表達式(稱為驗證條件)，并試圖使用一個自動定理驗證器來驗證這些數學表達式。如果驗證失敗，VCC會將失敗的原因反映到用戶的程序代碼身上。因此，用戶通常是在代碼和程序狀態層面與VCC交互的。通常情況下，用戶可以忽略在VCC內部的數學推理。例如，如果待驗證的程序使用了除法，如果VCC無法證明除數一定非零，它會報告待驗證的程序有(潛在的)錯誤。這并不意味著程序必然是不正確的。通常，可以通過增加注釋和斷言來解決這個“錯誤”。不過這可能又會導致其他的錯誤報告，迫使用戶添加更多的注釋。所以實際的驗證是一個迭代的過程。

如圖2所示，VCC的主要工作過程分為兩個步驟。

第一步，VCC工具將注釋的C代碼轉換為用于驗證的 BoogiePL中間語言，然后通過Boogie工具將其繼續轉化為一階邏輯表達式。其中，BoogiePL 是一種帶有嵌入式斷言的簡單命令式語言，它很容易生成一組一階邏輯公式，表明程序應該滿足性質，這里以斷言的形式呈現。

第二步，利用 SMT 求解器 Z3（自動化定理證明器）對轉換后的一階邏輯表達式進行驗證。Z3 求解器會返回兩種結果：（1）一階邏輯表達式通過驗證；（2）Z3 返回一個反例或者提示超時。

圖2VCC的工作流程

VCC可以自動驗證函數是否滿足用戶書寫函數規約。用戶使用時操作步驟如下：

（1）根據設計規約，利用VCC提供的接口，編寫前置條件、后置條件等函數契約；

（2）使用VCC自動驗證函數是否滿足這些契約；

（3）如果VCC報告驗證失敗，那么根據錯誤報告，修改代碼，或重寫函數契約；

（4）如果VCC報告驗證成功，則說明函數符合契約。

以下一個返回兩者之間更小的數的一個函數為例，進一步分析如何使用VCC工具對一個C語言代碼進行單元驗證。

表 1

在表1中，表左邊展示的是使用VCC標記過的源代碼，表右邊展示的是C語言轉化后的BoogiePL中間語言，其中為源代碼添加了一個前置條件和后置條件。前置條件表示在進入函數前假定滿足的條件，后置條件表示在執行完函數后所需要滿足的條件。BoogiePL中間語言轉化過程會將返回結果賦值給result；將前置條件轉化成assume語句來假定前置條件滿足；將后置條件轉化成assert語句對提出的后置條件進行驗證。

02

CBMC

CBMC是Bounded Model Checker for ANSI-C and C++ programs的縮寫，CBMC是C和C ++程序的綁定模型檢查器。CBMC實現了一種稱為邊界模型檢查（BMC，Bounded Model Checker）的技術。在BMC中，通過聯合解開復雜狀態機的轉換關系及其規范以獲得布爾公式，然后使用有效的SAT程序檢查布爾公式的可滿足性。如果該公式是可滿足的，則從SAT過程的輸出中提取一個反例。如果公式無法滿足要求，則可以展開更多程序以確定是否存在更長的反例。

在許多工程領域中，實時保證是嚴格的要求。例如是嵌入在汽車控制器中的軟件，這些類型的程序中的循環構造通常對迭代次數有嚴格的限制。CBMC能夠通過展開斷言來嚴格驗證這種范圍。建立迭代次數的界限后，CBMC便可以證明是否存在錯誤。

CBMC能夠驗證內存安全性（包括數組范圍檢查和指針是否安全使用的檢查）、檢查異常、檢查未定義行為的各種變體以及用戶指定的斷言。通過展開程序中的循環并將結果方程式傳遞到決策程序來執行驗證。CBMC像編譯器一樣，從命令行接收.c命名的文件，然后編譯程序并將不同文件定義的函數組合起來。但CBMC不像編譯器生成可執行二進制代碼，而是符號執行程序。

CBMC 的目標是分析 C/C++ 或者 JAVA 程序。CBMC 分析的過程是將輸入程序，生成對應的控制流圖，當獲取到程序的CFG時，就可以獲取每條路徑對應的公式 ，也就是說路徑能夠執行的條件是使路徑對應的公式能夠成立。然后針對獲得的公式，使用SAT求解命題邏輯，其中分析流程如圖3所示。

圖3CBMC的驗證流程

使用CBMC工具進行分析的過程可以劃分成如下四步：

（1）對源代碼進行插樁，放入部分約束或者標簽；

（2）將程序解析為語法樹，并基于語法樹轉換成CFG；

（3）在獲得程序的CFG后，我們計劃通過收集程序路徑，得到路徑對應的公式；

（4）結合程序插樁信息，進而通過SMT求解器得到驗證結果。

表2所示的是一個CBMC的示例，往代碼中注入了一個error標簽，可按照其CFG到斷言并建立與路徑對應的一階路徑進行驗證。

表 2

對于上表所示的代碼片段，構建的CFG，如圖4所示。

圖4 CFG圖示

圖5 路徑圖示

對于圖5所示的標紅路徑，可以得到公式0 ≤ t ≤ 79 ∧ t/20 != 0 ∧ t/20 == 1 ∧ TEMP2 = B ⊕ C ⊕ D ∧ TEMP3 = K 2，將這組公式放入SMT求解器進行求解時，可以得到一組解。當我們針對error標簽進行可達性驗證時、可以得到公式 0 ≤ t ≤ 79 ∧ t/20 != 0 ∧ t/20 != 1∧ t/20 != 2 ∧ t/20 != 3，使用SMT求解器進行求解時發現該公式不能得到滿足，即該路徑不可達。

03

PAT

PAT是Process Analysis Toolkit的簡稱，是由新加坡國立大學開發的一款形式化建模與驗證工具集，支持進程代數、實時進程代數、時間自動機等多種建模語言。此外，PAT工具的人機交互界面友好，支持多種驗證方法，包括精化驗證、死鎖驗證、可達性驗證、LTL性質驗證等。以PAT工具中最常使用的是語言CSP#為例，對如何使用PAT建模進行講解。

PAT的進程代數(Communication Sequential Process, 簡稱CSP)模塊。該模塊使用CSP#，作為建模語言，描述待驗證的系統。

CSP#在經典的CSP的基礎上，增加了數據狀態與相關的操作，使得建模更加方便、直觀。CSP#描述的系統主要包括下面三個部分：

（1）全局量：定義常量和全局變量，支持多維數組；

（2）進程：定義系統中的各個進程；

（3）斷言：描述系統應當滿足的性質，可以使用全局定義中的變量。

進程的定義如下：

圖 6

其中事件前綴可以和數據操作組合使用，例如：

P= add{x=x+1;}→Skip;

其中P是一個進程，add代表一個事件，x是全局變量，伴隨著事件add的發生, 執行賦值操作x=x+1。在PAT的建模過程中，我們廣泛使用這種機制表示數據的傳輸。

此處解釋關于外部選擇以及內部選擇：

（1）對于一個外部選擇：

P[]Q

選擇運算符[]指出可以執行P或Q。但該選擇由環境解決，如果P中事件首先發生，那么由P接管進程，否則是由Q接管進程。

（2）對于一個內部選擇：

P<>Q

其中P或Q可以執行。該選擇是內部確定的，意味著隨機執行進程P或者 Q。在建模階段，它對于隱藏不相關的信息很有用。它可以用于對黑盒過程的行為進行建模，而不用了解黑盒的具體實現。

對于內部選擇和外部選擇可以寫出它們的廣義形式：

[]x:{1..n}@ P(x) 等價于 P(1)[]...[]P(n)

<>x:{1..n}@ P(x) 等價于 P(1)<>...<>P(n)

圖 7

在PAT工具中，創建CSP#模型之后，然后就可以進行驗證。待驗證的性質可以劃分為兩類，一類是LTL性質，另一類是refine性質。PAT工具將驗證性質是否滿足。如果不滿足，可以查看反例。圖7展示的是一個操作系統任務調度算法建模的模型。模型中詳細描述了操作系統任務調度過程中創建進程、進程執行、進程搶占、進程掛起、進程中斷、進程調度等過程，以及進程各個狀態之間的遷移關系。并且在使用PAT工具進行驗證的時候，也可以驗證出該模型存在死鎖，并針對死鎖情況給出了一系列行為對應的反例，在此操作系統的任務調度算法中沒有發現死鎖，因此也不會給出反例。

04

基于形式化驗證與分析框架的應用

此套形式化驗證與分析框架曾用于某操作系統的調度算法驗證。在使用VCC工具進行驗證的合計77個函數、其中64個驗證通過，13個驗證不通過。在13個驗證不通過的函數中有6個類型不匹配問題、6個數組溢出問題以及一個指針內容可能為空問題。在使用CBMC工具進行驗證的77個函數中，其中21個未添加約束驗證通過，7個提示內存不足無法驗證，2個驗證崩潰。在添加了約束后77個函數中75個驗證成功、2個驗證崩潰。在使用PAT工具對其建模后，對操作系統內的調度算法進行了無死鎖驗證，在模擬6935684了狀態后得到了該操作系統無死鎖的結論。

參考資料：

[1] Ankit S , Arnab B , Lakshmanan K , et al. An overview of model checkers and CBMC as a tool. , 2017.

[2] Liu, Y., Sun, J., Dong, J. S.: Developing model checkers using PAT. In: International symposium on automated technology for verification and Analysis, pp. 371–377. Springer, Berlin, Heidelberg (2010).

[3]Ernie Cohen, Markus Dahlweid, Mark A. Hillebrand, Dirk Leinenbach, Michal Moskal, Thomas Santen, Wolfram Schulte, and Stephan Tobies. 2009. VCC: A Practical System for Verifying Concurrent C. In TPHOLs (LNCS, Vol. 5674). Springer, 23–42.

[4]繆淮扣,陳怡海.《軟件形式規格說明語言—Z》,清華大學出版社出版,2012年11月.

[5]Wing J M. A specifier's introduction to formal methods[J]. Computer, 1990, 23(9): 8-22.

[6]Miao, W. and S. Liu, A Formal Engineering Framework for Service-Based Software Modeling. IEEE Transactions on Services Computing, 2013. 6(4): p. 536-550.

審核編輯 黃昊宇