一種驗證指針程序的方法

隨著(zhù)國家、社會(huì )和日常生活對軟件系統的依賴(lài)程度日益增長(cháng)，安全攸關(guān)軟件的高可信成為保障國家安全、保持經(jīng)濟可持續發(fā)展和維護社會(huì )穩定的必要條件。
　形式驗證是提高軟件可信程度的重要方法。粗略地說(shuō)，軟件的形式驗證有兩種途徑，第一種是模型檢測，它通過(guò)遍歷系統所有狀態(tài)空間，能夠對有窮狀態(tài)系統進(jìn)行自動(dòng)驗證，并自動(dòng)構造不滿(mǎn)足驗證性質(zhì)的反例。這種方法在工業(yè)界較流行。第二種是邏輯推理，它利用某種程序邏輯進(jìn)行演算，對程序性質(zhì)進(jìn)行嚴格的推理，產(chǎn)生驗證條件，再利用定理證明器進(jìn)行證明。本文所討論的方法是基于邏輯推理的方式。
　對于指針程序的推理，關(guān)鍵在于別名的判斷和處理。通常所采用的Hoare邏輯的一個(gè)重要限制是程序中不同的名字代表不同的程序對象，即不允許出現別名。
　對于指針別名判斷的一種解決辦法是采用分離邏輯。使用分離邏輯的一個(gè)問(wèn)題是，通常的自動(dòng)定理證明器都不能證明帶分離合取連接詞（*，Separating Conjunction）的驗證條件，必須為分離邏輯設計專(zhuān)用的自動(dòng)定理證明工具。
　本文提出一種利用形狀圖信息來(lái)消除訪(fǎng)問(wèn)路徑別名，使得指針程序仍然可以用Hoare邏輯來(lái)進(jìn)行驗證的方法。
1 PointerC語(yǔ)言和形狀圖邏輯
1.1 PointerC語(yǔ)言
　PointerC是一個(gè)強調指針類(lèi)型并增加形狀聲明的類(lèi)C小語(yǔ)言，詳細的語(yǔ)法信息請見(jiàn)參考文獻[1]。在結構體聲明中，通過(guò)指針域指向形狀的聲明來(lái)確定這種結構體用來(lái)構造什么形狀的數據結構，同時(shí)也限定了該結構體類(lèi)型的指針所能指向的形狀。這是對應形狀分析的需求所做的語(yǔ)言擴展，所允許的形狀有單鏈表、循環(huán)單鏈表、雙向鏈表、循環(huán)雙向鏈表。
1.2 形狀圖和形狀邏輯
　程序驗證之前，首先基于形狀圖邏輯對程序進(jìn)行形狀分析，形狀分析為每個(gè)程序點(diǎn)構建形狀圖，這些形狀圖構成程序驗證所需要的指針信息。在此通過(guò)舉例來(lái)介紹形狀圖[1]。
　以圖1（參考文獻[1]中有序鏈表節點(diǎn)插入函數循環(huán)不變式的形狀圖）為例說(shuō)明形狀圖和程序點(diǎn)指針等信息的聯(lián)系。在圖1中，圓節點(diǎn)表示指針類(lèi)型的聲明變量；虛邊框的矩形節點(diǎn)不代表任何程序元素；矩形節點(diǎn)表示由malloc生成的結構體變量；灰色矩形節點(diǎn)是濃縮節點(diǎn)，表示若干個(gè)（可以是0個(gè)）相鄰的、屬于同一數據結構的、同類(lèi)型的結構體變量，下側可以有無(wú)代表被濃縮節點(diǎn)個(gè)數的整型表達式以及約束該表達式的斷言。若沒(méi)有，則表示被濃縮節點(diǎn)個(gè)數是某個(gè)自然數，但和任何變量或常數聯(lián)系不起來(lái)。由圖1可知，head == ptr1，ptr == ptr1->next，head指向鏈表的長(cháng)度是m，ptr指向濃縮節點(diǎn)代表m-1個(gè)節點(diǎn)，可用head(->next)m-1上角標的方式來(lái)表示。

可見(jiàn)，形狀圖可以作為程序斷言，它是該圖所能表達的指針相等、不相等和別名斷言等的合取，包括其中謂詞節點(diǎn)和濃縮節點(diǎn)下側有關(guān)表長(cháng)或被濃縮節點(diǎn)個(gè)數的整型數據斷言。
　　形狀圖邏輯就是基于上面觀(guān)點(diǎn)來(lái)設計的Hoare邏輯的一種擴展。程序規范的形式是{G∧Q}S{G′∧Q′}，其中G是形狀圖，Q是表達程序其他性質(zhì)的符號斷言，兩部分的合取G∧Q作為程序點(diǎn)完整的斷言。本文程序驗證器的第一步工作，在無(wú)需程序員提供有關(guān)形狀的函數前后條件和循環(huán)不變式的情況下，利用形狀圖邏輯對程序進(jìn)行形狀分析。由于從一個(gè)語(yǔ)句前的G推導該語(yǔ)句后的G′不受Q的影響，因此形狀分析時(shí)，把程序規范簡(jiǎn)化為{G}S{G′}，以此來(lái)使用形狀圖邏輯的推理規則，建立各程序點(diǎn)的形狀圖G。在形狀分析的過(guò)程中，還利用循環(huán)不變式推斷算法得出各循環(huán)的循環(huán)不變形狀圖[2]。
　在完成形狀分析后，程序驗證器進(jìn)行程序其他性質(zhì)Q的驗證。在{G∧Q}S{G′∧Q′}中，若S不是指針操作語(yǔ)句，則G′和G一樣，但Q′可能不同于Q。若S是指針操作語(yǔ)句（指針賦值、分配空間和釋放空間等），則除了G′和G可能不同外，Q′和Q可能也有一些細微的區別。下面是本文關(guān)注的部分。
2 指針程序的驗證方法
　程序點(diǎn)數據結構構成的形狀有多種可能時(shí)，則G表示為G1∨G2∨…∨Gn。同樣，Q也可能是Q1∨Q2∨…∨Qm的析取形式。完整的斷言可以整理成析取范式（Disjunctive Normal Form）G1∧Q1∨G2∧Q2∨…∨Gk∧Qk的形式。根據形狀圖邏輯，可以用析取范式的一種情況為例來(lái)討論，寫(xiě)成G∧Q，G和Q分別都是合取形式。
程序驗證器基于形狀圖邏輯[2]進(jìn)行最強后條件演算并產(chǎn)生驗證條件，驗證條件由證明器Z3[3]自動(dòng)證明。
2.1 形狀圖和符號斷言之間的聯(lián)系
　符號斷言Q中允許出現指針是否等于NULL或兩個(gè)指針是否相等的斷言。即使函數前后條件和循環(huán)不變式中沒(méi)有這樣的斷言，它們也會(huì )因為出現在條件語(yǔ)句或循環(huán)語(yǔ)句的布爾表達式中，而在最強后條件演算過(guò)程中被加到Q中。
　Q中指針等于NULL或兩個(gè)指針相等的斷言會(huì )因為和G中的信息重復而被吸收，或因有矛盾而使得G∧Q為假。
　Q中訪(fǎng)問(wèn)路徑的合法性依賴(lài)于G。例如，在Q中若出現非指針型的訪(fǎng)問(wèn)路徑p -> … -> data，則忽略->data所剩下的前綴應該是G上到達某個(gè)結構節點(diǎn)的一條訪(fǎng)問(wèn)路徑，若是到達懸空節點(diǎn)、null節點(diǎn)或不存在這樣的路徑則都非法的，若是到達謂詞節點(diǎn)則視謂詞節點(diǎn)展開(kāi)后的情況決定。
　Q中的訪(fǎng)問(wèn)路徑之間是否有別名，Q中的訪(fǎng)問(wèn)路徑和下一條語(yǔ)句S中的訪(fǎng)問(wèn)路徑之間,以及S中的訪(fǎng)問(wèn)路徑之間是否有別名都依賴(lài)于G，即利用G可以判斷。
　在指針操作語(yǔ)句中，在對指針u賦值時(shí)可能會(huì )影響符號斷言：符號斷言中若有以u或u為前綴的訪(fǎng)問(wèn)路徑，則要用和u相等但不是別名的u′來(lái)代換u。另一個(gè)影響符號斷言的場(chǎng)合是，在free語(yǔ)句之后應該刪除涉及被釋放節點(diǎn)上數據的原子斷言。
　G中也會(huì )有符號斷言，附加在濃縮節點(diǎn)上，用來(lái)限制它代表結構節點(diǎn)的個(gè)數。G的符號斷言和Q的符號斷言不會(huì )有矛盾，但前者有時(shí)會(huì )給出更準確的信息。

2.2 程序推理規則的擴展
　在使用推理規則從語(yǔ)句S的前條件G∧Q產(chǎn)生后條件G′∧Q′時(shí)，要保證Q合法、Q和G無(wú)重復與矛盾。
　先考慮S是指針操作語(yǔ)句。修改指針型數據的簡(jiǎn)單語(yǔ)句會(huì )引起指針值的變化，或者是存儲堆塊的增減，因而導致形狀圖的變化。根據2.1節的介紹知道，對Q的影響是訪(fǎng)問(wèn)路徑的替換或者刪除部分斷言。先假定Q和S無(wú)別名，有別名的情況在考慮非指針操作語(yǔ)句時(shí)介紹。下面給出各種語(yǔ)句規則。
　(1)指針型賦值語(yǔ)句u=v
　若u既不是null指針也不是懸空指針，則按下面規則得到后斷言。
　{G∧Q} u = v {G′∧Q[u′/u]}
其中G′是由形狀分析得到的形狀圖，Q[u′/u]表示Q中作為訪(fǎng)問(wèn)路徑（包括作為前綴情況）的u和其相等且不互為別名的訪(fǎng)問(wèn)路徑u′代換。
　(2)對指針賦值的其他語(yǔ)句
　分配空間語(yǔ)句u=malloc(t)和函數調用語(yǔ)句ret=f(act)有關(guān)Q的處理同上面賦值語(yǔ)句的規則一樣。
　(3)釋放空間語(yǔ)句free(u)
　釋放u指向的節點(diǎn)后，Q中含u或u的別名的原子斷言不應再存在，因此規則如下：
{G∧Q} free(u) {G′∧Q′}
其中Q′由把Q中含u或u的別名的原子斷言都刪除而得到。
　很容易明白，若Q無(wú)別名，則這些語(yǔ)句的規則不會(huì )導致Q′出現別名，因為它們對Q做的小修改都不會(huì )引入別名。
　再考慮非指針操作語(yǔ)句。只要前斷言Q和語(yǔ)句S中無(wú)別名，則使用Hoare的賦值公理就是可靠的。若有別名，則可以先用G的信息來(lái)消除別名（把互為別名的訪(fǎng)問(wèn)路徑改成都用其中同一條訪(fǎng)問(wèn)路徑），然后再用賦值公理。定義eliminate_aliases函數為(S′,Q′)=eliminate_aliases(G, S, Q),它根據G消除S和Q中的別名，得到S′和Q′。
　把Hoare邏輯的賦值公理限定為無(wú)別名時(shí)才能使用，并增加下面的消除別名推理規則，就可以對含訪(fǎng)問(wèn)路徑別名的程序進(jìn)行推理。
對于修改指針型數據的語(yǔ)句，其前斷言Q可能是程序員提供的，例如不排除循環(huán)不變式中 Q存在別名，因此有時(shí)也需要這條規則。
　復合、條件和循環(huán)語(yǔ)句的規則以及推論規則的形式和Hoare邏輯相應規則的形式一致。

3 系統原型
　基于形狀圖邏輯，實(shí)現了PointerC語(yǔ)言的一個(gè)程序驗證器[1]，它能夠驗證使用圖1所定義的各種形狀的程序。除了驗證形狀外，還能驗證節點(diǎn)上數據的一些性質(zhì)。本文對有序鏈表插入節點(diǎn)的函數進(jìn)行了驗證。
　該驗證器分成下面幾個(gè)模塊，按所列次序順序執行：
　(1)普通編譯器的前端。對源程序進(jìn)行詞法分析、語(yǔ)法分析和靜態(tài)語(yǔ)義檢查后，生成抽象語(yǔ)法樹(shù)。
　(2)形狀分析。遍歷抽象語(yǔ)法樹(shù)，根據形狀聲明和形狀圖邏輯來(lái)生成各程序點(diǎn)的形狀圖。
　(3)驗證條件的生成。遍歷抽象語(yǔ)法樹(shù)，根據程序員提供的函數前后條件和循環(huán)不變式，按最強后條件演算方式為各函數生成驗證條件。
　(4)驗證條件的證明。將生成的各驗證條件G∧Q?圯Q′，按照上一節所介紹的方法翻譯成P∧Q?圯Q′的形式，逐個(gè)交給證明器進(jìn)行證明。
本文提出一種利用形狀圖信息來(lái)消除訪(fǎng)問(wèn)路徑別名，使得指針程序仍然可以用Hoare邏輯來(lái)進(jìn)行驗證的方法，并利用可自動(dòng)定理證明器的支持，開(kāi)發(fā)了一個(gè)PointerC語(yǔ)言的程序驗證器原型，展示了該方法的可行性。
參考文獻
[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.