基于PROMELA模型的安全關(guān)鍵軟件形式化驗(yàn)證技術(shù)

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

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

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

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

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

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

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

1 相關(guān)工作

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

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

本文基于PROMELA模型，結(jié)合SPIN，提出C程序“一鍵式”形式化驗(yàn)證技術(shù)，實(shí)現(xiàn)5類故障模式的驗(yàn)證，并給出C程序存在故障的反例路徑。

2 基于PROMELA模型的安全關(guān)鍵軟件形式化驗(yàn)證方法

2.1 C程序到PROMELA模型的映射機(jī)制

2.1.1 C程序到PROMELA模型的映射規(guī)則

本節(jié)定義了C程序抽象語法樹節(jié)點(diǎn)(C程序語法結(jié)構(gòu))到PROMELA模型的19個映射規(guī)則，部分規(guī)則如表1所示。

表1 抽象語法樹節(jié)點(diǎn)到PROMELA模型的映射規(guī)則

續(xù)表1

由于篇幅所限，本文僅闡述循環(huán)節(jié)點(diǎn)For到PROMELA模型的映射規(guī)則：

1) 識別For循環(huán)體，生成do...od結(jié)構(gòu)；

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

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

4) 對For第2個子節(jié)點(diǎn)的返回值取反，生成PROMELA模型，作為do...od結(jié)構(gòu)中條件語句；

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

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

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

2.1.2 與驗(yàn)證屬性相關(guān)的函數(shù)到PROMELA模型的映射規(guī)則

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

表2 部分函數(shù)節(jié)點(diǎn)到PROMELA模型的映射規(guī)則

續(xù)表2

2.2 PROMELA模型自動生成方法

算法1實(shí)現(xiàn)基于映射規(guī)則的PROMELA模型自動生成。1至15行對抽象語法樹進(jìn)行遞歸遍歷，獲取當(dāng)前節(jié)點(diǎn)及子節(jié)點(diǎn)信息，并根據(jù)節(jié)點(diǎn)名稱，應(yīng)用映射規(guī)則，生成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模型生成方法的理論分析

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

首先借鑒文獻(xiàn)[12]中提出的圖同構(gòu)思想，結(jié)合圖1對構(gòu)建方法的語義保留性進(jìn)行證明。圖1中Gramc指C語言的語法規(guī)則，Gramp指PROMELA建模語言的語法規(guī)則，pro(Gramc)指C程序，pro(Gramp)指PROMELA模型實(shí)例。符號h表示C語言語法規(guī)則到PROMELA語法規(guī)則的映射；符號r表示C程序到PROMELA模型實(shí)例的轉(zhuǎn)換函數(shù)；符號t和t′分別表示C語言和PROMELA語言語法規(guī)則到程序?qū)嵗g的映射函數(shù)，它們?yōu)轭愋捅Ａ粲成?type prserve mapping,TPM)，符號F表示C語言語法規(guī)則到PROMELA模型實(shí)例之間的映射關(guān)系。

圖1 語法規(guī)則和程序?qū)嵗g的映射關(guān)系

2.1節(jié)中29種映射規(guī)則是建立在形式化模型與抽象語法樹節(jié)點(diǎn)語義一致的基礎(chǔ)上，所以C程序抽象語法樹節(jié)點(diǎn)到PROMELA模型的映射規(guī)則函數(shù)h是同構(gòu)的。

定義1定義圖同構(gòu)函數(shù)f表示從圖G到圖H的轉(zhuǎn)換：f=G→H。N(G)為圖G的節(jié)點(diǎn)集合,N(H)為圖H的節(jié)點(diǎn)集合,E(G)為圖G的邊的點(diǎn)集合,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)

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

命題1Graml為一種程序語言的語法規(guī)則，pro(Graml)為該語言對應(yīng)的程序?qū)嵗?，那么在語法規(guī)則及其程序?qū)嵗g的TPM函數(shù)是圖同構(gòu)的。

由命題1，C語言語法規(guī)則到C程序?qū)嵗g的映射函數(shù)t，以及PROMELA語言到PROMELA模型實(shí)例之間的映射函數(shù)t′是圖同構(gòu)的。

命題2如果映射函數(shù)f是圖同構(gòu)的，并且映射函數(shù)g是圖同構(gòu)的，那么f和g的復(fù)合運(yùn)算f°g也是圖同構(gòu)的。

根據(jù)命題2，因?yàn)楹瘮?shù)h,t′是圖同構(gòu)的，所以F(ht′)是圖同構(gòu)的。

定理1已知Gramc和Gramp之間存在同構(gòu)映射h，Gramc和它的程序?qū)嵗齪ro(Gramc)之間存在類型保留映射函數(shù)t，Gramp和它的模型實(shí)例之間pro(Gramp)存在類型保留映射函數(shù)t′，則pro(Gramc)和pro(Gramp)之間的映射函數(shù)r是圖同構(gòu)的。

證明上文已經(jīng)證明函數(shù)h,t,t′,F是圖同構(gòu)的，分別用公式(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)

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

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

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

(6)

根據(jù)公式(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):

根據(jù)公式(8)，因?yàn)門PM函數(shù)t是圖同構(gòu)的，結(jié)合公式(1)表示的同構(gòu)函數(shù)的約束，因此推斷映射函數(shù)r也是圖同構(gòu)的，即定理1得證。

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

2.4 基于PROMELA模型的C程序驗(yàn)證方法

1) 違反斷言的驗(yàn)證方法

在C程序中添加的斷言稱為基本斷言，以檢查表達(dá)式的合法性。如果表達(dá)式中變量值確定，則斷言表達(dá)式可以直接驗(yàn)證；如果變量值依賴函數(shù)參數(shù)、函數(shù)返回值或全局變量時，例如變量var的地址以實(shí)參形式傳入函數(shù)fun中，則導(dǎo)致C程序轉(zhuǎn)換成PROMELA模型后，斷言語句assert(var小于1 000)的邏輯值無法確定，針對變量無法確定取值的情況，本文提出將激勵函數(shù)插入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程序斷言的驗(yàn)證范圍，對包含規(guī)約運(yùn)算的情況作等價處理，例如，斷言表達(dá)式assert(i++>0)等價變換為i++和assert(i>0)即可。

表3 C程序斷言驗(yàn)證方法的驗(yàn)證范圍

2) 數(shù)組越界的驗(yàn)證方法

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

表4 數(shù)組越界驗(yàn)證方法的驗(yàn)證范圍

3) 空指針解引用的驗(yàn)證方法

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

表5 空指針解引用驗(yàn)證方法的驗(yàn)證范圍

4) 死鎖和饑餓的驗(yàn)證方法

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

表6 死鎖及饑餓驗(yàn)證方法的驗(yàn)證范圍

在并發(fā)C程序轉(zhuǎn)換為PROMELA模型后，使用“end”標(biāo)簽來標(biāo)識程序結(jié)束狀態(tài)，如果“end”標(biāo)簽未被執(zhí)行，則存在死鎖問題；使用“progress”標(biāo)簽標(biāo)記重復(fù)被執(zhí)行的語句，如果存在沒有被執(zhí)行的“progress”，即存在饑餓問題。

3 實(shí)驗(yàn)驗(yàn)證

3.1 某實(shí)驗(yàn)案例的驗(yàn)證過程

本文以存在數(shù)組越界故障的Driver-receiv1553程序?yàn)槔U釋驗(yàn)證原理。該程序從1553b總線接收數(shù)據(jù)，對數(shù)據(jù)有效性進(jìn)行判斷，讀取數(shù)據(jù)長度、數(shù)據(jù)塊等信息，對無效數(shù)據(jù)通過調(diào)用trans16函數(shù)進(jìn)行處理。該C程序的流程圖如圖2所示。

圖2 Driver-receiv1553程序流程圖

本文研制輔助工具完成C程序到PROMELA模型的轉(zhuǎn)換，并與SPIN集成，實(shí)現(xiàn)對C程序的驗(yàn)證。輔助工具生成的PROMELA模型原理如圖3所示。

圖3 PROMELA模型流程圖

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

圖4 反例路徑有向圖示意

3.2 驗(yàn)證方法對比

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

表7 C程序驗(yàn)證方法對比

4 結(jié) 論

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