基于PROMELA模型的安全關鍵軟件形式化驗證技術

邢亮, 丁成鈞, 杜虎鵬, 馬春燕

(1.航空工業西安航空計算技術研究所, 陜西 西安 710076; 2.西北工業大學 軟件學院, 陜西 西安 710072)

當前安全關鍵軟件在航空、航天、醫療、交通等領域應用廣泛，該類軟件存在資源競爭、空指針和數組越界等問題，而檢測相應故障主要依賴開發人員的經驗和技術能力，保障其可靠性存在很大困難。形式化驗證[1]是故障檢測技術之一，其通過嚴格的數學語義進行推理以保障代碼的可靠性。

形式化建模語言PROMELA支持對任務關鍵C程序邏輯進行建模以及C程序的嵌入，具有驗證C程序的優勢。目前，用PROMELA建模C程序時，主要通過人工方式實現，需要較高技術門檻和代價，限制了安全關鍵軟件進行形式化驗證的廣泛應用。本文提出了從C程序到PROMELA模型的自動生成方法，實現對安全關鍵C程序中5類故障模式進行一鍵式形式化驗證。本文貢獻如下：

1) 制定了C程序到PROMELA模型2類映射規則，提出了PROMELA模型自動生成的方法，并對方法進行理論分析；

2) 針對C程序中違反斷言、數組越界、空指針解引用、死鎖以及饑餓5類故障，給出形式化驗證方法和驗證范圍；

3) 研制了輔助工具，覆蓋每類故障的驗證范圍，分別選取12個來源于開源代碼托管平臺GitHub的C程序案例，進行實證研究。

1 相關工作

文獻[1]提出了針對并發故障的形式化驗證方法，實現了PROMELA模型生成工具C2Spin。Jiang[2]使用語法導向技術，采用PROMELA建模C程序，但缺少并發C程序庫函數的建模。Wagner等[3]提出檢測緩沖區溢出的方法，但其檢測精度較低。文獻[4]提出基于插樁的方法驗證C程序數組越界，但存在重復和等價插樁點，驗證效率較低。Klieber等[5]提出針對緩沖區溢出的自動化修復技術。文獻[6]將隨機內存分配算法和虛擬內存相結合，改進內存分配策略，避免程序執行時的內存錯誤。文獻[7]綜合程序切片和謂詞抽象技術，提出C程序斷言的靜態驗證方法。Yong等[8]設計了用于檢查空指針解引用的C程序安全工具。Zhe等[9]通過代碼插樁技術，設計針對內存漏洞的分析工具，但僅能處理較簡單的C程序。

目前，大部分方法存在過多人工干預，并且驗證的故障類型較少，也未給出存在故障的反例路徑。PROMELA對有限狀態分布式系統進行建模[10]。SPIN工具支持PROMELA模型中以斷言形式和線性時間邏輯(linear-time logic,LTL)公式形式撰寫的驗證屬性，生成并仿真執行驗證程序[11]。

本文基于PROMELA模型，結合SPIN，提出C程序“一鍵式”形式化驗證技術，實現5類故障模式的驗證，并給出C程序存在故障的反例路徑。

2 基于PROMELA模型的安全關鍵軟件形式化驗證方法

2.1 C程序到PROMELA模型的映射機制

2.1.1 C程序到PROMELA模型的映射規則

本節定義了C程序抽象語法樹節點(C程序語法結構)到PROMELA模型的19個映射規則，部分規則如表1所示。

表1 抽象語法樹節點到PROMELA模型的映射規則

續表1

由于篇幅所限，本文僅闡述循環節點For到PROMELA模型的映射規則：

1) 識別For循環體，生成do...od結構；

2) 遞歸遍歷For第1個子節點，生成PROMELA模型，將返回值作為語句插入do...od結構前；

3) 遞歸遍歷For第2個子節點，生成PROMELA模型，將返回值作為do...od中條件語句；

4) 對For第2個子節點的返回值取反，生成PROMELA模型，作為do...od結構中條件語句；

5) 遞歸遍歷For第4個子節點，生成PROMELA模型，將返回值作為第1個條件語句后的語句；

6) 遞歸遍歷For的第3個子節點，生成PROMELA模型，將返回值按順序作為第1個條件語句后的語句；

7) 為第2個條件語句添加break。

2.1.2 與驗證屬性相關的函數到PROMELA模型的映射規則

基于2.1.1生成的PROMELA模型，可以實現對斷言違反、數組越界、空指針解引用的驗證。為驗證死鎖、饑餓并發故障，本文進一步提出10條映射規則，部分規則如表2所示。

表2 部分函數節點到PROMELA模型的映射規則

續表2

2.2 PROMELA模型自動生成方法

算法1實現基于映射規則的PROMELA模型自動生成。1至15行對抽象語法樹進行遞歸遍歷，獲取當前節點及子節點信息，并根據節點名稱，應用映射規則，生成PROMELA模型。16至26行以For為例，給出其PROMELA模型生成算法。

算法1PROMELA model instance generator

input:tis the abstract tree root node of a C program; map is the mapping relationships between the abstract tree nodes and mapping rules

output: pr is an instance of PROMELA model

1. while (t!= null) do

2. if(map.containsValue(t.name)) then

3. rule←map.get(t.name)

4. instanceGenerator(rule);

5. end if

6. ift.char is "thr-suspend"

7. return 1

8. end if

9. ift.char is "rand"

10. returnt.char

11. end if

12. returnt.char

13. otherwise do error

14. end if

15. end while

16. Procedure instanceGenerator(rule)

17. if rule is R10 then

18. PROMELAGeneration(node.firstchild)

19. Emit("do")

20. Emit("::")

21. bool var = PROMELAGeneration(node.secondchild)

22. Emit("!var->break")

23. PROMELAGeneration(node.forthchild)

24. PROMELAGeneration(node.thirdchild)

25. Emit("od")

26. end if

27. else if rule is one of other rules then

28. Generator the corresponding instance fragments

29. end procedure

2.3 PROMELA模型生成方法的理論分析

從構建方法的語義保留、確定性和有邊界3個方面，證明C程序到PROMELA模型生成方法的合理性。

首先借鑒文獻[12]中提出的圖同構思想，結合圖1對構建方法的語義保留性進行證明。圖1中Gramc指C語言的語法規則，Gramp指PROMELA建模語言的語法規則，pro(Gramc)指C程序，pro(Gramp)指PROMELA模型實例。符號h表示C語言語法規則到PROMELA語法規則的映射；符號r表示C程序到PROMELA模型實例的轉換函數；符號t和t′分別表示C語言和PROMELA語言語法規則到程序實例之間的映射函數，它們為類型保留映射(type prserve mapping,TPM)，符號F表示C語言語法規則到PROMELA模型實例之間的映射關系。

圖1 語法規則和程序實例之間的映射關系

2.1節中29種映射規則是建立在形式化模型與抽象語法樹節點語義一致的基礎上，所以C程序抽象語法樹節點到PROMELA模型的映射規則函數h是同構的。

定義1定義圖同構函數f表示從圖G到圖H的轉換：f=G→H。N(G)為圖G的節點集合,N(H)為圖H的節點集合,E(G)為圖G的邊的點集合,E(H)為圖H的邊的集合。f滿足公式(1)中的約束。

?x,y∈N(G)∧f(x),f(y)∈N(H)∧xy

∈E(G)?f(x)f(y)∈E(H)

(1)

結合定義1和本文的映射規則可知，圖G類似C語言的語法規則，圖H類似PROMELA語言的語法規則。而N(G)表示C語言抽象語法樹節點，E(G)表示映射規則中的29種抽象語法樹節點，N(H)表示PROMELA的語法節點集合，E(H)表示PROMELA語法節點。

命題1Graml為一種程序語言的語法規則，pro(Graml)為該語言對應的程序實例，那么在語法規則及其程序實例之間的TPM函數是圖同構的。

由命題1，C語言語法規則到C程序實例之間的映射函數t，以及PROMELA語言到PROMELA模型實例之間的映射函數t′是圖同構的。

命題2如果映射函數f是圖同構的，并且映射函數g是圖同構的，那么f和g的復合運算f°g也是圖同構的。

根據命題2，因為函數h,t′是圖同構的，所以F(ht′)是圖同構的。

定理1已知Gramc和Gramp之間存在同構映射h，Gramc和它的程序實例pro(Gramc)之間存在類型保留映射函數t，Gramp和它的模型實例之間pro(Gramp)存在類型保留映射函數t′，則pro(Gramc)和pro(Gramp)之間的映射函數r是圖同構的。

證明上文已經證明函數h,t,t′,F是圖同構的，分別用公式(2)至(5)表示。

h(Gramc)=Gramp

(2)

t(Gramc)=pro(Gramc)

(3)

t′(Gramp)=pro(Gramp)

(4)

F(Gramc)=t′(h(Gramc))=t′(Gramp)=

pro(Gramp)

(5)

根據公式(1)和(2)可得公式(6):

?x,y∈N(Gramc)∧h(x),h(y)∈N(Gramp)

∧xy∈E(Gramc)?h(x)h(y)∈E(Gramp)

(6)

根據公式(1)和(5)可得公式(7):

?x,y∈N(Gramc)∧F(x),F(y)∈N(pro(Gramp))

∧xy∈E(Gramc)?F(x)F(y)∈E(pro(Gramp))

(7)

將公式(7)中的F替換成r°t，化簡得到公式(8):

根據公式(8)，因為TPM函數t是圖同構的，結合公式(1)表示的同構函數的約束，因此推斷映射函數r也是圖同構的，即定理1得證。

C程序到PROMELA模型生成方法是基于C語言和PROMELA建模語言的語法規則提出的，而C語言和PROMELA語言的語法結構是精確無二義性的，且抽象語法樹節點的映射規則是一一映射的，所以生成方法是確定性的。由于C程序的抽象語法樹節點數量是有限的，所以生成方法是有限的。綜上，本文提出的C程序到PROMELA模型生成方法是正確的。

2.4 基于PROMELA模型的C程序驗證方法

1) 違反斷言的驗證方法

在C程序中添加的斷言稱為基本斷言，以檢查表達式的合法性。如果表達式中變量值確定，則斷言表達式可以直接驗證；如果變量值依賴函數參數、函數返回值或全局變量時，例如變量var的地址以實參形式傳入函數fun中，則導致C程序轉換成PROMELA模型后，斷言語句assert(var小于1 000)的邏輯值無法確定，針對變量無法確定取值的情況，本文提出將激勵函數插入PROMELA模型的算法2。

算法2Excitation function generation algorithm genStubs()

input:tis the abstract tree root node of a C program;

output: void

1. while (tis not null)

2. if (tis TN-FUNC-CALL) then

3. line←t.cont

4. fun-name←t.lnode.value

5. params =t.rnode

6. for(params hasNext())

7. param = params.next()

8. if param is ASSERT-VAR then

9. param-range←param

10. fun-name=fun-name+"-stubs"

11. for num in param-range

12. fun-body←num

13. new-funcall←line，fun-name

14. end for

15. end if

16. end for

17. end if

18. end while

表3是基于C程序斷言的驗證范圍，對包含規約運算的情況作等價處理，例如，斷言表達式assert(i++>0)等價變換為i++和assert(i>0)即可。

表3 C程序斷言驗證方法的驗證范圍

2) 數組越界的驗證方法

表4是C程序數組越界的驗證范圍。對于數組長度和索引均確定的情況，可以采用1)中斷言的形式進行驗證。而當數組長度或索引依賴函數參數或全局變量時，則根據算法2插入激勵函數；如果多維數組中每一維度長度和索引范圍均靜態確定，則插入斷言assert(index1

表4 數組越界驗證方法的驗證范圍

3) 空指針解引用的驗證方法

本方法對空指針解引用類型的驗證范圍如表5所示。對于一級靜態確定指針，可以采用斷言表達式驗證。指針變量動態依賴函數參數或全局變量需調用算法2生成靜態確定指針變量的激勵函數后再進行驗證；多級指針與1級指針驗證時插入的斷言不同，假設二級指針int**p; 則插入斷言assert(p &&*p)，即需要對每一級指針進行驗證。

表5 空指針解引用驗證方法的驗證范圍

4) 死鎖和饑餓的驗證方法

死鎖及饑餓問題驗證是基于C程序Pthread庫中線程創建函數pthread_create、互斥鎖以及條件變量等。死鎖及饑餓問題驗證范圍如表6所示。

表6 死鎖及饑餓驗證方法的驗證范圍

在并發C程序轉換為PROMELA模型后，使用“end”標簽來標識程序結束狀態，如果“end”標簽未被執行，則存在死鎖問題；使用“progress”標簽標記重復被執行的語句，如果存在沒有被執行的“progress”，即存在饑餓問題。

3 實驗驗證

3.1 某實驗案例的驗證過程

本文以存在數組越界故障的Driver-receiv1553程序為例，闡釋驗證原理。該程序從1553b總線接收數據，對數據有效性進行判斷，讀取數據長度、數據塊等信息，對無效數據通過調用trans16函數進行處理。該C程序的流程圖如圖2所示。

圖2 Driver-receiv1553程序流程圖

本文研制輔助工具完成C程序到PROMELA模型的轉換，并與SPIN集成，實現對C程序的驗證。輔助工具生成的PROMELA模型原理如圖3所示。

圖3 PROMELA模型流程圖

該模型的驗證表達式為c-code[(Pp-receiv1553->ix<32)]，根據本文的驗證方法，該程序存在數組越界故障，C程序反例路徑如圖4所示。由于圖2中變量uslength的值為32，因此該有向圖中的108→109→108路徑會執行32次，此時ix的值為32。而根據驗證表達式，ix的值應小于32，所以該程序出現數組越界故障，且故障出現在C程序的第109行。

圖4 反例路徑有向圖示意

3.2 驗證方法對比

本文針對違反斷言、數組越界、空指針解引用、死鎖及饑餓，覆蓋各故障類型的所有驗證范圍，分別使用12個來源于GitHub的C程序案例進行實驗驗證，并與相關工作中的其他方法進行對比，如表7所示，其中，驗證故障類型中的編號為2.4節相應表中的編號。本文方法驗證的故障類型多、自動化程度高，并展示C程序故障出現的反例路徑，在這三個方面具有明顯的優勢。

表7 C程序驗證方法對比

4 結 論

本文在定義C程序抽象語法樹節點到PROMELA模型映射規則的基礎上，增加了驗證屬性相關函數到PROMELA模型的映射規則，提出了一種C程序到PROMELA模型自動生成算法，并給出包含違反斷言、數組越界、空指針解引用、死鎖、饑餓這5種故障類型的C程序形式化驗證方法。在對實驗案例分析后，對比現有C程序形式化驗證方法的優缺點，本文方法具有明顯優勢。