安全C語言驗證器中形狀系統(tǒng)的形狀檢查方法

孫 科,羅奇鳴,李薛劍,陳意云

(中國科學技術(shù)大學 計算機科學與技術(shù)學院,合肥 230026)

1 引 言

1.1 研究背景

隨著計算機技術(shù)的發(fā)展,各行各業(yè)與計算機軟件的關(guān)系日益緊密,且軟件的規(guī)模和復雜度也在不斷增加,在這種大背景下,整個行業(yè)對于軟件的可信度提出了更高的要求,尤其是安全攸關(guān)的領(lǐng)域.遺憾的是,許多程序設計語言在發(fā)展的同時,并未在語言的安全層面提供太多保障,典型代表就是C語言.

對此,多種基于不同切入點的工作正在穩(wěn)步進行.在程序設計語言層面,Rust作為一門新興語言,在編譯過程中引入了諸多概念,約束程序的行為,以期在程序編譯期間盡可能發(fā)現(xiàn)內(nèi)存、數(shù)據(jù)競爭等方面的問題;SPARK[1]則是一門基于Ada語言的形式化定義語言,它將形式化方法引入軟件的設計中,藉此提升軟件的可信度.而對于既有的程序設計語言,基于演繹推理的形式化驗證則是提高軟件可信度的重要方法,例如Ynot[2]、Spec#[3]、ESC/Java[4]等.本課題組面向C語言開發(fā)了一套基于演繹推理的程序驗證工具——安全C語言驗證器(以下簡稱“驗證器”),該驗證器基于霍爾邏輯[5]和形狀圖邏輯[6,7].

1.2 研究目的

基于演繹推理的驗證工具大多基于如下實現(xiàn):根據(jù)用戶提供的函數(shù)前條件、后條件以及循環(huán)不變式,驗證工具采用正向或逆向演算,將程序需要滿足的性質(zhì)轉(zhuǎn)換為驗證條件,后采用自動定理證明器實現(xiàn)驗證.為解決霍爾邏輯難以處理C語言中由于指針帶來的別名問題,安全C語言驗證器采用形狀圖邏輯處理堆指針,將程序狀態(tài)描述為G和Q,其中G表示描述指針性質(zhì)的形狀圖,遵循形狀圖邏輯,Q表示描述程序其它性質(zhì)的符號斷言,遵循霍爾邏輯.形狀系統(tǒng)是對于形狀圖邏輯的一個實現(xiàn),主要用以限制利用動態(tài)內(nèi)存分配和指針能夠構(gòu)造的易變數(shù)據(jù)結(jié)構(gòu)的種類,并約束程序操作這些數(shù)據(jù)結(jié)構(gòu)的行為.這里的易變數(shù)據(jù)結(jié)構(gòu)指的是通過節(jié)點指針域?qū)崿F(xiàn)連接的,結(jié)構(gòu)完整性和節(jié)點個數(shù)等性質(zhì)在程序執(zhí)行過程中容易發(fā)生變化的數(shù)據(jù)結(jié)構(gòu),諸如鏈表和二叉樹.形狀系統(tǒng)的演算依賴于程序的操作語義,然而易變數(shù)據(jù)結(jié)構(gòu)的常規(guī)操作容易造成易變數(shù)據(jù)結(jié)構(gòu)性質(zhì)的變化,其中不免對易變數(shù)據(jù)結(jié)構(gòu)造成破壞,使其不符合指定的形狀定義,例如雙向鏈表的插入操作.

不符合形狀定義的易變數(shù)據(jù)結(jié)構(gòu)給形狀系統(tǒng)帶來了嚴峻的挑戰(zhàn),其一,對不符合形狀定義的易變數(shù)據(jù)結(jié)構(gòu)進行演算,是無法推斷別名的一個重要根源,例如指針訪問路徑p->nxt懸空,此時尋找該路徑的別名則是一個無意義的操作;其二,用戶通過斷言描述形狀圖,而斷言的構(gòu)造語義無法確保新構(gòu)造的易變數(shù)據(jù)結(jié)構(gòu)符合形狀定義,例如可能存在用戶錯誤描述形狀圖的情況,這將影響驗證的正確性;其三,不符合形狀定義的易變數(shù)據(jù)結(jié)構(gòu)也是造成循環(huán)不變形狀圖自動推斷操作[8,9]不終止的主要原因;其四,驗證器依賴于Z3自動定理證明器[10]進行證明,而從不符合形狀定義的易變數(shù)據(jù)結(jié)構(gòu)中導出的指針關(guān)系通常是存在問題的,為Z3自動定理證明器的證明帶來較大壓力.

1.3 本文工作

本文工作基于安全C語言驗證器的形狀系統(tǒng)進行設計與實現(xiàn),提出了形狀檢查方法,它能夠?qū)幸鬃償?shù)據(jù)結(jié)構(gòu)操作的C程序源碼進行檢查,判斷相關(guān)程序點的易變數(shù)據(jù)結(jié)構(gòu)是否符合形狀定義.本方法在形狀系統(tǒng)中分別實現(xiàn)了隱式形狀檢查和顯式形狀檢查,前者由系統(tǒng)在重要演算點自動對易變數(shù)據(jù)結(jié)構(gòu)進行形狀檢查,避免不符合定義的易變數(shù)據(jù)結(jié)構(gòu)對形狀圖邏輯演算的正確性造成影響,后者允許用戶在程序點主動指定需要形狀檢查的易變數(shù)據(jù)結(jié)構(gòu),以盡早發(fā)現(xiàn)其中的潛在問題,提升形狀檢查的靈活性和易用性.此外,形狀檢查方法采用3階段處理框架,分解由于易變數(shù)據(jù)結(jié)構(gòu)中指針域靈活指向帶來的復雜性,降低算法實現(xiàn)上的難度.

本文的內(nèi)容結(jié)構(gòu)組織如下:第2節(jié)概述安全C語言驗證器和形狀系統(tǒng);第3節(jié)介紹形狀檢查的相關(guān)概念;第4節(jié)詳細介紹形狀檢查中多階段檢查的相關(guān)規(guī)則及算法;第5節(jié)通過實驗檢驗方法的效果;第6節(jié)介紹相關(guān)工作;第7節(jié)進行總結(jié).

2 安全C語言驗證器及形狀系統(tǒng)概述

本課題組基于霍爾邏輯和形狀圖邏輯開發(fā)了安全C語言驗證器,實現(xiàn)對于符合安全C語言規(guī)范1的C語言代碼的驗證.驗證器復用Clang/LLVM編譯器的前端,將源程序與用戶標注的斷言轉(zhuǎn)換為抽象語法樹,由驗證條件生成器遍歷抽象語法樹產(chǎn)生程序性質(zhì)相關(guān)的斷言,其中堆指針相關(guān)性質(zhì)的演算與證明操作交由形狀系統(tǒng)執(zhí)行,其余驗證條件交由Z3證明.目前的形狀系統(tǒng)支持5種簡單形狀:單向鏈表、雙向鏈表、循環(huán)單向鏈表、循環(huán)雙向鏈表及二叉樹.易變數(shù)據(jù)結(jié)構(gòu)和形狀之間的關(guān)系,可以類比于靜態(tài)類型語言中變量和類型的關(guān)系.因此,在一定程度上,形狀系統(tǒng)可以視為面向易變數(shù)據(jù)結(jié)構(gòu)的類型系統(tǒng),但兩者又存在本質(zhì)上的不同:

1)形狀系統(tǒng)依賴程序的操作語義,而類型系統(tǒng)則是給出對程序代碼的上下文相關(guān)的約束,不涉及語言的操作語義.

2)對于形狀系統(tǒng)而言,指針指向的易變數(shù)據(jù)結(jié)構(gòu)并不需要時刻符合形狀定義,對于類型系統(tǒng)而言,某個類型的變量只能保存該類型的值.

形狀系統(tǒng)通過圖形形式表示易變數(shù)據(jù)結(jié)構(gòu)的內(nèi)存狀態(tài)以及指針指向關(guān)系,包含6種不同類型的形狀圖節(jié)點[11]:圓形節(jié)點稱為聲明節(jié)點,表示程序中聲明的指針變量;含N的虛線矩形表示NULL節(jié)點,用于描述對應指針為NULL;含D的虛線矩形表示懸空節(jié)點,用于描述指針懸空;實線矩形節(jié)點稱為結(jié)構(gòu)節(jié)點,表示動態(tài)分配的結(jié)構(gòu)體單元;含e和a的灰底實線矩形稱為濃縮節(jié)點,表示指定數(shù)量的結(jié)構(gòu)節(jié)點的折疊,其中e為描述數(shù)量的表達式,a為關(guān)于e的約束斷言;含P的實線矩形稱為謂詞節(jié)點,表示具有指定謂詞性質(zhì)的節(jié)點.通過上述的節(jié)點類型,可以構(gòu)造如圖1(a)中的單向鏈表及圖1(b)中的循環(huán)單向鏈表,分別具有指針關(guān)系p->nxt->…->nxt == NULL和p->nxt->…->nxt == p,其中nxt重復e+1次,聲明節(jié)點的出邊表示指定名稱的指針變量的指向,其它節(jié)點的出邊表示指定名稱的結(jié)構(gòu)體域指針指向.

圖1 易變數(shù)據(jù)結(jié)構(gòu)示例Fig.1 Mutable data structure examples

安全C語言規(guī)范指定需要通過形狀標注對程序中使用的堆指針變量或者結(jié)構(gòu)體類型進行描述,以雙向鏈表為例,聲明如圖2所示.形狀標注通過注釋的形式規(guī)避對于程序語義的影響,相關(guān)標注以“@”開頭,“shape”表示該標注屬于形狀標注,其含義為該結(jié)構(gòu)體的next和prev域共同組成雙向鏈表的主形狀域.出于擴展考慮,形狀系統(tǒng)引入了嵌套形狀域:次要形狀域和共享次要形狀域,例如聲明中標注有“secondary”的域即為次要形狀域.嵌套形狀域用于描述多個簡單形狀的組合,本文將這類形狀簡稱為嵌套形狀.嵌套形狀域存在如下性質(zhì):

1)獨占性:一個易變數(shù)據(jù)結(jié)構(gòu)僅能被一個嵌套形狀域指向;

2)共享性:一個易變數(shù)據(jù)結(jié)構(gòu)中所有節(jié)點的同名共享次要形狀域只能指向同一易變數(shù)據(jù)結(jié)構(gòu)的入口節(jié)點;

3)無環(huán)性:易變數(shù)據(jù)結(jié)構(gòu)不能通過嵌套形狀域構(gòu)成循環(huán)指向.

其中共享性通過賦值演算中的不變式進行保證,不屬于形狀檢查的內(nèi)容.為明確表述,以下先行闡述下文中使用的名詞:

1)前向主形狀域:簡稱前向域,記作forward,是鏈表形狀中濃縮節(jié)點展開的依據(jù).

2)后向主形狀域:簡稱后向域,記作backward,與前向主形狀域共同組成雙向鏈表的主形狀域,單向鏈表和循環(huán)單向鏈表不存在該形狀域.

3)非主形狀域:對于聲明節(jié)點域、次要形狀域、共享次要形狀域的統(tǒng)稱.

4)主結(jié)構(gòu):僅由主形狀域構(gòu)成的易變數(shù)據(jù)結(jié)構(gòu).

5)次結(jié)構(gòu):主結(jié)構(gòu)通過嵌套形狀域指向的易變數(shù)據(jù)結(jié)構(gòu).

1 struct dlist {2 int data;3 struct dlist* next;4 struct dlist* prev;5 struct list* sub;6 }; //@shape prev,next:dlist,primary; //@shape sub:list,secondary;

圖2 雙向鏈表的聲明
Fig.2 Declaration of doubly linked list

3 形狀檢查概述

形狀檢查即檢查指針所指向的易變數(shù)據(jù)結(jié)構(gòu)是否符合該指針聲明所指定的形狀定義的過程.類似于類型系統(tǒng)中關(guān)于類型的相容性檢查,本方法引入3種不同的形狀級別,表示形狀檢查的不同嚴格程度:

1)標準形狀(STANDARD):最嚴格的形狀級別,在易變數(shù)據(jù)結(jié)構(gòu)符合形狀特征(4.2節(jié)詳細描述形狀特征)的情況下,僅允許一個非主形狀域指針指向易變數(shù)據(jù)結(jié)構(gòu),常見于函數(shù)的前形狀圖和后形狀圖;

2)可接受形狀(ACCEPTABLE):除標準形狀中所述,還允許其它非主形狀域指針指向易變數(shù)據(jù)結(jié)構(gòu).常見于易變數(shù)據(jù)結(jié)構(gòu)的各種操作中,例如通過額外的指針遍歷鏈表;

3)待完善形狀(UNACCEPTABLE):除標準形狀和可接受形狀之外,其余的易變數(shù)據(jù)結(jié)構(gòu)均屬于待完善形狀.通常認為該級別的易變數(shù)據(jù)結(jié)構(gòu)是不安全的.

圖3 復雜形狀圖示例Fig.3 Example of complicated shape graph

在較為復雜的程序中,主形狀域和嵌套形狀域共存,多種形狀類別的易變數(shù)據(jù)結(jié)構(gòu)共存的情況十分常見,如圖3所示,這給形狀檢查的規(guī)則設計以及具體的算法實現(xiàn)造成較大麻煩.為此,如下對破壞形狀定義的原因進行了分類匯總:第一,主形狀域的錯誤指向或者嵌套形狀域的指向破壞性質(zhì);第二,節(jié)點類型不滿足約束;第三,非主形狀域指向的節(jié)點不合要求或者主結(jié)構(gòu)和次結(jié)構(gòu)的形狀級別組合沖突.

形狀檢查方法的總體思路為通過預處理分離形狀圖中不同的形狀域,將其轉(zhuǎn)換為便于處理的統(tǒng)一表述,并根據(jù)造成易變數(shù)據(jù)結(jié)構(gòu)不符合形狀定義的原因,通過多個階段實現(xiàn)檢查,每個階段只需著眼于檢查特定的內(nèi)容,以達到控制算法及實現(xiàn)的復雜度的目的.如圖4所示,形狀檢查方法的輸入為含有待檢查易變數(shù)據(jù)結(jié)構(gòu)的形狀圖,輸出為該易變數(shù)據(jù)結(jié)構(gòu)的形狀級別,將其與預期的級別進行比較,即可判斷該易變數(shù)據(jù)結(jié)構(gòu)是否符合形狀定義.形狀檢查方法分為形狀分割、形狀分析和形狀推斷三個階段,它們的作用分別為:

1)形狀分割:對形狀圖進行預處理,將其中的主結(jié)構(gòu)轉(zhuǎn)換成形狀元信息,并生成節(jié)點-元信息映射表供后續(xù)分析使用;

2)形狀分析:依次通過形狀間分析和形狀內(nèi)分析,分析由嵌套形狀域和主形狀域產(chǎn)生的指針指向關(guān)系以及節(jié)點位置對節(jié)點類型的約束,從而預先判斷部分屬于待完善形狀的易變數(shù)據(jù)結(jié)構(gòu),將結(jié)果保存于結(jié)果表中;

3)形狀推斷:根據(jù)非主形狀域指針的指向推斷主結(jié)構(gòu)的形狀級別并結(jié)合其所有次結(jié)構(gòu)的形狀級別最終推斷易變數(shù)據(jù)結(jié)構(gòu)整體的形狀級別.

圖4 形狀檢查方法總體流程Fig.4 Overall flow of shape checking approach

根據(jù)形狀圖邏輯理論,用戶可以通過提供期望的形狀圖,憑借形狀圖的蘊含證明,檢查易變數(shù)據(jù)結(jié)構(gòu)是否符合形狀定義.但在實際系統(tǒng)實現(xiàn)中,這類方式存在以下問題:其一,僅憑形狀圖斷言的構(gòu)造語義無法保證形狀圖構(gòu)造的正確性,即無法保證蘊含式后件中的易變數(shù)據(jù)結(jié)構(gòu)一定符合形狀定義,因為用戶亦可能會錯誤描述斷言;其二,蘊含證明方法需要用戶通過斷言描述程序狀態(tài),繁瑣且容易造成疏漏;其三,蘊含證明僅在幾個固定的驗證點進行,對于稍復雜的程序,不夠靈活,且不利于盡早發(fā)現(xiàn)易變數(shù)據(jù)結(jié)構(gòu)中的問題.

check ∷=check_shapecheck_selection check_selection ∷=shape_levelid(,id)*shape_level ∷=standard|acceptable

圖5 形狀檢查文法
Fig.5 Grammar of shape checking

針對上述問題,本工作分別引入了隱式形狀檢查與顯式形狀檢查,它們的實現(xiàn)均基于形狀檢查方法,區(qū)別在于觸發(fā)檢查操作的方式.隱式形狀檢查由系統(tǒng)在重要驗證點進行自動檢查,這類驗證點包括函數(shù)入口、函數(shù)出口、循環(huán)入口、函數(shù)調(diào)用點等,主要用于確保新構(gòu)造形狀圖中的易變數(shù)據(jù)結(jié)構(gòu)符合定義,它們通常就是蘊含式后件中的形狀圖,除非用戶特別指定,默認情況下確保所有易變數(shù)據(jù)結(jié)構(gòu)至少為可接受形狀.顯式形狀檢查允許用戶通過圖5中定義的文法,在任意程序點對指定范圍的易變數(shù)據(jù)結(jié)構(gòu)進行形狀檢查,例如“check_shape standard p,q”表示檢查指針p和q所指向的易變數(shù)據(jù)結(jié)構(gòu)是否屬于標準形狀.相較于通過斷言描述程序狀態(tài),然后依賴蘊含證明的方式檢查易變數(shù)據(jù)結(jié)構(gòu)是否符合形狀定義,顯式形狀檢查更具易用性和靈活性,且能夠盡早發(fā)現(xiàn)易變數(shù)據(jù)結(jié)構(gòu)的問題.

4 形狀檢查的具體方法分析

4.1 形狀分割

形狀分割指的是從形狀圖中分離主結(jié)構(gòu),并將其轉(zhuǎn)換成形狀元信息表述的過程.例如圖3經(jīng)過形狀分割處理后,等效可得圖中所標注的主結(jié)構(gòu)A～E,但形狀分割操作并不會丟棄由非主形狀域表述的指針關(guān)系,而是將它們保存于形狀元信息中.形狀元信息表現(xiàn)為四元組,Type表示易變數(shù)據(jù)結(jié)構(gòu)所聲明的形狀種類,Entry表示易變數(shù)據(jù)結(jié)構(gòu)的入口節(jié)點集合,Src表示通過非主形狀域指向該易變數(shù)據(jù)結(jié)構(gòu)的節(jié)點集合,Dst表示當前易變數(shù)據(jù)結(jié)構(gòu)的非主形狀域指向的節(jié)點集合.根據(jù)嵌套形狀域的共享性和獨占性,Src僅保留共享次要形狀域源節(jié)點中的入口節(jié)點.為便于后續(xù)分析工作根據(jù)節(jié)點獲取對應的形狀元信息,形狀分割操作會導出節(jié)點-形狀元信息映射表(以下簡稱節(jié)點映射表).

Input:Shape meta tuple T,shape node N,mapping from node to shape meta tuple M1 T.Type ← Get ShapeType(N);2 Q←CreateQueue();3 Enqueue(Q,N);4 while IsEmpty(Q)==False do5 cur←Dequeue(Q);6 if HasKey(M,cur)==Ture then7 continue;8 end if9 M[cur]←T;10 if IsEntryNode(cur)==Ture then11 Insert(T.Entry,cur);12 end if13 if HasNonprimaryField(cur)==True then14 Insert(T.Src,peer nodes of non-primarypoint-in fields);15 Insert(T.Dst,peer nodes of non-primarypoint-out fields);16 end if17 Enqueue(Q,peer nodes of the primary fields of cur);18 end while19 if Size(T.Entry)==0 then20 Insert(T.Entry,N);21 end if

圖6 形狀元信息填寫算法
Fig.6 Algorithm of filling shape meta information

入口節(jié)點Entry作為后續(xù)階段中遍歷各易變數(shù)據(jù)結(jié)構(gòu)的入口,是確保通過一次遍歷覆蓋易變數(shù)據(jù)結(jié)構(gòu)所有節(jié)點的關(guān)鍵.對于所有形狀而言,由非主形狀域直接指向的NULL節(jié)點均可作為入口節(jié)點,其它情況下,不同形狀種類的入口節(jié)點的判定存在區(qū)別:對于單向鏈表和二叉樹,入口節(jié)點為主形狀域入度為0的節(jié)點;對于雙向鏈表,入口節(jié)點為前向主形狀域入度為0的節(jié)點;對于循環(huán)單向鏈表和循環(huán)雙向鏈表,入口節(jié)點優(yōu)先選擇嵌套形狀域指向的節(jié)點,否則,任意聲明節(jié)點指向的節(jié)點均可.需要特別說明的是,不符合形狀定義的易變數(shù)據(jù)結(jié)構(gòu)可能不存在或者存在多個入口節(jié)點.

顯式形狀檢查通過標注指針變量的形式,約束待檢查易變數(shù)據(jù)結(jié)構(gòu)的范圍,而隱式形狀檢查則默認檢查所有易變數(shù)據(jù)結(jié)構(gòu),可認為其標注了所有指針變量.由于無法排除存在多個指針變量指向相同易變數(shù)據(jù)結(jié)構(gòu)的可能性,因此它們僅可作為遍歷易變數(shù)據(jù)結(jié)構(gòu)的參考.據(jù)此,形狀分割算法引入待遍歷節(jié)點集合,初始即為標注中指針所指向的節(jié)點集合,依次根據(jù)其中的節(jié)點提取形狀元信息.

形狀元信息填充算法的本質(zhì)為對由主形狀域和節(jié)點構(gòu)成的無向圖進行廣度優(yōu)先遍歷,并在遍歷過程中完成對于形狀元信息的填寫.如圖6所示,算法首先使用GetShapeType函數(shù)獲取節(jié)點N所聲明的形狀類別,并保存到元信息的Type中.然后創(chuàng)建一個隊列,將參數(shù)N對應的節(jié)點入隊,第4行至第18行的循環(huán)為廣度優(yōu)先遍歷的迭代過程,該循環(huán)將不斷迭代直至隊列為空.在循環(huán)體中,每次迭代均會從隊首取出一個節(jié)點,判斷該節(jié)點是否已訪問,若映射表M中已經(jīng)含有關(guān)于節(jié)點的鍵,則說明該節(jié)點為已訪問節(jié)點,需要略過本次迭代,否則將節(jié)點到形狀元信息的映射存入映射表M,標記該節(jié)點已訪問.第10行至第12行的分支語句通過IsEntryNode函數(shù)判斷當前節(jié)點是否為入口節(jié)點,若是,則將其作為元信息中的Entry.第13行至第16行的分支語句通過HasNonPrimaryField函數(shù)判斷當前節(jié)點是否含有非主形狀域,若存在,則通過第14行與第15行的語句分別提取非主形狀域中的起始節(jié)點集合和目標節(jié)點集合,將它們分別存入元信息中的Src和Dst集合.在循環(huán)體的最后,需要通過主形狀域提取下一節(jié)點,并將其入隊.若在算法的遍歷過程中,沒有找到符合要求的入口節(jié)點,則默認將輸入的節(jié)點N作為元信息中的Entry,由第19行至第21行的語句實現(xiàn),形狀分析階段能夠識別這種情況,并作出處理.

為覆蓋所有僅含嵌套形狀域指向的主結(jié)構(gòu),在每次填充元信息之后,需要額外將嵌套形狀域指向的節(jié)點加入待遍歷集合,如此即可實現(xiàn)等價于標注中存在指針變量直接指向該主結(jié)構(gòu)的效果.

4.2 形狀分析

形狀分析是通過分析不同形狀域指針的指向以及節(jié)點的類型,實現(xiàn)對待完善形狀預先判斷的操作,包含2個子階段:形狀間分析和形狀內(nèi)分析.

形狀間分析是通過分析主結(jié)構(gòu)之間由嵌套形狀域構(gòu)成的連接關(guān)系,確定對應易變數(shù)據(jù)結(jié)構(gòu)是否屬于待完善形狀的操作.根據(jù)形狀分割階段導出的形狀元信息以及節(jié)點映射表,可以構(gòu)造有向圖G(V,E),其中V為由形狀元信息表示的主結(jié)構(gòu)集合,E為主結(jié)構(gòu)之間的嵌套形狀域連接關(guān)系.

通過將主結(jié)構(gòu)抽象成節(jié)點的形式,可以將圖3中的形狀圖轉(zhuǎn)換成圖7中所示的有向圖,其中由A指向B的邊即表示主結(jié)構(gòu)A存在嵌套形狀域指向主結(jié)構(gòu)B.根據(jù)嵌套形狀域的獨占性和無環(huán)性要求,可知符合定義的有向圖是由多叉樹構(gòu)成的森林,這樣就可將形狀間分析轉(zhuǎn)換為判斷有向圖是否為森林的問題.

圖7 有向圖示例Fig.7 Example of directed graph

如圖8所示,算法根據(jù)SplitConnectedGraph函數(shù)完成對于依賴圖的連通分量的劃分,并保存于集合S中.然后通過第2行至第8行的循環(huán)遍歷每個連通分量,通過IsPolyTree函數(shù)判斷當前連通分量是否為一顆多叉樹,若不是,則意味著易變數(shù)據(jù)結(jié)構(gòu)無法通過形狀間分析,需要通過第4行至第6行的循環(huán)遍歷連通分量的每個頂點,并在結(jié)果表R中將它們所表示的易變數(shù)據(jù)結(jié)構(gòu)標記為待完善形狀,其中GetVertexSet函數(shù)用于獲取圖的頂點集.

Input:Shape dependency graph G and shape level table R1 S←SplitConnectedGraph(G);2 foreach g in S do3 if IsPolyTree(g)==False then4 foreach n in GetVertexSet(g)do5 R[n]←UNACCEPTABLE;6 end foreach7 end if8 end foreach9 return L;

圖8 形狀間分析算法
Fig.8 Algorithm of inter-shape analysis

形狀內(nèi)分析是通過分析主結(jié)構(gòu)的形狀特征,結(jié)合相應規(guī)則確定其是否符合形狀定義的過程.雖然形狀內(nèi)分析僅關(guān)注主形狀域,但是由于指針的靈活性,依舊存在大量不符合形狀定義的情況.為正確辨別所有不合形狀定義的易變數(shù)據(jù)結(jié)構(gòu),本方案分別就5種簡單形狀提出了形狀特征約束規(guī)則,若易變數(shù)據(jù)結(jié)構(gòu)不符合約束規(guī)則,即可斷定其屬于待完善形狀.根據(jù)關(guān)注點的不同,可將約束規(guī)則劃分為3類:

1)關(guān)于節(jié)點在易變數(shù)據(jù)結(jié)構(gòu)中所處位置對于節(jié)點類型的約束,如謂詞節(jié)點僅可作為二叉樹的葉子節(jié)點等;

2)關(guān)于節(jié)點主形狀域入度的約束,用于判斷絕大多數(shù)的異常指針指向關(guān)系,如單向鏈表中的環(huán)等;

3)關(guān)于節(jié)點間指針關(guān)系的約束,如用于描述雙向鏈表和循環(huán)雙向鏈表中相鄰節(jié)點間指針的雙向指向關(guān)系.

為簡化各形狀的表述,這里引入單向鏈表表段和雙向鏈表表段,并在此基礎(chǔ)上提供5種簡單形狀的謂詞定義,如圖9所示,其中p表示指向入口節(jié)點的指針,head和tail表示指向表頭和表尾節(jié)點的指針.以上謂詞定義均基于初始語義,確保從定義推出的任意兩個有效指針都不相等.

根據(jù)形狀的謂詞定義,除入口節(jié)點即為NULL節(jié)點的情況之外,可以導出如下形狀特征(入度指代主形狀域入度,前向入度指代前向主形狀域入度,后向入度指代后向主形狀域入度):

1)單向鏈表表段(list_seg):所有節(jié)點均為結(jié)構(gòu)節(jié)點或濃縮節(jié)點,除表頭節(jié)點外,其余節(jié)點的入度為1;

2)雙向鏈表表段(dlist_seg):所有節(jié)點均為結(jié)構(gòu)節(jié)點或濃縮節(jié)點,相鄰節(jié)點間的指針存在相互指向關(guān)系,且除表頭和表尾節(jié)點外,其余節(jié)點的入度為2;

3)單向鏈表(list):在表段基礎(chǔ)上,表頭節(jié)點的入度為0,表尾節(jié)點的主形狀域指向NULL節(jié)點;

4)循環(huán)單向鏈表(c_list):在表段基礎(chǔ)上,表頭節(jié)點的入度為1,表尾節(jié)點的主形狀域指向表頭節(jié)點;

5)雙向鏈表(dlist):在表段基礎(chǔ)上,表頭節(jié)點的后向主形狀域和表尾節(jié)點的前向主形狀域均指向NULL節(jié)點,除非表頭和表尾為同一節(jié)點,使其入度為0,否則它們的入度均為1,其中表頭節(jié)點被后向主形狀域指向,表尾節(jié)點被前向主形狀域指向;

6)循環(huán)雙向鏈表(c_dlist):在表段基礎(chǔ)上,表頭和表尾節(jié)點間存在指針的雙向指向關(guān)系,且其入度均為2;

7)二叉樹(tree):根節(jié)點的入度為0,其余節(jié)點的入度為1,且葉子節(jié)點為謂詞節(jié)點或NULL節(jié)點,其余節(jié)點為結(jié)構(gòu)節(jié)點或濃縮節(jié)點.

inductive list_seg(head,tail)= head=tail∪head≠tail∩ list_seg(head.forward,tail)inductive dlist_seg(head,tail)= head=tail∪head≠tail∩head.forward.backward =head∩dlist_seg(head.forward,tail)predicate list(p)= p=null∪?q.list+seg(p,q)∩q.forward=nullpredicate c_list(p)= p=null∪?q.list_seg(p,q)∩q.forward=ppredicate dlist(p)= p=null∪?q.dlist_seg(p,q)∩q.forward= null∩p.backward=nullpredicate c_dlist(p)= p=null∪?q.dlist_seg(p,q)∩q.forward= p∩p.backward=qinductive tree(p)= p=null∪tree(p.l)∩tree(p.r)

圖9 形狀的謂詞定義
Fig.9 Predicate definition of shape

形狀內(nèi)分析的挑戰(zhàn)在于需要處理的形狀種類較多,不同形狀擁有各自的形狀特征,適宜的遍歷方式亦不盡相同,為降低算法實現(xiàn)層面上的復雜度,形狀內(nèi)分析算法將算法分為兩大部分:形狀種類無關(guān)的遍歷框架和位置相關(guān)的形狀約束分析算法.如圖10所示,算法首先通過GetNodeKind函數(shù)判斷形狀入口節(jié)點的類別,若為NULL節(jié)點(NODE_NULL),則直接通過形狀內(nèi)分析,因為所有形狀類別的易變數(shù)據(jù)結(jié)構(gòu)均可僅由一個NULL節(jié)點構(gòu)成.之后,算法通過CheckHeadNode、CheckTailNode和CheckNormalNode函數(shù)進行位置相關(guān)的約束檢查,它們是上述形狀特征規(guī)則的實現(xiàn),將節(jié)點的檢查分為3種類型:對于鏈表形狀,它們分別用于檢查表頭節(jié)點、表尾節(jié)點和其它節(jié)點,對于二叉樹,CheckHeadNode用于檢查根節(jié)點,CheckNormalNode用于檢查其余節(jié)點,CheckTailNode沒有意義,直接返回True,表示略過.算法的第10行至第16行為關(guān)于主結(jié)構(gòu)節(jié)點的廣度優(yōu)先遍歷,該循環(huán)的終止條件通過IsEnd函數(shù)實現(xiàn)判斷,循環(huán)體每次從隊首取出一個節(jié)點,使用CheckNormalNode進行檢查,若通過則使用EnqueueNextNode函數(shù)根據(jù)形狀類別獲取相鄰節(jié)點入隊,對于鏈表,該相鄰節(jié)點為前向主形狀域指向的節(jié)點,對于二叉樹則為當前節(jié)點的子節(jié)點,以此完成對于不同形狀類別的主結(jié)構(gòu)的統(tǒng)一遍歷.

Input:Shape entry node E and shape kind TOutput:If the ADT can pass the analysis1 if GetNodeKind(E)==NODE_NULLthen2 return Ture;3 end if4 if CheckHeadNode(E.T)==Falsethen5 return False;6 end if7 Q←QueueCreate();8 EnqueueNextNode(Q,cur,T);9 cur←E;10 while IsEnd(cur,E,Q,T)==False do11 cur←Dequeue(Q);12 if CheckNormalNode(cur,T)==False then13 return False;14 end if15 EnqueueNextNode(Q,cur,T);16 end while17 if CheckTailNode(cur,E,T)==False then18 return False;19 end if20 return True;

圖10 形狀內(nèi)分析算法
Fig.10 Algorithm of intra-shape analysis

算法通過IsEnd函數(shù)確定遍歷是否終止,對于不同的形狀種類,該函數(shù)的判斷如下:對于二叉樹,返回隊列Q是否為空;對于單向鏈表或雙向鏈表,返回前向主形狀域指向的節(jié)點是否為NULL節(jié)點;對于循環(huán)單向鏈表或循環(huán)雙向鏈表,返回前向主形狀域指向的節(jié)點是否為入口節(jié)點.

4.3 形狀推斷

形狀分析階段預先判斷了部分屬于待完善形狀的易變數(shù)據(jù)結(jié)構(gòu),對于通過形狀分析的易變數(shù)據(jù)結(jié)構(gòu),形狀推斷會進一步分析非主形狀域指針的指向,得到主結(jié)構(gòu)和所有次結(jié)構(gòu)的形狀級別,并根據(jù)內(nèi)置規(guī)則,實現(xiàn)易變數(shù)據(jù)結(jié)構(gòu)所屬形狀級別的最終推斷.如下給出3種形狀級別的推斷規(guī)則:

1)標準形狀:僅存在1個非主形狀域指向主結(jié)構(gòu)的入口節(jié)點,不存在次結(jié)構(gòu),或者所有次結(jié)構(gòu)均屬于標準形狀;

2)可接受形狀:存在1個及以上的非主形狀域指向主結(jié)構(gòu)節(jié)點,僅存在聲明節(jié)點域指向除入口節(jié)點以外的節(jié)點,不存在次結(jié)構(gòu),或者對于具有非主形狀域指向的節(jié)點,其所指向的次結(jié)構(gòu)屬于標準形狀或可接受形狀,其余節(jié)點指向的次結(jié)構(gòu)屬于標準形狀;

3)待完善形狀:存在1個以上入口節(jié)點的易變數(shù)據(jù)結(jié)構(gòu),無法通過形狀分析的易變數(shù)據(jù)結(jié)構(gòu),以及所有上述定義之外的易變數(shù)據(jù)結(jié)構(gòu).

形狀推斷規(guī)則指定,易變數(shù)據(jù)結(jié)構(gòu)的形狀級別由其主結(jié)構(gòu)和所有次結(jié)構(gòu)的形狀級別共同決定.結(jié)合形狀間分析階段得到的結(jié)論,對于嵌套形狀,各主結(jié)構(gòu)通過嵌套形狀域構(gòu)成多叉樹,也就是說,推斷多叉樹中某個節(jié)點的形狀級別,即為對以該節(jié)點為根節(jié)點的子樹的遞歸分析操作,分析起始于根節(jié)點,終止于形狀級別已知的節(jié)點或不含次結(jié)構(gòu)的易變數(shù)據(jù)結(jié)構(gòu),亦即葉子節(jié)點.形狀間分析提前判定具環(huán)連通分量的形狀級別,規(guī)避了遞歸分析算法不終止的情況.

1 Function DeduceShape(S,R) Input:Shape meta tuple S and shape level table R Output:Shape level2 if R[S]!=null then3 return R[S];4 end if5 L←ApplyRule(S);6 R[S]←L;7 if L==UNACCEPTABLE then8 return R[S];9 end if10 foreach s in GetSubStructure(S) do11 LS←DeduceShape(s);12 if L== STANDARD and LS== ACCEPTABLE then13 R[S]←ACCEPTABLE;14 L←ACCEPTABLE;15 end if16 if LS==UNACCEPTABLE or(L== ACCEPTABLE and LS==ACCEPTABLE and HasNonPrimaryPointInField(the node which points to s)==False)then17 R[S]←UNACCEPTABLE;18 break;19 end if20 end foreach21 return R[S];

圖11 形狀推斷算法
Fig.11 Algorithm of shape deduction

在圖11的算法中,首先通過第2行至第4行的分支語句判斷結(jié)果表R中是否已經(jīng)存在指定形狀元信息S對應的形狀級別,若存在則直接返回該結(jié)果.之后,通過ApplyRule函數(shù)推斷S所對應的主結(jié)構(gòu)的形狀級別,如第7行至第9行所示,若主結(jié)構(gòu)的形狀級別就是待完善形狀,則無需繼續(xù)推斷其次結(jié)構(gòu)的形狀級別,根據(jù)推斷規(guī)則,無論次結(jié)構(gòu)的形狀級別為何,均不會改變該情況下主結(jié)構(gòu)的形狀級別.對于形狀級別不為待完善形狀的情況,則需要通過第10行至第20行所示的循環(huán)語句依次遍歷其次結(jié)構(gòu),其中函數(shù)GetSubStructure用于根據(jù)特定形狀元信息獲取其次結(jié)構(gòu),循環(huán)體首先通過遞歸調(diào)用函數(shù)DeduceShape獲取次結(jié)構(gòu)的形狀級別,然后結(jié)合次結(jié)構(gòu)的形狀級別實現(xiàn)對于最終形狀級別的進一步修正,并將結(jié)果保存于結(jié)果表R之中,相關(guān)內(nèi)容梳理如下,它們是推斷規(guī)則的簡化實現(xiàn):若主結(jié)構(gòu)為標準形狀,且存在次結(jié)構(gòu)為可接受形狀,則需要將最終形狀級別修改為可接受形狀,實現(xiàn)如第12行至第15行的分支語句所示;若次結(jié)構(gòu)為待完善形狀或者主結(jié)構(gòu)與次結(jié)構(gòu)均為可接受形狀,但指向該次結(jié)構(gòu)的節(jié)點沒有被非主形狀域指向,則需要將最終形狀級別修改為待完善形狀,實現(xiàn)如第16行至第19行所示,其中HasNonPrimaryPointInField函數(shù)用于判斷是否存在非主形狀域指向目標節(jié)點.

5 實例驗證

本研究在安全C語言驗證器的形狀系統(tǒng)中,實現(xiàn)了文中所述的形狀檢查方法.為檢查文中算法和相關(guān)實現(xiàn)的正確性以及真實系統(tǒng)環(huán)境下的效率,我們設計了不同形狀級別預期的易變數(shù)據(jù)結(jié)構(gòu)實驗用例,其組成如表1所示,按照由簡至繁的順序,這些用例可以分為:簡單形狀、嵌套形狀以及復雜形狀,其中復雜形狀用例表示含有多個不通過嵌套形狀域相連的易變數(shù)據(jù)結(jié)構(gòu)的形狀圖,如圖3所示.本實驗通過上述用例確保其能夠覆蓋形狀檢查方法的各處理階段以及其中的判定規(guī)則.

表1 實驗用例組成
Table 1 Composition of experimental cases

形狀級別簡單形狀嵌套形狀復雜形狀標準形狀1042可接受形狀1042待完善形狀2482

實驗在如下平臺中進行:Windows 10 PC,Intel Core i7-6700 3.4GHz CPU和8GB DDR4內(nèi)存,形狀檢查方法正確識別了所有用例的形狀級別,結(jié)果如表2所示.

表2 實驗結(jié)果
Table 2 Result of experiment

形狀級別例子數(shù)量最短耗時最長耗時標準形狀16235us564us可接受形狀16246us694us待完善形狀34164us644us

根據(jù)實驗結(jié)果,不難發(fā)現(xiàn)在最短耗時場景下,待完善形狀用例集的耗時最少,標準形狀用例集次之,可接受形狀用例集的最長.根據(jù)形狀檢查方法的設計,可以進行簡要分析.屬于標準形狀和可接受形狀的易變數(shù)據(jù)結(jié)構(gòu)均需要經(jīng)過3個階段的完整檢查方能得到最終形狀級別,而嵌套形狀域指向不符合定義的易變數(shù)據(jù)結(jié)構(gòu)在最快情況下,于形狀間分析階段即可得到最終結(jié)論,使得后續(xù)階段直接返回該結(jié)果,而無需進一步的處理,這使得該類用例的最短耗時少于其它用例,而在形狀推斷階段才得到待完善形狀結(jié)論,則是該類用例的最長耗時場景,這與可接受形狀用例的最長耗時差別不大.導致標準形狀用例集處理耗時少于可接受形狀用例集的原因在于,無論易變數(shù)據(jù)結(jié)構(gòu)是否含有嵌套形狀域,在相同形狀的前提下,屬于標準形狀的易變數(shù)據(jù)結(jié)構(gòu)普遍比屬于可接受形狀的易變數(shù)據(jù)結(jié)構(gòu)簡單,具體體現(xiàn)在:其一,節(jié)點數(shù)量更少;其二,包含更少的形狀域.這些區(qū)別主要影響形狀分割以及形狀內(nèi)分析階段的耗時.

此外,為衡量引入隱式形狀檢查后,對形狀系統(tǒng)主要驗證點蘊含操作的影響,我們還對當前系統(tǒng)的蘊含證明操作的耗時進行了采樣,對于較為簡單的易變數(shù)據(jù)結(jié)構(gòu)而言,如單向鏈表,一次蘊含操作的平均耗時在30000us以上,該耗時取決于斷言的復雜度以及Z3的證明效率,相較表2中的最長處理耗時而言,我們認為形狀檢查操作帶來的時間開銷幾乎可以忽略不計.

6 相關(guān)工作

DRYAD[12]是分離邏輯[13]的一種方言,它提供了更加自然的方式描述堆塊,并通過遞歸定義的方式描述易變數(shù)據(jù)結(jié)構(gòu),規(guī)避顯式的量詞使用,使得程序的自動化證明成為可能.該工作通過蘊含證明的方式完成對于易變數(shù)據(jù)結(jié)構(gòu)的驗證,本質(zhì)上該方式將檢查工作交由斷言提供者完成,系統(tǒng)僅需要確保證明的正確性即可,可以保持系統(tǒng)的精簡,且關(guān)于易變數(shù)據(jù)結(jié)構(gòu)的檢查亦更加自由,但也增加了斷言描述的難度,對使用者要求更高,且檢查僅在含有蘊含證明的大驗證點進行,不利于及時發(fā)現(xiàn)易變數(shù)據(jù)結(jié)構(gòu)中的問題.

文獻[14]提出了針對命令式的數(shù)據(jù)結(jié)構(gòu)的逐步精化驗證方法,通過自頂向下的方式,將復雜數(shù)據(jù)結(jié)構(gòu)拆分為算法思想與底層實現(xiàn)分別驗證以簡化證明過程,同時允許復用已驗證的基本數(shù)據(jù)結(jié)構(gòu)構(gòu)造復雜數(shù)據(jù)結(jié)構(gòu),并將其作為算法驗證的基礎(chǔ).該工作的亮點在于支持更加復雜的數(shù)據(jù)結(jié)構(gòu)的證明,并通過相關(guān)工具實現(xiàn)使得模塊化地構(gòu)建經(jīng)過證明的復雜數(shù)據(jù)結(jié)構(gòu)成為可能.該工作使用分離邏輯處理堆內(nèi)存的操作,需要使用者自行描述易變數(shù)據(jù)結(jié)構(gòu)的定義,而系統(tǒng)則根據(jù)定義通過蘊含證明的方式完成數(shù)據(jù)結(jié)構(gòu)的檢查,對于使用者的要求較高,在復雜程序中同樣難以及時發(fā)現(xiàn)問題.

PEDANTIC[15]是一款基于分離邏輯的可擴展交互式證明框架,基于Coq實現(xiàn),能夠用于驗證含復雜動態(tài)數(shù)據(jù)結(jié)構(gòu)操作的類C語言程序.該工作的特色在于其提供了一系列證明策略,盡可能實現(xiàn)斷言正向演算的自動化,并在演算后簡化斷言的表述,針對易變數(shù)據(jù)結(jié)構(gòu),該工作的最大亮點在于其提出了跨結(jié)構(gòu)不變式的概念,證明由不同類型的數(shù)據(jù)結(jié)構(gòu)組成的復雜數(shù)據(jù)結(jié)構(gòu).與其它基于Coq實現(xiàn)的交互式證明框架一樣,該框架同樣無法徹底實現(xiàn)自動化證明,需要使用者手動證明部分定理,且對于易變數(shù)據(jù)結(jié)構(gòu)是否符合定義的檢查同樣依賴蘊含證明,局限性和上述工作相同.

7 總 結(jié)

形狀系統(tǒng)限制了程序中可以構(gòu)造和使用的易變數(shù)據(jù)結(jié)構(gòu)的種類,規(guī)避任意構(gòu)造和操作易變數(shù)據(jù)結(jié)構(gòu)給程序驗證帶來的困難,然而由于易變數(shù)據(jù)結(jié)構(gòu)操作的特點,無法時刻確保其符合形狀定義,為形狀系統(tǒng)的演算帶來了隱患.本工作提出了一種通過多階段處理的方式檢查易變數(shù)據(jù)結(jié)構(gòu)是否符合形狀定義的方法,它適用于含有易變數(shù)據(jù)結(jié)構(gòu)操作的C程序的檢查,能夠支持單向鏈表、雙向鏈表、循環(huán)單向鏈表、循環(huán)雙向鏈表、二叉樹以及這些數(shù)據(jù)結(jié)構(gòu)的組合.分階段檢查的思想,簡化了各階段的關(guān)注點,從而降低相關(guān)檢查算法與實現(xiàn)的復雜度.而提供顯式形狀檢查和隱式形狀檢查,則免除使用者通過繁瑣的斷言描述程序狀態(tài),使得形狀檢查能夠在任意程序點進行,更具靈活性和易用性.

形狀檢查方法同樣存在一些局限性:第一,對于復雜數(shù)據(jù)結(jié)構(gòu)的支持有限,例如B樹、跳表等數(shù)據(jù)結(jié)構(gòu);第二,每次形狀檢查均需要完整地執(zhí)行3個階段的操作,在很多情況下是不必要的,例如在相鄰顯式形狀檢查之間的程序語句并不修改指針域,則此時兩次檢查得到的形狀級別并不會改變.

針對形狀檢查方法存在的局限性,進一步的研究如下:第一,改進形狀系統(tǒng)對于形狀的表述方式,并增加相應的判定規(guī)則,使得系統(tǒng)整體可以驗證和檢查更多形狀種類的易變數(shù)據(jù)結(jié)構(gòu);第二,研究形狀檢查的增量檢查方法,在增量檢查方法中,形狀檢查操作隨程序語句的演算進行,在檢查點僅需直接將實際的形狀級別與預期的形狀級別進行對比即可,可以規(guī)避無意義的操作,并且將檢查的時間開銷分攤.