面向Android應用的靜態(tài)污點分析結果的正確性驗證

秦彪 郭帆 涂風濤

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

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

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

中圖分類號：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手機最嚴重的安全問題之一，它是指應用程序中存在一條從讀取隱私數(shù)據(jù)的Source方法調用語句到送出隱私輸出的Sink方法調用的執(zhí)行路徑，并且未經(jīng)用戶許可。污點分析是檢測隱私泄露的主流檢測方法之一，它從Source開始跟蹤外部引入的數(shù)據(jù)（污點），檢查它們是否未經(jīng)驗證就直接傳播到Sink位置，如果是則可能存在漏洞。

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

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

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

1 相關工作

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

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

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

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

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

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

2 半自動驗證方法

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

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

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

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

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

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

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

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

2.1 污點分析

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

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

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

2.2 路徑條件反轉

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

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

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

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

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

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

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

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

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

3 原型實現(xiàn)

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

3.1 別名分析模塊

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

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

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

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

3.1.1 參數(shù)傳遞語句（IdentityStmt）

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

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

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

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

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

3.1.2 賦值語句（AssignStmt）

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

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

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

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

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

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

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

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

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

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

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

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

3.1.3 方法調用語句（InvokeStmt）

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

3.1.4 方法返回語句（ReturnStmt）

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

3.2 污點分析模塊

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

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

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

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

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

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

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

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

3.3 路徑條件反轉驗證模塊

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

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

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

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

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

4 實驗分析

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

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

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

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

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

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

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

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

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

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

5 結語

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

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

未來工作主要包括：1）研究跨組件污點數(shù)據(jù)流事實的傳播;2）對Android庫方法的污點傳播語義進行更為完備的建模;3）研究結合Fuzzing測試和動態(tài)符號執(zhí)行來獲得初始種子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] 趙云山， 宮云戰(zhàn)， 王前， 等. 靜態(tài)缺陷檢測中的誤報消除技術研究[J]. 計算機研究與發(fā)展， 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++程序靜態(tài)內存泄漏警報自動確認方法[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.