C程序分析工具中程序切片的設計與實現

蔣 剛,李兆鵬

1(中國科學技術大學 計算機科學與技術學院,合肥 230026) 2(中國科學技術大學 先進技術研究院 中國科大—國創高可信軟件工程中心,合肥 230027)

1 引 言

隨著當今計算機技術的飛速發展,在航空航天、醫療等安全攸關領域高可信軟件的需求與日俱增,提高軟件的可靠性和安全性是軟件開發中所追求的目標之一,目前確保軟件安全質量的方法有程序驗證,動態測試和靜態分析.程序驗證作為保證程序正確性的嚴格手段,通過形式化方法如霍爾邏輯[1]、分離邏輯[2]等對程序中的各種性質給出嚴格的數學證明,從而保證程序的高可靠性,程序驗證目前還未實現完全的自動化證明,需要大量的人工輔助證明,因此未能在工業界得到廣泛應用.程序動態測試在實踐中具有廣泛的應用,它提供了程序運行時的檢查,但是其精確性和覆蓋率依賴于給定的測試集,缺少良好的測試集,將導致高漏報率和低覆蓋率,而且運行時的檢查成本和風險相對較高.靜態分析技術不需要運行程序,是對代碼進行分析,與形式化驗證相比,靜態分析能自動分析程序中的相關信息,與動態測試相比,靜態分析可以以較低的成本更早地發現程序中的缺陷.

目前較為成熟的靜態分析技術有模型檢測[3]、抽象解釋[4]、數據流分析[5]和符號執行[6].其中符號執行被廣泛用于測試例的自動生成[7],它的主要思想是對代碼中變量的取值進行符號化,使用一定的執行策略,以帶約束的符號值代替程序變量運行時的具體值,較為精確地模擬程序的執行過程,從而達到分析的高覆蓋率,得到較精確的分析結果.符號執行技術對路徑敏感,模擬執行程序時會嘗試所有可能的路徑,因此比動態測試的覆蓋率高.另一方面,符號執行隨著程序中控制結構的增加,所需執行的狀態數目呈指數級增長,會帶來路徑爆炸問題,這嚴重制約了使用符號執行技術的分析工具的可伸縮性.

隨著軟件的規模越來越大,要使符號執行技術依然保持低漏報率、低誤報率并且具有良好的性能和可伸縮性成為一大挑戰.目前筆者所在的課題組已實現一個基于開源編譯框架LLVM[8]的符號執行分析工具ShapeChecker[9],它的總體框架如圖1所示.

ShapeChecker是一個C程序靜態分析工具,首先源代碼經由Clang編譯器翻譯成LLVM的中間表示(Intermediate Representation,簡稱IR),ShapeChecker符號執行引擎通過解析IR字節碼來分析程序,分析完畢后生成bug報告.

圖1 ShapeChecker的總體框架Fig.1 Framework of ShapeChecker

由于分析工具中的執行引擎采用的是符號執行的方法,在分析大規模程序時,會降低工具的運行效率.針對工具中符號執行技術的不足,可采用程序切片的方法來提高工具的時間性能,即根據用戶的興趣點來專門檢測某一類或幾類缺陷,與關心的缺陷無關的代碼可被切除不分析,這樣在一定程度上緩解了狀態爆炸問題.

本文的組織結構如下:第2節介紹切片準則生成模塊,根據各類缺陷分析IR生成切片準則;第3節介紹切片模塊,分析IR得到程序依賴圖,再根據切片準則進行切片,得到切片后的程序,最后將切片后的程序交給符號執行引擎分析;第4節介紹程序切片的實驗結果;第5節是相關工作和總結.

2 生成切片準則

切片準則生成模塊的輸入是LLVM IR,根據用戶指定的缺陷分析IR產生切片準則,下面簡要介紹LLVM IR的核心語法,如圖2所示.編譯過程中的每個翻譯單元對應IR的一個模塊(module),包含函數聲明、函數定義和全局變量.

LLVM IR以函數為單位,每個函數包含若干基本塊b,每個基本塊包含若干條指令c,指令有函數調用指令,棧變量分配指令,算術運算指令,load與store指令,getelementptr指令等.其中getelementptr指令用于獲取聚合數據類型中子元素的地址,如獲取數組元素或結構體成員.

本系統共設計了針對八類缺陷的切片準則,分別是內存泄漏、文件描述符未釋放、除零、整數溢出、懸空指針或空指針解引用、緩沖區溢出、使用未初始化的變量、返回棧變量的地址,下面是由各類缺陷生成切片準則的設計.

圖2 LLVM IR的核心語法
Fig.2 Core grammar of LLVM IR

1)內存泄漏:檢測指令是否是malloc,realloc,calloc或free四種函數調用指令中的一種,如果是則將該條指令加入切片準則.

2)文件描述符未釋放:檢測指令是否是fopen,freopen,fclose,open,openat,creat,close函數調用指令中的一種,如果是則將該條指令加入切片準則.

3)除零:檢測指令是否是無符號除法,有符號除法,浮點數除法,無符號取模,有符號取模,浮點數取模運算中的一種,如果是則將指令加入切片準則.

4)整數溢出:將截斷指令,加減乘除指令,取余指令,求絕對值的函數調用指令加入切片準則,之所以加絕對值函數是為了檢測求最大負數的絕對值導致溢出的缺陷.

5)懸空指針或空指針解引用:在C語言上表現為對指針解引用和對數組作下標訪問操作,它們分別有取值和賦值兩種操作.比如對指針解引用的取值操作是*p,它的LLVM IR是

%1 = load i32*,i32** %p,align 8

%2 = load i32,i32* %1,align 4

檢測load指令的操作數是否來自上一條load指令,是則將其加入切片準則,此例中第二條load指令的操作數%1來自上一條load指令,故將第二條load指令加入切片準則;對數組取元素的取值操作,比如p[0],它的IR是

%0 = load i32*,i32** %p,align 8

%arrayidx = getelementptr inbounds i32,i32* %0,i64 0

%1 = load i32,i32* %arrayidx,align 4

檢測load指令的操作數是否來自getelementptr指令,滿足則加入切片準則;同理,賦值操作如*p = 2,它的IR是

%1 = load i32*,i32** %p,align 8

store i32 2,i32* %1,align 4

檢測store指令的操作數是否來自load,滿足則加入切片準則;對數組元素賦值,如p[0] = 2的IR是

%0 = load i32*,i32** %p,align 8

%arrayidx = getelementptr inbounds i32,i32* %0,i64 0

store i32 2,i32* %arrayidx,align 4

檢測store指令的操作數是否來自getelementptr指令,是則加入切片準則.

6)緩沖區溢出:緩沖區溢出的缺陷在C上表現為數組解引用,如arr[1],它的IR是

%arrayidx3 = getelementptr inbounds [3 x i32],[3 x i32]* %arr,i64 0,i64 1

%2 = load i32,i32* %arrayidx3,align 4

檢測load指令的操作數是否來自getelementptr指令,是則加入切片準則;同理,arr[1] = 0這樣的對數組元素賦值則檢測store指令是否來自getelementptr指令;最后,對C庫函數中與操作緩沖區相關的函數調用也加入切片準則,有memset、memcpy、memmove、strcpy、strncpy、strcat、strncat、wmemset、wmemcpy、wmemmove、wcscpy、wcsncpy、wcscat和wcsncat.

7)使用未初始化的變量:第一種情況是使用未初始化變量的值本身,如int a;printf(“%d ”,a);它的IR是

%a = alloca i32,align 4

%0 = load i32,i32* %a,align 4

%call = call i32(i8*,...)@printf(i8* getelementptr inbounds([4 x i8],[4 x i8]* @.str,i32 0,i32 0),i32 %0)

如果load指令的操作數來自alloca,則將load指令加入切片準則;第二種情況是將未初始化的變量的地址賦給指針,如int a;int *p = &a;它的IR是

%a = alloca i32,align 4

%p = alloca i32*,align 8

store i32* %a,i32** %p,align 8

因此若store指令的值操作數來自alloca,則將store指令加入切片準則.

8)返回棧變量的地址:這類缺陷分三種情況.第一種是將棧變量的地址賦值給指針類型的全局變量;第二種情況是將棧變量的地址賦值給二級指針的形參指向的區域,可通過形參傳回主調函數,這兩種情況都是將棧變量的地址賦給某變量,如store i32* %a,i32** %p,align 8,檢測store指令的值操作數的類型是否是指針,是則將store指令加入切片準則;第三種情況是在被調函數中返回指針或變量的地址,如ret i32* %p,所以檢測return指令的類型是否是指針,是則將它加入切片準則.

以上缺陷模式的檢測均是作保守分析,只要指令符合缺陷的特征,就將它加入切片準則,這樣保證了分析過程中與所關注的缺陷相關的程序語義的完備性.用戶可以指定多種缺陷,根據每一種缺陷獲取相應的切片準則,最后合并再交給切片模塊.

3 程序切片模塊

程序切片模塊根據切片準則,對LLVM IR做切片,由于C代碼的結構與IR等價,為便于圖示,下面的分析基于C代碼.本模塊分兩步,先構建程序依賴圖,然后根據程序切片準則在程序依賴圖上標記節點,計算反向可達性,所有可達的語句即是程序切片.

3.1 構建程序依賴圖

程序依賴圖表示程序中各語句間的依賴關系,包括數據依賴和控制依賴,程序依賴圖由數據依賴圖和控制依賴圖構成,依賴圖中的每個節點是一條語句.

3.1.1 構建數據依賴圖

定義1.數據依賴.語句p中定值的變量可能會在語句q中被使用,稱語句q數據依賴于語句p.

如圖3的示例程序所示,用戶在循環后動態分配了i個字節的內存,后續程序未釋放堆內存.

1 intmain(){2 void?p；3 intsum=0；4 inti=1；5 while(i<11){6 sum=sum+i；7 i=i+1；8 }9 p=malloc(i)；10 printf(″%d ″，sum)；11 }

圖3 示例程序
Fig.3 Sample program

第4條語句int i=1定義了變量i,在循環的判斷語句while(i< 11)中使用了i,所以while(i< 11)這條語句數據依賴于int i=1.LLVM在IR級別上提供了變量的DEF-USE信息,可得到語句間的定值和使用的關系,由此構建出圖3程序的數據依賴圖,如圖4所示,其中entry節點表示程序的入口,語句間的指向表示數據依賴.

圖4 圖3程序的數據依賴圖Fig.4 Data dependence graph of program in Fig.3

3.1.2 構建控制依賴圖

定義2.控制依賴.語句p的直接后繼至少有兩個,從其中一條路徑出發可到達語句q,從另外的一條路徑出發可能不會到達q,則稱語句q控制依賴于語句p.

通俗地說,語句p能決定語句q能否被執行,如圖3中的第6條語句sum = sum + i控制依賴于判斷條件while(i< 11).一定會被執行的語句控制依賴于程序的入口點entry.圖3示例程序的控制依賴圖如圖5所示,其中的虛線箭頭表示語句間的控制依賴關系.

最后,將數據依賴圖與控制依賴圖合并,構成程序依賴圖,圖6是圖3示例程序的程序依賴圖.

3.2 計算反向可達性

假設用戶關心內存泄漏的缺陷,由切片準則生成模塊分析圖3得到切片準則是malloc函數調用語句,如圖7中的深灰色節點所示,以它為起始點,對程序依賴圖反向遍歷,所能到達的所有節點即為程序切片,如灰色節點所示.

圖5 圖3程序的控制依賴圖Fig.5 Control dependence graph of program in Fig.3

圖6 圖3程序的程序依賴圖Fig.6 Program dependence graph of program in Fig.3

圖7 圖3程序的反向可達性Fig.7 Inverse reachability of program in Fig.3

由此得到源程序中與內存泄漏缺陷相關的語句,圖8是程序切片的源代碼表示,它的規模較原有程序要小,最后將切片交給分析工具ShapeChecker檢測.

1 intmain(){2 void?p；3 inti=1；4 while(i<11){5 i=i+1；6 }7 p=malloc(i)；8 }

圖8 圖3程序的切片結果
Fig.8 Result of slicing program in Fig.3

4 實驗結果

實驗的硬件平臺是Intel(R)Core(TM)i7-4790 CPU @ 3.60GHz 4核8線程,20G內存;操作系統是Ubuntu 16.04.1 LTS64位.被測程序采用美國國家安全局的Common Weakness Enumeration(CWE)公共測試集*The MITRE Corporation.Common Weakness Enumeration [EB/OL].http://cwe.mitre.org/data/definitions/1000.html, 2017.,選取其中八類缺陷目錄,分別是內存泄漏(CWE401)、文件描述符未釋放(CWE773、775)、除零(CWE369)、整數溢出(CWE190、191)、懸空指針或空指針解引用(CWE476、690)、緩沖區溢出(CWE121、122、124、126、127)、使用未初始化的變量(CWE457)、返回棧變量的地址(CWE562),用靜態分析工具ShapeChecker檢測缺陷,加程序切片功能前后的時間對比如表1所示,其中切片后的分析時間包括切片本身的耗時.

表1 程序切片前后的分析時間比較
Table 1 Analysis time of before and after slicing

分析時間(s)切片前切片后時間減少的百分比內存泄漏603．87253．0558．10%文件描述符泄漏71．0539．5444．35%除零625．27363．2741．90%整數溢出3565．41911．2346．40%空指針解引用432．54172．9560．02%緩沖區溢出17036．1212915．6824．19%用未初始化變量2622．662403．798．35%返回棧變量地址0．890．4153．93%

從測試結果來看,程序切片減少了分析工具的運行時間,平均減少了27.64%.CWE的每種測試目錄專門針對某種缺陷,在用戶指定檢測相應缺陷時,程序切片可將無關的控制結構刪除,減少了程序的規模和符號執行中的狀態數目,在一定程度上提高了靜態分析的性能.表2是加程序切片功能前后的平均漏報率和誤報率.

表2 程序切片前后的精度比較
Table 2 Precision of before and after slicing

切片前切片后漏報率1．86%3．73%誤報率15．75%18．77%

加程序切片之后,分析工具的漏報率和誤報率有略微的上升,這是由于靜態分析本身是不完備的,將切片后的程序交給符號執行引擎執行時可能會影響它的分析策略.程序切片剔除的是與所關心的缺陷無關的代碼,不會改變與缺陷相關的程序語義,因此漏報率和誤報率只是有略微上升,相比工具在時間性能上的提升,精度損失在可接受的范圍之內.

5 相關工作和總結

程序切片的思想由Weiser[10]提出,最初用于調試程序[11],程序中某一條語句出錯后,為了找到影響該語句的所有前面的語句,只關注出錯部分,方便程序員的調試.這一思想也可用于程序分析領域,用戶想專門檢測某種缺陷,這種缺陷關聯的語句即是興趣點.

Swarup等[12]用一組自動生成的近似滿足程序不變量的輸入來檢測軟件缺陷,之后用動態后向切片技術逐步過濾輸入集以提高分析精度.

Marek[13]等開發的Symbiotic靜態分析工具將指令制導、程序切片和符號執行工具KLEE[7]組合起來,其中切片部分使用數據流方程迭代方式計算.

趙云山等[14]使用有限狀態自動機描述的缺陷模式和路徑條件來生成切片準則,并有選擇地對控制流圖中的匯合點進行缺陷狀態合并以減少誤報率及提高分析效率.

本文在LLVM中間語言上提出針對缺陷的程序切片方法,筆者所在的課題組目前仍在改進靜態分析工具ShapeChecker,下一步是支持C++的分析,C++有繼承、多態和異常等獨有的特性,在LLVM中間語言級別上會生成新的指令,可以將程序切片擴展成對C++中異常安全、線程安全等缺陷的處理.程序切片技術也可用于逆向分析中,逆向分析關心軟件的基本原理和算法,可通過切片技術去除GUI和輸入輸出等部分,這樣減少了我們理解程序的負擔.

[1] Hoare Charles Antony Richard.An axiomatic basis for computer programming [J].Communications of the ACM,1969,12(10):576-580.

[2] Reynolds John C.Separation logic:a logic for shared mutable data structures[C].Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science,IEEE,2002.

[3] Clarke Edmund,Allen Emerson.Design and synthesis of synchronization skeletons using branching time temporal logic[M].Workshop on Logic of Programs,Springer Berlin Heidelberg,1981.

[4] Cousot Patrick,RadhiaCousot.Abstract interpretation:a unified lattice model for static analysis of programs by construction or approximation of fixpoints [C].Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages,ACM,1977.

[5] Kildall Gary.A unified approach to global program optimization[C].Proceedings of the 1st ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages,ACM,1973.

[6] King James C.Symbolic execution and program testing [J].Communications of the ACM,1976,19(7):385-394.

[7] Cristian Cadar,Daniel Dunbar,Dawson Engler.KLEE:unassisted and automatic generation of high-coverage tests for complex systems programs[C].Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation,2008:209-224.

[8] Lattner Chris,VikramAdve.LLVM:a compilation framework for lifelong program analysis & transformation [C].Proceedings of the International Symposium on Code Generation and Optimization:Feedback-directed and Runtime Optimization,IEEE Computer Society,2004.

[9] Liang Jia-biao,Li Zhao-peng,Zhu Ling,et al.Symbolic execution engine with shape analysis [J].Computer Science,2016,43(3):193-198.

[10] Weiser Mark.Program slicing [C].Proceedings of the 5th International Conference on Software Engineering,IEEE Press,1981:439-449.

[11] Weiser Mark.Programmers use slices when debugging [J].Communications of the ACM,1982,25(7):446-452.

[12] Swarup Kumar Sahoo,John Criswell,Chase Geigle,et al.Using likely invariants for automated software fault localization[J].ACM SIGARCH Computer Architecture News,2013,41(1):139-152.

[13] Marek Chalupa,Martin Joná?,Jiri Slaby,et al.Symbiotic 3:new slicer and error-witness generation[R].International Conference on Tools and Algorithms for the Construction and Analysis of Systems,Springer Berlin Heidelberg,2016.

[14] Zhao Yun-shan,Gong Yun-zhan,Liu Li,et al.Improving the efficiency and accuracy of path-sensitive defect detecting [J].Chinese Journal of Computers,2011,34(6):1100-1113.

附中文參考文獻：

[9] 梁家彪,李兆鵬,朱 玲,等.支持形狀分析的符號執行引擎的設計與實現 [J].計算機科學,2016,43(3):193-198.

[14] 趙云山,宮云戰,劉 莉,等.提高路徑敏感缺陷檢測方法的效率及精度研究 [J].計算機學報,2011,34(6):1100-1113.