ASLR機制脆弱性自動分析方法*

黃 寧，黃曙光，潘祖烈，常 超

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

隨著信息技術的發展，軟件漏洞的挖掘與利用成了一個熱點問題。針對不同類型的漏洞利用技術，各種保護機制也層出不窮。但是，多年的漏洞利用實踐證明，由于各方面條件的限制，依然存在許多可繞過這些保護機制，成功實施漏洞利用的技術手段[1]。

一般情況下，通過劫持程序控制流，跳轉至指定內存地址，實現任意代碼執行，需要在觸發程序控制流劫持狀態的同時，注入目標內存地址。地址隨機化(Address Space Layout Randomization, ASLR)機制對加載于程序內存空間中的各模塊進行隨機化布局，導致攻擊者無法準確定位目標代碼的內存地址，從而阻止控制流劫持攻擊[2-3]。但是，ASLR依然存在不少局限性[4-5]。受地址隨機化的影響，內存中各模塊的加載地址隨機分布，但各模塊的內部結構依然相對固定，是導致內存信息泄漏的重要原因。

隨著程序分析技術的發展，近年來，出現多種針對二進制程序漏洞自動化分析與測試用例生成技術。早期的漏洞自動利用技術多依賴于對程序漏洞補丁的分析[6-8]。近年來出現了多種針對特殊類型漏洞利用及保護機制繞過的技術方案[9-10]，但仍然缺少一款針對ASLR機制脆弱性進行自動化分析的方案。

文獻[11]提出了基于符號執行的自動化程序漏洞利用(CRash analysis of Automatic eXploit, CRAX)方法。該方法使用選擇性符號執行技術，引導程序運行并觸發控制流劫持狀態，生成控制流劫持點可達的輸入測試用例。該方案的局限性在于，缺少對ASLR影響的分析，導致測試用例難以應用于ASLR環境下。

文獻[12]針對控制流處于有效防御的環境時，提出了面向數據流的漏洞自動分析與利用方案FlowStitch。該方案在不改變程序控制流的前提下，利用已知漏洞，通過構造特殊數據，實現利用代碼自動生成。但是，由于ASLR機制對內存模塊布局的隨機化處理，導致數據流分析無法應用于ASLR脆弱性分析過程。

文獻[13]提出了首個針對Android系統的進行符號執行，實現漏洞自動利用的方案Centaur。該方案著重分析程序控制流狀態變化過程，同時構造漏洞觸發點可達的路徑約束。該方案的局限性在于，未考慮漏洞觸發與控制流劫持狀態間的程序狀態依賴，導致生成的測試用例不能實現控制流劫持攻擊。

為了準確分析漏洞程序能否在ASLR環境下實現控制流劫持攻擊，本文結合已有的漏洞自動分析與利用技術，針對四種內存泄漏場景，提出了一種基于控制流狀態檢測的ASLR脆弱性自動分析方法。

本文首先建立了有限狀態機模型，描述被測程序的動態運行狀態。然后，根據內存泄漏技術特點，篩選出ASLR繞過過程的狀態依賴。在程序有限狀態機模型的基礎上，使用符號執行工具S2E[14-15]實現了地址隨機化脆弱性分析(Address Randomization Vulnerability Analysis, ARVA)系統。原型系統檢查內存泄漏狀態的路徑約束與控制流劫持狀態的路徑約束是否兼容，判斷被測程序是否存在同時滿足上述兩種狀態的路徑。

1 ASLR環境下的程序有限狀態機模型

根據常見的內存泄漏技術特點，結合污點數據傳播和程序動態運行狀態特征，本文提出了一種基于程序狀態變遷的地址隨機化脆弱性分析方法。該方法以上述各程序狀態為分析單元，結合污點數據傳播驅動程序動態運行過程，設計了針對ASLR環境下程序運行狀態的有限狀態機模型，如圖1所示。該有限狀態機(Finite States Machine, FSM)可用式(1)所示五元組進行描述：

M=(U,Σ,T,δ,u0)

(1)

T={S_State,T_State,Event,Constraint,Action}

(2)

式中：S_State和T_State分別表示T的初始狀態和目標狀態；Event表示S_State和T_State狀態變遷依賴的輸入事件，每次狀態變遷依賴的Event屬于Σ中的一個子集；Constraint表示監護條件或事件Event的參數等約束條件；Action表示狀態變遷過程中的執行動作。Action對于狀態變遷過程不是必需的，當條件滿足時，也可以在不執行任何動作的情況下實現程序狀態變遷。

狀態集合U′中各狀態的狀態變遷過程所依賴的事件輸入σ、約束條件c和執行動作a如下：

1)StateInput狀態表示程序從開始接收外部數據(即污點源)，到下一次任意污點數據傳播或約束改變時刻之間的程序狀態。外部輸入事件可視為一種特殊的針對污點數據的操作事件σInput。事件σInput與StateInput狀態轉換的映射關系可如式(3)所示：

UxσInput→T:T_State=StateInput

(3)

由于程序執行過程可能不止一次地觸發事件σInput，且每次觸發事件σInput均會驅動程序進入StateInput狀態，因此事件σInput和事件輸入集合Σ的關系為：{σInput0,…,σInputn}?Σ。

圖1 ASLR環境下程序有限狀態機模型Fig.1 Program finite state machine model in ASLR environment

前置狀態向輸入狀態變遷過程中的執行動作ainput：程序通過輸入功能，將輸入數據寫入內存地址。

2)StateMem是從程序滿足內存泄漏條件的時刻到目標內存信息泄漏時刻間的程序狀態。本文總結了四種典型內存泄漏場景的StateMem狀態依賴條件。

①容錯攻擊[16-17]。

事件輸入σMem：循環執行事件集合EventLoop；內存讀取事件EventReadMem；異常處理操作EventExcept。

集合EventLoop中的元素為二元組(Pos,Event)，其中Pos表示事件Event的執行優先度，Pos越小，優先度越高。

約束條件cMem：{(Pos1,EventReadMem)，(Pos2,EventExcept)}EventLoop∧(Pos1

執行動作aMem：EventLoop集合中的事件根據各自的執行優先級循環執行，直至內存讀取事件EventReadMem讀取目標地址。

②格式化字符串[18]。

事件輸入σMem：調用格式化字符串函數事件EventFormat。

約束條件cMem：格式化字符串函數的格式化控制符參數為污點數據。

執行動作aMem：通過格式化字符串函數輸出目標地址。

③任意地址讀取。

事件輸入σMem：內存讀取事件EventReadMem。

約束條件cMem：事件EventReadMem的讀取對象為帶長度信息的數據結構 ∧(待讀取數據結構長度信息為污點數據 ∨ 待讀取數據結構指針為污點數據)。

執行動作aMem：事件EventReadMem讀取指定內存信息。

④部分地址定位。

事件輸入σMem：返回地址覆蓋事件EventRetCover。

約束條件cMem：事件EventRetCover可通過污點數據覆蓋函數返回地址。

執行動作aMem：覆蓋返回地址的低地址部分。

3)StateHijack表示了程序控制流被劫持時刻的程序狀態。程序處于控制流劫持狀態，可實現任意地址跳轉。

狀態所依賴的事件輸入σHijack：指令指針(Instruction Pointer, IP)寄存器值為污點數據。

約束條件cHijack：目標內存地址已泄漏。

執行動作aHijack：將目標內存地址寫入IP寄存器。

后置狀態：StateShell狀態。

4)任意代碼執行狀態StateShell。該狀態抽象描述了程序開始非法執行一段攻擊者指定的代碼到該段代碼執行結束時刻間的程序狀態?？刂屏鹘俪止舻慕Y果取決于跳轉目的地址的可執行屬性，當且僅當目標地址是可執行的，程序轉入任意代碼執行狀態StateShell，表示控制流劫持攻擊成功。

狀態所依賴的事件輸入σShell：IP寄存器值指向目標內存地址。

約束條件cShell：目標地址內存可執行。

前置狀態S_StateShell：StateHijack狀態。

ASLR環境下，基于內存泄漏的控制流劫持攻擊要求程序狀態集合U′是全體程序狀態集合U的子集。集合U′至少要包含以下幾種狀態：

{StateEntry,StateInput,StateMem,StateHijack,StateShell}?U′

2 原型系統實現

本文使用符號執行技術，實現目標程序動態運行過程中的污點數據跟蹤、程序狀態監測與地址隨機化脆弱性分析等工作。分析工作架構如圖2所示。

圖2 ASLR脆弱性分析架構Fig.2 Structure of ASLR vulnerability analysis system

分析架構通過符號執行組件對動態運行的目標程序狀態進行監視與分析，構造滿足地址隨機化機制繞過的程序狀態約束，并由約束求解器求解約束，生成測試用例。符號執行組件需要三項輸入：可執行文件格式的目標程序，可觸發目標程序內存泄漏狀態的種子輸入以及可觸發控制流劫持狀態的種子輸入。

內存泄漏種子文件為可觸發程序內存泄漏狀態的輸入數據。通過該種子文件，引導程序在動態運行過程中觸發內存泄漏，并收集從入口點到內存泄漏狀態的約束條件，構建目標程序的內存泄漏約束。

控制流劫持種子文件為可觸發目標程序控制流劫持狀態的輸入數據。該過程不考慮ASLR對控制流劫持攻擊的影響。本文將所有由外部傳入目標程序的污點數據標記為符號化數據。目標程序在動態運行過程中，所有被污點數據污染的內存空間或寄存器會被標記為符號化內存或寄存器。通過檢查某一內存地址或寄存器的符號化屬性，可判斷內存地址或寄存器的可控性。

針對目標程序進行分析時，分別通過內存泄漏種子文件和控制流劫持種子文件驅動目標程序動態運行，生成內存泄漏狀態約束ConstraintMem與控制流劫持狀態約束ConstraintHijack。約束求解器求解上述約束間的兼容性，判斷兩者是否具備在同一程序路徑觸發的可能性。當且僅當上述兩種約束滿足式(4)所示關系時，表示兩者互相兼容。

ConstraintMem∧ConstraintHijack=True

(4)

若兩種約束互相兼容，表明目標程序存在至少一條路徑，可同時抵達內存泄漏狀態和控制流劫持狀態，即目標程序滿足ASLR環境下的控制流劫持攻擊條件。

為了降低符號執行對目標程序控制流劫持點檢測的時間開銷，符號執行組件采用了經過路徑選擇算法優化的導向式符號執行技術。以種子輸入作為目標程序的輸入文件，引導目標程序沿著確定的程序路徑動態運行，直至觸發相應的程序狀態。圖3是通過種子輸入引導符號執行觸發相應程序狀態的過程。

符號執行組件用于監視程序動態運行狀態，并分析程序狀態變遷過程是否滿足基于內存泄漏的地址隨機化繞過的依賴條件。在此過程中，符號執行組件收集程序運行的路徑約束，并根據程序狀態，構造滿足狀態變遷條件的數據約束。符號執行組件的工作架構如圖4所示。

符號執行組件對程序狀態分析的過程，是一種面向過程模式的FSM結構實現過程。當程序狀態滿足變遷約束，并觸發狀態變遷操作時，當前狀態(源狀態)執行退出動作。每個源狀態的退出動作由兩部分組成：根據源狀態構造數據約束；根據事件及事件約束選擇目標狀態。源狀態退出動作過程如算法1所示。

(a) 控制流劫持種子驅動程序運行過程(a) Control-flow hijack seed input direct the running path of program

(b) 內存泄漏種子驅動程序運行過程(b) Memory leakage seed input direct the running path of program圖3 種子輸入引導符號執行觸發程序狀態的過程Fig.3 Seed input trigger the program states in symbolic execution

圖4 符號執行組件工作架構Fig.4 Structure of symbolic execution parts

算法1 當前程序狀態(源狀態)退出過程Alg.1 Exit process of current program state (source state)

算法1通過下述操作為程序狀態退出過程建立數據約束：

Constraint=Eq(Value,Addr)

其中：Value為關鍵內存地址在相應的狀態退出過程中需要滿足的條件值；Addr表示約束構建的目標內存地址或寄存器。

完成數據約束構造后，通過事件輸入判斷程序狀態，實現程序狀態變遷邏輯。該過程如算法2所示。

3 實驗評估

本文使用S2E作為原型系統ARVA的符號執行引擎，針對快速模擬器(Quick EMUlator, QEMU)下運行的目標程序及其系統環境進行全系統模擬的基礎上，實現程序狀態監測與ASLR脆弱性分析。本文選取了8個實際的漏洞利用攻擊樣本對ARVA原型系統進行評估。實驗中，原型系統運行在配備了3.40 GHz Intel Core i7-6700 CPU、8 GB 內存、250 GB 硬盤的計算機上。

算法2 程序狀態變遷過程Alg.2 States conversion process

目標程序與系統均運行于QEMU虛擬機中，各樣本的漏洞編號、運行環境與目標程序如表1所示。

表1 實驗樣本信息Tab.1 Information of experimental sample

3.1 ASLR脆弱性分析結果

本文選取了近年來影響較大的控制流劫持攻擊漏洞，對ARVA原型系統及其理論的有效性進行驗證評估。實驗中，內存泄漏種子文件觸發各樣本程序內存泄漏狀態信息如表2所示。

表2中，ASLR環境表示樣本程序的依賴系統對程序內存空間的隨機化效果。由于早期的Windows系統未設置ASLR機制，因此樣本程序不受地址隨機化的影響。Windows XP系統的ASLR機制只能實現堆棧等部分內存空間的隨機化效果，本文將該環境稱為部分隨機化環境。在Windows 7以后的系統中，ASLR機制基本實現了針對全部內存空間的隨機化效果，本文將實現這一效果的隨機化環境稱為整體隨機化環境。最終泄漏目標地址表示內存泄漏種子文件引導樣本程序執行至最后一次內存泄漏狀態時，泄漏的目標地址。

由控制流劫持種子文件觸發各程序控制流劫持狀態信息如表3所示。

表3中，控制流劫持目標地址表示樣本程序進入控制流劫持狀態時，下一指令的跳轉目的地址；目標跳轉指令為該目的地址處對應的匯編指令；控制流劫持攻擊類型表示樣本程序在控制流劫持種子文件驅動下執行的攻擊類型。

表4列舉了各樣本程序從初始狀態到控制流劫持狀態變遷過程中，StateMem狀態的觸發次數以及每次觸發該狀態時泄漏的內存信息。

根據表2、表3與表4的信息，僅MS-06-055與CVE-2010-3333的控制流劫持攻擊選用了覆蓋返回地址的方式。原因如下：

1)Windows 2000未設置任何地址隨機化機制。MS-06-055的控制流劫持種子可通過JavaScript實現堆噴射布局shellcode以及固定值0×0c0c0c0c覆蓋返回地址，導致任意代碼執行。這一過程不涉及內存泄漏。

表2 樣本程序內存泄漏狀態信息Tab.2 Information of memory leakage of experimental sample

表3 樣本程序控制流劫持狀態信息Tab.3 Information of control-flow hijack of experimental sample

表4 基于內存泄漏的樣本程序狀態變遷過程Tab.4 States conversion of memory leakage of experimental sample

2)Windows XP SP3設置了針對堆棧等部分內存區域的地址隨機化。CVE-2010-3333實驗中，控制流劫持種子將Shellcode布局于棧內存中。但由于堆棧隨機化影響，需要通過跳板指令jmp esp確定棧內存的位置(即定位?？臻g地址的前四位)。Office 2003中，存在不受隨機化影響的地址0x7d1f5fb7固定為jmp esp指令。當程序處于控制流劫持狀態時，將返回地址覆蓋為0x7d1f5fb7，執行跳板指令后，可定位?？臻g前四位地址，驅動樣本程序開始執行棧內存中的Shellcode，觸發任意代碼執行狀態。

CVE-2014-0322、CVE-2015-3090、CVE-2015-5119與CVE-2015-5122實驗分別驗證了整體隨機化環境下的漏洞可利用性。上述漏洞均可通過Action Script腳本觸發IE的Flash插件漏洞并實現漏洞利用。本文分別選取Kernel32.dll與Flash32.dll模塊作為最終內存泄漏目標。內存泄漏種子文件可覆蓋Flash Vector數組長度，導致任意內存讀寫。上述樣本程序中，基于容錯攻擊的CVE-2014-0322觸發了一次內存泄漏狀態；其余樣本至少觸發兩次以上內存泄漏狀態。

與其他實驗相比，CVE-2014-6332實驗涉及特殊的IE瀏覽器沙盒機制。本文針對該機制構造的控制流劫持種子文件在觸發樣本控制流劫持狀態后，不會轉入匯編指令層面的任意代碼執行狀態?？刂屏鹘俪址N子文件通過將IE瀏覽器安全標志置于位置0，使用VBScript腳本可調用系統的任意功能。該攻擊方法被稱為數據虛擬執行DVE。

根據表4的信息，除MS-06-055實驗不涉及ASLR環境外，其余各實驗的內存泄漏約束與控制流劫持約束的判定結果均為互相兼容。該結果表明，這些實驗樣本均至少擁有一條程序路徑，同時滿足內存泄漏和控制流劫持的條件。在此路徑下，ASLR機制可被繞過。

上述實驗表明， ARVA原型系統可有效識別部分地址定位、容錯攻擊、任意地址讀寫等內存泄漏狀態，以及覆蓋返回地址、ROP、ret-to-libc等控制流劫持類型。另一方面，ARVA通過求解內存泄漏狀態約束與控制流劫持狀態約束，可判斷兩者的約束是否兼容。實驗結果表明，基于內存泄漏的ASLR繞過過程中，可能需要觸發不止一次內存泄漏狀態，才能非法獲取目標內存信息。

3.2 案例分析

本文挑選了CVE-2014-6332案例來對ARVA的檢測過程與效果進行詳細闡述。此漏洞利用任意地址讀寫實現ASLR繞過；通過DVE，Heap Spray等攻擊技術實現控制流劫持。本文的系統能準確識別樣本程序的內存泄漏狀態與控制流劫持狀態，構造并判斷兩種狀態約束的兼容性。

案例CVE-2014-6332漏洞程序ASLR脆弱性分析。此漏洞是一個整數溢出漏洞。該漏洞可通過篡改IE瀏覽器的安全模式標志位，繞過瀏覽器沙盒保護，進而導致腳本文件獲取任意功能執行權限。

CVE-2014-6332實驗的種子文件為VBScript腳本文件。其中，內存泄漏種子輸入的目標為：引導漏洞程序在ASLR環境下準確定位IE安全模式標志位的地址；控制流劫持種子文件的目標為：引導漏洞程序執行任意功能。

IE瀏覽器通過OLEAUT32.dll對VBScript中的數組進行管理。假設有數組arr，其初始長度為a0；后又將數組arr的長度更改為a1=a0+0×80000000，OLEAUT32將根據a1-a0=0×80000000計算數組arr的新索引值。由于0×80000000被系統默認為有符號整數，換算成十進制數為0，因此數組arr的實際大小仍為a0。此時，通過arr的索引值，可實現越界讀寫。

內存泄漏種子文件觸發的程序狀態變遷過程為：

StateInput狀態：向進程內存中布置兩個錯位分布的污點數據數組arrA與arrB。兩個數組在內存中的布局如圖5所示。

圖5 數組arrA與arrB結構分布Fig.5 Layout of arrA and arrB

構建數據約束：Constraint1=Eq(arrA, &arrA)∧Eq(arrB, &arrB)。

VBScript語言的數據存儲時，每個數據都占據16字節，其中，前8個字節表示數據類型，后8個字節表述數據值。

StateInput狀態：通過種子文件布局一個sub類型函數func，并將函數地址&func存儲于arrA(a1)。

構建數據約束：Constraint2 =Eq(&func, &arrA(a1))。

StateInput狀態：typeof(&func)= 0x1(NULL類型)。構建數據約束Constraint3=Eq(0x1, &arrA(a1-1))。

StateInput狀態：arrB(2) =1.740 885 347 313 24E-310(arrB(2)數據值=arrA(a1+2)類型值= 0×200C)。

構建數據約束：Constraint4=Eq(1.740 885 347 313 24E-310, &arrB(2))。

StateInput狀態：布局Safe Array型數組myArr起始地址為0×0，包含0×7ffffff0個元素，每個元素大小為1 Byte。

構建數據約束：Constraint5=Eq(myArr, &myArr)。

StateInput狀態：arrA(a1+2)=&myArr。

構建數據約束：Constraint6=Eq(&myArr,arrA (a1+2))。

檢查任意地址讀取類型依賴的約束條件，數組arrA滿足下述條件：

數組arrA帶長度信息的數據結構∧數組arrA長度信息a1為污點數據。

因此，ARVA判斷數組arrA滿足任意地址讀取的觸發條件。

StateMem狀態：利用arrA數組越界讀寫泄漏&func+ 12處CScriptEntryPoint對象指針。

構建數據約束：Constraint7=Eq(&CScriptEntryPoint, &func+ 12)。

StateMem狀態：泄漏&CScriptEntryPoint+20處COleScript對象指針。

構建數據約束：Constraint8=Eq(&COleScript, &CScriptEntryPoint+20)。

StateMem狀態：泄漏&COleScript+0×174處的IE安全模式標志位地址。

構建數據約束：Constraint9=Eq(& SecurityBit, &COleScript+0×174)。該地址在正常權限下僅可通過Safe Array數組進行寫操作。

StateInput狀態：myArr[&SecurityBit]=0。

構建數據約束：Constraint10=Eq(0,myArr[&SecurityBit])。

內存泄漏的路徑約束構建過程中，共觸發6次StateInput狀態，3次StateMem狀態，并在觸發StateMem狀態時針對狀態依賴的事件輸入與約束條件進行了1次檢查。

ARVA在該過程中建立的污點源數據約束如式(5)所示。

srcConstraint=Constraint1∧Constraint2∧

Constraint3∧Constraint4∧

Constraint5∧Constraint6∧

Constraint10

(5)

ARVA建立的內存泄漏數據約束如式(6)所示。

memConstraint=Constraint7∧Constraint8∧

Constraint9

(6)

當該漏洞程序處于任意代碼執行狀態StateShell時，指定的代碼為VBScript腳本文件中任意功能調用代碼。由于DVE利用技術的特殊性，可認為該案例中的控制流劫持狀態StateHijack與StateShell是同時觸發的?？刂屏鹘俪址N子文件觸發的程序狀態變遷過程為：

StateHijack狀態：ShellExecute “cmd.exe”。

CVE-2014-6332的最終數據約束如式(7)所示：

dataConstraint=ConstraintMem∧ConstraintHijack

=srcConstraint∧memConstraint∧ConstraintHijack

(7)

其中，ConstraintHijack因不涉及IP寄存器的污點傳播，其默認值為True。求解約束dataConstarint值為True，表示內存泄漏約束ConstraintMem與控制流劫持約束ConstraintHijack兼容，因此可得出結論，CVE-2014-6332可通過內存泄漏繞過地址隨機化，實現控制流劫持攻擊。

3.3 時間開銷分析

在原型系統ARVA中，測量時間t1定義為內存泄漏種子輸入驅動樣本程序開始運行，至求得內存泄漏約束所用時間；t2定義為控制流劫持種子輸入驅動程序開始運行，至求得控制流劫持約束所用時間。同時，本文也在原生S2E系統中，以結合了ASLR繞過和控制流劫持功能的腳本文件為輸入，運行同樣的樣本程序，并記錄樣本程序的運行時間t′。具體數據如圖6所示。

圖6 ARVA與原生S2E運行時間開銷對比Fig.6 Comparison of running time of ARVA and S2E

根據圖6數據，MS-06-055不涉及地址隨機化繞過，ARVA針對其控制流劫持約束求解時間t2大于S2E的運行時間。CVE-2010-3333的使用部分地址定位，內存泄漏約束求解過程與控制流劫持約束求解過程基本一致，兩者的時間t1與t2基本相等，與S2E的運行時間t′也基本持平。

CVE-2012-1876、CVE-2014-0322、CVE-2014-6332、CVE-2015-3090、CVE-2015-5119與CVE-2015-5122等實驗時間開銷基本呈現下述兩種特點：t1>t′>t2；t1+t2≈2t′。

上述特點說明，ARVA針對樣本程序的地址隨機化脆弱性檢測的時間開銷主要集中于內存泄漏約束的構建與求解方面。

此外，由于ARVA的控制流劫持約束求解過程不考慮地址隨機化對樣本程序的影響，而原生S2E系統在運行同一樣本程序時，種子文件結合了地址隨機化繞過與控制流劫持兩方面功能，導致ARVA的控制流劫持約束求解時間t2小于S2E運行時間t′。

4 結論

本文提出了一種基于有限狀態機的ASLR機制脆弱性分析方法。該方法能夠分析目標程序是否可通過內存泄漏技術繞過ASLR保護，實現控制流劫持攻擊。本文使用有限狀態機模型描述程序狀態變遷過程，分析通過內存泄漏導致ASLR繞過的程序狀態依賴，在此基礎上，針對四種常見的內存泄漏場景分別建立了內存泄漏狀態的進入與退出條件，使該模型更好地適用于不同的漏洞攻擊模式。根據上述理論與模型，本文實現了一套基于符號執行工具S2E的ASLR脆弱性分析原型系統ARVA。該系統針對目標程序的內存泄漏狀態與控制流劫持狀態分別進行約束構建，并對二者的兼容性進行求解，檢查目標程序是否滿足地址隨機化環境下實施控制流劫持攻擊的條件。通過對若干實際漏洞程序的實驗表明，本文方法能夠準確檢測到被測程序的動態運行狀態，求解相關程序狀態約束，并有效識別ASLR環境下漏洞程序的可利用性。