張志 天 ， 陳意云 ， 劉 剛

（1.中國科學(xué)技術(shù)大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，合肥 230026；2.中國科學(xué)技術(shù)大學(xué) 蘇州研究院軟件安全實(shí)驗(yàn)室，蘇州 215123）

隨著國家、社會(huì)和日常生活對軟件系統(tǒng)的依賴程度日益增長，安全攸關(guān)軟件的高可信成為保障國家安全、保持經(jīng)濟(jì)可持續(xù)發(fā)展和維護(hù)社會(huì)穩(wěn)定的必要條件。

形式驗(yàn)證是提高軟件可信程度的重要方法。粗略地說，軟件的形式驗(yàn)證有兩種途徑，第一種是模型檢測，它通過遍歷系統(tǒng)所有狀態(tài)空間，能夠?qū)τ懈F狀態(tài)系統(tǒng)進(jìn)行自動(dòng)驗(yàn)證，并自動(dòng)構(gòu)造不滿足驗(yàn)證性質(zhì)的反例。這種方法在工業(yè)界較流行。第二種是邏輯推理，它利用某種程序邏輯進(jìn)行演算，對程序性質(zhì)進(jìn)行嚴(yán)格的推理，產(chǎn)生驗(yàn)證條件，再利用定理證明器進(jìn)行證明。本文所討論的方法是基于邏輯推理的方式。

對于指針程序的推理，關(guān)鍵在于別名的判斷和處理。通常所采用的Hoare邏輯的一個(gè)重要限制是程序中不同的名字代表不同的程序?qū)ο螅床辉试S出現(xiàn)別名。

對于指針別名判斷的一種解決辦法是采用分離邏輯。使用分離邏輯的一個(gè)問題是，通常的自動(dòng)定理證明器都不能證明帶分離合取連接詞（*，Separating Conjunction）的驗(yàn)證條件，必須為分離邏輯設(shè)計(jì)專用的自動(dòng)定理證明工具。

本文提出一種利用形狀圖信息來消除訪問路徑別名，使得指針程序仍然可以用Hoare邏輯來進(jìn)行驗(yàn)證的方法。

1 PointerC語言和形狀圖邏輯

1.1 PointerC語言

PointerC是一個(gè)強(qiáng)調(diào)指針類型并增加形狀聲明的類C小語言，詳細(xì)的語法信息請見參考文獻(xiàn)[1]。在結(jié)構(gòu)體聲明中，通過指針域指向形狀的聲明來確定這種結(jié)構(gòu)體用來構(gòu)造什么形狀的數(shù)據(jù)結(jié)構(gòu)，同時(shí)也限定了該結(jié)構(gòu)體類型的指針?biāo)苤赶虻男螤?。這是對應(yīng)形狀分析的需求所做的語言擴(kuò)展，所允許的形狀有單鏈表、循環(huán)單鏈表、雙向鏈表、循環(huán)雙向鏈表。

1.2 形狀圖和形狀邏輯

程序驗(yàn)證之前，首先基于形狀圖邏輯對程序進(jìn)行形狀分析，形狀分析為每個(gè)程序點(diǎn)構(gòu)建形狀圖，這些形狀圖構(gòu)成程序驗(yàn)證所需要的指針信息。在此通過舉例來介紹形狀圖[1]。

以圖1（參考文獻(xiàn)[1]中有序鏈表節(jié)點(diǎn)插入函數(shù)循環(huán)不變式的形狀圖）為例說明形狀圖和程序點(diǎn)指針等信息的聯(lián)系。在圖1中，圓節(jié)點(diǎn)表示指針類型的聲明變量；虛邊框的矩形節(jié)點(diǎn)不代表任何程序元素；矩形節(jié)點(diǎn)表示由malloc生成的結(jié)構(gòu)體變量；灰色矩形節(jié)點(diǎn)是濃縮節(jié)點(diǎn)，表示若干個(gè)（可以是0個(gè)）相鄰的、屬于同一數(shù)據(jù)結(jié)構(gòu)的、同類型的結(jié)構(gòu)體變量，下側(cè)可以有無代表被濃縮節(jié)點(diǎn)個(gè)數(shù)的整型表達(dá)式以及約束該表達(dá)式的斷言。若沒有，則表示被濃縮節(jié)點(diǎn)個(gè)數(shù)是某個(gè)自然數(shù)，但和任何變量或常數(shù)聯(lián)系不起來。由圖 1可知，head==ptr1，ptr==ptr1-＞next，head指向鏈表的長度是 m，ptr指向濃縮節(jié)點(diǎn)代表m-1個(gè)節(jié)點(diǎn)，可用 head(-＞next)m-1上角標(biāo)的方式來表示。

圖1 形狀圖的一個(gè)例子

可見，形狀圖可以作為程序斷言，它是該圖所能表達(dá)的指針相等、不相等和別名斷言等的合取，包括其中謂詞節(jié)點(diǎn)和濃縮節(jié)點(diǎn)下側(cè)有關(guān)表長或被濃縮節(jié)點(diǎn)個(gè)數(shù)的整型數(shù)據(jù)斷言。

形狀圖邏輯就是基于上面觀點(diǎn)來設(shè)計(jì)的Hoare邏輯的一種擴(kuò)展。程序規(guī)范的形式是{G∧Q}S{G′∧Q′}，其中G是形狀圖，Q是表達(dá)程序其他性質(zhì)的符號(hào)斷言，兩部分的合取G∧Q作為程序點(diǎn)完整的斷言。本文程序驗(yàn)證器的第一步工作，在無需程序員提供有關(guān)形狀的函數(shù)前后條件和循環(huán)不變式的情況下，利用形狀圖邏輯對程序進(jìn)行形狀分析。由于從一個(gè)語句前的G推導(dǎo)該語句后的G′不受Q的影響，因此形狀分析時(shí)，把程序規(guī)范簡化為{G}S{G′}，以此來使用形狀圖邏輯的推理規(guī)則，建立各程序點(diǎn)的形狀圖G。在形狀分析的過程中，還利用循環(huán)不變式推斷算法得出各循環(huán)的循環(huán)不變形狀圖[2]。

在完成形狀分析后，程序驗(yàn)證器進(jìn)行程序其他性質(zhì)Q的驗(yàn)證。在{G∧Q}S{G′∧Q′}中，若 S不是指針操作語句，則G′和 G一樣，但Q′可能不同于Q。若 S是指針操作語句（指針賦值、分配空間和釋放空間等），則除了 G′和G可能不同外，Q′和Q可能也有一些細(xì)微的區(qū)別。下面是本文關(guān)注的部分。

2 指針程序的驗(yàn)證方法

程序點(diǎn)數(shù)據(jù)結(jié)構(gòu)構(gòu)成的形狀有多種可能時(shí)，則G表示為 G1∨G2∨…∨Gn。 同樣，Q也可能是 Q1∨Q2∨…∨Qm的析取形式。完整的斷言可以整理成析取范式（Disjunctive Normal Form）G1∧Q1∨G2∧Q2∨…∨Gk∧Qk的形式。根據(jù)形狀圖邏輯，可以用析取范式的一種情況為例來討論，寫成G∧Q，G和Q分別都是合取形式。

程序驗(yàn)證器基于形狀圖邏輯[2]進(jìn)行最強(qiáng)后條件演算并產(chǎn)生驗(yàn)證條件，驗(yàn)證條件由證明器Z3[3]自動(dòng)證明。

2.1 形狀圖和符號(hào)斷言之間的聯(lián)系

符號(hào)斷言Q中允許出現(xiàn)指針是否等于NULL或兩個(gè)指針是否相等的斷言。即使函數(shù)前后條件和循環(huán)不變式中沒有這樣的斷言，它們也會(huì)因?yàn)槌霈F(xiàn)在條件語句或循環(huán)語句的布爾表達(dá)式中，而在最強(qiáng)后條件演算過程中被加到Q中。

Q中指針等于NULL或兩個(gè)指針相等的斷言會(huì)因?yàn)楹虶中的信息重復(fù)而被吸收，或因有矛盾而使得G∧Q為假。

Q中訪問路徑的合法性依賴于G。例如，在Q中若出現(xiàn)非指針型的訪問路徑 p-＞… -＞data，則忽略-＞data所剩下的前綴應(yīng)該是G上到達(dá)某個(gè)結(jié)構(gòu)節(jié)點(diǎn)的一條訪問路徑，若是到達(dá)懸空節(jié)點(diǎn)、null節(jié)點(diǎn)或不存在這樣的路徑則都非法的，若是到達(dá)謂詞節(jié)點(diǎn)則視謂詞節(jié)點(diǎn)展開后的情況決定。

Q中的訪問路徑之間是否有別名，Q中的訪問路徑和下一條語句S中的訪問路徑之間,以及S中的訪問路徑之間是否有別名都依賴于G，即利用G可以判斷。

在指針操作語句中，在對指針u賦值時(shí)可能會(huì)影響符號(hào)斷言：符號(hào)斷言中若有以u或u為前綴的訪問路徑，則要用和u相等但不是別名的u′來代換 u。另一個(gè)影響符號(hào)斷言的場合是，在free語句之后應(yīng)該刪除涉及被釋放節(jié)點(diǎn)上數(shù)據(jù)的原子斷言。

G中也會(huì)有符號(hào)斷言，附加在濃縮節(jié)點(diǎn)上，用來限制它代表結(jié)構(gòu)節(jié)點(diǎn)的個(gè)數(shù)。G的符號(hào)斷言和Q的符號(hào)斷言不會(huì)有矛盾，但前者有時(shí)會(huì)給出更準(zhǔn)確的信息。

2.2 程序推理規(guī)則的擴(kuò)展

在使用推理規(guī)則從語句S的前條件G∧Q產(chǎn)生后條件G′∧Q′時(shí)，要保證Q合法、Q和 G無重復(fù)與矛盾。

先考慮S是指針操作語句。修改指針型數(shù)據(jù)的簡單語句會(huì)引起指針值的變化，或者是存儲(chǔ)堆塊的增減，因而導(dǎo)致形狀圖的變化。根據(jù)2.1節(jié)的介紹知道，對Q的影響是訪問路徑的替換或者刪除部分?jǐn)嘌?。先假定Q和S無別名，有別名的情況在考慮非指針操作語句時(shí)介紹。下面給出各種語句規(guī)則。

(1)指針型賦值語句u=v

若u既不是null指針也不是懸空指針，則按下面規(guī)則得到后斷言。

其中 G′是由形狀分析得到的形狀圖，Q[u′/u]表示 Q中作為訪問路徑（包括作為前綴情況）的u和其相等且不互為別名的訪問路徑u′代換。

2.10.5 專屬性及線性曲線考察 精密量取100 μL的Lut質(zhì)量濃度為3 000、1 500、750、300、30 ng/mL的系列對照品溶液，分別加入50 μL的內(nèi)標(biāo)溶液，氮?dú)獯等ビ袡C(jī)溶劑，加入100 μL大鼠空白血漿，按照“2.10.3”項(xiàng)下方法操作，記錄HPLC色譜峰面積，結(jié)果見圖8，該方法專屬性較高。以Lut質(zhì)量濃度為橫坐標(biāo)（X），Lut與香葉木素峰面積比為縱坐標(biāo)（Y），繪制標(biāo)準(zhǔn)曲線，回歸方程為Y＝1.304 4 X＋0.091 3，r＝0.990 7。因此，Lut在30.0～3 000 ng/mL呈現(xiàn)良好的線性關(guān)系。

(2)對指針賦值的其他語句

分配空間語句u=malloc(t)和函數(shù)調(diào)用語句ret=f(act)有關(guān)Q的處理同上面賦值語句的規(guī)則一樣。

(3)釋放空間語句free(u)

釋放u指向的節(jié)點(diǎn)后，Q中含u或u的別名的原子斷言不應(yīng)再存在，因此規(guī)則如下：

{G∧Q}free(u){G′∧Q′}

其中Q′由把Q中含u或u的別名的原子斷言都刪除而得到。

很容易明白，若Q無別名，則這些語句的規(guī)則不會(huì)導(dǎo)致Q′出現(xiàn)別名，因?yàn)樗鼈儗做的小修改都不會(huì)引入別名。

再考慮非指針操作語句。只要前斷言Q和語句S中無別名，則使用Hoare的賦值公理就是可靠的。若有別名，則可以先用G的信息來消除別名（把互為別名的訪問路徑改成都用其中同一條訪問路徑），然后再用賦值公 理 。 定 義 eliminate_aliases函 數(shù) 為 (S′,Q′)=eliminate_aliases(G,S,Q),它根據(jù)G消除S和Q中的別名，得到 S′和 Q′。

對于修改指針型數(shù)據(jù)的語句，其前斷言Q可能是程序員提供的，例如不排除循環(huán)不變式中 Q存在別名，因此有時(shí)也需要這條規(guī)則。

復(fù)合、條件和循環(huán)語句的規(guī)則以及推論規(guī)則的形式和Hoare邏輯相應(yīng)規(guī)則的形式一致。

在沒有指針類型的情況下，使用Hoare邏輯的賦值公理從賦值語句的前斷言Q去得到后斷言Q′時(shí)，不用關(guān)心Q是否為Q1∨Q2的形式。但是在有指針類型的情況下，G1∨G2代表相應(yīng)程序點(diǎn)的形狀圖有兩種可能，需要對它們分別考慮，因此需要增加一條分情況規(guī)則：

先前提到的用析取范式 G1∧Q1∨G2∧Q2∨…∨Gn∧Qn的一種情況來討論就是基于這條規(guī)則。

3 系統(tǒng)原型

基于形狀圖邏輯，實(shí)現(xiàn)了PointerC語言的一個(gè)程序驗(yàn)證器[1]，它能夠驗(yàn)證使用圖1所定義的各種形狀的程序。除了驗(yàn)證形狀外，還能驗(yàn)證節(jié)點(diǎn)上數(shù)據(jù)的一些性質(zhì)。本文對有序鏈表插入節(jié)點(diǎn)的函數(shù)進(jìn)行了驗(yàn)證。

該驗(yàn)證器分成下面幾個(gè)模塊，按所列次序順序執(zhí)行：

(1)普通編譯器的前端。對源程序進(jìn)行詞法分析、語法分析和靜態(tài)語義檢查后，生成抽象語法樹。

(2)形狀分析。遍歷抽象語法樹，根據(jù)形狀聲明和形狀圖邏輯來生成各程序點(diǎn)的形狀圖。

(3)驗(yàn)證條件的生成。遍歷抽象語法樹，根據(jù)程序員提供的函數(shù)前后條件和循環(huán)不變式，按最強(qiáng)后條件演算方式為各函數(shù)生成驗(yàn)證條件。

(4)驗(yàn)證條件的證明。將生成的各驗(yàn)證條件G∧Q?Q′，按照上一節(jié)所介紹的方法翻譯成 P∧Q?Q′的形式，逐個(gè)交給證明器進(jìn)行證明。

本文提出一種利用形狀圖信息來消除訪問路徑別名，使得指針程序仍然可以用Hoare邏輯來進(jìn)行驗(yàn)證的方法，并利用可自動(dòng)定理證明器的支持，開發(fā)了一個(gè)PointerC語言的程序驗(yàn)證器原型，展示了該方法的可行性。

[1]ZHANG Y,LI Z P,CHEN Y Y,et al.Shape graph logic and A shape system(Extended Verison).URL：http：//ssg.ustcsz.edu.cn/content/shape-graph-logic.2010(11).

[2]NECULA G.Proof-carrying code,In Proc.24th ACM Symp.On Principles of Prog.Lang.New York,1997(1)：106-119.

[3]MOURA L D,BJORNER N.Z3：An Efficient SMT solver,conference on tools and algorithms for the construction and analysis of Systems(TACAS).Budapest,Hungary,volume 4963 of LNCS,2008：337-340.