System Service Call-oriented Symbolic Execution of Android Framework with Applications to Vulnerability Discovery and Exploit Generation

用於Android框架與應用程式的面向系統服務呼叫的符號執行來進行漏洞發現和漏洞利用生成

概要

Android應用程式框架上的一個漏洞可以被利用導致大規模的網路攻擊，並對使用者的安全和隱私造成嚴重的危害，然而現在大多數現有研究僅限於分析Android應用程式，而很少有開發用於分析Android框架的技術和工具。文獻提出了第一個用於Android框架的符號執行系統，Centaur。為了避免由於複雜的初始化而導致狀態空間爆炸問題，提出了分階段的從具體執行到符號執行（PC2SE），在初始化階段執行具體執行，為符號執行提供執行上下文。而在執行上下文中存在大量的變數，微小汙染分析（slim tainting）跟蹤特徵訪問模式，用以識別從惡意應用程式到出的變數，並作為符號輸入。為了實現解耦設計，將符號執行器從Android中分離出來，將具體執行提供的執行上下文從Android ART程序遷移到Java VM。最後文章對這個系統進行了評估，評估表明Centuar在漏洞發現和漏洞利用方面都非常有效。

問題與解決方案

問題：現有的研究大多侷限於分析Android應用程式，很少有技術和工具是為分析Android框架而研發的，且先前的工作中沒有通過符號執行來分析Android框架的。本文的動機是填充這方面的空白。

解決方案：設計開發出一個能夠實現對Android框架的程式碼進行符號執行的系統（Centaur），然後根據給出的利用Android框架的新型攻擊的描述，將系統應用於準確和自動地查詢零日漏洞例項，並生成PoC漏洞以驗證結構。

方案難點

由於Android框架的中介軟體性質和複雜性會導致以下難點：

難點1：Android框的初始化階段很複雜，如果符號執行從main入口進行，會導致路徑爆炸問題，如果跳過初始階段，直接分析一個服務介面方法，會導致上下文資訊（比如變數的型別和值）丟失，如何處理上下文資訊丟失是一個難題。
解決方案：採用一種結合具體執行和符號執行的分析方案，提出了PC2SE，先執行初始化階段作為全系統的具體執行，然後根據具體執行提供的執行上下文，從中介軟體的一個入口點方法開始執行符號執行。

難點2：Android應用程式框架包含了大量為系統服務和應用程式儲存的資料結構，而給定的一個惡意軟體派生出來的變數以物件欄位和陣列元素的形式散佈在眾多的資料結構中，難點在於如何在大量複雜的資料結構中識別來自呼叫應用程式的變數，並作為符號輸入。

傳統解決方法：為確定指定app派生出來的變數，傳統方法是通過汙點分析追蹤從app到Android框架的資訊流，但是這樣非常複雜，且現存的汙點分析方法只能追蹤指定的系統服務呼叫流返回的資訊，而不是從整個app應用層次來分析，且分析結果不精確。

解決方案：不是跟蹤資訊從應用程式流向框架的方式，而是假設當框架服務app呼叫時存在用於訪問app特定資訊的固定模式（基於陣列的變數使用索引來獲取app的資訊，基於雜湊表的變數使用包名作為訪問元素的關鍵），根據這個模式如何在系統服務呼叫時訪問app特定變數，設計一個稱為微小汙染的汙點分析方法，在路徑探索過程中精確和自動地確定app特定變數，並作為符號輸入識別。

難點3：如果將符號執行引擎放在Android系統中，雖然可以使分析器利用主機執行環境，但是這樣使得符號執行器的實現變得非常複雜，且由於各種不相容問題使系統變得脆弱而難以除錯同時耦合性高，如何設計實現可以利用Android執行環境而不會導致複雜的和耦合的架構是一個難題。

解決方案：提出一種解耦設計的新型架構，適用於PC2SE，通過在Android系統外構建符號執行引擎，但是仍然能夠利用Android執行環境。該系統的創新和關鍵元件是將Android中生成的資訊（如類和物件）遷移到符號執行環境。

符號執行

符號執行適合漏洞發現的原因：

1、  能夠有效和自動地探索所有可能的路徑，能夠發現儘可能多的漏洞例項

2、  對於探索的每個路徑，記錄描述路徑被採用時輸入值應該滿足的條件的符號表達式，即路徑條件

Slim Tainting

由汙染源（taint sources）、汙染傳播邏輯（taint propagation logic）、汙染池（taint sinks）組成

如何確定符號輸入：

首先通過應用程式的唯一標識UID或者包名作為汙染源，然後根據汙染傳播邏輯傳播，最後通過get函式將通過被汙染的索引訪問到的元素設定為符號輸入。

Centaur的體系架構

在Android系統上執行具體執行，Android系統和符號執行引擎之間的執行上下文查詢伺服器用於將上下文資訊從Android中移植到符號執行引擎

執行上下文移植

只有執行上下文中的堆（類和物件的集合）需要被移植

Snapshot：快照，執行上下文中的堆記憶體映像。

● 移植快照中捕獲的堆資訊需要解決的三個問題：

1、  如何獲得快照中位和位元組的語義

2、  在符號執行過程中如何進行移植

3、  如何引導移植

● 移植演算法存在的問題與解決方案

存在的問題：對於引用型別欄位，深層複製太低效，而對於簡單的淺層複製，引用值將因其只顯示具體執行環境中物件的位置（快照捕獲的地方）而不起作用

解決方案：選擇一個變形的簡單的淺層複製，當移植物件時，簡單地複製所有的欄位值，但是對於每個引用型別欄位，標記它為對具體執行環境中的一個引用值，然後當使用這種引用型別欄位中的來訪問目標物件時，目標物件將被移植，或者如果目標物件已經被移植則在符號執行環境中將這個欄位值用這個引用值更新。

● 雜湊表conc2Sym：將具體執行環境中的引用值對映到符號執行環境中的引用值●

維護雜湊表的目的：1、防止物件的重複移植  2、將存在在雜湊表中的具體執行環境中的引用值轉為符號執行環境中的引用值

● 如何移植一個物件

1、  如果物件是字串，則演算法現在虛擬機器的執行時常量池中搜索具有相同值的字串已進行符號執行，如果沒找到則在符號執行環境中建立一個具有相同值的新字串

2、  如果物件是陣列，則會分配一個數組將所有元素複製到新陣列中。因為該演算法是淺拷貝，所以如果是多維陣列，只複製頂層陣列中的元素，當要呼叫其他元素時必須呼叫aaload指令，這也是為了移植多維陣列而改寫aaload的解釋的原因。由於淺拷貝在訪問物件的引用前不會複製陣列物件。

3、  對於普通物件，通過分配一個新物件並複製所有欄位來處理。

引導欄位

對引導欄位的訪問能夠觸發第一個物件的移植。引導欄位位於測試驅動程式類中，它是對包含入口點方法的系統服務類的呼叫。下圖為移植一個堆的例子

可疑漏洞的驗證

傳統的驗證方法：用基於可達性分析的靜態分析來查詢ISPE bugs可能會導致假陽性，由於一些路徑在實際執行中是不可行的。目前，主要是通過人工檢查每條報告路徑的程式碼，但是這樣是費力且乏味的，也難以驗證手動檢查結果的正確性。

本文的解決方法：結合靜態分析和符號執行來查詢ISPE bugs。對於靜態分析報告的每個可疑漏洞，Centaur：（1）找到能到達敏感操作的所有可行路徑（2）給出每個可行路徑所需的許可權（3）驗證可行路徑之間的許可權一致性（4）生成執行可行路徑的輸入來驗證可疑漏洞

貢獻

1、  第一個支援Android框架的符號執行系統，提供了一種在Android框架中自動和精確探索路徑的方法，可以潛在地應用於其他複雜中介軟體的符號執行。

2、  分別分析中介軟體的服務介面方法，大大提高可擴充套件性同時提供了完整的執行上下文。

3、  提出了一種新穎的汙染分析技術來精確識別從給定的app出來派生的框架變數。

4、  在Android系統外構建符號執行器，設計出將執行上下文資訊從Android遷移到符號執行器的強大演算法。

不足

1、Centaur只能執行Java程式碼的符號執行

PS：如果本人關於Centaur的理解有誤，歡迎指出，我將及時更正。另外文中圖片來自於文獻截圖~