秦彪 郭帆 涂風(fēng)濤

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

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

關(guān)鍵詞： 程序驗(yàn)證;污點(diǎn)分析;活變量分析;程序變換;路徑敏感

中圖分類號：TP311.53

文獻(xiàn)標(biāo)志碼：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 引言

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

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

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

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

1 相關(guān)工作

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

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

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

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

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

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

2 半自動(dòng)驗(yàn)證方法

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

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

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

并安裝到Android模擬器或真機(jī)中。

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

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

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

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

2.1 污點(diǎn)分析

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

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

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

2.2 路徑條件反轉(zhuǎn)

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

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

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

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

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

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

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

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

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

3 原型實(shí)現(xiàn)

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

3.1 別名分析模塊

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

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

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

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

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

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

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

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

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

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

3.1.2 賦值語句（AssignStmt）

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

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

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

3）調(diào)整與左值相關(guān)的別名信息，如訪問路徑中父域記錄的子域信息。

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

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

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

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

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

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

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

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

3.1.3 方法調(diào)用語句（InvokeStmt）

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

3.1.4 方法返回語句（ReturnStmt）

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

3.2 污點(diǎn)分析模塊

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

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

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

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

1）發(fā)生污點(diǎn)狀態(tài)變化的變量是實(shí)例域?qū)ο蟆８鶕?jù)實(shí)例域和它的父域的污點(diǎn)狀態(tài)信息的不同，分別對污點(diǎn)狀態(tài)信息做不同的調(diào)整操作，共存在三種情況：

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

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

3）發(fā)生污點(diǎn)狀態(tài)改變的變量是靜態(tài)域?qū)ο?。調(diào)整相關(guān)污點(diǎn)狀態(tài)信息的操作與1）相同，但需要對其他與靜態(tài)域所屬類的類型相同的所有變量都進(jìn)行調(diào)整，因?yàn)殪o態(tài)域?qū)傩员凰袑?shí)例對象共享。

3.3 路徑條件反轉(zhuǎn)驗(yàn)證模塊

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

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

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

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

輸出 是否反轉(zhuǎn)輸入的條件語句。

4 實(shí)驗(yàn)分析

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

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

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

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

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

針對其余的8個(gè)樣本程序的實(shí)驗(yàn)結(jié)果如表2所示。

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

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

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

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

5 結(jié)語

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

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

未來工作主要包括：1）研究跨組件污點(diǎn)數(shù)據(jù)流事實(shí)的傳播;2）對Android庫方法的污點(diǎn)傳播語義進(jìn)行更為完備的建模;3）研究結(jié)合Fuzzing測試和動(dòng)態(tài)符號執(zhí)行來獲得初始種子Trace。

參考文獻(xiàn)（References）

[1] 王蕾， 李豐， 李煉， 等. 污點(diǎn)分析技術(shù)的原理和實(shí)踐應(yīng)用[J]. 軟件學(xué)報(bào)， 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)缺陷檢測中的誤報(bào)消除技術(shù)研究[J]. 計(jì)算機(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] 李筱， 周嚴(yán)， 李孟宸， 等. C/C++程序靜態(tài)內(nèi)存泄漏警報(bào)自動(dòng)確認(rèn)方法[J]. 軟件學(xué)報(bào)， 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應(yīng)用隱私泄露檢測的多源污點(diǎn)分析技術(shù)[J]. 軟件學(xué)報(bào)， 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.