C程序內(nèi)存安全缺陷分析PPT課件

1、C程序內(nèi)存安全缺陷分析李兆鵬中國(guó)科大-國(guó)創(chuàng)高可信軟件工程中心中國(guó)科學(xué)技術(shù)大學(xué)2016-11所在實(shí)驗(yàn)室項(xiàng)目組的背景 近年來(lái)，在C程序驗(yàn)證方面有些積累 C程序驗(yàn)證方法及工具（合作人：陳意云教授、張昱副教授） 指針邏輯及原型工具 形狀圖邏輯及原型工具 安全C子集程序驗(yàn)證工具（陳意云教授負(fù)責(zé)，在研）相關(guān)課題及定位 “ “重量級(jí)重量級(jí)” ” 半自動(dòng)驗(yàn)證半自動(dòng)驗(yàn)證 C/OS II操作系統(tǒng)驗(yàn)證 “ “中量級(jí)中量級(jí)” ” 全自動(dòng)驗(yàn)證工具全自動(dòng)驗(yàn)證工具 安全C子集程序驗(yàn)證器 “ “輕量級(jí)輕量級(jí)” ” 全自動(dòng)靜態(tài)分析工具全自動(dòng)靜態(tài)分析工具 本課題 借助在該C程序驗(yàn)證領(lǐng)域的一些積累構(gòu)建輕量級(jí)的分析工具提綱 背景和目

2、標(biāo) 工具概要 工作的重點(diǎn)難點(diǎn) 未來(lái)工作經(jīng)典案例 價(jià)值$2000萬(wàn)的C程序bug SunSoft公司的OS研發(fā)部門(mén)1993 一個(gè)軟硬件訂單 交付前，客戶(hù)發(fā)現(xiàn)一個(gè)庫(kù)函數(shù)總是不能按照預(yù)期運(yùn)行 異步(asynchronous)I/O庫(kù)5最終，問(wèn)題追蹤到的一個(gè)語(yǔ)句：x =2;經(jīng)典案例 JDK的二分查找缺陷6* Bug ID: 5045582 (coll) binarySearch() fails for size larger than 1=0) result = y; else result = -y; return result;/int main() / return abs(10)+abs(-1

3、0);/abs()函數(shù)符號(hào)執(zhí)行的簡(jiǎn)單介紹不太嚴(yán)格的說(shuō)：不太嚴(yán)格的說(shuō)： 符號(hào)執(zhí)行即在符號(hào)符號(hào)執(zhí)行即在符號(hào)內(nèi)存上內(nèi)存上根據(jù)語(yǔ)句（指令）的操作語(yǔ)義根據(jù)語(yǔ)句（指令）的操作語(yǔ)義進(jìn)行演算（執(zhí)行）。進(jìn)行演算（執(zhí)行）。從一個(gè)簡(jiǎn)單例子說(shuō)起int abs(int y) int result; if(y=0) result = y; else result = -y; return result;/int main() / return abs(10)+abs(-10);/abs()函數(shù)符號(hào)執(zhí)行的簡(jiǎn)單介紹運(yùn)行內(nèi)存S_yy：_y代表y的初值；這里是任意值從一個(gè)簡(jiǎn)單例子說(shuō)起int abs(int y) int resu

4、lt; if(y=0) result = y; else result = -y; return result;/int main() / return abs(10)+abs(-10);/abs()函數(shù)符號(hào)執(zhí)行的簡(jiǎn)單介紹運(yùn)行內(nèi)存S_yy：-res：-result：函數(shù)返回值從一個(gè)簡(jiǎn)單例子說(shuō)起int abs(int y) int result; if(y=0) result = y; else result = -y; return result;/int main() / return abs(10)+abs(-10);/abs()函數(shù)符號(hào)執(zhí)行的簡(jiǎn)單介紹運(yùn)行內(nèi)存S_yy：-res：-resu

5、lt：_y = 0 ?_y =0) result = y; else result = -y; return result;/int main() / return abs(10)+abs(-10);/abs()函數(shù)符號(hào)執(zhí)行的簡(jiǎn)單介紹運(yùn)行內(nèi)存S 運(yùn)行內(nèi)存S_yy：-res：-result：約束：_y = 0約束：_y =0) result = y; else result = -y; return result;/int main() / return abs(10)+abs(-10);/abs()函數(shù)符號(hào)執(zhí)行的簡(jiǎn)單介紹運(yùn)行內(nèi)存S 運(yùn)行內(nèi)存S_yy：-res：_yresult：約束：_y =

6、0約束：_y =0) result = y; else result = -y; return result;/int main() / return abs(10)+abs(-10);/abs()函數(shù)符號(hào)執(zhí)行的簡(jiǎn)單介紹運(yùn)行內(nèi)存S 運(yùn)行內(nèi)存S_yy：_yres：_yresult：約束：_y = 0約束：_y =0) result = y; else result = -y; return result;/int main() / return abs(10)+abs(-10);/abs()函數(shù)符號(hào)執(zhí)行的簡(jiǎn)單介紹運(yùn)行內(nèi)存S 運(yùn)行內(nèi)存S_yy：_yres：_yresult：約束：_y = 0約束：

7、_y =0) result = y; else result = -y; return result;/int main() / return abs(10)+abs(-10);/abs()函數(shù)符號(hào)執(zhí)行的簡(jiǎn)單介紹運(yùn)行內(nèi)存S 運(yùn)行內(nèi)存S_yy：_yres：_yresult：約束：_y = 0約束：_y = 0運(yùn)行內(nèi)存S符號(hào)狀態(tài)符號(hào)內(nèi)存路徑約束_y=0_y= 0 ？判定約束求解重要問(wèn)題 符號(hào)狀態(tài)如何描述關(guān)乎符號(hào)執(zhí)行的表達(dá)能力（斷言語(yǔ)言與定理證明問(wèn)題） 分支對(duì)于符號(hào)執(zhí)行來(lái)說(shuō)，可能會(huì)引起狀態(tài)的指數(shù)級(jí)爆炸（狀態(tài)爆炸問(wèn)題） 多層次分支問(wèn)題 循環(huán)問(wèn)題 多個(gè)狀態(tài)執(zhí)行順序有沒(méi)有差別？（符號(hào)執(zhí)行調(diào)度策略問(wèn)題）x0

8、y=0y=0 x=0y0y=0) result = y; else result = -y; return result;int main() return abs(10)+abs(-10);斷言語(yǔ)言描述狀態(tài)_yy：_yres：_yresult：約束：_y = 0運(yùn)行內(nèi)存Sold(y)y：old(y)res：old(y)result：約束：old(y)= 0符號(hào)狀態(tài)S寫(xiě)成前后條件的形式即前條件：old(y)= 0后條件：res = old(y)基于函數(shù)摘要的符號(hào)執(zhí)行Pre: y=0Post: res = old(y)Pre: y=0y=0) result = y; else result =

9、-y; return result;int main() return abs(10)+abs(-10);特色比較是否支是否支持?jǐn)?shù)組持?jǐn)?shù)組是否支持是否支持內(nèi)存泄露內(nèi)存泄露檢查檢查是否支持是否支持?jǐn)?shù)據(jù)結(jié)構(gòu)性數(shù)據(jù)結(jié)構(gòu)性質(zhì)分析質(zhì)分析是否支持是否支持循環(huán)不變循環(huán)不變式推斷式推斷不需要修不需要修改源代碼改源代碼KLEE(Open Source)Clang SA(Open Source)SpaceInvader(Microsoft)Parfait(Oracle)ShapeChecker(Our Tool)工具架構(gòu)C CodeC-to-LLVM Compilere.g., ClangLLVM IR Code

10、Symbolic Execution Scheduler (strategy)Symbolic Execution Engine (Core)Solvere.g., STPError & WarningReportSpecs of Standard Libraries約1.5萬(wàn)行約0.5萬(wàn)行約2.5萬(wàn)行輔助代碼約2.5萬(wàn)行實(shí)現(xiàn)：復(fù)用KLEE的部分框架代碼，修改新增約8萬(wàn)行C+代碼工具現(xiàn)狀 在開(kāi)發(fā)完善過(guò)程中，目前工作著重改善性能在開(kāi)發(fā)完善過(guò)程中，目前工作著重改善性能/可縮放性與誤報(bào)?？煽s放性與誤報(bào)。 小型程序基本能夠做到快速準(zhǔn)確對(duì)于某些幾十行至幾百行的測(cè)試?yán)龑?duì)于某些幾十行至幾百行的測(cè)試?yán)?/p>

11、（包括自編寫(xiě)和公認(rèn)測(cè)試集中選用的），一般運(yùn)行100毫秒至10秒量級(jí)能夠能夠準(zhǔn)確準(zhǔn)確的定位程序的定位程序缺陷缺陷（低漏報(bào)（低漏報(bào)、低誤、低誤報(bào)）報(bào)） 中大型可以分析，但一般性能較低 幾百行至幾千行代碼的實(shí)際代碼，但有些程序分析會(huì)遇到可縮放性問(wèn)題（幾分鐘到幾小時(shí)） Linux Coreutils工具集中的tty.c等千行以?xún)?nèi)的程序運(yùn)行低于3分鐘，部分復(fù)雜代碼要若干小時(shí)。針對(duì)CWE測(cè)試集的評(píng)估 CWE（Common Weakness Enumeration）介紹 網(wǎng)址:/ CWE是美國(guó)國(guó)土安全部網(wǎng)絡(luò)安全和通訊辦公室的US-CERT贊助(CWE is spons

12、ored by US-CERT in the office of Cybersecurity and Communications at the U.S. Department of Homeland Security. )基于該測(cè)試集等相關(guān)技術(shù), MITRE提供分析工具的認(rèn)證服務(wù). 我們?cè)u(píng)估使用的是我們?cè)u(píng)估使用的是Juliet_Testsuit_for_C_C+_1.2版版 該測(cè)試集包括該測(cè)試集包括C/C+的測(cè)試?yán)臏y(cè)試?yán)? 用于評(píng)估分析工具的分析準(zhǔn)確性用于評(píng)估分析工具的分析準(zhǔn)確性. 包括包括C+測(cè)試測(cè)試?yán)?，其中共有例，其中共?萬(wàn)多個(gè)測(cè)試?yán)f(wàn)多個(gè)測(cè)試?yán)槍?duì)CWE測(cè)試集的評(píng)估（續(xù)） 測(cè)試樣本

13、：約測(cè)試樣本：約15000個(gè)測(cè)試?yán)齻€(gè)測(cè)試?yán)?我們選擇了本課題工具支持的缺陷目錄下所有的工具支持的缺陷目錄下所有的C測(cè)測(cè)試試?yán)?通過(guò)測(cè)試，“漏報(bào)率漏報(bào)率” ”和和“ “誤報(bào)率誤報(bào)率” ”均在均在在在5%以?xún)?nèi)以?xún)?nèi) 使用腳本而非人工統(tǒng)計(jì)，有漏報(bào)和誤報(bào)則計(jì)入統(tǒng)計(jì)有漏報(bào)和誤報(bào)則計(jì)入統(tǒng)計(jì) 真實(shí)的漏報(bào)率和誤報(bào)率應(yīng)該更低真實(shí)的漏報(bào)率和誤報(bào)率應(yīng)該更低 發(fā)現(xiàn)了測(cè)試集中的一些錯(cuò)誤等測(cè)試用例發(fā)現(xiàn)了測(cè)試集中的一些錯(cuò)誤等測(cè)試用例 對(duì)對(duì)snprintf接口規(guī)范理解有誤接口規(guī)范理解有誤評(píng)估統(tǒng)計(jì)結(jié)果CWE測(cè)試種類(lèi)目錄文件數(shù)文件數(shù)代碼行數(shù)代碼行數(shù)誤報(bào)誤報(bào)漏報(bào)漏報(bào)“ “誤報(bào)率誤報(bào)率” ”“ “漏報(bào)率漏報(bào)率” ”運(yùn)行時(shí)間運(yùn)行時(shí)間

14、(s)CWE121_Stack_Based_Buffer_Overflow2844378664060.00%0.21%1391.55CWE122_Heap_Based_Buffer_Overflow173624282002050.00%11.81%845.93CWE124_Buffer_Underwrite8961409720100.00%1.12%290CWE126_Buffer_Overread7081124440220.00%3.11%262.16CWE127_Buffer_Underread8961370840100.00%1.12%259.84CWE190_Integer_Overf

15、low3024397290312610.32%0.20%590.99CWE191_Integer_Underflow184824518618049.74%0.22%354.41CWE369_Divide_by_Zero467102848000.00%0.00%137.04CWE401_Memory_Leak628945790890.00%14.17%236.37CWE415_Double_Free156229561207.69%0.00%26.22CWE416_Use_After_Free12623103000.00%0.00%91.68CWE457_Use_of_Uninitialized_

16、Variable50495582000.00%0.00%83.29CWE476_NULL_Pointer_Dereference20428748000.00%0.00%30.82CWE562_Return_of_Stack_Variable_Address2170000.00%0.00%0.36CWE690_NULL_Deref_From_Return52057580040.00%0.77%114.08CWE773_Missing_Reference_to_Active_File_Descriptor_or_Handle526450080.00%15.38%12.72CWE775_Missin

17、g_Release_of_File_Descriptor_or_Handle5256860260.00%50.00%8.99總計(jì)1466320921625044233.44%3.44%2.88%2.88%4736.45Linux CoreUtils程序集的分析 目前工具還在調(diào)優(yōu)過(guò)程中，多數(shù)情況下作為分析性能可縮放性的評(píng)價(jià)參照 并沒(méi)有集中精力去對(duì)這些較為大型程序進(jìn)行分析結(jié)果的審查 曾在2014年就發(fā)現(xiàn)的一處內(nèi)存泄漏問(wèn)題（localcharset.c）向社區(qū)報(bào)告，相關(guān)開(kāi)發(fā)人員認(rèn)為“Its not harmful”. 針對(duì)中大型實(shí)際代碼的評(píng)估 未來(lái)重點(diǎn)工作之一 最佳方式是和開(kāi)發(fā)這些代碼的團(tuán)隊(duì)合作工具

18、演示 整數(shù)溢出 內(nèi)存泄漏與單鏈表操作提綱 背景和目標(biāo) 工具概要 工作的重點(diǎn)難點(diǎn) 未來(lái)工作工作的重點(diǎn)難點(diǎn) 目前工作著重改善性能目前工作著重改善性能/可縮放性與誤可縮放性與誤報(bào)等。報(bào)等。 解決如下分析難題：約束求解負(fù)擔(dān)過(guò)重的問(wèn)題約束求解負(fù)擔(dān)過(guò)重的問(wèn)題狀態(tài)爆炸狀態(tài)爆炸 原因：分支、循環(huán)、多函數(shù)行為、內(nèi)存分情況討論 誤報(bào)和漏報(bào)問(wèn)題約束求解瓶頸問(wèn)題（1） 下面的場(chǎng)合都需要大量使用約束求解： Load和Store指令處理； Call指令應(yīng)用已知函數(shù)行為； ret指令建立當(dāng)前函數(shù)行為 約束求解器目前使用的是STP(Simple Theorem Prover) 約95-99%的分析時(shí)間為求解器求解時(shí)間 其中3

19、050%的求解時(shí)間用在了符號(hào)地址解析過(guò)程中 另外，STP也在開(kāi)發(fā)中，時(shí)常遇到超時(shí)和bug崩潰（求解失敗）約束求解瓶頸問(wèn)題（2） 解決辦法：降低各場(chǎng)合對(duì)約束求解的負(fù)擔(dān) 案例一：使用Cache對(duì)符號(hào)地址解析結(jié)果進(jìn)行存儲(chǔ) 符號(hào)地址表達(dá)式在整個(gè)程序運(yùn)行中是唯一的 使用100個(gè)存儲(chǔ)單元的Cache可以使得解析時(shí)間降低解析時(shí)間降低為原解析時(shí)間的為原解析時(shí)間的515% 案例二：使用LLVM IR的mem2reg對(duì)輸入代碼進(jìn)行優(yōu)化，減少訪存指令 大約可以減少20%40%的約束求解數(shù)量狀態(tài)爆炸問(wèn)題與緩解 多層分支造成狀態(tài)爆炸 循環(huán)的問(wèn)題 程序驗(yàn)證中需要程序員（驗(yàn)證人員）提供循環(huán)不變式 程序分析沒(méi)有這種提示，常用

20、方法： 對(duì)循環(huán)進(jìn)行多次迭代！ 其他相關(guān)處理也會(huì)引起狀態(tài)分裂過(guò)快 函數(shù)行為個(gè)數(shù)過(guò)多？有冗余？ 外部參數(shù)(指針）描述過(guò)弱，分情況考慮？例程2int foo(int x, int y) int result; if(x0) printf(“x is greater than zero”); else printf(“x is not greater than zero”); if(y=0) result = y; else result = -y; return result;Pre: x0 / y0Post: res = old(y)Pre: x0 / y=0Post: res = -old(y)

21、 Pre: x0Post: res = old(y)Pre: x=0 / y0y=0y=0 x=0y0y0y=0y=0 x=0y0y0) printf(“x is greater than zero”); else printf(“x is not greater than zero”); if(y=0) result = y; else result = -y; return result;Pre: x0 / y0Post: res = old(y)Pre: x0 / y0y=0 x=0y0Post: res = old(y)Pre: y=0Post: res = -old(y) 依據(jù)命中情

22、況對(duì)已有函數(shù)行為進(jìn)行變換狀態(tài)緩存實(shí)驗(yàn)數(shù)據(jù)（部分） 分析時(shí)間分析時(shí)間函數(shù)行為數(shù)量函數(shù)行為數(shù)量命中次數(shù)命中次數(shù)代碼規(guī)模代碼規(guī)模緩存前緩存前緩存后緩存后緩存前緩存前緩存后緩存后micro_httpd.c3 min. 35 sec. 557 ms20 sec. 844 ms5545101290 LOCcat.c73 min. 49 sec. 650 ms8 min. 32 sec. 324 ms840255526780 LOC（不含庫(kù)） 值得一提的是，對(duì)于cat.c例程，同時(shí)開(kāi)啟函數(shù)行為合并和狀態(tài)緩存僅需要2分鐘分析時(shí)間。緩解辦法（三） 循環(huán)不變式推斷循環(huán)不變式推斷 減少迭代造成的狀態(tài)爆炸 因?yàn)镵LE

23、E 在執(zhí)行createList 中的循環(huán)時(shí)需要知道確切的循環(huán)次數(shù)，所以KLEE 需要考慮n 從0 到255 間所有的取值，最終KLEE分析該程序時(shí)產(chǎn)生了256 個(gè)狀態(tài) 而我們的工具在分析createList 中的循環(huán)時(shí)能夠?yàn)樵撗h(huán)構(gòu)建出一個(gè)循環(huán)不變式且不需要關(guān)系n 的具體取值，因此分析該程序（main）時(shí)只產(chǎn)生了2個(gè)分支狀態(tài)。緩解辦法（三） 循環(huán)不變式推斷 select sort程序我們的工具我們的工具只只產(chǎn)生了產(chǎn)生了10 個(gè)分支個(gè)分支狀態(tài)狀態(tài)，而而KLEE 產(chǎn)生產(chǎn)生了了30844 個(gè)分支狀態(tài)個(gè)分支狀態(tài)（只關(guān)心是否發(fā)生了數(shù)組只關(guān)心是否發(fā)生了數(shù)組越界訪問(wèn)越界訪問(wèn)等等內(nèi)存安全，不考慮排序功能）內(nèi)存

24、安全，不考慮排序功能） 循環(huán)推斷方面仍需大量工作循環(huán)推斷方面仍需大量工作緩解辦法（四） 程序切片 根據(jù)用戶(hù)關(guān)注的缺陷種類(lèi)、程序變量等，形成興趣點(diǎn)(切片準(zhǔn)則)來(lái)簡(jiǎn)化程序int i;int sum = 0;int product = 1;for(i = 1; i N; +i) sum = sum + i; product = product * i;write(sum);write(product);int i;int sum = 0;for(i = 1; i N; +i) sum = sum + i;write(sum);只關(guān)心 sum值緩解辦法（四） 基于缺陷種類(lèi)的切片技術(shù) 支持八類(lèi)重要缺陷及

25、其組合 例如，內(nèi)存泄漏、除零、空指針解引用、整數(shù)溢出等等 性能提升約30%-83%缺陷種類(lèi)缺陷種類(lèi)測(cè)試?yán)郎y(cè)試?yán)龑?duì)比對(duì)比漏報(bào)文件漏報(bào)文件誤報(bào)文件誤報(bào)文件分析時(shí)間分析時(shí)間(秒秒)節(jié)省時(shí)間節(jié)省時(shí)間Buffer Overflow14切片前0 2 24.3440.43%切片后0 2 14.50Divide By Zero11切片前0 0 9.2783.28%切片后0 0 1.55File IO15切片前0 1 15.6146.00%切片后2 2 8.43Memory Leak15切片前0 0 18.2652.52%切片后2 0 8.67Uninitialized Variable26切片前00 68.4232.81%切片后0 0 45.97緩解辦法（五） 借助修改影響分析技術(shù)復(fù)用分析結(jié)果（on-going) 比較兩個(gè)版本代碼之間差別 并通過(guò)調(diào)用圖標(biāo)記所有受影響的函數(shù)緩解辦法（五） 借助修改影響分析技術(shù)復(fù)用分析結(jié)果 比較兩個(gè)版本代碼之間差別 并通過(guò)調(diào)用圖標(biāo)記所有受影響的函數(shù)緩解辦法（五） 借助修改影響分析技