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

(國(guó)防科技大學(xué)電子對(duì)抗學(xué)院，合肥，230037)

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

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

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

1 格式化字符串漏洞

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

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

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

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

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

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

表1 常見(jiàn)type類型及其含義

1.2 格式化字符串漏洞

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

2 漏洞自動(dòng)驗(yàn)證方法設(shè)計(jì)

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

圖1 方法核心流程

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

2.1 漏洞存在性檢測(cè)

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

首先對(duì)程序中目標(biāo)危險(xiǎn)函數(shù)進(jìn)行掛鉤操作。當(dāng)測(cè)試程序運(yùn)行至目標(biāo)函數(shù)時(shí)對(duì)其進(jìn)行攔截，并對(duì)目標(biāo)函數(shù)的格式化字符串參數(shù)進(jìn)行判斷，若當(dāng)前參數(shù)取值為符號(hào)值，則表明當(dāng)前函數(shù)的格式化字符串參數(shù)已被系統(tǒng)引入的符號(hào)變?cè)廴荆丛搮?shù)會(huì)被外部輸入污染，從而證明格式化字符串漏洞的存在，反之，則說(shuō)明當(dāng)前函數(shù)不存在格式化字符串漏洞，如圖2所示。

圖2 漏洞存在性檢測(cè)方法

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

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

圖3 ?？臻g格式化字符串漏洞任意地址讀寫方法

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

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

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

(1)

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

1)算法1：計(jì)算格式化字符串漏洞驗(yàn)證載荷。

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

輸出：目標(biāo)格式化字符串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;

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

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

2)算法2：?jiǎn)l(fā)式算法計(jì)算shellcode的合理布置位置。

輸入：符號(hào)區(qū)域起始位置SymStart, 符號(hào)區(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段格式化字符串漏洞驗(yàn)證約束構(gòu)建

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

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

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

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

圖5 棧遷移的流程

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

2.4 約束求解

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

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

(Eq Formatstring0(Read w8 0 buf))∩

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

?

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

ExploitConstraints

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

3 實(shí)驗(yàn)

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

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

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

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

3.2 實(shí)驗(yàn)驗(yàn)證

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

為了證明系統(tǒng)的有效性，本文以一個(gè)典型格式化字符串參數(shù)存儲(chǔ)于?？臻g的漏洞示例FMT-3，來(lái)驗(yàn)證系統(tǒng)在應(yīng)對(duì)格式化字符串參數(shù)位于棧空間時(shí)自動(dòng)驗(yàn)證的有效性。

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

圖7 FMT-3程序源碼

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

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

圖8 BRHG-A0012程序源碼

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

圖9 FMT-3漏洞驗(yàn)證代碼

圖10 BRHG-A0012漏洞驗(yàn)證代碼

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

表2 各系統(tǒng)對(duì)不同類型實(shí)例測(cè)試結(jié)果

針對(duì)該實(shí)驗(yàn)結(jié)果分析如下：

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

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

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

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

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

4 結(jié)語(yǔ)

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