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

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

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

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

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

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

1 格式化字符串漏洞

1.1 格式化字符串參數

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

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

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

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

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

表1 常見type類型及其含義

1.2 格式化字符串漏洞

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

2 漏洞自動驗證方法設計

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

圖1 方法核心流程

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

2.1 漏洞存在性檢測

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

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

圖2 漏洞存在性檢測方法

2.2 棧空間格式化字符串漏洞驗證約束構建

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

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

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

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

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

(1)

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

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

輸入：目標地址Ta，目標值Tv，參數偏移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;

接下來，會構建符號內存內容與格式化字符串漏洞驗證載荷相等的約束：

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

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

輸入：符號區域起始位置SymStart, 符號區域結束位置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的布置位置后，構建shellcode布置的約束條件為：

2.3 堆區及BSS段格式化字符串漏洞驗證約束構建

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

在程序運行時，程序的棧空間一般不會存在期望修改地址的指針，所以需要一個指向棧地址的指針，間接向棧空間填入期望修改的地址。而EBP寄存器在程序運行中的作用是將各個函數調用串聯起來，所以EBP指針就是一條存在于棧空間內的指針鏈，因此系統會利用棧下存儲的EBP指針，間接實現任意地址讀寫，如圖4所示。

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

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

圖5 棧遷移的流程

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

2.4 約束求解

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

此時得到的約束由程序運行時的符號執行路徑約束CrashConstraints和輸入約束InputConstraints構成，當前約束能夠觸發程序漏洞路徑，但其與第2.2、第2.3節中最終得到的約束產生了沖突，如下式所示。

(Eq Formatstring0(Read w8 0 buf))∩

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

?

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

ExploitConstraints

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

3 實驗

3.1 系統實現

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

圖6 FSAEG系統框架

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

3.2 實驗驗證

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

為了證明系統的有效性，本文以一個典型格式化字符串參數存儲于棧空間的漏洞示例FMT-3，來驗證系統在應對格式化字符串參數位于棧空間時自動驗證的有效性。

FMT-3的代碼如圖7所示。在代碼的13行，存在明顯的格式化字符串漏洞，傳入printf的格式化字符串為可以通過用戶輸入改變的s1，而s1的位置則處在棧空間內。

圖7 FMT-3程序源碼

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

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

圖8 BRHG-A0012程序源碼

在實驗結果上，本系統能夠對上述示例產生漏洞驗證代碼，如圖9、圖10所示，并成功實現漏洞驗證，獲取系統權限。

圖9 FMT-3漏洞驗證代碼

圖10 BRHG-A0012漏洞驗證代碼

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

表2 各系統對不同類型實例測試結果

針對該實驗結果分析如下：

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

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

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

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

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

4 結語

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