面向Android應用的靜態污點分析結果的正確性驗證

秦彪 郭帆 涂風濤

摘 要：應用靜態污點分析檢測Android應用的隱私泄露漏洞會產生許多虛警，為此提出一種上下文敏感、路徑敏感和域敏感的半自動程序分析方法，僅需遍歷少量執行路徑即可判定漏洞是否虛警。首先，運行插樁后的應用來獲得一條覆蓋Source和Sink的種子Trace。然后，應用基于Trace的污點分析方法來驗證Trace中是否存在污點傳播路徑，

是則表明漏洞真實存在;否則進一步收集Trace的條件集合和污點信息，結合活變量分析和基于條件反轉的程序變換方法設計約束選擇策略，以刪除大部分與污點傳播無關的可執行路徑。最后，遍歷剩余執行路徑并分析相應Trace來驗證漏洞是否虛警。基于FlowDroid實現原型系統，對DroidBench的75個應用和10個真實應用進行驗證，每個應用平均僅需遍歷15.09%的路徑，虛警率平均降低58.17%。實驗結果表明該方法可以較高效地減少靜態分析結果的虛警。

關鍵詞： 程序驗證;污點分析;活變量分析;程序變換;路徑敏感

中圖分類號：TP311.53

文獻標志碼：A

Abstract： Many false positives are generated when an Android application is detected by? static taint analysis to discover potential privacy-leak bugs. For that， a context-sensitive， path-sensitive and field-sensitive semi-auto analysis method was proposed to verify if a potential bug is a true positive by only traversing a few executable paths. Firstly， a seed Trace covering both Source and Sink was obtainedmanually?by running the instrumented application. Then， a Trace-based taint analysis method was used to verify if there was a taint propagating path in the Trace. If there was a taint propagating path， it meaned a real privacy leak bug existed. If not， the conditioin set and taint information of the Trace were further collected， and by combining the live-variable analysis and the program transformation approach based on conditional inversion， a constraint selection policy was designed to prune most executable paths irrelevant to taint propagation. Finally， remaining executable paths were traversed and corresponding Traces were analyzed to verify if the bug is a false positive. Seventy-five applications of DroidBench and ten real applications were tested by a prototype system implemented on FlowDroid. Results show that only 15.09% paths traversed averagely in each application， the false positive rate decreases 58.17% averagely. Experimental results demonstrate the analysis can effectively reduce the false positives generated by static taint analysis.Key words：? program verification; taint analysis; live-variable analysis; program transformation; path sensitive

0 引言

隨著智能手機的普及，Android應用的安全性備受關注。隱私泄露是Android手機最嚴重的安全問題之一，它是指應用程序中存在一條從讀取隱私數據的Source方法調用語句到送出隱私輸出的Sink方法調用的執行路徑，并且未經用戶許可。污點分析是檢測隱私泄露的主流檢測方法之一，它從Source開始跟蹤外部引入的數據（污點），檢查它們是否未經驗證就直接傳播到Sink位置，如果是則可能存在漏洞。

污點分析分為靜態分析和動態分析。靜態分析不運行代碼，直接對代碼或者轉換后的中間代碼掃描，提取其中的詞法、語法和語義，結合控制流分析和數據流分析，判定污點是否能從Source傳遞到Sink[1]。靜態分析可靠性高，但是需要耗費大量資源并且時間性能較差，為了實現精度和效率的平衡，往往會對所有分支的數據流信息進行保守的合并，從而產生大量虛警。動態分析指插樁并監控程序運行時行為，動態獲取程序的控制流和數據流，實時跟蹤污點傳播，在Sink位置檢測是否有污點信息輸出[1]。動態分析的精確度高，但是動態分析難以覆蓋程序的所有可執行路徑，會遺漏許多潛在漏洞，可靠性不高。

為了降低靜態分析的虛警率，研究人員提出了不少方案，主要分為基于約束求解[2-4]和基于機器學習[5]兩類。約束求解常常與控制流分析和動態符號執行（Dynamic Symbolic Execution， DSE）技術相結合，在收集執行路徑約束集合后，使用可滿足性模理論（Satisfiability Modulo Theories， SMT）求解器判定路徑是否可行，進而驗證是否虛警。然而在實際應用中，路徑條件復雜多變，約束求解存在約束表達困難和無法獲得正確解的問題，導致虛警驗證失敗。機器學習通過統計方法或神經網絡分析真實報警和虛警之間的特征差異，但是存在虛警驗證錯誤的問題。

本文提出一種路徑敏感、上下文敏感和域敏感的半自動分析方法，可以高效可靠地驗證靜態污點分析結果的正確性，在插樁和運行應用獲得覆蓋Source和Sink的運行Trace后，結合程序插樁、基于Trace的污點分析、活變量分析和程序變換方法，對程序的執行路徑集合進行剪枝和遍歷，進而驗證分析結果是否虛警，針對DroidBench和真實應用的實驗結果表明了該方法的有效性。

1 相關工作

靜態分析技術是檢查程序漏洞的有效手段，它通過靜態掃描程序來找到匹配規則模式的代碼從而發現代碼中的問題。靜態分析往往采用基于近似的分析方法，其分析結果不夠精確，所以大多數靜態分析工具生成的控制流圖存在許多不確定性，如弱類型檢查、未定義的行為以及別名指針等。根據Rice定理[6]，靜態分析針對程序的任何非平凡屬性（例如程序是否存在數組越界），無法做到既完備又可靠，導致靜態分析結果存在誤報和漏報[2]。

國內外學者為消除靜態分析結果中的誤報，提出了不同的解決方法并進行大量的研究工作，設計和實現了各種靜態漏洞檢測工具。

王蕾等[5]認為惡意應用的多個Source之間的相關性與正常應用存在差異，提出一種分析結果中的多個Source是否綁定觸發Sink的污點分析技術，利用這種差異可以降低虛警率。趙云山等[2]以靜態分析的結果作為輸入，逆向搜索可能發生缺陷的約束條件，使用約束求解判斷缺陷的可滿足性，進而驗證結果是否虛警。李筱等[3]對目標程序進行控制流分析，判斷警報的可達性并得到制導信息，再利用混合執行測試的方法，跟蹤程序運行時內存狀態并判斷內存是否泄漏，驗證漏洞是否虛警。AppIntent[7]從可疑敏感數據泄露路徑中抽取事件處理方法集合，形成事件處理方法約束圖，并根據約束條件產生用戶輸入，驗證該路徑是否是用戶許可的路徑，從而排除虛警。DyTa[4]是一種自動漏洞檢測工具，它的檢測過程分為靜態和動態兩個階段，靜態階段中利用靜態檢測技術發現程序的潛在漏洞;動態階段中通過動態符號執行（DSE）技術生成測試用例，以新的測試用例執行被測程序來驗證靜態階段中發現的漏洞是否真實存在。

TASMAN[8]基于動態符號執行技術，結合污點分析收集程序控制流圖的路徑約束，通過SMT求解器[9]計算路徑約束的可滿足性以判斷路徑是否可行，過濾掉不可行路徑中的警報來消除誤報。

Fuzzing測試[10]和動態符號執行是兩種對程序安全進行動態測試的主流技術，經典Fuzzing測試使用隨機產生的程序輸入，會導致路徑覆蓋率較低，無法發現復雜執行路徑中潛在的漏洞。Cai等[11]結合符號執行的優點，搜索更多目標問題的執行路徑，從而提高代碼覆蓋率，同時運用污點分析檢測每條路徑，并用依賴路徑的污點信息指導Fuzzing測試生成相關的測試用例，以此發現程序內的問題。T-Fuzz[12] 采用程序變換技術刪除被測程序中復雜的完整性檢查過程，從而暴露目標程序的潛在漏洞，然后跟蹤觸發漏洞的執行過程信息，收集源程序的路徑約束，判斷它們的可滿足性以消除誤報。

動態符號執行技術存在路徑爆炸問題，為此業界提出了不同的路徑搜索算法，通過選擇策略覆蓋關鍵路徑，其中最具代表性的是SAGE系統[13]。它設計了代搜索（generation search）算法，使用啟發式搜索策略，對搜集到的路徑條件中的分支約束依次進行取反求解，生成新用例并將它們依次執行然后統計代碼覆蓋率，依據代碼覆蓋率為各新用例打分，接著在符號執行過程中選取打分高的用例執行，然后重復上述過程。代搜索雖然有利于提高代碼覆蓋率、緩解路徑爆炸問題，但是打分過程開銷大，影響了算法的性能。另外，DyTa在動態階段，采用文獻[14]方法，根據靜態階段獲得的信息指導DSE搜索程序的路徑，并使用靜態發現潛在缺陷的定位技術，對與反轉不相關的分支節點進行剪枝，從而使DSE過程更高效。約束求解是動態符號執行的必要過程，但是現有求解器無法求解所有約束，同時求解器的運行效率較低導致動態符號執行的效率低下。本文提出一種驗證污點分析結果正確性的半自動方法，首先插樁并手工運行Android應用獲得一條覆蓋Source和Sink的Trace。接著對Trace進行污點分析判定是否存在從Source到Sink的污點傳播路徑，是則驗證結果正確;否則收集Trace的條件約束和污點信息，結合活變量分析和程序變換[12]的方法設計約束選擇策略，對可行路徑集合進行剪枝和遍歷，判定是否存在污點傳播路徑，進而驗證分析結果是否虛警。該方法沒有采用動態符號執行生成測試用例，而是使用程序變換技術將程序中的條件約束逐一取反，生成變換后的程序并按照原有執行動作重復執行，進而獲得其他執行路徑信息，從而有效提高路徑覆蓋率。

2 半自動驗證方法

本文方法的總體結構如圖1所示，其執行流程如下：

1）被檢測的APK靜態插樁，生成新的.dex文件，使轉換后的Android應用在執行時能夠記錄程序的執行路徑信息（Trace）。

2）將新生成的.dex文件打包成插樁后的APK，

并安裝到Android模擬器或真機中。

3）在保證程序執行時能同時覆蓋Source和Sink的前提下，手工執行插樁后的Android應用并記錄執行時的操作序列（events），得到程序執行結束后的Trace，即種子Trace。

4）分析模塊對種子Trace進行別名分析和污點分析，獲得程序執行過程中的運行時信息。

5）根據污點分析結果，如果發現一條從Source到Sink的污點傳播路徑，則整個驗證過程結束，報告缺陷真實存在;否則，遍歷Source與Sink之間的所有其他可能的執行路徑，并對遍歷過程中產生的每一條Trace進行污點分析，判斷其中是否存從Source到Sink的未經驗證的污點傳播路徑，如果存在則停止遍歷，驗證結束并報告缺陷真實存在。

6）直到遍歷完所有路徑后都沒有發現一條從Source到Sink的污點傳播路徑，則結束驗證過程，報告該缺陷是虛警。

2.1 污點分析

手工執行經插樁的Android應用獲得的種子Trace本質上是一條順序的代碼序列，污點分析的目標是根據Trace中的信息分析它記錄的每條指令處的全局污點信息。Java定義的變量都是以引用的形式標識程序運行時具體的內存位置，因此會有不同變量指向同一塊內存空間，即它們互為別名，污點分析必須建立在準確的別名信息基礎之上。 Android應用存在大量的方法調用，特別是事件觸發的回調方法和注冊監聽組件事件的處理方法，在進行別名分析之前需要收集Trace中的方法調用現場信息，包括發生方法調用的位置信息和實參與形參之間的映射關系。

圖2是分析模塊的內部層次結構，方法調用現場信息收集子模塊處在最底層，作為整個分析模塊的基石，在別名分析時需要查找方法調用現場信息以確定實參到形參的別名數據流走向，進而別名分析又為污點分析提供支撐。

本文方法沒有對底層系統調用庫、JDK和SDK庫方法的內部數據流進行污點分析，而是采用建模的方式定義庫方法的污點傳播摘要，根據摘要來記錄調用庫方法前后內存中污點信息的變化，同時，也對庫方法中的驗證方法（Sanitizer）建模定義無害化處理的污點傳播摘要。方法采用白名單結合正則匹配的策略對自定義驗證方法進行識別，主要基于方法名稱、傳遞參數類型和返回值類型。例如，對于名字中包含“validate”“encrypt”或“check”等子串的方法調用語句，如果參數類型和返回值類型的簽名滿足預定義規則，就使用預定義的污點傳播摘要直接生成方法調用后的內存污點信息。

2.2 路徑條件反轉

在遍歷Source到Sink之間的所有可執行路徑時，為緩解路徑爆炸的問題，方法設計了一種路徑條件的選擇策略，以程序變換的方式反轉選取的路徑條件，重新生成新轉換的Android應用，然后將原執行動作序列（events）重放于轉換后的Android應用，進而獲得包含其他分支路徑信息的Trace。選擇策略是選取同時滿足以下兩點的條件語句：

1）在程序的反向跨方法控制流圖（Interprocedural Reverse Control Flow Graph， IRCFG）中，剪去位于Sink前方的子圖，在剩下的子圖中，以Sink為起點進行跨方法的活變量分析，要求條件語句的活變量集合中必須至少有一個污點變量。

2）如果一條條件語句與Sink屬于同一個方法體，那么在這個方法體對應的控制流圖（Control Flow Graph， CFG）中，從這條條件語句的另一個分支出發的路徑集合中至少有一條路徑會經過Sink節點。

如果在某條條件語句處已經不存在任何活的污點變量，說明Source在該條件語句之前已經被驗證過或后續沒有任何與Source相關的數據流傳播，那么在該條件語句后面的所有分支路徑就不可能從Source傳播到Sink處，即不存在從Source到Sink的污點傳播路徑，因此沒有必要反轉此條件。而與Sink屬于同一方法體的條件語句，必須滿足從該條件語句的另一個分支出發的路徑集合中至少有一條路徑會經過Sink語句;否則反轉后產生的新Trace不會經過Sink，更不可能存在Source到Sink的污點傳播路徑。

條件語句處的活變量信息通過對Android應用進行跨方法的活變量分析得到。活變量分析問題是一種典型的數據流分析問題，FlowDroid[15]將跨方法的數據流分析問題統一轉換為程序間的有限分配子集（Interprocedural， Finite， Distributive Subset， IFDS）[16]問題，按照框架抽取的“exploded super graph”中的不同流邊定義相應的流處理方法，操作具體數據事實的傳播動作即可實現活變量分析。Android程序在執行過程會大量調用系統回調方法，例如Activity的onCreate、onResume， Button按鈕注冊的點擊事件方法等，這些方法沒有顯示調用。在FlowDroid構建的跨方法控制流圖（Inter-procedural CFG， ICFG）中，這些回調方法可能會成為孤立節點，也就是說，從ICFG中的入口節點無法到達這些孤立點。因此在進行靜態分析時，通過它們傳遞的方法間數據流事實將會丟失，導致分析結果不精確。因此，方法在實現活變量分析時作了保守處理，認為這類回調方法將出口處的活變量數據流事實傳遞給了ICFG中所有其他節點，但是不包括調用方法內部的節點。

為判定從條件語句的另一個分支出發的路徑集合中是否至少存在一條路徑經過Sink，方法引入必經節點（dominator）的概念，如果每一條從流圖的入口節點到節點n的路徑都經過節點d，則認為d支配（dominate）n，稱作d是n的必經節點，記為“d dom n”。例如圖3（a），從節點0出發，3號節點是4號節點的必經節點;并且每個節點都是自己的必經節點。

通過反轉路徑條件來遍歷Source到Sink每條可行路徑時，需要反轉的每條條件語句的分支匯聚點必須在Sink之前。也就是說，沿著其在CFG中不同分支路徑的匯聚點開始深度遍歷CFG產生的節點序列必須包含Sink節點。因為Trace中出現的每條條件語句已經有一條分支路徑經過了Sink節點，所以如果從該條件語句的兩個不同分支出發的兩個路徑集合都至少存在一條經過Sink節點的路徑，顯然該條件語句的另一個分支出發的路徑集合滿足至少存在一條經過Sink的路徑。

根據上述分析，在判斷條件語句是否滿足第2）條選擇策略的方法時，生成方法體的反向控制流圖（Reverse Control Flow Fraph， RCFG），選擇同時滿足以下條件的條件語句進行反轉：

圖3（b）中每個節點的標號對應代碼行號。以這個CFG為例，置反后就得到圖3（c）中的RCFG。在RCFG子圖中，以節點8作為起點，它是節點3的必經節點，滿足條件1）。然后從節點8開始深度遍歷，獲得的節點序列是8→4→3→2→1→6，其中包含節點3的直接前繼節點4和節點6，滿足條件2），所以可以選擇反轉節點3處的條件。然而，前面得到的深度遍歷序列中，只包含了節點2的直接前繼3，沒有包含另一個前繼節點10，所以不滿足條件2），因此對節點2處的條件語句不能進行反轉。

3 原型實現

原型系統由插樁模塊、別名分析模塊、污點分析模塊和路徑條件反轉驗證模塊組成，如圖4所示。

3.1 別名分析模塊

別名分析的基礎是方法調用現場信息，重點是方法調用過程中的實參與形參的映射關系。定義數據結構“Stack〈HashMap〈String， Object〉〉”記錄方法調用現場信息，每個現場元素以HashMap〈String， Object〉鍵值對的形式存儲，包含兩種信息：一是“position”，表示方法調用語句在Trace中的位置信息，直接從Trace中記錄的語句信息獲得。二是“actual_formal_map”，使用“LinkedList〈Pair〈Object， Object〉〉”類型，根據方法簽名存儲實參與形參之間的映射關系，Pair的第一個元素表示實參，第二個元素表示形參;LinkedList中最后一個元素用于記錄實例方法的this引用的傳遞信息，如果不是實例方法調用語句則不記錄。

別名分析模塊按Trace中的指令順序模擬實際運行時動態分配的內存空間，在每塊內存空間中記錄所有指向該內存空間的別名引用，即別名集合。根據不同語句類型判斷別名信息的傳遞，進而跟蹤內存空間的別名信息的變化。內存空間的數據結構定義如下：

以鏈表的形式存儲程序申請的所有內存塊，其中每一個Pair代表一個內存塊，在每個內存塊中記錄了兩種信息：別名信息和內存塊信息。它們各映射成一個集合（HashSet），分別是PointsToSet和BlocksSet。PointsToSet記錄所有指向該內存塊的變量，集合中的所有變量它們之間都互為別名。BlocksSet記錄的是內存塊集合。集合中的元素類型是HashMap〈String， Object〉，每個元素記錄了申請內存塊的位置信息、內存塊的子空間位置信息和內存塊的污點信息，具體字段記錄的內容如表1所示。

依照表1的定義，順序遍歷Trace中的語句信息，分析每條指令并跟蹤別名信息的傳遞過程。對Android應用執行時的別名信息產生影響的語句類型共有四種，分別是參數傳遞語句（IdentityStmt）、賦值語句（AssignStmt）、方法調用語句（InvokeStmt）和方法返回語句（ReturnStmt）。

3.1.1 參數傳遞語句（IdentityStmt）

在分析參數傳遞語句時，查找記錄的方法調用現場信息中是否包含實參與形參之間的映射關系，如果包含則將形參指針信息添加到實參所指向的內存塊的別名指針集合（PointsToSet）中。例如圖5中第13）行發生的自定義方法調用，后面緊跟著參數的傳遞過程，實參$r6、和26分別傳遞給下面的$r1、$r0和$i0（圖5中箭頭①②③），即它們兩兩互為別名。

由于Android程序中存在大量的底層系統回調方法，并且Trace僅包含APK的應用程序代碼，不包含Android框架代碼，所以有時會無法匹配方法調用時實參和形參的映射關系。在這種情形下需要按參數傳遞語句右值的不同類型分別記錄數據流傳遞：

1）右值類型是ThisRef（圖5第4）行語句），代表這是this引用的傳遞。在記錄的內存塊鏈中反向查詢與方法this引用類型一致的內存塊，如果找到則近似認為左值引用是指向該內存塊，否則直接視為在當前語句位置為左值分配新的內存空間;在圖5第4）行語句處沒有與$r9匹配的實參，所以反向查找類型一致的內存塊，定位到第1）行的$r0所指向的內存塊，即$r0與$r9互為別名。

2）右值類型是ParameterRef（圖5第5）行語句），代表這是方法調用的參數傳遞，可直接認為左值在該語句處分配新的內存空間。

3）此外，參數傳遞語句中右值還有一種類型：CaughtExceptionRef，表示傳遞拋出異常變量的信息，如圖5中第65）行的語句;它實際上是接收上面第64）行拋出的異常變量$r26，別名信息的傳遞如圖中④號箭頭方向所示。為記錄異常拋出時參數的傳遞，方法在遍歷Trace的過程中定義一個棧（throw_value_stack），每遇到一條異常拋出語句（ThrowStmt）拋出異常變量時，就壓棧記錄拋出的異常變量所指向的內存塊的位置信息。當遇到接收拋出異常變量的參數傳遞語句時，可直接將語句的左值引用指向throw_value_stack的棧頂元素代表的內存塊。

3.1.2 賦值語句（AssignStmt）

賦值語句的特點是將左值引用指向右值標識的內存空間，記錄賦值語句的別名數據流事實傳遞分為三步：

1）在別名指針集合中清除已記錄的與左值相關的指針信息，同時清除包括記錄相關內存塊之間關系（父子域或數組元素域）的信息;

2）具體定位右值引用指向的內存塊，將左值指針信息加入該內存塊的別名指針集合中;

3）調整與左值相關的別名信息，如訪問路徑中父域記錄的子域信息。

第2）～3）需要根據賦值語句的右值和左值的具體類型進行不同的操作。

第2）步定位右值引用指向的內存塊，分為幾種情況：

①右值是Local（局部變量）或CastExpr（強制類型轉換表達式）時，在記錄的內存塊鏈中查找右值指向的內存塊，然后直接將左值指針添加到內存塊的別名指針集合中。例如圖5中第32）行的$r7[1]指向$r11原來的內存塊，第37）行語句執行后$r13和$r14互為別名。

②右值類型是InvokeExpr、NewExpr、BinopExpr、InstanceOfExpr、UnopExpr或Constant時，分別對應圖5第8）、10）、39）、34）、43）和11）行的語句，即認為在執行語句處為左值分配新的內存空間。

③右值類型屬于StaticFieldRef、InstanceFieldRef或ArrayRef時，分別對應圖5第51）、58）和33）行，如果不能找到右值對應的內存塊，可以在滿足污點傳播一致性約束的前提下，根據父域的污點狀態分配新的內存塊。例如a已經是完全污染的，當第一次使用a.f對象時為其分配新的內存塊，新內存塊也標記為完全污染;但如果a是部分污染或可信時，新分配的a.f的內存塊應該標記為可信。定位好右值指向的內存塊后，直接將左值引用添加到內存塊的別名集合中即可。

第3）步調整與左值相關的別名信息，主要是對左值類型是靜態域（StaticFieldRef）、實例域（InstanceFieldRef）和數組元素（ArrayRef）三種情形做調整：

1）左值是靜態域時，找出所有類型是靜態域所在類的類型的內存塊，將這些內存塊中記錄的相應靜態子域空間的位置標識修改為右值所指向的位置。例如圖5第11）行的靜態域type所在類的類型是Person，所以查找所有類型是Person的內存塊，并將這些內存塊的type子域的內存空間位置標識成第11）行右值所指向的內存位置。

2）左值是實例域或數組元素時，分別找到實例域的父對象或數組對象所指向的內存塊，將記錄子域內存塊位置的標識修改為相應的右值的內存塊位置。例如圖5第18）和19）行$r1的兩個子域對象name和age分別指向$r0和$i0，那么父對象$r1中記錄的子域集合中的信息也需要調整，如圖6（a）所示。再有圖5第26）和32）行，分別將$r10和$r11賦值給數組元素$r7[0]和$r7[1]，那么對應的數組對象$r7中記錄的數組下標0和1的元素分別指向$r10和$r11指向的內存塊，如圖6（b）所示。

3.1.3 方法調用語句（InvokeStmt）

在Java中，方法調用語句不會對已記錄的內存塊鏈和別名集合造成太大的影響，加上之前已經對參數傳遞語句進行過分析（確保實參形參互為別名），所以在方法調用語句處無需過多的操作。但有一種情況例外，就是調用對象實例初始化方法（〈init〉），該方法表示在被調用位置給方法調用的this變量分配內存空間;因此需要將this變量所對應的內存塊分配位置（position）修改為〈init〉方法的調用位置。如圖5中第2）行的變量$r0，它指向的內存塊的分配位置應該修改成這條語句所在的位置。一般調用〈init〉方法都是緊跟在實例對象New完之后，所以在調用〈init〉方法之前在內存塊鏈中就已經記錄了實例對象的內存塊。

3.1.4 方法返回語句（ReturnStmt）

如果在方法調用現場接收方法的返回值，即方法調用現場是賦值語句，那么接收變量就與方法的返回值變量互為別名，如圖5中⑤號箭頭標識的$r1接收返回語句的返回值r0，它們互為別名。隨后具體別名信息傳遞的操作與前面賦值語句的處理過程類似，相當于把賦值語句中的右值替換成方法返回語句的返回變量。

3.2 污點分析模塊

根據獲得的別名分析結果，將污點狀態信息標記到別名變量指向的內存塊上，以此來跟蹤污點傳播過程。污點分析中傳遞的數據流事實是被污染變量的污染狀態集合，稱為污點狀態集合。在污點狀態集合中的每個元素以二元組的形式定義（var， taint_level），其中：var表示變量的訪問路徑（Access Path）;taint_level表示被污染變量的受污染程度。方法規定三種污染程度：部分污染（pa）、完全污染（ta）和可信（trust）。影響污點數據流傳播的執行語句包括方法調用語句和賦值語句。

方法調用語句分為調用庫方法和調用自定義方法。分析庫方法調用時，以污點傳播摘要的方式對庫方法執行產生的污點信息流建模，根據具體的摘要調整并記錄方法執行后各相關內存塊的污點狀態信息。分析自定義方法調用時需進一步遞歸分析方法體內部每條語句的污點傳播語義來實現跨方法污點傳播過程。

分析賦值語句時，首先按賦值語句右值的不同類型定義污點傳播語義規則，依照規則記錄污點傳播過程;然后再按左值的不同類型，調整相關變量的污點狀態信息。對內存塊的污點狀態信息的修改或調整都必須滿足污點傳播的一致性約束，避免錯誤記錄污點傳播信息。

在污點分析過程中，如果變量a.f的污點狀態改變，那么a的污點狀態應該作相應的調整。同時，對所有與a互為別名的實例域、數組元素和靜態域，需要對與它們相關的內存塊（父域內存塊、數組對象內存塊）的污點信息作進一步調整。此時存在一個向上遞歸調整相關變量的污點狀態信息的過程，方法將它定義為up_transmit_taint（var， tainted_level， deepth），其中：參數var表示發生污點狀態改變的變量，tainted_level表示改變的污染程度。遞歸深度變量deepth記錄每次遞歸的深度，用于控制向上遞歸調整污點狀態信息的最大遞歸層數（一般不超過5層）。up_transmit_taint方法根據已發生污點狀態改變的變量類型調整污點狀態信息，分為如下三種情形（MustAlias（a）表示所有肯定與a互為別名的變量集合）。

1）發生污點狀態變化的變量是實例域對象。根據實例域和它的父域的污點狀態信息的不同，分別對污點狀態信息做不同的調整操作，共存在三種情況：

第①種情況表示如果實例域是可信的并且父域是完全污染，那么將父域調整為部分污染，接著對父域的別名繼續向上遞歸調整;第②種情況表示實例域是部分污染，那么直接將父域標記成部分污染，然后對父域的別名向上遞歸調整;第③種情況表示如果實例域完全污染，并且父域不是完全污染，那么父域應該調整為部分污染，接著對父域的別名遞歸向上調整。

2）發生污點狀態改變的變量是數組元素時。為保證數組對象和各元素的污點狀態信息的一致性，方法保守地規定數組中只要有一個元素不可信，就將整個數組標記為被完全污染，其中所有元素都標記為不可信，而且數組中所有元素的污點狀態都保持一致，即數組元素要么可信要么完全污染。

3）發生污點狀態改變的變量是靜態域對象。調整相關污點狀態信息的操作與1）相同，但需要對其他與靜態域所屬類的類型相同的所有變量都進行調整，因為靜態域屬性被所有實例對象共享。

3.3 路徑條件反轉驗證模塊

為遍歷Source到Sink的所有可執行路徑，方法通過收集Source到Sink之間的條件語句，結合程序變換方法，反轉路徑條件來覆蓋所有路徑。為緩解路徑爆炸問題，設計了反轉條件的選擇策略，即選擇滿足2.2節中的兩條選擇策略。

第1）條選擇策略判斷是否存在活的被污染變量，通過靜態的跨方法分析，收集每條語句處的活變量信息。方法基于FlowDroid中提供的IFDS框架，定義四種相應的流方法，完成對活變量數據流事實的傳遞，實現跨方法的活變量分析。算法1用于判斷第2）條選擇策略，結合反向Dominator和深度遍歷方法。Global聲明全局變量，共定義了4個函數：Is_reverse、Domination、DFS和Contain。其中DFS是經典深度遍歷算法，Domination判斷在圖graph中以start為起點的圖中各節點之間的必經節點（dominator）關系。Contain分別從條件語句的兩個分支開始遍歷路徑，判斷遍歷的節點序列是否都經過參數stmt的語句節點，結果記錄在全局變量contains中。Is_reverse函數判斷條件語句是否可以加入反轉條件的集合中。

算法1 判斷從條件語句的另一個分支出發的所有路徑中至少有一條路徑會經過Sink。

輸入 方法體的反向控制流圖RCFG;條件語句IfStmt;污點匯聚節點Sink。

輸出 是否反轉輸入的條件語句。

4 實驗分析

原型系統基于Soot-trunk 3.0和FlowDroid 2.0框架實現，使用JDK 1.8開發，總計8000余行代碼，其中插樁模塊1400余行，分析模塊4300余行，路徑條件反轉驗證模塊2200余行。實驗環境為Genymotion搭建的模擬器，運行系統版本為Android 4.4，操作系統版本是Ubuntu 18.04.1 LTS，處理器i5-3230M，CPU 2.6GHz，內存8GB。

實驗測試選取DroidBench 2.0作為測試數據集，它包含了13類共119個Android應用。剔除跨組件通信、應用間通信和多線程等3類測試樣本共34個，原型系統目前還不支持這三類的應用程序。另外還剔除了實驗環境無法模擬的10個樣本，并在Android開源軟件倉庫F-Droid和Github上采集10個真實的Android應用，最后，對85個Android應用樣本進行實驗。

FlowDroid對其中77個樣本報告71個泄露缺陷，每個缺陷都只存在一條可執行路徑。經過別名分析和污點分析后，方法準確地驗證其中7個泄露是虛警。

下面以實驗中的一段Android程序源碼片段作為例，簡述在實驗過程中，驗證只存在一條可執行路徑的泄露缺陷是否虛警的流程。

FlowDroid報告其中第26）行Source分別傳播到第11）、12）、20）和27）行Sink的4條泄露。但其中button2按鈕點擊事件的處理方法在第20）行Sink調用Source變量imei之前，imei變量已經被置空，即此時imei變為可信的，同時，由于這對Source-Sink之間只存在一條路徑，因此方法判斷這條（Source，Sink）泄露是虛警。

針對其余的8個樣本程序的實驗結果如表2所示。

第1組和第7組應用只存在一個Source，MultiFlow的多源分析階段被阻斷，導致MultiFlow未能正確驗證虛警。雖然MutiFlow對第5和第8組應用正確驗證了不少虛警，但是經過進一步人工分析源碼，MultiFlow沒有精確跟蹤回調方法間的污點傳播，導致將發生在回調方法間傳遞的污點傳播路徑誤判為虛警。

在MultiFlow對DroidBench的驗證結果中，有3組應用的真實報警被誤判為虛警。兩組發生在回調方法中：一組是回調方法修改SharedPreference過程中的污點傳播;另一組是回調方法構造Fragment過程中的污點傳播;第三組是在多源分析階段將2條泄露報警錯誤地合并成一條泄露報警。因此，本文方法相比MultiFlow的驗證結果更為可靠。

在85個樣本應用中，平均遍歷路徑比為15.09%，虛警率平均降低58.17%，MultiFow將虛警率平均降低了18.25%。

實驗結果表明，本文方法能高效可靠地驗證靜態分析結果的正確性，在驗證過程中裁剪不必要的路徑遍歷，極大緩解路徑爆炸問題，提升驗證效率。

5 結語

本文提出一種半自動驗證污點分析結果的正確性的方法，實現基于Trace的別名分析和污點分析，判定Trace中是否有Source到Sink的污點傳播。設計一種路徑剪枝方法，提出結合活變量分析的路徑約束選擇策略，以程序變換的方式搜索路徑，極大緩解路徑爆炸問題，基于FlowDroid實現的原型系統對真實的Android應用分析表明了方法的有效性。

本文方法的不足主要包括：1）不支持跨組件、跨應用程序之間的數據通信過程的污點分析，對多線程并發的處理也不夠完善;2）不支持Java語言的某些特性如反射，另外，對Android庫方法的建模不完備，可能導致污點分析不精確;3）需要手工執行Android應用獲得同時覆蓋Source和Sink的初始種子Trace，當程序規模較大時，該項工作費時費力。

未來工作主要包括：1）研究跨組件污點數據流事實的傳播;2）對Android庫方法的污點傳播語義進行更為完備的建模;3）研究結合Fuzzing測試和動態符號執行來獲得初始種子Trace。

參考文獻（References）

[1] 王蕾， 李豐， 李煉， 等. 污點分析技術的原理和實踐應用[J]. 軟件學報， 2017， 28（4）： 860-882. （WANG L， LI F， LI L， et al. Principle and practice of taint analysis[J]. Journal of Software， 2017， 28（4）： 860-882.）

[2] 趙云山， 宮云戰， 王前， 等. 靜態缺陷檢測中的誤報消除技術研究[J]. 計算機研究與發展， 2012， 49（9）： 1822-1831. （ZHAO Y S， GONG Y Z， WANG Q， et al. False positive elimination in static defect detection[J]. Journal of Computer Research and Development， 2012， 49（9）： 1822-1831.）

[3] 李筱， 周嚴， 李孟宸， 等. C/C++程序靜態內存泄漏警報自動確認方法[J]. 軟件學報， 2017， 28（4）： 827-844. （LI X， ZHOU Y， LI M C， et al. Automatically validating static memory leak warnings for C/C++programs[J]. Journal of Software， 2017， 28（4）： 827-844.）

[4] GE X， TANEJA K， XIE T， et al. DyTa： dynamic symbolic execution guided with static verification results[C]// Proceedings of the 33rd International Conference on Software Engineering. New York： ACM， 2011： 992-994.

[5] 王蕾， 周卿， 何東杰， 等. 面向Android應用隱私泄露檢測的多源污點分析技術[J]. 軟件學報， 2019， 30（2）： 211-230. （WANG L， ZHOU Q， HE D J， et al. Multi-sources taint analysis technique for privacy leak detection of Android apps[J]. Journal of Software， 2019， 30（2）： 211-230.）

[6] RICE H G. Classes of recursively enumerable sets and their decision problems[J]. Transactions of the American Mathematical Society， 1953， 74（2）： 358-366.

[7] YANG Z， YANG M， ZHANG Y， et al. AppIntent： analyzing sensitive data transmission in Android for privacy leakage detection[C]// Proceedings of the 2013 ACM SIGSAC Conference on Computer & Communications Security. New York： ACM， 2013： 1043-1054.

[8] ARZT S， RASTHOFER S， HAHN R， et al. Using targeted symbolic execution for reducing false-positives in dataflow analysis[C]// Proceedings of the 4th ACM SIGPLAN International Workshop on State of the Art in Program Analysis. New York： ACM， 2015： 1-6.

[9] JUNKER M， HUUCK R， FEHNKER A， et al. SMT-based false positive elimination in static program analysis[C]// Proceedings of the 2012 International Conference on Formal Engineering Methods， LNCS 7635. Berlin： Springer， 2012： 316-331.

[10] ZHANG L， THING V L L. A hybrid symbolic execution assisted fuzzing method[C]// Proceedings of the 2017 IEEE Region 10 Conference. Piscataway： IEEE， 2017： 822-825.

[11] CAI J， YANG S， MEN J， et al. Automatic software vulnerability detection based on guided deep fuzzing[C]// Proceedings of the IEEE 5th International Conference on Software Engineering and Service Science. Piscataway： IEEE， 2014： 231-234.

[12] PENG H， SHOSHITAISHVILI Y， PAYER M. T-Fuzz： fuzzing by program transformation[C]// Proceedings of the 2018 IEEE Symposium on Security and Privacy. Piscataway： IEEE， 2018： 697-710.

[13] GODEFROID P， LEVIN M Y， MOLNAR D. SAGE： whitebox fuzzing for security testing[J]. Communications of the ACM， 2012， 55（3）： 40-44.

[14] TANEJA K， XIE T， TILLMANN N， et al. Guided path exploration for regression test generation[C]// Proceedings of the 31st International Conference on Software Engineering. Piscataway： IEEE， 2009： 311-314.

[15] ARZT S， RASTHOFER S， FRITZ C， et al. FlowDroid： precise context， flow， field， object-sensitive and lifecycle-aware taint analysis for Android apps[J]. ACM SIGPLAN Notices， 2014， 49（6）： 259-269.

[16] BODDEN E. Inter-procedural data-flow analysis with IFDS/IDE and soot[C]// Proceedings of the ACM SIGPLAN International Workshop on State of the Art in Java Program Analysis. New York： ACM， 2012： 3-8.