基于符號執(zhí)行的格式化字符串漏洞自動驗證方法研究

王瑞鵬, 張 旻, 黃 暉, 沈 毅

(國防科技大學電子對抗學院，合肥，230037)

隨著信息化程度的不斷提高，信息系統(tǒng)被廣泛應(yīng)用于金融、醫(yī)療、國防、工控等重要領(lǐng)域。高度信息化帶來便利的同時也對網(wǎng)絡(luò)空間安全提出了更高的要求。漏洞是威脅網(wǎng)絡(luò)空間安全的重要因素，其中格式化字符串漏洞是一種常見的軟件漏洞，它由Tymm Twillman首次發(fā)現(xiàn)于1999年[1]，其主要成因是程序未對來自外部的輸入內(nèi)容做出嚴格過濾，導致格式化控制符參數(shù)能夠被外部輸入所影響[2]，進而對信息系統(tǒng)產(chǎn)生較大威脅。例如CVE-2012-0809漏洞[3]，該漏洞可以提升Linux用戶的權(quán)限，危害較大。因此對格式化字符串漏洞的挖掘和驗證意義十分重大。

現(xiàn)有的自動化漏洞挖掘方法能夠挖掘到大量的軟件漏洞[4-8]，但不能對產(chǎn)生漏洞的可利用性進行驗證。因此，漏洞自動驗證技術(shù)在近些年成為了軟件安全領(lǐng)域的一個研究熱點。在漏洞自動驗證領(lǐng)域，符號執(zhí)行技術(shù)的準確性和可靠性使其成為自動化程序分析的重要工具。目前基于符號執(zhí)行的自動化漏洞自動驗證系統(tǒng)有很多，如AEG[9]、Mayhem[10]、CRAX[11]等，其中AEG系統(tǒng)利用到了源碼信息，其余系統(tǒng)都在二進制程序?qū)用鎸β┒催M行自動驗證。上述的系統(tǒng)都期望解決通用的漏洞自動驗證，其漏洞驗證模型中包含針對多種不同漏洞類型的驗證方式，同時存在很多文獻[12～17]針對特定漏洞或特定的漏洞驗證方法，如黃釗等人的FSVDTG[12]主要針對格式化字符串漏洞進行漏洞驗證方法研究，方皓[13]等人主要針對Return-to-dl-resolve漏洞驗證方法進行研究。上述的大部分漏洞自動驗證系統(tǒng)都是通過分析漏洞利用特點，構(gòu)建漏洞驗證模型，生成漏洞驗證約束條件，約束求解得到漏洞驗證代碼。因此，漏洞驗證系統(tǒng)的適用范圍，通常由系統(tǒng)內(nèi)漏洞驗證模型適用范圍決定?，F(xiàn)有系統(tǒng)在針對格式化字符串漏洞自動驗證時，構(gòu)建了參數(shù)位于?？臻g的漏洞驗證模型，而忽略了參數(shù)位于其他空間時的情況。

本文提出了一種基于符號執(zhí)行的格式化字符串漏洞自動驗證方法，對現(xiàn)有的格式化字符串漏洞驗證系統(tǒng)的漏洞驗證模型進行了拓展，提高了格式化字符串漏洞自動驗證系統(tǒng)的性能，降低了對于漏洞可利用性的誤判，擴大了系統(tǒng)的適用范圍，解決了對格式化字符串參數(shù)位于堆區(qū)及BSS段空間的漏洞自動驗證的問題。

1 格式化字符串漏洞

1.1 格式化字符串參數(shù)

格式化字符串參數(shù)是格式化字符串函數(shù)用于將指定的字符串轉(zhuǎn)換為期望的輸入輸出格式的控制符參數(shù)，格式化字符串參數(shù)的格式如下：

%[parameter][flags][width][precision]
[length]type

一般以%開始，以type結(jié)束，例如“%d”。配合printf()等格式化字符串函數(shù)，能夠?qū)⒑瘮?shù)參數(shù)以指定格式進行輸入輸出。

其中parameter一般為n$，指獲取格式化字符串中的指定參數(shù)，flags表示標志位，width輸出的最小字段寬度，precision表示輸出精度，即輸出的最大長度，length表示輸出的字節(jié)長度。

格式化字符串中的type表示了預(yù)期輸入輸出的格式。常見的type類型及其使用效果如表1所示[18]。

表1 常見type類型及其含義

1.2 格式化字符串漏洞

格式化字符串漏洞是格式化控制符參數(shù)被程序的外部輸入污染所導致的。例如printf(a,b)語句，假設(shè)這里的a參數(shù)可被外部輸入污染，若此時參數(shù)a中的內(nèi)容為合法的格式化字符串內(nèi)容時，變量b中的內(nèi)容就會按照指定格式打印出來，但若a中內(nèi)容為“%d%d”等非法格式化字符串內(nèi)容，程序不僅會將變量b打印出來，而且會嘗試將函數(shù)未定義的第3個參數(shù)打印出來，由于此時程序未定義第3個參數(shù)，所以系統(tǒng)便打印了非預(yù)期的內(nèi)存內(nèi)容[19]。如果精心構(gòu)造格式化字符串漏洞中格式化控制符參數(shù)的內(nèi)容，可以實現(xiàn)任意內(nèi)存地址的讀寫，進而獲取系統(tǒng)權(quán)限，引發(fā)嚴重的系統(tǒng)安全問題。

2 漏洞自動驗證方法設(shè)計

本文提出了一種基于符號執(zhí)行的格式化字符串漏洞自動驗證方法。該方法核心流程如圖1所示。

圖1 方法核心流程

首先，監(jiān)控程序的運行狀態(tài)，在程序運行至格式化字符串函數(shù)時，進行漏洞的存在性檢測；之后判斷當前格式化字符串參數(shù)的存儲位置，并根據(jù)參數(shù)的不同存儲位置，構(gòu)建對應(yīng)的漏洞驗證約束；最后，將構(gòu)建好的約束作為約束求解器輸入，約束求解得到最終漏洞驗證輸入實例。

2.1 漏洞存在性檢測

如第1.1節(jié)中所述，格式化字符串漏洞是由于外部輸入對格式化字符串參數(shù)的污染而導致的。本方法會監(jiān)控程序中每個格式化字符串函數(shù)，判斷格式化字符串參數(shù)是否被外部輸入影響，從而判斷漏洞的存在性。

首先對程序中目標危險函數(shù)進行掛鉤操作。當測試程序運行至目標函數(shù)時對其進行攔截，并對目標函數(shù)的格式化字符串參數(shù)進行判斷，若當前參數(shù)取值為符號值，則表明當前函數(shù)的格式化字符串參數(shù)已被系統(tǒng)引入的符號變元所污染，即該參數(shù)會被外部輸入污染，從而證明格式化字符串漏洞的存在，反之，則說明當前函數(shù)不存在格式化字符串漏洞，如圖2所示。

圖2 漏洞存在性檢測方法

2.2 ?？臻g格式化字符串漏洞驗證約束構(gòu)建

當漏洞的格式化字符串參數(shù)存儲于?？臻g時，可通過格式化字符串函數(shù)在棧空間內(nèi)布置任意地址，進而利用格式化字符串漏洞實現(xiàn)對任意地址讀寫。利用形如address+%offset $s的漏洞驗證載荷進行任意地址讀操作，利用形如address + padding + %offset $n的漏洞驗證載荷進行任意地址寫操作。其中address表示目標讀寫地址，offset表示address與危險函數(shù)參數(shù)的相對偏移，該方法如圖3所示。

圖3 棧空間格式化字符串漏洞任意地址讀寫方法

通常期望寫入address地址的數(shù)值遠大于緩沖區(qū)大小，導致address + padding的長度無法滿足漏洞驗證條件，所以通常利用形如% num s的格式化字符串產(chǎn)生長度為num的字符串。

為了構(gòu)建上述漏洞驗證載荷，實現(xiàn)對address地址的讀寫操作，需要首先計算offset的取值，當前的格式化字符串緩沖區(qū)地址保存在第1個參數(shù)內(nèi)，因此*(ESP+4)為棧中address的地址，因此offset的取值如式(1)所示。

offset=(*(ESP+4)-(ESP-4))/4

(1)

在計算格式化字符串時，由于期望向目標地址寫入的值往往較大，采取一次覆蓋目標地址為期望值的時間效率極為低下，所以，在這種情況下，可以采用兩次寫入的方法，既節(jié)省緩沖區(qū)大小，又可以縮短漏洞驗證時間，即利用“%hn”一次寫入下2字節(jié)數(shù)據(jù)，上述計算格式化字符串漏洞驗證載荷過程如算法1所示。

1)算法1：計算格式化字符串漏洞驗證載荷。

輸入：目標地址Ta，目標值Tv，參數(shù)偏移Offset

輸出：目標格式化字符串Fs

1.Tv_high=Tv<<16;

2.Tv_low=Tv mod 65536;

3.if Tv_high

4.Fs=(Ta+2)+(Ta)+＂%＂+(Tv_high-8)+＂s＂;

5.Fs +=＂%＂+(Offset) +＂$n%＂+(Tv_low - Tv_high) +＂s%＂+(Offset+1)+＂$n＂;

6.else

7.Fs=(Ta)+(Ta+2)+＂%＂+(Tv_low-8)+＂s＂ ;

8.Fs+=＂%＂+(Offset)+＂$n%＂+(Tv_high-Tv_low)+＂s%＂+(Offset+1)+＂$n＂;

9.end if

10.return Fs;

接下來，會構(gòu)建符號內(nèi)存內(nèi)容與格式化字符串漏洞驗證載荷相等的約束：

若未指定Ta或Tv，默認Ta為當前?？臻g中存儲的EIP值，并在?？臻g內(nèi)布置shellcode，使Tv等于shellcode的地址。但由于格式化字符串漏洞驗證載荷長度受到Ta和Tv的影響，所以無法直接斷定shellcode布置位置，進而無法確定Tv具體數(shù)值。為了解決這一問題，本文采用了啟發(fā)式算法來探尋shellcode的合理布置位置。從符號值的起始位置開始解嘗試，并利用約束求解判斷當前解是否為可行解，從而得到shellcode的合理布置位置，其過程如算法2所示。

2)算法2：啟發(fā)式算法計算shellcode的合理布置位置。

輸入：符號區(qū)域起始位置SymStart, 符號區(qū)域結(jié)束位置SymEnd, Shellcode,格式化字符串Fs

輸出：shellcode布置位置ShellcodeLocal

1.for i = Symstart to SymEnd-len(Shellcode) do

2.Set(Shellcode,SymStart + i);

3.Fs= CalcFs(SymStart + i);

4.Set(Fs,SymStart);

5.if getSymSolution() then

6.return ShellcodeLocal;

7.end if

8.end for

在確定了shellcode的布置位置后，構(gòu)建shellcode布置的約束條件為：

2.3 堆區(qū)及BSS段格式化字符串漏洞驗證約束構(gòu)建

當漏洞函數(shù)的格式化字符串參數(shù)存儲于堆區(qū)及BSS段時，?？臻g無法被直接寫入地址。由于無法向棧空間寫入目標地址，所以2.2節(jié)中的方法在當前情況下失效。目前大多的格式化字符串漏洞自動驗證系統(tǒng)在遇到該情況時，會判定當前的漏洞無法被攻擊者利用，從而給予該漏洞以中低危風險等級。但事實上，這種漏洞仍有可能通過間接方式，達到對目標地址的任意讀寫。

在程序運行時，程序的?？臻g一般不會存在期望修改地址的指針，所以需要一個指向棧地址的指針，間接向?？臻g填入期望修改的地址。而EBP寄存器在程序運行中的作用是將各個函數(shù)調(diào)用串聯(lián)起來，所以EBP指針就是一條存在于?？臻g內(nèi)的指針鏈，因此系統(tǒng)會利用棧下存儲的EBP指針，間接實現(xiàn)任意地址讀寫，如圖4所示。

圖4 堆區(qū)及BSS段格式化字符串漏洞任意地址讀寫方法

若此時目標地址Address的值無法確定，默認通過修改EBP將函數(shù)棧遷移至堆區(qū)及BSS段，并在該部分內(nèi)存區(qū)域構(gòu)建棧內(nèi)存布局，控制程序執(zhí)行流程，如圖5所示。

圖5 棧遷移的流程

通過格式化字符串修改?？臻g內(nèi)存放EBP內(nèi)容的地址，使其指向格式化字符串參數(shù)所在空間，通過2次leave指令后，程序的ESP寄存器會指向該空間，此時程序的棧被遷移到該內(nèi)存空間，隨后的ret指令便會將程序執(zhí)行流程劫持至shellcode處。此時格式化字符串漏洞驗證載荷為“%”+value+“s%”+offset+“$nAAAA”+ShellcodeLocal+shellcode，其中ShellcodeLocal由算法2可得， offset為棧中EBP內(nèi)容存放地址的函數(shù)參數(shù)相對偏移，可由各個函數(shù)棧的EBP成鏈的特點計算得到。

2.4 約束求解

在得到不同類型的格式化字符串漏洞驗證用例約束后，對其進行處理，得到期望的漏洞驗證用例生成的約束。

此時得到的約束由程序運行時的符號執(zhí)行路徑約束CrashConstraints和輸入約束InputConstraints構(gòu)成，當前約束能夠觸發(fā)程序漏洞路徑，但其與第2.2、第2.3節(jié)中最終得到的約束產(chǎn)生了沖突，如下式所示。

(Eq Formatstring0(Read w8 0 buf))∩

(Eq "A" (Read w8 0 buf))

?

因此需要將輸入約束InputConstraints從最終的生成約束中減去，得到約束為：

ExploitConstraints

將最終的約束作為約束求解器的輸入，得到最終的漏洞驗證代碼。

3 實驗

3.1 系統(tǒng)實現(xiàn)

依照上述方法，本文基于S2E[20]實現(xiàn)了格式化字符串漏洞自動驗證原型系統(tǒng)FSAEG，框架如圖6所示。系統(tǒng)利用QEMU[21]進行全系統(tǒng)仿真，對目標程序運行狀態(tài)進行監(jiān)控，利用KLEE[22]實現(xiàn)系統(tǒng)的符號執(zhí)行功能，利用Z3[23]實現(xiàn)約束求解。

圖6 FSAEG系統(tǒng)框架

格式化字符串漏洞自動驗證插件通過監(jiān)控器獲取進程和模塊加載的時刻以及程序運行時的狀態(tài)，并利用獲取到的信息構(gòu)建漏洞自動驗證約束條件，實現(xiàn)漏洞自動驗證。

3.2 實驗驗證

本次實驗的環(huán)境為Linux 32位系統(tǒng)關(guān)閉ASLR、CANARY、NX等漏洞利用緩解機制。實驗宿主機配置為Windows 10、Intel Core i7-9750H@2.60 GHz、32 GB內(nèi)存、虛擬機配置為Ubuntu 16.04、7 GB內(nèi)存。

為了證明系統(tǒng)的有效性，本文以一個典型格式化字符串參數(shù)存儲于?？臻g的漏洞示例FMT-3，來驗證系統(tǒng)在應(yīng)對格式化字符串參數(shù)位于?？臻g時自動驗證的有效性。

FMT-3的代碼如圖7所示。在代碼的13行，存在明顯的格式化字符串漏洞，傳入printf的格式化字符串為可以通過用戶輸入改變的s1，而s1的位置則處在?？臻g內(nèi)。

圖7 FMT-3程序源碼

以2019年BRHG自動化漏洞挖掘競賽格式化字符串漏洞題目A0012來驗證系統(tǒng)在應(yīng)對格式化字符串參數(shù)位于棧以外空間時自動驗證的有效性。

A0012代碼如圖8所示。在代碼的23行，存在明顯的格式化字符串漏洞。傳入printf的格式化字符串為可以通過用戶輸入改變的buff，而buff處于bss段，漏洞函數(shù)調(diào)用前有3次其他函數(shù)調(diào)用。

圖8 BRHG-A0012程序源碼

在實驗結(jié)果上，本系統(tǒng)能夠?qū)ι鲜鍪纠a(chǎn)生漏洞驗證代碼，如圖9、圖10所示，并成功實現(xiàn)漏洞驗證，獲取系統(tǒng)權(quán)限。

圖9 FMT-3漏洞驗證代碼

圖10 BRHG-A0012漏洞驗證代碼

為了對比不同系統(tǒng)之間的性能差異，本文對HEAP-FMT、TEA-FMT程序做了測試，其中HEAP-FMT為格式化字符串參數(shù)存儲于堆空間的格式化字符串漏洞程序，TEA-FMT為帶有tea[24]加密的緩沖區(qū)位于?？臻g的格式化字符串漏洞程序。在對比FSVDTG、CRAX、AFL和本系統(tǒng)后，得到結(jié)果如表2所示。

表2 各系統(tǒng)對不同類型實例測試結(jié)果

針對該實驗結(jié)果分析如下：

1)AFL是模糊測試的常用工具之一，其采用模糊測試技術(shù)對漏洞進行挖掘和測試，能夠發(fā)現(xiàn)程序中格式化字符串漏洞，但是由于在FMT-3實例和BRHG-A0012實例中存在可持續(xù)輸入的循環(huán)結(jié)構(gòu)，導致AFL無法生成測試用例，且其并不支持對漏洞自動驗證功能。

2)CRAX是一種典型的基于符號執(zhí)行的漏洞自動驗證工具，其支持對漏洞產(chǎn)生漏洞驗證代碼，但在判斷格式化字符串時，需要格式化緩沖區(qū)長度大于50，故未能成功檢測FMT-4及HEAP-FMT中的格式化字符串漏洞，此外CRAX只采用了格式化字符串棧中任意讀寫的漏洞驗證模型，所以其不能對緩沖區(qū)位于其他空間的實例進行漏洞自動驗證。

3)FSVDTG是專門針對格式化字符串漏洞進行漏洞測試的工具，其能夠檢測各種格式化字符串漏洞，并對部分程序能夠進行漏洞自動驗證，但是由于其同樣只采用了單一的漏洞驗證模型，所以不能對格式化字符串參數(shù)位于其他空間的漏洞程序進行漏洞自動驗證。

本系統(tǒng)(FSAEG)能夠能夠檢測格式化字符串漏洞，并在格式化字符串參數(shù)位于棧外其他空間時，成功實現(xiàn)漏洞驗證代碼的自動生成，達到其他系統(tǒng)所無法達到的效果。

在此次實驗中，所有系統(tǒng)均無法對含有tea加密的實例TEA-FMT進行漏洞自動驗證，主要原因是符號執(zhí)行中約束求解器的性能瓶頸。

4 結(jié)語

本文總結(jié)了格式化字符串漏洞驗證的相關(guān)原理，并針對現(xiàn)有系統(tǒng)無法解決的參數(shù)位于棧以外內(nèi)存空間的漏洞自動驗證問題，設(shè)計實現(xiàn)了能夠適用于不同參數(shù)存儲位置的格式化字符串漏洞自動驗證系統(tǒng)FSAEG。最后通過實驗驗證了方法的有效性，并與同類方法進行了對比，證實了FSAEG系統(tǒng)能夠有效解決目標問題。但由于符號執(zhí)行本身的路徑爆炸問題，使得符號執(zhí)行并不能解決過于龐大的程序，因此在下一步的工作中，擬采用模糊測試、靜態(tài)分析等手段，輔助符號執(zhí)行，進一步提升系統(tǒng)的自動驗證效果。