一種用于指針程序安全性證明的指針邏輯陳意云 華保健 葛 琳 王志芳（中國(guó)科學(xué)技術(shù)大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)系，合肥 230026）（中國(guó)科學(xué)技術(shù)大學(xué)蘇州研究院軟件安全實(shí)驗(yàn)室，蘇州 215123）摘 要：在高可信軟件的各種性質(zhì)中，安全性是關(guān)注的重點(diǎn)，其中軟件滿足安全策略的證明方法是研究的熱點(diǎn)之一。本文根據(jù)我們所設(shè)想的安全程序的設(shè)計(jì)和證明框架，為類(lèi)C語(yǔ)言的一個(gè)子集設(shè)計(jì)了一個(gè)指針邏輯系統(tǒng)。該邏輯系統(tǒng)是Hoare邏輯系統(tǒng)的一種擴(kuò)展，它用推理規(guī)則來(lái)表達(dá)每一種語(yǔ)句引起指針信息的變化情況。它可用來(lái)對(duì)指針程序進(jìn)行精確的指針?lè)治?，所獲得信息用來(lái)證明指針程序是否滿足定型規(guī)則的附加條件，以支持程序的安全性驗(yàn)證。該邏輯系統(tǒng)也可用來(lái)證明指針程序的其它性質(zhì)。關(guān)鍵詞：軟件安全，指針邏輯，Hoare邏輯，指針?lè)治觯?lèi)型系統(tǒng)中圖法分類(lèi)號(hào)：TP301 1 引言在高可信的各種要求中，安全性（包括safety和security）是關(guān)注的重點(diǎn)。Safety是指軟件運(yùn)行時(shí)不引起危險(xiǎn)、災(zāi)難的能力，而security是指軟件系統(tǒng)對(duì)數(shù)據(jù)和信息提供保密性、完整性、可用性、真實(shí)性保障的能力。本文所講的安全性主要是指safety，但是軟件的safety和security是有聯(lián)系的，黑客通常就是利用緩沖區(qū)溢出、數(shù)組訪問(wèn)越界、懸空指針訪問(wèn)等低級(jí)的safety錯(cuò)誤，來(lái)破壞系統(tǒng)和獲取未經(jīng)授權(quán)的控制等。因此提高safety有助于保證security。程序性質(zhì)證明（而不是歷史上的程序正確性證明）領(lǐng)域近十年來(lái)有了很大的發(fā)展，許多學(xué)者提出了不同的思路，這些思路主要采取基于類(lèi)型的或基于邏輯的方法，用于高級(jí)語(yǔ)言程序或低級(jí)語(yǔ)言程序的性質(zhì)證明?；陬?lèi)型方法的典型研究有類(lèi)型化匯編語(yǔ)言（Typed Assembly Language）1和類(lèi)型細(xì)化（type refinement）理論2的研究?；谶壿嫹椒ǖ牡湫脱芯坑袛y帶證明的代碼（Proof-Carrying Code，簡(jiǎn)稱PCC）3和FPCC（Foundational Proof-Carrying Code）框架4。Zhong Shao的攜帶證明匯編編程項(xiàng)目CAP（Certified Assembly Programming）5和基于棧的CAP（SCAP）6是典型的基于邏輯的研究項(xiàng)目?；谶壿嫷姆椒ê突陬?lèi)型論的方法有很大的互補(bǔ)性，近年來(lái)出現(xiàn)了一些結(jié)合這兩種方法的研究。一種結(jié)合兩者的研究是Hongwei Xi等進(jìn)行的ATS（Applied Type System）項(xiàng)目的研究7，他們擴(kuò)展類(lèi)型系統(tǒng)，將程序狀態(tài)引入類(lèi)型系統(tǒng)，依靠ATS與Hoare邏輯的相似性，以ATS來(lái)編碼Hoare邏輯，從而可以在他們的類(lèi)型系統(tǒng)上模擬Hoare 邏輯的推理。在國(guó)際上這些研究的基礎(chǔ)上，我們認(rèn)為，對(duì)于那些有高安全性要求的軟件，程序設(shè)計(jì)和證明的一種新方式將是：（1）程序設(shè)計(jì)者將軟件的安全策略等描述成程序應(yīng)滿足的規(guī)范，連同程序一起提交給編譯器；（2）編譯器生成為證明程序滿足規(guī)范所需的驗(yàn)證條件，并且利用內(nèi)嵌的定理證明器自動(dòng)地或交互地證明這些驗(yàn)證條件；（3）編譯器在把源程序翻譯成目標(biāo)代碼的同時(shí)，將源程序滿足規(guī)范的證明翻譯成目標(biāo)代碼滿足等效規(guī)范的證明，這樣的編譯器稱為出具證明的編譯器（certifying compiler）；（4）在目標(biāo)代碼一級(jí)由證明檢驗(yàn)器利用代碼所攜帶的證明自動(dòng)進(jìn)行代碼滿足規(guī)范的檢驗(yàn)。該框架的優(yōu)點(diǎn)是，它向程序設(shè)計(jì)者提供源級(jí)而不是目標(biāo)級(jí)的程序性質(zhì)證明方法，以提高安全程序的開(kāi)發(fā)效率，同時(shí)它將編譯器、證明器等排除出受信任的計(jì)算基礎(chǔ)（Trusted Computing Base，簡(jiǎn)稱TCB），以盡量縮小系統(tǒng)的TCB。本文介紹我們?cè)谶@個(gè)框架的初步實(shí)現(xiàn)中，為類(lèi)C語(yǔ)言的一個(gè)子集PointerC設(shè)計(jì)的一個(gè)指針邏輯系統(tǒng)，它是Hoare邏輯的一種擴(kuò)展，本質(zhì)上是一種精確的指針?lè)治觯╬ointer analysis）工具。它可用來(lái)從前向后收集各指針是NULL指針、懸空指針（dangling pointer）還是有效指針（有指向?qū)ο蟮闹羔槪┑男畔?，收集各有效指針之間相等與否的信息。所收集信息用來(lái)證明指針程序是否滿足定型規(guī)則（typing rule）的附加條件，以支持對(duì)指針程序的安全性驗(yàn)證及其它性質(zhì)的驗(yàn)證。本文的組織如下：第二節(jié)介紹有關(guān)指針安全的一些基本概念，第三節(jié)是指針邏輯的設(shè)計(jì)，第四節(jié)給出一個(gè)證明實(shí)例，第五節(jié)是相關(guān)工作比較，第六節(jié)是總結(jié)。2 基本知識(shí)首先介紹PointerC在指針運(yùn)算方面的限制。在PointerC中，指針類(lèi)型的變量只能用于賦值、相等和不相等比較、存取指向?qū)ο蟮冗\(yùn)算以及作為函數(shù)（包括free）的參數(shù)，指針?biāo)阈g(shù)和取地址運(yùn)算（&）被禁止。malloc和free被看成是PointerC預(yù)定義的函數(shù)，并且滿足安全程序的最基本要求。例如malloc任何一次調(diào)用都能成功并且所分配空間同尚未釋放空間無(wú)任何重疊。上述限制的目的是為了便于靜態(tài)檢查程序的安全性。程序運(yùn)行時(shí)出現(xiàn)對(duì)NULL指針或懸空指針進(jìn)行存取指向?qū)ο蟮牟僮?、把NULL指針或懸空指針作為free函數(shù)調(diào)用的實(shí)在參數(shù)、發(fā)生內(nèi)存泄漏等都被認(rèn)為不滿足基本安全策略（類(lèi)型安全和內(nèi)存安全等）。該語(yǔ)言定型規(guī)則中的附加條件就是用來(lái)禁止這些情況的出現(xiàn)，本文指針邏輯的用途之一就是用來(lái)完成對(duì)這些附加條件的靜態(tài)檢查。下面明確本文有關(guān)指針類(lèi)型的一些術(shù)語(yǔ)和約定。程序中顯式聲明的變量稱為聲明變量，由malloc函數(shù)顯式和動(dòng)態(tài)分配的空間稱為動(dòng)態(tài)對(duì)象。在程序中，動(dòng)態(tài)對(duì)象的域只能通過(guò)指針類(lèi)型的聲明變量來(lái)訪問(wèn)，如s-data、和s-next-prior等，這種把脫引用（dereference）和域訪問(wèn)等組合的語(yǔ)法表達(dá)式稱為相應(yīng)聲明變量或動(dòng)態(tài)對(duì)象域的訪問(wèn)路徑，它是一個(gè)語(yǔ)法概念，是變量的名字。注意，若s是NULL指針或懸空指針時(shí)，s-next，s-data等在本文中都不看成訪問(wèn)路徑。下面用p，q和r作為代表一般訪問(wèn)路徑的元變量，它們最簡(jiǎn)單的情況就是聲明變量的名字。若訪問(wèn)路徑p的后面并置一個(gè)非空字符串后形成訪問(wèn)路徑q，則稱p是q的前綴。在用此定義時(shí)，需要把*p這種語(yǔ)法形式看成p*的形式。為方便起見(jiàn)，對(duì)訪問(wèn)路徑中重復(fù)出現(xiàn)的部分使用縮寫(xiě)表示，如s(-next)i用來(lái)表示s-next-next-next（其中-next出現(xiàn)i次），若i = 0則s(-next)i就表示s。各種類(lèi)型的指針變量（包括動(dòng)態(tài)對(duì)象中的指針類(lèi)型的域）都簡(jiǎn)稱為指針，NULL指針和懸空指針統(tǒng)稱為無(wú)效指針，有指向?qū)ο蟮闹羔樂(lè)Q為有效指針（effective pointer）。區(qū)分NULL指針和懸空指針是因?yàn)槌绦蛲ㄟ^(guò)判斷指針是否等于NULL可區(qū)別它們。訪問(wèn)路徑為p和q的兩個(gè)有效指針相等時(shí)，則訪問(wèn)路徑*p和*q（或p-next和q-next等）互為別名（alias）。由于PointerC對(duì)指針運(yùn)算的限制，再加上函數(shù)的參數(shù)都是傳值方式，一個(gè)聲明變量的名字不會(huì)和其它變量的名字互為別名（本文沒(méi)有討論數(shù)組元素的動(dòng)態(tài)別名問(wèn)題）；當(dāng)兩個(gè)有效指針的值相等，在代表它們的訪問(wèn)路徑上添加公共后綴后，所得兩條訪問(wèn)路徑形成別名。顯然，若能掌握有效指針相等與否的信息，就能判斷兩條訪問(wèn)路徑是否互為別名，及幫助選擇訪問(wèn)路徑的別名。3 指針邏輯的設(shè)計(jì)為證明程序滿足基本安全策略，除了要為PointerC設(shè)計(jì)一個(gè)類(lèi)型系統(tǒng)外，還需要設(shè)計(jì)一個(gè)證明系統(tǒng)。因?yàn)樵擃?lèi)型系統(tǒng)的某些定型規(guī)則中有附加條件，例如，下標(biāo)表達(dá)式不能越界、s-next必須是一條訪問(wèn)路徑等，它們不能由通常的類(lèi)型系統(tǒng)來(lái)檢查，本文采用一個(gè)證明系統(tǒng)來(lái)證明這些附加條件。我們通過(guò)對(duì)Hoare邏輯的擴(kuò)展來(lái)設(shè)計(jì)這樣一個(gè)證明系統(tǒng)，因?yàn)槲覀冊(cè)谀繕?biāo)語(yǔ)言級(jí)采用CAP方式。CAP證明目標(biāo)程序的性質(zhì)所采用的辦法是：把Hoare邏輯的方法直接綁定到目標(biāo)機(jī)器的操作語(yǔ)義上6, 7。我們?cè)谠凑Z(yǔ)言級(jí)使用Hoare邏輯方式有助于證明的翻譯。該邏輯系統(tǒng)也需要類(lèi)型系統(tǒng)的支持。例如，不同類(lèi)型的賦值語(yǔ)句需采用不同的推理規(guī)則。我們把Hoare邏輯的這個(gè)擴(kuò)展稱為指針邏輯，它的設(shè)計(jì)基于下面的考慮。由于別名問(wèn)題，Hoare邏輯不能直接用于有指針類(lèi)型的語(yǔ)言，需要對(duì)Hoare邏輯的規(guī)則增加一些約束并且需要增加一些規(guī)則來(lái)解決問(wèn)題。增加一些基本規(guī)則來(lái)表達(dá)值相等的訪問(wèn)路徑或互為別名的訪問(wèn)路徑的性質(zhì)是簡(jiǎn)單的，下面是這類(lèi)性質(zhì)的一些例子：（1）值相等的訪問(wèn)路徑中，若其中一個(gè)代表有效指針，則其它的也都是；（2）給值相等的訪問(wèn)路徑添加同樣的后綴，若形成訪問(wèn)路徑，則結(jié)果互為別名；（3）互為別名的訪問(wèn)路徑的值一定相等；（4）訪問(wèn)路徑的別名關(guān)系滿足自反性、傳遞性和對(duì)稱性。在Hoare邏輯的公式PSQ中，S是語(yǔ)法結(jié)構(gòu)，通常是語(yǔ)句，P和Q分別是它的前后條件。下面考慮兩種語(yǔ)句，首先是指針類(lèi)型的賦值語(yǔ)句p = q，Hoare邏輯的正向賦值公理是Q p=q $p. (p= qpp Qpp)其中ppFV(q)FV(Q)，F(xiàn)V得到變?cè)凶杂勺兞康募?。考慮p是有效指針的情況，下面的約束得到滿足時(shí)才能使用該公理。（1）前條件Q沒(méi)有p的其它別名（其它別名指不是p本身）。若不滿足，可以嘗試用上面提到的基本規(guī)則把Q變換到滿足這個(gè)條件。（2）訪問(wèn)路徑q也不以p的其它別名為前綴（在此對(duì)程序加這點(diǎn)限制是為了簡(jiǎn)化討論）。（3）前條件Q中一定有p=r這樣的斷言（r不是p的別名）。這是為了保證該賦值不會(huì)引起內(nèi)存泄漏。再考慮為free(p)設(shè)計(jì)推理規(guī)則，僅考慮p所指向?qū)ο蟛缓行е羔樳@種比較簡(jiǎn)單的情況?？紤]該規(guī)則的前條件和使用該規(guī)則的約束：（1）p應(yīng)該是有效指針。它直接出現(xiàn)在該規(guī)則的前條件中。（2）前條件中沒(méi)有以p（或與p相等的訪問(wèn)路徑）為前綴的訪問(wèn)路徑，除非出現(xiàn)在p-next=NULL或p-data=e（e是整型表達(dá)式）這樣的斷言中。該規(guī)則要能體現(xiàn)：前條件中涉及p（包括和p相等的訪問(wèn)路徑）的基本斷言，在后條件中都被刪除。這樣的要求難以僅用語(yǔ)法代換來(lái)表達(dá)。例如，若當(dāng)前程序點(diǎn)的斷言是p=q effective(p) p-next=NULL p-data=10，下一個(gè)語(yǔ)句是free(p)，則期望該語(yǔ)句后程序點(diǎn)的斷言是dangling(p) dangling(q)。要想完成上述兩種語(yǔ)句中的約束檢查和斷言刪除等，需要尋找新的方式來(lái)表達(dá)推理規(guī)則。指針邏輯的推理規(guī)則設(shè)計(jì)基于下面的考慮：（1）若在某程序點(diǎn)能區(qū)分有效指針、NULL指針和懸空指針，并且知道有效指針之間是否相等，則就能判斷有關(guān)指針的操作是否安全，還可以得出經(jīng)過(guò)這步操作后指針信息的變化。（2）推理規(guī)則的設(shè)計(jì)要有利于用工具來(lái)進(jìn)行自動(dòng)推導(dǎo)。（3）把相等的指針表達(dá)在一個(gè)集合中，便于在推理規(guī)則中表示語(yǔ)句執(zhí)行所引起的指針信息變化。本文主要介紹證明指針性質(zhì)的推理規(guī)則的設(shè)計(jì)。3.1基本運(yùn)算的定義在指針邏輯中，程序點(diǎn)的NULL指針集合用N表示，懸空指針的集合用D表示，有效指針集合用P表示。P中指針的具體值并不重要，重要的是它們是否相等，因此基于相等與否把它們劃分成若干等價(jià)集合。例如，若P中有等價(jià)集合p, q，它表示p和q是相等的有效指針，并且它們不等于其它集合中的指針。一個(gè)等價(jià)集合不能刪掉任何元素，也不能分成若干子集，因?yàn)檫@樣做都會(huì)使指針信息發(fā)生變化。因此，在指針邏輯的斷言演算中，P中的等價(jià)集合被看成命題常元；同樣，N和D也都被看成命題常元。這些集合只能用本節(jié)為指針賦值等設(shè)計(jì)的推理規(guī)則來(lái)改變。在語(yǔ)法結(jié)構(gòu)的前后條件中，P中的等價(jià)集合、N和D 雖以集合方式出現(xiàn)，但本質(zhì)上是邏輯表達(dá)式，因此用“”連接它們。作為縮寫(xiě)，有時(shí)用Y表示P N D。訪問(wèn)路徑是滿足一定語(yǔ)法要求的字符串，本文所說(shuō)的串都是指構(gòu)成訪問(wèn)路徑的串或子串，并用Paths表示訪問(wèn)路徑集合。若訪問(wèn)路徑p是q的前綴，則謂詞prefix(p, q)等于true，否則等于false。符號(hào)“”用于兩個(gè)串的連接；它也用于串的集合S和串s的連接，使得S中的每個(gè)串連接s：SsS where ss S iff s S若s1s2和s1（s1和s2都不是空串）是值相等的訪問(wèn)路徑，則稱s2是訪問(wèn)路徑s1s2s3（s3也不是空串）中的環(huán)。符號(hào)表示語(yǔ)法上等同，表示語(yǔ)法上等同測(cè)試。下面先定義訪問(wèn)路徑上的一些函數(shù)，它們都以程序點(diǎn)的指針信息Y或P為參數(shù)，下面統(tǒng)一都將它忽略。這些定義中出現(xiàn)的關(guān)鍵字在一些軟件語(yǔ)言中都出現(xiàn)過(guò)，在此忽略它們的解釋。需要強(qiáng)調(diào)一下，訪問(wèn)路徑p和q在本文中幾乎總是指稱指針，因此本文也經(jīng)常直接稱它們?yōu)橹羔?；但是，在下面的函?shù)中，使用的是它們的語(yǔ)法表達(dá)式（訪問(wèn)路徑）。1）別名集合的計(jì)算closure(p)計(jì)算訪問(wèn)路徑p的最簡(jiǎn)別名集合，稱為p的閉包，它包含且僅包含p所有的無(wú)環(huán)別名。 closure(p)if length(p)=1then pelse let s1 sn-1 sn p in compression (expansion(closure(s1 sn-1) sn) 其中l(wèi)ength(p)計(jì)算訪問(wèn)路徑p的長(zhǎng)度，它是指p由幾個(gè)有語(yǔ)法意義的部分組成，而不是指p的字符個(gè)數(shù)，例如t-next-data的長(zhǎng)度為3。expansion(S)用來(lái)在別名集合S中加入與其中訪問(wèn)路徑相等的訪問(wèn)路徑，其定義如下： expansion(S) if $S: (PND).(S S !=) then let p1, , pn= S- S where S (PND) S S != in S closure(p1) closure(pn) else compression(S)用來(lái)刪除別名集合S中帶環(huán)的訪問(wèn)路徑，其定義如下： compression(S)S-Swhere (SS) ( (s1 s2 s3)S iff (s1!=e) (s2!=e) (s3!=e) (s1 s3)S) (s1 s2= s1) ) 為清晰起見(jiàn)，上面給出的是closure的一個(gè)定義，而不是closure的實(shí)現(xiàn)算法，例如，該定義沒(méi)有考慮面臨雙向循環(huán)鏈表等帶環(huán)數(shù)據(jù)結(jié)構(gòu)時(shí)，遞歸計(jì)算的終止問(wèn)題。在closure的實(shí)現(xiàn)中是不難把計(jì)算的終止等問(wèn)題考慮進(jìn)去的。有了closure函數(shù)，也很容易刪掉訪問(wèn)路徑中的環(huán)，為方便討論，我們認(rèn)為程序中給出的都是最簡(jiǎn)訪問(wèn)路徑。2）訪問(wèn)路徑的單個(gè)別名函數(shù)alias(p, q)該函數(shù)從訪問(wèn)路徑p的別名集合中任取p，滿足p不以訪問(wèn)路徑q的別名為前綴。若找不到這樣的p，則結(jié)果仍是p。 alias(p, q)let S = p : closure(p) | q: closure(q). prefix(q, p) in if S = then p else p where pS3）訪問(wèn)路徑所在等價(jià)集合函數(shù)equals(p)若p的別名出現(xiàn)在某個(gè)等價(jià)集合中，則返回該集合，否則返回空集。 equals(p) if $S:P.(Sclosure(p) != ) then S where SP Sclosure(p) != else 下面介紹在推理規(guī)則中直接使用的運(yùn)算或謂詞，這些運(yùn)算表達(dá)語(yǔ)句后條件中的Y是如何從前條件的Y得到的。4）有效指針的替換和刪除運(yùn)算若S是P的一個(gè)等價(jià)集合，p是一個(gè)有效指針，則S/p表示對(duì)S中以p的別名為前綴的每個(gè)指針q，都用alias(q, p)尋找一個(gè)別名來(lái)代替它，然后將S中出現(xiàn)的p的別名和以它們?yōu)榍熬Y的訪問(wèn)路徑都刪除。 S/p let S=q : S | p:closure(p). prefix(p, q) q:Paths | $q:S.$p:closure(p).(prefix(p,q) q alias(q, p) in q: S| (qclosure(p) p:closure(p).prefix(p, q)若需要對(duì)P中每個(gè)S進(jìn)行替換和刪除p的運(yùn)算，則用P/p表示。當(dāng)有效指針q被賦予一個(gè)不等于q的值時(shí)，q和以q為前綴的訪問(wèn)路徑都需要從原來(lái)的等價(jià)集合中刪除，例如，若P=s, t-prior, t, s-next，則P/t=s, s-next-prior, s-next。5）無(wú)效指針替換運(yùn)算Np和Dp分別用來(lái)表示將N和D中以p的別名為前綴的訪問(wèn)路徑用它們的其它別名來(lái)代替。 Np q:N | p:closure(p).prefix(p, q) q:Paths | $q:N.$p:closure(p).(prefix(p,q) q alias(q, p)Dp的定義類(lèi)似。6）無(wú)效指針刪除運(yùn)算N/p和D/p分別用來(lái)表示將N和D中出現(xiàn)的p的別名刪除。 N/pq : N | (qclosure(p) N/p1, , pn(N/p1) /pn)D/p的定義類(lèi)似。7）指針添加運(yùn)算并集算符“”直接用來(lái)表示向指針集合中添加一個(gè)指針，例如S p。我們?yōu)镻中等價(jià)集合的增加、刪除和替換使用新的記號(hào)，它們基于集合運(yùn)算符號(hào)“”和“-”及它們的組合來(lái)定義。 P+pPp 把僅由p構(gòu)成的等價(jià)集合加到P中 P-pP-equals(p)刪掉P中p所在的等價(jià)集合 P add q to p(P- p) equals(p) q把q加到P中p所在的等價(jià)集合8）有效指針刪除是否引起內(nèi)存泄漏的測(cè)試leak(p)對(duì)有效指針p所在等價(jià)集合S進(jìn)行S/p計(jì)算，結(jié)果為空集合時(shí)則表示會(huì)出現(xiàn)內(nèi)存泄漏；否則不會(huì)。 leak(p)equals(p)/p = 9）一些基本謂詞的定義下面這些謂詞用來(lái)測(cè)試指針p的別名是否在某個(gè)集合中。 p : P$S:P.(Sclosure(p) != ) p : SSclosure(p) != （S是P中的一個(gè)等價(jià)集合） p : N(N closure(p) != p : D(D closure(p) != p : Y(p : P) (p : N) (p r1,p-rn的話，則可把該語(yǔ)句看成語(yǔ)句序列p-r1=NULL; ;p-rn=NULL; free(p)來(lái)進(jìn)行證明。這樣做的目的是簡(jiǎn)化free(p)的規(guī)則。 4 證明實(shí)例我們已經(jīng)用指針邏輯系統(tǒng)證明了單鏈表、雙向鏈表和二叉樹(shù)等數(shù)據(jù)結(jié)構(gòu)的一些函數(shù)。本節(jié)以刪除二叉排序樹(shù)一個(gè)結(jié)點(diǎn)并重接它的左或右子樹(shù)的函數(shù)struct node * DeleteNode(struct node *p)為例。在證明該函數(shù)時(shí)，參數(shù)所指向的樹(shù)上，有效指針和NULL指針的布局是不清楚的，但它必須滿足樹(shù)的定義。若樹(shù)結(jié)點(diǎn)定義是struct node int data; struct node *l，*r; ，那么以p為根結(jié)點(diǎn)指針的樹(shù)的定義如下： tree(p)pN (p tree(p-l) tree(p-r) )如果p不是空指針，通過(guò)下面的演算可以知道p是有效指針并且tree(p-l) tree(p-r)為真。 tree(p) (p!=NULL) (pN (p tree(p-l) tree(p-r) ) ) (p!=NULL) (pN (p!=NULL) (p tree(p-l) tree(p-r) (p!=NULL) false (p tree(p-l) tree(p-r) p tree(p-l) tree(p-r)程序設(shè)計(jì)者只要給出函數(shù)前后條件和循環(huán)不變式，其它程序點(diǎn)的斷言可以通過(guò)指針邏輯得到。圖1僅對(duì)形參p的左右子樹(shù)都非空的大部分程序點(diǎn)插入了斷言（該函數(shù)要求參數(shù)是非空樹(shù)），其它部分在關(guān)鍵點(diǎn)插入了斷言。在斷言中，直接列出各等價(jià)集合來(lái)表示P，N和D用下標(biāo)N和D來(lái)區(qū)分，它們?yōu)榭諘r(shí)則不出現(xiàn)在斷言中。我們沒(méi)有給出return語(yǔ)句后的斷言，因?yàn)楸疚臎](méi)有提供return語(yǔ)句的推理規(guī)則。5 相關(guān)工作Hoare邏輯的一個(gè)重要特征是用變量代換來(lái)抓住賦值的語(yǔ)義，本文的指針邏輯系統(tǒng)本質(zhì)上是一種指針?lè)治龉ぞ?，它用訪問(wèn)路徑的增加、刪除和替換來(lái)抓住指針操作帶來(lái)的影響。指針?lè)治鲆呀?jīng)研究了20多年，歷史上的指針?lè)治鲋饕卮穑簩?duì)指針類(lèi)型的變量，它們運(yùn)行時(shí)可能指向的對(duì)象集合是什么。這樣的指針?lè)治隹捎迷诔绦虻撵o態(tài)分析和優(yōu)化的很多方面：寄存器分配和常量傳播所需的活躍變量分析，還有像NULL指針脫引用這樣的潛在運(yùn)行錯(cuò)誤的靜態(tài)檢查等。近年來(lái)它還用在發(fā)現(xiàn)危及安全的緩沖區(qū)溢出和打印格式串錯(cuò)誤等。和其它靜態(tài)技術(shù)類(lèi)似，指針?lè)治鍪艿娇膳卸ㄐ詥?wèn)題的困擾，對(duì)大多數(shù)語(yǔ)言來(lái)說(shuō)，所得到的解總是一個(gè)近似。在指向?qū)ο蠹系木壬?，不同的?yīng)用要求不同的粒度。不同的精度要求采用不同的分析方法，有流敏感和流不敏感的區(qū)分，路徑敏感和路徑不敏感的區(qū)分以及過(guò)程內(nèi)和過(guò)程間的區(qū)分。例如，Bjame Steensgaard對(duì)C語(yǔ)言的一個(gè)禁止指針強(qiáng)制和指針?biāo)阈g(shù)等的子集，描述了一種基于類(lèi)型推導(dǎo)的過(guò)程間的、流不敏感的和路徑不敏感的指針?lè)治?。該方法基于變量的存儲(chǔ)模型，定義了類(lèi)型系統(tǒng)及推導(dǎo)指針指向的規(guī)則集合，用以分析運(yùn)行時(shí)指針變量可能指向的對(duì)象集合。Marc Berndl等首先把二叉決策圖用于流不敏感和路徑不敏感的指針?lè)治?，比較成功地解決了這類(lèi)分析的效率問(wèn)題。Michael Hind對(duì)這方面的研究做了一個(gè)總結(jié)10，列出了一些待解決的問(wèn)題。出于軟件安全方面的要求，本文實(shí)現(xiàn)的是精確而不是近似的指針?lè)治觯虼嗽诓挥绊懻Z(yǔ)言功能的情況下，對(duì)C語(yǔ)言中難以判定的指針使用方式進(jìn)行了限制，正是這種限制使得本文可以采用與通常的C語(yǔ)言指針?lè)治鐾耆煌姆椒ā?p!=NULL tree(p) struct node * DeleteNode(struct node *p)struct node *q, *s; p tree(p-l) tree(p-r) q, sD if(p-r=NULL) /* 右子樹(shù)為空，只需重接它的左子樹(shù) */ q = p; s = p-l; free(q); p, qD tree(s) return s; elseif(p-l=NULL)/* 左子樹(shù)為空，只需重接它的右子樹(shù) */ q = p; s = p-r; free(q); s p, qD tree(s) return s; else/* 左右子樹(shù)均不空 */ p p-l p-r q, sD tree(p-l) tree(p-r) q = p; s = p-l;if(s-r = NULL) /* 重接*q的左子樹(shù) */ q-l = s-l; p-data = s-data; free(s); p, q tree(p) return p; else p, q p-r p-l, s s-r tree(p-l-l) tree(p-l-r) tree(p-r) q = s; s = s-r; $n:N.( p p-r i:0.n-1.p-l(-r)i p-l(-r)n, q p-l(-r)n+1, s i:0.n.tree(p-l(-r)i-l) tree(p-l(-r)n+1) tree(p-r) ) 循環(huán)不變式while(s-r != NULL) /* 轉(zhuǎn)左，然后向右前進(jìn)到盡頭 */ q = s; s = s-r; $n:N.( p p-r i:0.n-1.p-l(-r)i p-l(-r)n, q p-l(-r)n+1, s s-rN i:0.n.tree(p-l(-r)i-l) tree(p-l(-r)n+1) tree(p-r) ) p-data = s-data;q-r = s-l;/* 重接*q的右子樹(shù) */ $n:N.( p p-r i:0.n-1.p-l(-r)i p-l(-r)n, q s ( (s-l, q-r s-rN) s-r, s-l, q-rN ) i:0.n.tree(p-l(-r)i-l) tree(p-l(-r)n+1) tree(p-r) ) free(s); $n:N.( p p-r i:0.n-1.p-l(-r)i p-l(-r)n, q (q-rq-rN) sD i:0.n.tree(p-l(-r)i-l) tree(p-l(-r)n+1) tree(p-r) ) /* 如果在返回調(diào)用者前，忽略q和s的信息，可以得到 p tree(p) */return p;圖1 刪除二叉樹(shù)結(jié)點(diǎn)的程序和斷言本文的指針邏輯和分離邏輯（separation logic）11, 12都是通過(guò)對(duì)Hoare邏輯的拓展，來(lái)證明在共享易變數(shù)據(jù)結(jié)構(gòu)（shared mutable data structure）上帶指針操作的程序的性質(zhì)。分離邏輯適合于對(duì)使用這些數(shù)據(jù)結(jié)構(gòu)的低級(jí)命令式語(yǔ)言的程序進(jìn)行推理。這樣的簡(jiǎn)單語(yǔ)言包括了訪問(wèn)和修改共享結(jié)構(gòu)的命令，包括了顯式分配存儲(chǔ)和釋放存儲(chǔ)的命令。分離邏輯在斷言語(yǔ)言中引入了“分離合取”等空間連接詞，它們可用來(lái)斷言存儲(chǔ)空間分離部分的性質(zhì)，例如P*Q表示P和Q在兩部分不相交的存儲(chǔ)空間上分別成立。分離提供了分離邏輯最關(guān)鍵的特征局部推理。分離邏輯還使用在抽象數(shù)據(jù)結(jié)構(gòu)上遞歸定義的謂詞，這些謂詞允許簡(jiǎn)潔和靈活地描述有控制地共享的結(jié)構(gòu)。分離邏輯在證明單鏈表、雙向鏈表和二叉樹(shù)等易變數(shù)據(jù)結(jié)構(gòu)的程序上的成功已經(jīng)展示出它的優(yōu)點(diǎn)。近來(lái)分離邏輯已經(jīng)出現(xiàn)在用低級(jí)語(yǔ)言寫(xiě)的操作系統(tǒng)一些核心程序的正確性證明上13。本文的指針邏輯和分離邏輯的主要區(qū)別有兩點(diǎn)。分離邏輯面向低級(jí)編程語(yǔ)言，指針邏輯面向高級(jí)編程語(yǔ)言。另外，由于PointerC不允許指針指向動(dòng)態(tài)申請(qǐng)存儲(chǔ)塊的中間，那么從指針是否相等就可以判斷它們指向的空間是否分離，因此指針邏輯不必引入分離合取這樣的空間連接詞。Bornat也采用Hoare邏輯來(lái)證明指針程序的性質(zhì)14，采用類(lèi)似方法的還有Mehta和Nipkow 15。Bornat把堆看成由指針?biāo)饕囊蝗簩?duì)象，把對(duì)象看成由名字索引的一組成員，然后把Hoare邏輯賦值公理拓展成能用于對(duì)象成員賦值的場(chǎng)合，用它來(lái)證明一些指針程序的性質(zhì)。由指針?biāo)饕嗟扰c否來(lái)判斷別名，基于此來(lái)拓展賦值公理是他和我們方法的共同特征，但是他的方法只能用于不提供free操作并且有無(wú)用單元收集（garbage collection）的語(yǔ)言。我們的方法雖然適用于提供free操作的場(chǎng)合，但是卻導(dǎo)致了指針邏輯的復(fù)雜。例如，在free(p)時(shí)，為防止懸空指針引用，需要保證以后不會(huì)用p或與p相等的指針去訪問(wèn)；再例如，在對(duì)有效指針p賦值時(shí)，為防止出現(xiàn)內(nèi)存泄漏，需要知道有和p相等的指針存在。這就導(dǎo)致指針邏輯像是從前向后計(jì)算最強(qiáng)后條件，而不是從后向前計(jì)算最弱前條件。6 結(jié)束語(yǔ)本文提出了一種可對(duì)指針程序進(jìn)行精確分析的邏輯系統(tǒng)，它可用來(lái)證明指針程序是否滿足定型規(guī)則的附加條件，以支持指針程序的安全性證明及其它性質(zhì)證明。我們已經(jīng)利用證明輔助工具Coq16完成了指針邏輯對(duì)PointerC操作語(yǔ)義可靠的證明。PointerC及其類(lèi)型系統(tǒng)、指針邏輯的斷言語(yǔ)言、指針邏輯可靠性證明、一些應(yīng)用程序的證明實(shí)例以及基于第1節(jié)所提框架的出具證明編譯器的一些實(shí)現(xiàn)工作，可在我們項(xiàng)目網(wǎng)頁(yè)/lss/doc/index.html上找到。下一步我們將考慮放寬對(duì)指針運(yùn)算的限制，有限制地允許指針?biāo)阈g(shù)，以適應(yīng)編程中經(jīng)常使用的calloc存儲(chǔ)分配。加上面向?qū)ο蟮恼Z(yǔ)言構(gòu)造，使程序性質(zhì)證明具有更好的模塊性也是下一步需要考慮的內(nèi)容。參 考 文 獻(xiàn)1 Morrisett G, Walker D, Crary K, Glew N. From system F to typed assembly language. Proceedings of 25th ACM Symposium on Principles of Programming Languages, San Diego, 1998: 85-97.2Mandelbaum Y, Walker D, Harper R. An effective theory of type refinements. Proceedings of the 8th International Conference on Functional Programming, Uppsala, Sweden, 2003: 213-225.3Necula G. Proof-carrying code, Proc.24th ACM Symposium On Principles of Programming Languages. New York, 1997: 106-119.4Appel A. W. Foundational proof-carrying code. Proc. 16th Annual IEEE Symposium on Logic in Computer Science, 2001: 247-258.5 Yu D, Hamid N. A., Shao Z. Building certified libraries for PCC: dynamic storage allocation. Science of Computer Programming, 2004, 50(1-3):101-127.6 Feng X, Shao Z, Vaynberg A, Xiang S, Ni Z. Modular Verification of Assembly Code with Stack-Based Control Abstractions. Proceedings of the 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation, Ottawa, Canada, 2006: 401-414.7Xi H. Applied type system: extended abstract. In the post-workshop proceedings of TYPES 2003, volume 3085 of LNCS, Springer-Verlag, 2004: 394-408.8 Steensgaard B. Points-to analysis in almost linear time. Proceedings of the 23th Annual ACM Symposium on Principles of Programming Languages, 1996: 32-41.9 Berndl M, Lhotk O, Qian F, Hendren L, Umanee N. Points-to analysis using BDDs. Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation, San Diego, 2003: 103-114.10 Hind M. Pointer Analysis: Havent We Solved This Problem Yet? Proceedings of ACM Workshop on Program Analysis for Software. Tools and Engineering, 2001: 54-61.11 Reynolds J. C. Separation logic: a logic for shared mutable data structures. Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, 2002: 55-74.12 Parkinson M, Bierman G. Separation logic and abstraction. Proceedings of 32th ACM Symposium on Principles of Programming Languages, 2005: 247-258.13 Bornat R, Calcagno C, OHearn P, Parkinson W. Permission accounting in separation logic. Proceedings of the 32nd ACM symposium on Principles of programming languages, 2005: 259-270.14 Bornat R. Proving pointer programs in Hoare logic. Proceedings of the 5th International Conference on Mathematics of Program Construction, 2000: 102-126.15 Mehta F, Nipkow T. Proving pointer programs in higher-order logic. Information and Computation, 2005, 199(1-2): 200-227.16 Bertot Y, Castran P, Interactive Theorem Proving and Program Development: CoqArt: The Calculus of Inductive Construction, Texts in Theoretical Computer Science, an EATCS series. Springer Verlag, 2004A Pointer Logic for Safety Verification of Pointer ProgramsCHEN Yi-Yun, HUA Bao-Jian, GE Lin, WANG Zhi-Fang(Department of Computer Science, University of Science and Technology of China, Hefei, 230026)(Software Security Lab., Suzhou Institute for Advanced Study, University of Science and Technology of China, Suzhou, 215123)Abstract:Safety is an important issue among the properties of high-assurance software and the verification methods for software to meet safety policies are one of the hot research. In terms of our sketch of design and verification of safety programs, we design a pointer logic system for a subset of C-like language. This logic system is an extension of Hoare logic system and inference rules are designed to express the modification of pointer information for every kind of statements. It can be used for accurate pointer analysis of pointer programs. The information from the analysis can be used to verify if pointer programs satisfy the side conditions of typing rules and then support safety verification for programs. The logic system can also be used to verify other properties of pointer programs.Key words:software safety, pointer logic, Hoare logic, pointer analysis, type system本課題得到國(guó)家自然科學(xué)基金（60673126）資助。陳意云1946生，男，教授，博士生導(dǎo)師，主要研究領(lǐng)域?yàn)槌绦蛟O(shè)計(jì)語(yǔ)言的理論和實(shí)現(xiàn)技術(shù)、形式描述技術(shù)、軟件安全。華保健 1979年生，男，博士生，主要研究領(lǐng)域?yàn)槌绦蝌?yàn)證、程序邏輯、軟件安全。葛 琳1979生，女，博士生，主要研究領(lǐng)域?yàn)槌绦蝌?yàn)證、軟件安全、類(lèi)型理論和系統(tǒng)。王志芳1982生，男，博士生，主要研究領(lǐng)域?yàn)檐浖踩?、程序邏輯、程序?yàn)證。CHEN Yi-Yun, born in 1946, professor, Ph. D. supervisor. His research interests include theory and implementation of programming languages, formal description technologies, and software safety and security.HUA Bao-Jian, born in 1979, Ph. D. candidate. His research interests include program verification