安全C語言驗證器中形狀系統的形狀檢查方法

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

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

1 引 言

1.1 研究背景

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

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

1.2 研究目的

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

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

1.3 本文工作

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

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

2 安全C語言驗證器及形狀系統概述

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

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

2)對于形狀系統而言,指針指向的易變數據結構并不需要時刻符合形狀定義,對于類型系統而言,某個類型的變量只能保存該類型的值.

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

圖1 易變數據結構示例Fig.1 Mutable data structure examples

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

1)獨占性:一個易變數據結構僅能被一個嵌套形狀域指向;

2)共享性:一個易變數據結構中所有節點的同名共享次要形狀域只能指向同一易變數據結構的入口節點;

3)無環性:易變數據結構不能通過嵌套形狀域構成循環指向.

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

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

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

3)非主形狀域:對于聲明節點域、次要形狀域、共享次要形狀域的統稱.

4)主結構:僅由主形狀域構成的易變數據結構.

5)次結構:主結構通過嵌套形狀域指向的易變數據結構.

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 形狀檢查概述

形狀檢查即檢查指針所指向的易變數據結構是否符合該指針聲明所指定的形狀定義的過程.類似于類型系統中關于類型的相容性檢查,本方法引入3種不同的形狀級別,表示形狀檢查的不同嚴格程度:

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

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

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

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

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

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

1)形狀分割:對形狀圖進行預處理,將其中的主結構轉換成形狀元信息,并生成節點-元信息映射表供后續分析使用;

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

3)形狀推斷:根據非主形狀域指針的指向推斷主結構的形狀級別并結合其所有次結構的形狀級別最終推斷易變數據結構整體的形狀級別.

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

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

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

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

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

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

4.1 形狀分割

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

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

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

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

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

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

4.2 形狀分析

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

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

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

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

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

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

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

1)關于節點在易變數據結構中所處位置對于節點類型的約束,如謂詞節點僅可作為二叉樹的葉子節點等;

2)關于節點主形狀域入度的約束,用于判斷絕大多數的異常指針指向關系,如單向鏈表中的環等;

3)關于節點間指針關系的約束,如用于描述雙向鏈表和循環雙向鏈表中相鄰節點間指針的雙向指向關系.

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

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

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

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

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

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

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

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

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

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

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

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 形狀內分析算法
Fig.10 Algorithm of intra-shape analysis

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

4.3 形狀推斷

形狀分析階段預先判斷了部分屬于待完善形狀的易變數據結構,對于通過形狀分析的易變數據結構,形狀推斷會進一步分析非主形狀域指針的指向,得到主結構和所有次結構的形狀級別,并根據內置規則,實現易變數據結構所屬形狀級別的最終推斷.如下給出3種形狀級別的推斷規則:

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

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

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

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

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

5 實例驗證

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

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

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

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

表2 實驗結果
Table 2 Result of experiment

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

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

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

6 相關工作

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

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

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

7 總 結

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

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

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