鑒源論壇 · 觀模丨形式化驗(yàn)證——以操作系統(tǒng)任務(wù)調(diào)度算法驗(yàn)證為案例

作者 |蔡雄上海控安可信軟件創(chuàng)新研究院研發(fā)工程師

版塊 |鑒源論壇 · 觀模

形式化方法是基于嚴(yán)格的數(shù)學(xué)基礎(chǔ)，通過(guò)采用數(shù)學(xué)邏輯證明來(lái)對(duì)計(jì)算機(jī)軟硬件系統(tǒng)進(jìn)行建模、規(guī)約、分析、推理和驗(yàn)證，是用于保證計(jì)算機(jī)軟硬件系統(tǒng)正確性以及安全性的一種重要方法。形式化方法是基于嚴(yán)格定義的數(shù)學(xué)概念和語(yǔ)言，其描述軟件及其性質(zhì)的語(yǔ)言是無(wú)歧義的，構(gòu)造和驗(yàn)證方法是嚴(yán)格的。加上形式化方法在開(kāi)發(fā)過(guò)程具備良好的可重復(fù)性，并且相應(yīng)的模型軟件也具有比較強(qiáng)的可分析性和可驗(yàn)證性，可以很好地支持抽象模型建立、系統(tǒng)精化、模型和證明重用，有效地提高和保障系統(tǒng)的可信性。

圖1驗(yàn)證與分析框架

其中主要將驗(yàn)證與分析框架劃分為三個(gè)部分：

（1）利用VCC做單元級(jí)別的函數(shù)驗(yàn)證，基于軟件架構(gòu)設(shè)計(jì)規(guī)范及軟件詳細(xì)設(shè)計(jì)規(guī)范等文檔，選取適用的審查、分析或測(cè)試等方法，驗(yàn)證軟件單元設(shè)計(jì)和實(shí)施的正確性和一致性；

（2）利用CBMC做多個(gè)函數(shù)的集成驗(yàn)證，集成驗(yàn)證主要是針對(duì)軟件高層設(shè)計(jì)進(jìn)行驗(yàn)證，一般來(lái)說(shuō)是對(duì)模塊和子系統(tǒng)為單位進(jìn)行驗(yàn)證，驗(yàn)證每個(gè)函數(shù)調(diào)用其他函數(shù)時(shí)，調(diào)用者的規(guī)范能否滿足；

（3）利用PAT做系統(tǒng)驗(yàn)證，確認(rèn)整個(gè)系統(tǒng)是否滿足了軟件規(guī)格說(shuō)明中的功能性和非功能性的各項(xiàng)需求，以及滿足的程度，系統(tǒng)驗(yàn)證應(yīng)能夠發(fā)現(xiàn)和找出因需求不正確、不完整或?qū)崿F(xiàn)與需求之間的不一致而引起的失效，并識(shí)別在沒(méi)有文檔化時(shí)或被遺失的那些需求，驗(yàn)證系統(tǒng)在運(yùn)行時(shí)能否滿足要求的性質(zhì)。

01

VCC

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

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

如圖2所示，VCC的主要工作過(guò)程分為兩個(gè)步驟。

第一步，VCC工具將注釋的C代碼轉(zhuǎn)換為用于驗(yàn)證的 BoogiePL中間語(yǔ)言，然后通過(guò)Boogie工具將其繼續(xù)轉(zhuǎn)化為一階邏輯表達(dá)式。其中，BoogiePL 是一種帶有嵌入式斷言的簡(jiǎn)單命令式語(yǔ)言，它很容易生成一組一階邏輯公式，表明程序應(yīng)該滿足性質(zhì)，這里以斷言的形式呈現(xiàn)。

第二步，利用 SMT 求解器 Z3（自動(dòng)化定理證明器）對(duì)轉(zhuǎn)換后的一階邏輯表達(dá)式進(jìn)行驗(yàn)證。Z3 求解器會(huì)返回兩種結(jié)果：（1）一階邏輯表達(dá)式通過(guò)驗(yàn)證；（2）Z3 返回一個(gè)反例或者提示超時(shí)。

圖2VCC的工作流程

VCC可以自動(dòng)驗(yàn)證函數(shù)是否滿足用戶書(shū)寫(xiě)函數(shù)規(guī)約。用戶使用時(shí)操作步驟如下：

（1）根據(jù)設(shè)計(jì)規(guī)約，利用VCC提供的接口，編寫(xiě)前置條件、后置條件等函數(shù)契約；

（2）使用VCC自動(dòng)驗(yàn)證函數(shù)是否滿足這些契約；

（3）如果VCC報(bào)告驗(yàn)證失敗，那么根據(jù)錯(cuò)誤報(bào)告，修改代碼，或重寫(xiě)函數(shù)契約；

（4）如果VCC報(bào)告驗(yàn)證成功，則說(shuō)明函數(shù)符合契約。

以下一個(gè)返回兩者之間更小的數(shù)的一個(gè)函數(shù)為例，進(jìn)一步分析如何使用VCC工具對(duì)一個(gè)C語(yǔ)言代碼進(jìn)行單元驗(yàn)證。

表 1

在表1中，表左邊展示的是使用VCC標(biāo)記過(guò)的源代碼，表右邊展示的是C語(yǔ)言轉(zhuǎn)化后的BoogiePL中間語(yǔ)言，其中為源代碼添加了一個(gè)前置條件和后置條件。前置條件表示在進(jìn)入函數(shù)前假定滿足的條件，后置條件表示在執(zhí)行完函數(shù)后所需要滿足的條件。BoogiePL中間語(yǔ)言轉(zhuǎn)化過(guò)程會(huì)將返回結(jié)果賦值給result；將前置條件轉(zhuǎn)化成assume語(yǔ)句來(lái)假定前置條件滿足；將后置條件轉(zhuǎn)化成assert語(yǔ)句對(duì)提出的后置條件進(jìn)行驗(yàn)證。

02

CBMC

CBMC是Bounded Model Checker for ANSI-C and C++ programs的縮寫(xiě)，CBMC是C和C ++程序的綁定模型檢查器。CBMC實(shí)現(xiàn)了一種稱為邊界模型檢查（BMC，Bounded Model Checker）的技術(shù)。在BMC中，通過(guò)聯(lián)合解開(kāi)復(fù)雜狀態(tài)機(jī)的轉(zhuǎn)換關(guān)系及其規(guī)范以獲得布爾公式，然后使用有效的SAT程序檢查布爾公式的可滿足性。如果該公式是可滿足的，則從SAT過(guò)程的輸出中提取一個(gè)反例。如果公式無(wú)法滿足要求，則可以展開(kāi)更多程序以確定是否存在更長(zhǎng)的反例。

在許多工程領(lǐng)域中，實(shí)時(shí)保證是嚴(yán)格的要求。例如是嵌入在汽車控制器中的軟件，這些類型的程序中的循環(huán)構(gòu)造通常對(duì)迭代次數(shù)有嚴(yán)格的限制。CBMC能夠通過(guò)展開(kāi)斷言來(lái)嚴(yán)格驗(yàn)證這種范圍。建立迭代次數(shù)的界限后，CBMC便可以證明是否存在錯(cuò)誤。

CBMC能夠驗(yàn)證內(nèi)存安全性（包括數(shù)組范圍檢查和指針是否安全使用的檢查）、檢查異常、檢查未定義行為的各種變體以及用戶指定的斷言。通過(guò)展開(kāi)程序中的循環(huán)并將結(jié)果方程式傳遞到?jīng)Q策程序來(lái)執(zhí)行驗(yàn)證。CBMC像編譯器一樣，從命令行接收.c命名的文件，然后編譯程序并將不同文件定義的函數(shù)組合起來(lái)。但CBMC不像編譯器生成可執(zhí)行二進(jìn)制代碼，而是符號(hào)執(zhí)行程序。

CBMC 的目標(biāo)是分析 C/C++ 或者 JAVA 程序。CBMC 分析的過(guò)程是將輸入程序，生成對(duì)應(yīng)的控制流圖，當(dāng)獲取到程序的CFG時(shí)，就可以獲取每條路徑對(duì)應(yīng)的公式 ，也就是說(shuō)路徑能夠執(zhí)行的條件是使路徑對(duì)應(yīng)的公式能夠成立。然后針對(duì)獲得的公式，使用SAT求解命題邏輯，其中分析流程如圖3所示。

圖3CBMC的驗(yàn)證流程

使用CBMC工具進(jìn)行分析的過(guò)程可以劃分成如下四步：

（1）對(duì)源代碼進(jìn)行插樁，放入部分約束或者標(biāo)簽；

（2）將程序解析為語(yǔ)法樹(shù)，并基于語(yǔ)法樹(shù)轉(zhuǎn)換成CFG；

（3）在獲得程序的CFG后，我們計(jì)劃通過(guò)收集程序路徑，得到路徑對(duì)應(yīng)的公式；

（4）結(jié)合程序插樁信息，進(jìn)而通過(guò)SMT求解器得到驗(yàn)證結(jié)果。

表2所示的是一個(gè)CBMC的示例，往代碼中注入了一個(gè)error標(biāo)簽，可按照其CFG到斷言并建立與路徑對(duì)應(yīng)的一階路徑進(jìn)行驗(yàn)證。

表 2

對(duì)于上表所示的代碼片段，構(gòu)建的CFG，如圖4所示。

圖4 CFG圖示

圖5 路徑圖示

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

03

PAT

PAT是Process Analysis Toolkit的簡(jiǎn)稱，是由新加坡國(guó)立大學(xué)開(kāi)發(fā)的一款形式化建模與驗(yàn)證工具集，支持進(jìn)程代數(shù)、實(shí)時(shí)進(jìn)程代數(shù)、時(shí)間自動(dòng)機(jī)等多種建模語(yǔ)言。此外，PAT工具的人機(jī)交互界面友好，支持多種驗(yàn)證方法，包括精化驗(yàn)證、死鎖驗(yàn)證、可達(dá)性驗(yàn)證、LTL性質(zhì)驗(yàn)證等。以PAT工具中最常使用的是語(yǔ)言CSP#為例，對(duì)如何使用PAT建模進(jìn)行講解。

PAT的進(jìn)程代數(shù)(Communication Sequential Process, 簡(jiǎn)稱CSP)模塊。該模塊使用CSP#，作為建模語(yǔ)言，描述待驗(yàn)證的系統(tǒng)。

CSP#在經(jīng)典的CSP的基礎(chǔ)上，增加了數(shù)據(jù)狀態(tài)與相關(guān)的操作，使得建模更加方便、直觀。CSP#描述的系統(tǒng)主要包括下面三個(gè)部分：

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

（2）進(jìn)程：定義系統(tǒng)中的各個(gè)進(jìn)程；

（3）斷言：描述系統(tǒng)應(yīng)當(dāng)滿足的性質(zhì)，可以使用全局定義中的變量。

進(jìn)程的定義如下：

圖 6

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

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

其中P是一個(gè)進(jìn)程，add代表一個(gè)事件，x是全局變量，伴隨著事件add的發(fā)生, 執(zhí)行賦值操作x=x+1。在PAT的建模過(guò)程中，我們廣泛使用這種機(jī)制表示數(shù)據(jù)的傳輸。

此處解釋關(guān)于外部選擇以及內(nèi)部選擇：

（1）對(duì)于一個(gè)外部選擇：

P[]Q

選擇運(yùn)算符[]指出可以執(zhí)行P或Q。但該選擇由環(huán)境解決，如果P中事件首先發(fā)生，那么由P接管進(jìn)程，否則是由Q接管進(jìn)程。

（2）對(duì)于一個(gè)內(nèi)部選擇：

P<>Q

其中P或Q可以執(zhí)行。該選擇是內(nèi)部確定的，意味著隨機(jī)執(zhí)行進(jìn)程P或者 Q。在建模階段，它對(duì)于隱藏不相關(guān)的信息很有用。它可以用于對(duì)黑盒過(guò)程的行為進(jìn)行建模，而不用了解黑盒的具體實(shí)現(xiàn)。

對(duì)于內(nèi)部選擇和外部選擇可以寫(xiě)出它們的廣義形式：

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

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

圖 7

在PAT工具中，創(chuàng)建CSP#模型之后，然后就可以進(jìn)行驗(yàn)證。待驗(yàn)證的性質(zhì)可以劃分為兩類，一類是LTL性質(zhì)，另一類是refine性質(zhì)。PAT工具將驗(yàn)證性質(zhì)是否滿足。如果不滿足，可以查看反例。圖7展示的是一個(gè)操作系統(tǒng)任務(wù)調(diào)度算法建模的模型。模型中詳細(xì)描述了操作系統(tǒng)任務(wù)調(diào)度過(guò)程中創(chuàng)建進(jìn)程、進(jìn)程執(zhí)行、進(jìn)程搶占、進(jìn)程掛起、進(jìn)程中斷、進(jìn)程調(diào)度等過(guò)程，以及進(jìn)程各個(gè)狀態(tài)之間的遷移關(guān)系。并且在使用PAT工具進(jìn)行驗(yàn)證的時(shí)候，也可以驗(yàn)證出該模型存在死鎖，并針對(duì)死鎖情況給出了一系列行為對(duì)應(yīng)的反例，在此操作系統(tǒng)的任務(wù)調(diào)度算法中沒(méi)有發(fā)現(xiàn)死鎖，因此也不會(huì)給出反例。

04

基于形式化驗(yàn)證與分析框架的應(yīng)用

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

參考資料：

[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]繆淮扣,陳怡海.《軟件形式規(guī)格說(shuō)明語(yǔ)言—Z》,清華大學(xué)出版社出版,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.

審核編輯 黃昊宇