袁占慧，楊智，張紅旗，金舒原，杜學(xué)繪

基于通信順序進(jìn)程的Android程序復(fù)雜信息流分析方法

袁占慧1，楊智1，張紅旗1，金舒原2，杜學(xué)繪1

（1. 信息工程大學(xué)，河南 鄭州 450001；2. 中山大學(xué)，廣東 廣州 510006）

Android隱私泄露問題日益嚴(yán)重，信息流分析是發(fā)現(xiàn)隱私泄露的一種主要方法。傳統(tǒng)信息流分析方法以單一可達(dá)性分析為主，難以分析復(fù)雜信息流。提出一種基于通信順序進(jìn)程的信息流分析方法，建立應(yīng)用程序行為的形式化模型，從而全面刻畫程序信息流行為。基于進(jìn)程跡等價分析方法能夠自動化驗(yàn)證信息流關(guān)聯(lián)、信息流約束等復(fù)雜信息流問題，進(jìn)而判斷是否存在敏感信息泄露。實(shí)驗(yàn)表明，所提方法能夠達(dá)到90.99%的準(zhǔn)確率。

安卓；信息流分析；隱私防護(hù)；形式化分析；通信順序進(jìn)程

1 引言

智能手機(jī)逐漸融入人們的日常生活，成為生活中不可或缺的一部分，越來越多的隱私信息、私人數(shù)據(jù)等被存儲在智能手機(jī)中。Android系統(tǒng)在智能手機(jī)的操作系統(tǒng)中占有極高份額，然而由于其具有開放性，大量不可信組件和第三方應(yīng)用程序威脅著用戶的隱私信息安全。針對Android系統(tǒng)的隱私敏感信息流分析具有很高的應(yīng)用價值，是當(dāng)前Android應(yīng)用程序安全和用戶隱私信息保護(hù)的迫切需要。

當(dāng)前比較常見的信息流分析（IFA，information flow analysis）方法，主要采用污點(diǎn)跟蹤的方式，分別從靜態(tài)、動態(tài)或動態(tài)與靜態(tài)混合的方向入手，將信息流分析問題抽象為可達(dá)性問題，最終獲得可達(dá)性信息流路徑結(jié)果。只對信息流處理可達(dá)性問題具有很大的局限性，無法處理復(fù)雜信息流。例如，在針對多污點(diǎn)源的信息流分析，以及存在反射的信息流分析問題時，以FlowDroid為代表的一類信息流分析方法無法給出復(fù)雜的信息流分析結(jié)果。本文采用基于通信順序進(jìn)程（CSP，communicating sequential process）[1]的形式化分析方法全面捕捉信息流行為，完成復(fù)雜情況下的信息流分析。

CSP是由Hoare[1]提出的一種著名的進(jìn)程代數(shù)模型，能夠很好地描述并發(fā)進(jìn)程之間的相互作用。CSP可以通過代數(shù)推演對具有并發(fā)性、不確定性的分布式軟件系統(tǒng)進(jìn)行分析，通過定義進(jìn)程的跡，將進(jìn)程從開始運(yùn)行到某一時刻內(nèi)所有順序發(fā)生的事件進(jìn)行建模，通過事件序列刻畫進(jìn)程行為。CSP的特性很好地契合了復(fù)雜信息流分析的要求?；贑SP對Android程序進(jìn)行信息流分析，是形式化方法在信息流分析領(lǐng)域的創(chuàng)新性應(yīng)用。

信息流分析是一種重要的軟件分析方法，在Android應(yīng)用程序的安全性分析以及隱私防護(hù)方面有廣泛的應(yīng)用。TaintDroid[2]是一個動態(tài)的全系統(tǒng)信息流跟蹤工具，可以同時跟蹤多個敏感數(shù)據(jù)源，通過集成變量級、消息級、方法級和文件級粒度的污點(diǎn)傳播實(shí)現(xiàn)跟蹤分析。這種動態(tài)的信息流分析方法能夠獲得足夠的上下文信息且有效減少誤報，已被應(yīng)用于信息流控制[3-6]、漏洞發(fā)現(xiàn)[7-10]、安全攻擊[10-12]、惡意軟件檢測[13-14]、隱私泄露分析[15-17]等領(lǐng)域。FlowDroid[18]是著名的靜態(tài)信息流分析工具，在Android應(yīng)用程序的單個組件中執(zhí)行靜態(tài)污染分析。FlowDroid充分模擬了Android特有的應(yīng)用程序生命周期和回調(diào)方法，用于減少漏報或誤報。Amandroid[19]和IccTA[20]執(zhí)行組件間通信污點(diǎn)分析，以檢測基于組件間通信（ICC，inter-component communicaiton）的隱私泄露。Bianchi等[21]采用反向數(shù)據(jù)流分析方法跟蹤API的信息流，針對觸摸屏界面存在的安全風(fēng)險及帶有視圖覆蓋替換的釣魚攻擊，深度挖掘具有風(fēng)險的系統(tǒng)調(diào)用。InputScope[22]使用靜態(tài)污點(diǎn)分析來標(biāo)記用戶輸入并監(jiān)視其傳播，以識別用戶輸入驗(yàn)證，這些驗(yàn)證會暴露隱私信息，如后門和黑名單。傳統(tǒng)信息流分析方法往往缺乏復(fù)雜信息流分析能力。

形式化方法在Android信息流分析檢測中的應(yīng)用研究相對有限，當(dāng)前研究主要對程序進(jìn)行形式化建模，以進(jìn)行模型檢驗(yàn)[23-28]。Song等[23]利用下推系統(tǒng)對Android應(yīng)用程序的Smali代碼進(jìn)行建模，并通過計算樹邏輯或線性時態(tài)邏輯來表達(dá)惡意行為。Bai等[24]構(gòu)建了一個通用框架DROIDPF，用以驗(yàn)證Android應(yīng)用程序的安全性，由于DROIDPF側(cè)重于應(yīng)用程序中常見的安全漏洞，因此需要手動建立每個漏洞的狀態(tài)機(jī)模型。Mercaldo等[25]圍繞惡意軟件家族的檢測和分類發(fā)表了一系列研究成果。他們在文獻(xiàn)[25-27]中分別檢測到了與勒索軟件、更新攻擊和重新包裝相關(guān)的系列惡意軟件，并在此基礎(chǔ)上提出了一種通用的分類方法，命名為LEILA[28]。這一系列研究通過基于通信系統(tǒng)演算（CCS，calculus of communicating system）的Java字節(jié)碼建模[29]來解決相關(guān)問題，定義選擇性演算公式[30]，對惡意軟件家族的時序邏輯屬性進(jìn)行編碼，并通過模型檢查獲得家族分類。

形式化檢測的關(guān)鍵是能夠用形式化語言準(zhǔn)確、全面地描述代碼行為，并建立行為模型。模型檢查過程通過數(shù)學(xué)推導(dǎo)由形式化工具實(shí)現(xiàn)自動化。然而，現(xiàn)有的形式化信息流分析方法存在不足。例如，文獻(xiàn)[28]中的LEILA系統(tǒng)，無法處理虛擬調(diào)用和反射調(diào)用的混淆。此外，數(shù)據(jù)流沒有被考慮，因?yàn)樗鼪]有對賦值語句建模。

為了彌補(bǔ)傳統(tǒng)信息流分析方法和現(xiàn)有形式化分析方法在復(fù)雜信息流分析方面存在的不足，本文提出了一種基于通信順序進(jìn)程的Android程序復(fù)雜信息流分析方法，其核心思想是利用CSP對信息流傳播過程進(jìn)行建模，利用形式化的方法，更加詳細(xì)地刻畫出復(fù)雜信息流的傳播過程，全面捕捉信息流行為，完成復(fù)雜情況下的信息流分析。

本文的主要貢獻(xiàn)如下。

（1）提出了基于通信順序進(jìn)程的Android程序復(fù)雜信息流分析方法，解決了傳統(tǒng)信息流分析方法難以對復(fù)雜信息流進(jìn)行分析的問題，包括多信息流關(guān)聯(lián)關(guān)系分析、控制行為觸發(fā)的復(fù)雜信息流分析等，進(jìn)而判斷Android程序是否存在敏感信息泄露。

（2）按照信息流性質(zhì)進(jìn)行分類，對不同種類信息流路徑分別進(jìn)行建模分析，基于Jimple中間語言建立了適合Android應(yīng)用程序的CSP信息流分析模型。

（3）對信息流的多種特征進(jìn)行了建模，包括反射、過程間函數(shù)調(diào)用等，解決了傳統(tǒng)靜態(tài)信息流分析的短板問題。實(shí)驗(yàn)表明，所提方法能夠正確執(zhí)行信息流分析功能，并達(dá)到90.99%的準(zhǔn)確率，高于傳統(tǒng)靜態(tài)信息流分析方法FlowDroid。

圖1 整體工作流程系統(tǒng)框架

Figure 1 The framework of the work process system

2 系統(tǒng)設(shè)計

本文提出的基于通信順序進(jìn)程的Android程序復(fù)雜信息流分析方法，是基于將應(yīng)用程序的信息流傳播過程用CSP模型進(jìn)行建模而完成的，在此基礎(chǔ)上，再進(jìn)行信息流行為提取，判斷是否存在敏感信息泄露，最后報告敏感信息流路徑。整體工作流程和系統(tǒng)框架如圖1所示。

首先，對目標(biāo)APK文件進(jìn)行分析和代碼轉(zhuǎn)換，將APK文件轉(zhuǎn)換為中間表示形式再建立CSP模型。然后，建立CSP模型，刻畫典型信息流性質(zhì)。最后，將目標(biāo)應(yīng)用程序的CSP模型和典型信息流CSP模型同時輸入FDR（failures divergence refinement）檢測器進(jìn)行檢測，獲得信息流路徑的進(jìn)程報告。

由于Java源代碼和Java字節(jié)碼中的語句類型非常復(fù)雜，因此快速有效地提取代碼中的信息非常重要?；谝陨峡紤]，首先進(jìn)行APK文件反編譯，然后調(diào)用SOOT將Java字節(jié)碼轉(zhuǎn)換成Jimple中間語言[31]。Jimple具有語句類型少、類型清晰、3種地址形式等優(yōu)點(diǎn)，有利于后續(xù)的形式化建模。

將Jimple語句轉(zhuǎn)化為對應(yīng)的CSP進(jìn)程，即可完成對Android應(yīng)用程序的正式建模。由于Jimple中只有15條語句，而且3個地址形式使語義非常清晰，因此將Jimple表示為CSP會更容易。每一個語句的過程范式都是建立在其特征的基礎(chǔ)上的，是對代碼行為的準(zhǔn)確抽象表達(dá)。本文在此基礎(chǔ)上提出了一個完整的Android應(yīng)用程序模型。

本文使用FDR模型檢測器檢測Android惡意軟件，F(xiàn)DR模型檢測器是一個應(yīng)用于CSP的正式工具。對樣本行為建模的CSP過程被認(rèn)為是需要驗(yàn)證的過程，它被簡化為只包含屬性過程中出現(xiàn)的事件，最終結(jié)果是斷言測試（如果存在）的反例。

本文使用模型檢測工具FDR對目標(biāo)信息流進(jìn)行形式化分析。該工具引入了跡的概念，用可以執(zhí)行的有限通信序列的集合表示進(jìn)程?；谯E模型，F(xiàn)DR用跡提煉來定義兩個進(jìn)程之間的特殊關(guān)系。

如果存在兩個進(jìn)程和，的所有特定行為對于來說都具有，那么稱提煉，或是的一個提煉，記為í。進(jìn)一步，將跡模型應(yīng)用到提煉的概念中：如果的所有通信事件序列對于來說也是可能的，即traces()ítraces()，那么稱跡提煉，或是的一個跡提煉，記為íT。

在對信息流進(jìn)行FDR分析檢測時，將作為抽象每條目標(biāo)信息流特有性質(zhì)的進(jìn)程，將作為建模目標(biāo)APK文件樣本中信息流行為的進(jìn)程。在一次測試中，只將一個樣本的待測進(jìn)程與一個信息流進(jìn)程同時輸入FDR檢測器，在樣本進(jìn)程只保留該性質(zhì)中事件的基礎(chǔ)上，判斷其是否是信息流進(jìn)程的跡提煉。如果模型檢測通過，則說明該樣本具有該信息流類型所具有的性質(zhì)，因此報告該信息流路徑；否則，認(rèn)為樣本不存在該進(jìn)程類型的信息流路徑，可以繼續(xù)將該樣本進(jìn)程與其他信息流進(jìn)程進(jìn)行測試。

3 CSP形式化建模

為了更加便捷高效地對信息流傳播過程進(jìn)行建模，本文引入了Jimple中間語言[31]。這種基于SOOT框架的三地址中間表示形式，語句種類較少且每條語句最多只會出現(xiàn)3個量值，非常適合對Java語言的分析及優(yōu)化。信息流傳播中涉及的Jimple語句類型如圖2所示。

圖2 15種Jimple語句類型（If/Goto語句為一組）

Figure 2 15 Jimple statements (If/Goto statements are a group)

如果將一段Jimple代碼視為一個整體系統(tǒng)，那么其中包含的每一條語句都是它的組成部分，都可以建模成一個CSP。語句的進(jìn)程名稱由帶參數(shù)類型的完整方法名和下標(biāo)組成，第一個下標(biāo)是當(dāng)前語句在方法中的編號，然后是當(dāng)前方法中的所有非靜態(tài)局部變量、方法所在類的所有非靜態(tài)成員變量以及方法中創(chuàng)建的所有類對象的非靜態(tài)成員變量，以便更好地表明變量值的變化。例如，某方法的第條語句對應(yīng)的進(jìn)程名可以表示為Test_example(int)0,i0,…，其中的值不大于該方法的Jimple語句總數(shù)（從定義語句后開始計數(shù)）。將不同種類的Jimple語句轉(zhuǎn)換成對應(yīng)的CSP時，所有的進(jìn)程均可以被命名為P, r0, i0, …的形式。

當(dāng)涉及類的成員變量或成員方法的變量時，需要在兩個進(jìn)程間傳遞數(shù)據(jù)。若對其進(jìn)行賦值，如. = temp$1對應(yīng)的CSP進(jìn)程為P, r0, i0, …= (set.class.!temp$1?P+1, r0, i0, …)；否則，如temp$1 =.對應(yīng)的CSP進(jìn)程為P, r0, i0, …, temp$1,…= (get.class.??P+1, r0, i0, …, a, …)。其中，set.class.!temp$1是輸出temp$1作為class.賦值的事件，get.class.?是接收class.的值的事件。

本文為每個類建模一個進(jìn)程來管理類中所有成員變量和成員方法中變量的值，同時，為每個實(shí)例化的類建立編號ID。若類class中有個上述類型的變量，則它對應(yīng)的CSP進(jìn)程為(ID, a)= (IDset.class.??P| IDgetclass!?P)。其中，編號ID能夠?qū)崿F(xiàn)對類的記錄，通過編號值區(qū)分不同類的成員變量和成員方法中變量的值。set.class.?是class接收作為的賦值的事件，getclass!是class輸出的值的事件。

典型的信息流行為模式包括數(shù)據(jù)流行為、控制流行為、反射行為、虛函數(shù)等?；趯Σ煌N類的Jimple語句進(jìn)行CSP建模分析，本文分別建立了5種信息流行為的CSP模型。

3.1 數(shù)據(jù)流行為建模

數(shù)據(jù)流行為可以認(rèn)為是由NopStmt、IdentityStmt和AssignStmt這3種類型的語句進(jìn)行組合的行為。NopStmt表示變量值未發(fā)生變化的語句，這條語句沒有經(jīng)過任何能引起變量值變化的事件，此時直接進(jìn)入下一條語句的進(jìn)程；IdentityStmt表示將參數(shù)值賦值給變量的語句，將調(diào)用語句中的實(shí)參傳入被調(diào)用方法；AssignStmt表示變量的一般賦值語句，體現(xiàn)變量被感染的過程。數(shù)據(jù)流行為建模如圖3所示。

圖3 數(shù)據(jù)流行為建模

Figure 3 Modeling for data flow

IdentityStmt語句的兩種模型形式分別對應(yīng)與參數(shù)有關(guān)的變量賦值語句和與this引用有關(guān)的變量賦值語句，param.method?arg表示當(dāng)前方法method接收實(shí)參arg的事件。對涉及參數(shù)的賦值語句，需要在調(diào)用語句和被調(diào)用語句之間傳遞實(shí)參。在多參數(shù)情況下，按序進(jìn)行的參數(shù)賦值更便于查找輸入值。

3.2 過程內(nèi)控制流行為建模

本文將過程內(nèi)控制流行為認(rèn)為是由IfStmt/ GotoStmt、TableSwitchStmt和LookupSwitchStmt這3種類型的語句組合而成的行為。IfStmt/ GotoStmt表示條件判斷和跳轉(zhuǎn)語句，能夠指示滿足判斷條件時要進(jìn)行處理的語句位置；TableSwitchStmt是表轉(zhuǎn)換語句，用于switch分支的條件值分布比較集中的情況；LookupSwitchStmt是查找轉(zhuǎn)換語句，用于switch分支的條件值分布比較稀疏的情況。過程內(nèi)控制流行為建模如圖4所示。

IfStmt/GotoStmt語句的第一種模型形式中的是跳轉(zhuǎn)目標(biāo)的語句序號。為了得到的值，需要在當(dāng)前方法的后續(xù)語句范圍內(nèi)搜索該label標(biāo)記。該進(jìn)程不執(zhí)行任何實(shí)際的事件，只是跳轉(zhuǎn)到標(biāo)號所在的語句進(jìn)程繼續(xù)執(zhí)行。第二種模型形式的進(jìn)程提供兩個選擇，如果IfStmt給出的判斷條件成立，則按照相應(yīng)label標(biāo)記處的語句進(jìn)程繼續(xù)執(zhí)行；否則按照下一條語句的進(jìn)程順序執(zhí)行。

圖4 過程內(nèi)控制流行為建模

Figure 4 Modeling for intraprocedural control flow

TableSwitchStmt和LookupSwitchStmt語句分別通過鍵值匹配和索引訪問跳轉(zhuǎn)表，模型中是case分支的條件值，goto()是處理該情況的語句的起始編號。該進(jìn)程表示在選擇合適的case分支后，跳轉(zhuǎn)到相應(yīng)標(biāo)號位置處繼續(xù)執(zhí)行。兩種代碼的形式完全相同，因此共享相同的CSP進(jìn)程。

3.3 過程間控制流行為建模

過程間控制流行為包括函數(shù)調(diào)用行為、反射行為以及虛函數(shù)，本節(jié)將依次對這3種情況進(jìn)行建模分析。

3.3.1 函數(shù)調(diào)用建模

本文將函數(shù)調(diào)用行為認(rèn)為是由InvokeStmt、ReturnStmt和ReturnVoidStmt這3種類型的語句進(jìn)行組合形成的。InvokeStmt表示調(diào)用語句；ReturnStmt指有返回值的返回語句，ReturnVoidStmt指沒有返回值的返回語句“return”。函數(shù)調(diào)用行為建模如圖5所示。

圖5 函數(shù)調(diào)用行為建模

Figure 5 Modeling for function call

對于InvokeStmt調(diào)用語句，當(dāng)被調(diào)用的method有參數(shù)和返回值時，CSP模型中的param.method!arg0、param.method!1等表示向method依次傳遞實(shí)參的事件，retval.method?val表示從method接收val的事件，call.method和return.method分別表示method調(diào)用開始和結(jié)束的事件。當(dāng)被調(diào)用的方法沒有參數(shù)或返回值時，在進(jìn)程表達(dá)式中去掉相應(yīng)的事件，通過IdentityStmt語句進(jìn)行實(shí)參接收。

新線程的創(chuàng)建過程也遵循InvokeStmt方法調(diào)用的形式，但有所不同的是，它不需要像一般調(diào)用中那樣等待被調(diào)用方完成后才能繼續(xù)執(zhí)行，因此具有如圖5所示的新的CSP模型形式，其中thread.run指要創(chuàng)建的線程類thread的run方法對應(yīng)的進(jìn)程。

對于ReturnStmt語句的CSP模型進(jìn)程，retval.method!val是當(dāng)前方法method返回變量val的事件。該進(jìn)程表示返回需要的結(jié)果后結(jié)束所在方法的此次執(zhí)行，并回到方法開始處等待下次調(diào)用。

對于ReturnVoidStmt語句的CSP模型進(jìn)程，用method表示當(dāng)前方法，該進(jìn)程不返回任何值，只用于結(jié)束所在方法的此次執(zhí)行。

在對過程間通信行為進(jìn)行建模時，需要考慮系統(tǒng)調(diào)用的同步機(jī)制。為了確保任意方法在同一時刻最多只能被另一個方法調(diào)用，用SYNM進(jìn)程來描述系統(tǒng)的調(diào)用同步機(jī)制，如圖6所示。系統(tǒng)調(diào)用同步機(jī)制模型由各個調(diào)用同步事件的控制進(jìn)程SYNM_method組成，其中method指代被調(diào)用的方法，method1、method2等則是系統(tǒng)中不同的被調(diào)用方法。

圖6 系統(tǒng)的調(diào)用同步機(jī)制

Figure 6 System call synchronization mechanism

調(diào)用語句與被調(diào)用方法之間的同步關(guān)系如圖7所示。在調(diào)用語句中，call和return事件將分別作為本次調(diào)用的開始和結(jié)束事件。SYNM進(jìn)程的同步集是call、begin、end、return事件，被調(diào)用方法執(zhí)行完畢后會將控制返回到InvokeStmt的下一條語句。

圖7 InvokeStmt及被調(diào)用方法之間的同步

Figure 7 Synchronization between invokeStmt and the called method

3.3.2 反射行為建模

反射行為作為Java語言獨(dú)特的功能，能夠在過程間信息流中動態(tài)獲取信息并調(diào)用對象方法，需要單獨(dú)進(jìn)行建模分析。為了靜態(tài)地解析反射，本文定義allclasses數(shù)組來記錄程序中的所有類。反射行為中包含forName、getMethod和invoke這3種比較重要的方法調(diào)用，方法調(diào)用的示例如圖8所示。

圖8 反射行為中的方法調(diào)用示例

Figure 8 Example of method calls in reflection

forName方法的調(diào)用，在allclasses數(shù)組中查找名稱為cla的值的類，并將其索引allclasses_ index(cla)賦值給，對應(yīng)的CSP進(jìn)程如圖9(a)所示。

getMethod方法的調(diào)用，在cla類的方法數(shù)組allmethodc中查找名稱為send，參數(shù)類型為ARG_ type的值的方法，并將其索引m_index（“send”，ARG_type）&賦給，相應(yīng)的CSP進(jìn)程如圖9(b)所示。

invoke方法的調(diào)用，主要負(fù)責(zé)反射調(diào)用的具體執(zhí)行，CSP進(jìn)程如圖9(c)所示。

圖9 反射行為建模

Figure 9 Modeling for reflection

程序中每個動態(tài)加載的方法都被記錄下來后，構(gòu)造相應(yīng)的反射過程來控制方法的執(zhí)行，如圖10所示。

圖10 構(gòu)造反射過程

Figure 10 Constructing for reflection

3.3.3 虛函數(shù)建模

以Java的繼承機(jī)制為基礎(chǔ)虛函數(shù)調(diào)用，也是Java語言一種獨(dú)特的函數(shù)調(diào)用方式，因此單獨(dú)進(jìn)行建模分析。Java支持繼承，允許創(chuàng)建層次類。子類不僅可以繼承父類的特性和行為，還可以通過虛調(diào)用使用父類的方法。

與反射行為建模過程類似，同樣要為程序中所有類依照從屬關(guān)系建立一個數(shù)組allclasses來存儲它們的父類。此外，還要為類建立一個數(shù)組allmethodc來記錄類中的所有方法名。

在處理調(diào)用語句時，首先檢查被調(diào)用方法的類層次結(jié)構(gòu)是否正確，如果正確，則根據(jù)上述規(guī)范對流程進(jìn)行建模；否則，搜索其父類并依次執(zhí)行，直到找到方法為止，并用模型中實(shí)際調(diào)用的方法名替換該方法。圖11(a)所示的語句為一個虛函數(shù)調(diào)用，getIMEI()方法在源類中不存在，但可以在其父類SourceFather中找到該方法。因此，相應(yīng)的CSP過程模型如圖11(b)所示。

圖11 虛函數(shù)建模

Figure 11 Modeling for virtual function

4 信息流性質(zhì)刻畫與驗(yàn)證

4.1 信息流性質(zhì)刻畫

在信息流泄露事件中，部分信息流行為模式普遍存在，是構(gòu)成泄露事件的重要步驟。即使這些行為模式存在多種不同的具體實(shí)現(xiàn)方式，然而信息流傳播邏輯相同，形式化表達(dá)方式也相同。因此本文將不同種類的信息流行為模式認(rèn)定為信息流的性質(zhì)，結(jié)合對典型信息流行為模式的建模，刻畫出泄露事件的信息流性質(zhì)。

為了簡化FDR模型檢測的復(fù)雜程度，對CSP模型中與信息流傳播不相關(guān)的代碼行為進(jìn)行隱藏，流程為：uselessevents={|transfer,calldeal, api.normalx|}，SAFE_SAMPLE=SAMPLE uselessevents。接下來定義信息流發(fā)生泄露的性質(zhì)為PROPERTY=source.taint->sink.taint->STOP?；趯喕畔⒘鰿SP模型和信息流泄露性質(zhì)的定義，得出在CSP模型中發(fā)現(xiàn)信息流泄露路徑的方式為assert SAFE_SAMPLE [T= PROPERTY。

最終結(jié)果作為斷言測試的反例生成，當(dāng)判定結(jié)果為真時，則認(rèn)為存在信息泄露行為，并且FDR模型檢測工具能夠報告出滿足判定結(jié)果為真的信息流路徑，該路徑即為本方法所求的目標(biāo)信息流泄露路徑。當(dāng)此處判定結(jié)果為假時，則說明不存在信息泄露行為。

基于以上信息流性質(zhì)和泄露路徑提取方式，本文針對典型信息流分析過程，建立了細(xì)化的信息流檢測CSP模型與FDR驗(yàn)證方法。

（1）待分析程序中含有多個敏感信息源（source）和敏感信息泄露點(diǎn)（sink）時（如將地理位置、麥克風(fēng)、通話記錄信息等認(rèn)定為敏感源，將網(wǎng)絡(luò)發(fā)送、短信發(fā)送、寫入本地文件等認(rèn)定為敏感信息泄露點(diǎn)），為了找出從所有source點(diǎn)到所有sink點(diǎn)的信息流，即找出所有可能存在的隱私敏感信息泄露路徑，本文提出如下CSP模型檢測方法：Leakage_Flow ≡ (sink.{sinklist}.taint. {sourcelist}|sinklist<-{1…MAX},sourcelist<-{1… MAX})；PROPERTY≡CHAOS(ΣLeakage_Flow)；PROPERTY [T= Assert SYSTEM。此方法將從所有source點(diǎn)出發(fā)到達(dá)所有sink點(diǎn)的信息流路徑作為系統(tǒng)CSP模型的跡提煉輸出，能夠得到覆蓋所有source點(diǎn)和sink點(diǎn)的信息流路徑。

（2）針對某應(yīng)用程序進(jìn)行分析時，有需要挖掘從指定source點(diǎn)到指定sink點(diǎn)的信息流路徑的需求，即信息流定向搜索需求。例如，針對地理位置信息，搜索是否存在以地理位置信息為敏感源，以寫入本地文件為泄露點(diǎn)的信息流路徑，就屬于信息流定向搜索。本文針對此類情況提出如下CSP模型檢測方法：Leakage_Flow ≡ (sink.sinkx.taint.sourcex)；PROPERTY ≡ CHAOS (ΣLeakage_Flow)；PROPERTY [T= Assert SYSTEM。此方法通過將確定的source點(diǎn)和sink點(diǎn)引入模型檢測過程，完成定向搜索功能。

（3）在惡意應(yīng)用程序中，某條信息流同時包含多個敏感信息的情況也比較常見，即一條信息流路徑同時被多個敏感源感染，有多個source點(diǎn)。例如，惡意軟件可能將通話記錄和通信錄以及其他非敏感信息打包，經(jīng)過一條信息流路徑，向網(wǎng)絡(luò)發(fā)送。這種多污點(diǎn)聚合類的信息流分析對于傳統(tǒng)的靜態(tài)信息流分析工具也是不小的挑戰(zhàn)。本文針對此類多污點(diǎn)聚合發(fā)送的信息流分析問題提出如下CSP模型檢測方法：Leakage_Flow ≡(sink.taint.{sourcelist}|sourcelist<-{source,source,source…source})；PROPERTY≡ CHAOS (ΣLeakage_Flow)；PROPERTY [T= Assert SYSTEM。此方法針對指定的sink點(diǎn)，對個source點(diǎn)進(jìn)行跡提煉，從而挖掘出多污點(diǎn)聚合發(fā)送復(fù)雜信息流路徑。

（4）由控制行為觸發(fā)的復(fù)雜信息流路徑是傳統(tǒng)靜態(tài)信息流分析的難點(diǎn)，控制行為對信息流分析產(chǎn)生的影響在進(jìn)行靜態(tài)分析時很難識別。當(dāng)某條信息流需要控制行為才能觸發(fā)時（如當(dāng)用戶點(diǎn)擊發(fā)送某張圖片時，觸發(fā)泄露地理位置信息），將會產(chǎn)生傳統(tǒng)靜態(tài)分析方法無法識別的信息流。本文針對這種情況提出如下CSP模型檢測方法：Leakage_Flow ≡ (sink.event.taint.source|event<- {button.click.OK})；PROPERTY ≡ CHAOS (ΣLeakage_Flow)；PROPERTY [T=Assert SYSTEM。

形如上述類型的復(fù)雜信息流分析模型，都能夠轉(zhuǎn)化為以CSP模型描述的信息流性質(zhì)，進(jìn)而應(yīng)用到模型檢測中實(shí)現(xiàn)信息流分析挖掘功能。

在實(shí)際應(yīng)用中，往往不是針對應(yīng)用程序的源碼進(jìn)行分析，而是只有APK文件資源。此時需要首先調(diào)用SOOT框架，直接將APK文件轉(zhuǎn)化為Jimple中間代碼形式，再進(jìn)行后續(xù)CSP建模和FDR模型檢測分析。

4.2 信息流性質(zhì)驗(yàn)證

本文使用精化檢測工具FDR對建立的形式化模型進(jìn)行分析。FDR已廣泛應(yīng)用于學(xué)術(shù)界和工業(yè)界，在協(xié)議漏洞挖掘、軟件安全性驗(yàn)證、數(shù)學(xué)邏輯運(yùn)算方面獲得了成功應(yīng)用。FDR實(shí)現(xiàn)了CSP的3個驗(yàn)證模型，分別為跡模型、穩(wěn)定失敗模型和失敗/發(fā)散模型，3個模型驗(yàn)證進(jìn)程間等價性的程度和需要驗(yàn)證的狀態(tài)空間個數(shù)都是遞增的。穩(wěn)定失敗模型可以驗(yàn)證非確定性行為，如驗(yàn)證活性。失敗/發(fā)散模型避免因進(jìn)程加入屏蔽算子導(dǎo)致的發(fā)散對分析帶來的影響，實(shí)際上如果不是實(shí)際存在發(fā)散跡，而是用于驗(yàn)證分析時出現(xiàn)發(fā)散跡，則發(fā)散攻擊是不存在的，不一定要求發(fā)散跡也等價。而且跡模型可以對“不存在違背某個安全性質(zhì)的反例”之類的斷言進(jìn)行驗(yàn)證。所以本文選取跡模型作為驗(yàn)證模型，這樣可以降低復(fù)雜度且能滿足本文的安全性質(zhì)要求。

FDR內(nèi)部通過有限狀態(tài)系統(tǒng)等價性分析驗(yàn)證斷言的正確性，主要分析復(fù)雜信息流的可達(dá)性和關(guān)聯(lián)關(guān)系。對于單個污點(diǎn)源，假設(shè)程序的變量個數(shù)為，語句個數(shù)為，則程序的CSP對應(yīng)的有限狀態(tài)機(jī)的狀態(tài)個數(shù)最大為2，每個狀態(tài)的出度最大為。FDR的精化算法采用互模擬等價原則分析程序的有限狀態(tài)機(jī)M1和安全屬性的有限狀態(tài)機(jī)M2之間的等價包含關(guān)系。首先選擇程序運(yùn)行時的初始狀態(tài)然后遞歸分析，對于M1中的每個狀態(tài)10，查找M2中是否存在等價狀態(tài)20，則查找復(fù)雜度為2，對于每一個備選的20'，驗(yàn)證所有從該狀態(tài)的出邊是否等價，則驗(yàn)證復(fù)雜度為。所以最壞情況下總的計算開銷為×22m，假設(shè)做個不同污點(diǎn)源復(fù)雜信息流分析，則最壞情況的計算開銷為×22mk。

FDR采用了很多高效的方法進(jìn)行了優(yōu)化。狀態(tài)可達(dá)性分析，只分析從初始狀態(tài)可達(dá)的狀態(tài)；狀態(tài)壓縮技術(shù)，包括explicate（枚舉），sbisim（強(qiáng)節(jié)點(diǎn)標(biāo)記互模擬），tau_loop_factor（循環(huán)消除），diamond（菱形消除），normalise（標(biāo)準(zhǔn)化）和model_compress（語義等價分解）。在本文研究的信息流復(fù)雜性分析中，一般程序全局/靜態(tài)變量相對較少，大多數(shù)變量是局部變量，離開了所在函數(shù)，這些局部變量沒有意義，意味著絕大部分的狀態(tài)變遷根本不會發(fā)生。每條語句通常只會影響少量變量的狀態(tài)變化，意味著狀態(tài)機(jī)中總的邊數(shù)通常不會超過10。所以這些優(yōu)化技術(shù)可以極大地降低信息流分析的復(fù)雜度。另外，大部分的信息流性質(zhì)驗(yàn)證公式驗(yàn)證的是作用了隱藏算子后的進(jìn)程等價性分析，這其實(shí)是弱互模擬等價分析。驗(yàn)證所有從該狀態(tài)的出邊是否等價時，復(fù)雜度進(jìn)一步大幅降低。本文的實(shí)驗(yàn)表明了FDR在驗(yàn)證具體的信息流分析實(shí)例時具有良好的性能。

5 實(shí)驗(yàn)評估

本節(jié)將會對本文提出的信息流分析方法進(jìn)行實(shí)驗(yàn)評估，主要分為功能測試和性能測試兩部分。為了保證實(shí)驗(yàn)條件的一致性，本文的實(shí)驗(yàn)部分采用了與FlowDroid相同的source列表和sink列表。實(shí)驗(yàn)中FlowDroid涉及的部分參數(shù)配置如表1所示。

5.1 功能測試

功能測試的目的是驗(yàn)證本文提出的信息流分析方法的基本功能是否正確，即本文方法是否能夠正確執(zhí)行信息流分析功能，正確報告信息流泄露路徑。

文獻(xiàn)[32]提出了一種惡意應(yīng)用程序中包含的復(fù)雜信息流情況，文獻(xiàn)舉例的惡意應(yīng)用程序偽裝成視頻播放器，但卻開啟后臺服務(wù)竊取包括IMEI、IMSI在內(nèi)的用戶敏感信息；另一個良性應(yīng)用程序同樣使用了這兩項敏感信息并進(jìn)行發(fā)送。兩種應(yīng)用程序中都含有通過Internet發(fā)送國際移動設(shè)備識別碼（IMEI，international mobile equipment identity）、國際移動用戶識別碼（IMSI，international mobile subscriber identity）的信息流路徑，但兩種信息流結(jié)構(gòu)卻大不相同，如圖12所示。

表1 FlowDroid參數(shù)配置

圖12 良性和惡意軟件應(yīng)用程序的行為比較

Figure 12 Behavior comparison between benign and malicious applications

實(shí)驗(yàn)表明，惡意App中的信息流泄露行為大多數(shù)采用這種捆綁式的泄露方式。使用文獻(xiàn)[32]提供的良性和惡意應(yīng)用程序進(jìn)行測試，結(jié)果表明本文提出的基于通信順序進(jìn)程的復(fù)雜信息流分析方法，能夠正確執(zhí)行多敏感源捆綁式的惡意信息流分析，并能夠得出與良性應(yīng)用程序的區(qū)別。本文還對傳統(tǒng)數(shù)據(jù)流分析工具FlowDroid進(jìn)行了測試，由于忽視了不同信息流的關(guān)系以及這兩個應(yīng)用程序的不同行為，F(xiàn)lowDroid無法區(qū)分惡意應(yīng)用程序行為。

本文提出的方法屬于靜態(tài)信息流分析方法，因此選取靜態(tài)信息流分析方法FlowDroid作為實(shí)驗(yàn)對比對象，對比兩種分析方法檢測到的信息流路徑是否一致。

FlowDroid[18]是Android應(yīng)用程序的高精度靜態(tài)信息流分析方法，文獻(xiàn)[18]使用了InsecureBank APP和DroidBench測試套件，測試方法的有效性和準(zhǔn)確性。本文方法也將分別在這兩個平臺上與FlowDroid進(jìn)行對比分析。

（1）首先選取InsecureBankv2作為測試用例進(jìn)行實(shí)驗(yàn)分析，測試本文方法挖掘復(fù)雜App內(nèi)多條信息流路徑的能力。對InsecureBankv2中存在的9個典型的信息流泄露漏洞進(jìn)行測試的結(jié)果如表1所示。表中的★表示找到了信息流泄露路徑。實(shí)驗(yàn)結(jié)果表明，兩種信息流分析方法都發(fā)現(xiàn)了所有的信息流泄露路徑。證明本文方法能夠正確執(zhí)行信息流分析功能。

表2 InsecureBankv2信息流泄露路徑檢測結(jié)果

（2）接下來利用DroidBench2.0[18]驗(yàn)證本文方法挖掘不同App內(nèi)多條信息流路徑的能力。DroidBench2.0是一個開源的基準(zhǔn)測試套件，常用于測試針對Android系統(tǒng)的信息流分析工具在數(shù)組、方法、指令、應(yīng)用內(nèi)外通信等方面的跟蹤分析性能及有效性。DroidBench2.0中13個類別的120個應(yīng)用程序都被用于本實(shí)驗(yàn)，實(shí)驗(yàn)結(jié)果如表3所示。其中，TP表示正確報告App存在的信息泄露路徑數(shù)，F(xiàn)P表示誤報數(shù)，F(xiàn)N表示漏報數(shù)。

所有測試用例中共有115條泄露路徑。FlowDroid和本文的分析方法都發(fā)現(xiàn)了101條路徑，但FlowDroid誤報了13條路徑，本文方法誤報了10條路徑。FlowDroid誤報但本文方法未誤報的3條路徑實(shí)際上從未出現(xiàn)在測試用例Unregister1/Callbacks、Exceptions3/General Java和VirtualDispatch3/General Java中。FlowDroid沒有為從未注冊的回調(diào)、從未發(fā)生的異常和從未調(diào)用的方法中的代碼提供更精確的分析。本文分析方法誤報的10條路徑涉及粗粒度數(shù)組或列表跟蹤、未定義的源、不準(zhǔn)確的反向別名分析等。為了避免巨大的存儲開銷，數(shù)組或列表中的所有數(shù)據(jù)項共享相同的污點(diǎn)標(biāo)記，這會導(dǎo)致粗粒度跟蹤和4次誤報。FlowDroid和本文提出的信息流分析方法定義的源比DroidBench定義的源更多，如getLastKnownLocation、findViewById、getIntent等，因此這兩種方法都跟蹤了過多的source，所以這些誤報事實(shí)上是合理的。

表3 DroidBench2.0信息流泄露檢測結(jié)果

FlowDroid和本文方法都漏掉了14條路徑，主要是因?yàn)橐恍┨厥獯a沒有被跟蹤，包括在獨(dú)立組件（Singletons1/ICC）、ICC處理程序（ServiceCommunication1/ICC）、靜態(tài)初始化方法（StaticInitialization1/General java）、格式化程序（StringFormatter1/General java）、文件系統(tǒng)訪問（PrivateDataLeak3/AndroidSpecific）、無目標(biāo)類的類型信息的方法反射調(diào)用（Reflection3/ Reflection）中的污點(diǎn)傳播等情況。

本文提出的信息流分析方法在此項實(shí)驗(yàn)中的召回率為87.83%，準(zhǔn)確率為90.99%。FlowDroid的召回率同樣為87.83%，但其準(zhǔn)確率僅為88.60%。

5.2 性能測試

本文的性能測試部分在具有6核1.10 GHz，英特爾i7-10710U處理器和16 GB內(nèi)存的計算機(jī)上完成。

信息流靜態(tài)分析工具分析應(yīng)用程序的時間消耗可以作為性能指標(biāo)，反應(yīng)分析方法的性能優(yōu)劣。在進(jìn)行性能測試時，本文仍然以FlowDroid為實(shí)驗(yàn)對比方法，以DroidBench2.0為實(shí)驗(yàn)測試集。性能測試結(jié)果如表4所示。

DroidBench2.0共有13個類別，如表4第一列所示，本文對每個類中所有的應(yīng)用程序分別進(jìn)行測試并取平均值。表4中第二列表示FlowDroid的時間消耗，記錄的是將APK文件輸入FlowDroid并最終獲得信息流路徑的時間；第3列到第5列分別表示本方法中3個步驟分別消耗的時間，即代碼轉(zhuǎn)換、形式化建模和模型檢測分別消耗的時間；最后一列表示本文提出的分析方法消耗的總時間。表中所有實(shí)驗(yàn)數(shù)據(jù)均為針對每個APK文件分別運(yùn)行3次取平均值的結(jié)果。

代碼轉(zhuǎn)換和形式化建模消耗了部分時間來更全面地處理應(yīng)用程序，但占總體消耗時間的比例較小，分別為3.61%和2.18%；模型檢測部分為本文方法輸出信息流路徑的關(guān)鍵部分，需要更多的時間，其時間消耗占總時間消耗的94.22%。

實(shí)驗(yàn)結(jié)果表明，本文提出的信息流分析方法雖然與其他形式化方法相同，均具有分析過程耗時較長的問題，但與傳統(tǒng)信息流分析方法FlowDroid相比，在時間消耗相差不大的情況下（120個測試用例的平均時間差值僅為5.64 s），獲得了更高的準(zhǔn)確率。

表4 性能測試結(jié)果

6 結(jié)束語

本文對Android敏感信息流進(jìn)行分析，以更加全面地挖掘隱私泄露信息流路徑，助力用戶隱私信息防護(hù)為出發(fā)點(diǎn)，提出了一種基于通信順序進(jìn)程的Android程序復(fù)雜信息流分析方法。該方法利用通信順序進(jìn)程模型對應(yīng)用程序的信息流傳播過程進(jìn)行建模，在此基礎(chǔ)上，刻畫復(fù)雜信息流性質(zhì)，再進(jìn)行信息流行為提取，全面分析應(yīng)用程序復(fù)雜信息流，判斷是否存在敏感信息泄露。該方法克服了傳統(tǒng)信息流分析方法通過求解可達(dá)性問題獲取路徑，難以處理復(fù)雜信息流的局限性，實(shí)現(xiàn)了反射行為等信息流特征刻畫，解決了多種復(fù)雜信息流分析問題，能夠全面捕捉信息流行為，完成復(fù)雜情況下的信息流泄露路徑檢測。通過與傳統(tǒng)靜態(tài)信息流分析方法對比分析，表明本文方法能夠正確執(zhí)行信息流分析功能，并能夠達(dá)到90.99%的準(zhǔn)確率，高于傳統(tǒng)靜態(tài)信息流分析方法FlowDroid。

[1] HOARE C A R. Communicating sequential processes[M]. NJ, USA: Prentice Hall, 1985.

[2] ENCK W, GILBERT P, CHUN B G, et al. TaintDroid: an information-flow tracking system for realtime privacy monitoring on smartphones[J]. ACM Transactions on Computer Systems, 2010, 57(3): 393-407.

[3] VACHHARAJANI N, BRIDGES M J, CHANG J, et al. RIFLE: an architectural framework for user-centric information-flow security[C]//Proceedings of 37th International Symposium on Microarchitecture (MICRO-37'04). 2004: 243-254.

[4] BANERJEE S, DEVECSERY D, CHEN P M, et al. Iodine: fast dynamic taint tracking using rollback-free optimistic hybrid analysis[C]//Proceedings of 2019 IEEE Symposium on Security and Privacy (SP). 2019: 490-504.

[5] ZHANG M, YIN H. Efficient, context-aware privacy leakage confinement for android applications without firmware modding[C]// Proceedings of the 9th ACM Symposium on Information, Computer and Communications Security. 2014: 259-270.

[6] JIA Y J, CHEN Q A, WANG S Q, et al. ContexIoT: towards providing contextual integrity to appified IoT platforms[C]//Proceedings of 2017 Network and Distributed System Security Symposium. 2017.

[7] ZONG P, LV T, WANG D, et al. FuzzGuard: filtering out unreachable inputs in directed grey-box fuzzing through deep learning[C]//Proceedings of 29th USENIX Security Symposium (USENIX-SS'20). 2020.

[8] SHE D D, CHEN Y Z, SHAH A, et al. Neutaint: efficient dynamic taint analysis with neural networks[C]//Proceedings of 2020 IEEE Symposium on Security and Privacy (SP). 2020: 1527-1543.

[9] NGUYEN-TUONG A, GUARNIERI S, GREENE D, et al. Automatically hardening web applications using precise tainting[M]//Security and Privacy in the Age of Ubiquitous Computing. Boston, MA: Springer US, 2005: 295-307.

[10] NEWSOME J, SONG D. Dynamic taint analysis for automatic detection, analysis, and signature generation of exploits on commodity software[C]//Proceedings of the Network and Distributed System Secu-rity Symposium (NDSS '05). 2005.

[11] KONG J F, ZOU C C, ZHOU H Y.Improving software security via runtime instruction-level taint checking[C]//Proceedings of the 1st Workshop on Architectural and System Support for Improving Software Dependability. 2006: 18-24.

[12] HALDAR V, CHANDRA D, FRANZ M. Dynamic taint propagation for Java[C]//Proceedings of 21st Annual Computer Security Applications Conference (ACSAC'05). 2005: 311.

[13] VOGT P, NENTWICH F, JOVANOVIC N, et al. Cross site scripting prevention with dynamic data tainting and static analysis[C]//Proceedings of the Network and Distributed System Security Symposium (NDSS '07). 2007.

[14] CABALLERO J, POOSANKAM P, MCCAMANT S, et al. Input generation via decomposition and restitching: finding bugs in malware[C]//Proceedings of the 17th ACM Conference on Computer and Communications Security. 2010: 413-425.

[15] ENCK W, GILBERT P, CHUN B G, et al. TaintDroid: an information-flow tracking system for realtime privacy monitoring on smartphones[C]//Proceedings of the 9th USENIX Symposium on Operating Systems Design and Implementation. 2019: 393-407.

[16] ZHU D Y, JUNG J, SONG D, et al. TaintEraser[J]. ACM SIGOPS Operating Systems Review, 2011, 45(1): 142-154.

[17] KANG M G, MCCAMANT S, POOSANKAM P, et al. DTA++: dynamic taint analysis with targeted control-flow propagation[C]//Proceedings of the Network and Distributed System Security Symposium (NDSS '11). 2011.

[18] ARZT S, RASTHOFER S, FRITZ C, et al. FlowDroid: precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for Android Apps[C]//Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation. 2014: 259-269.

[19] WEI F G, ROY S, OU X M, et al. Amandroid: a precise and general inter-component data flow analysis framework for security vetting of Android Apps[C]//Proceedings of the ACM Conference on Computer and Communications Security. 2014: 1329-1341.

[20] LI L, BARTEL A, BISSYANDé T F, et al. IccTA: detecting inter-component privacy leaks in android Apps[C]//Proceedings of 2015 IEEE/ACM 37th IEEE International Conference on Software Engineering. 2015: 280-291.

[21] BIANCHI A, CORBETTA J, INVERNIZZI L, et al. What the App is that? Deception and countermeasures in the android user interface[C]//Proceedings of 2015 IEEE Symposium on Security and Privacy. 2015: 931-948.

[22] ZHAO Q C, ZUO C S, DOLAN-GAVITT B, et al. Automatic uncovering of hidden behaviors from input validation in mobile Apps[C]//Proceedings of 2020 IEEE Symposium on Security and Privacy (SP). 2020: 1106-1120.

[23] SONG F, TOUILI T. Model-checking for android malware detection[M]//Programming Languages and Systems. Cham: Springer International Publishing, 2014: 216-235.

[24] BAI G D, YE Q Q, WU Y Z, et al. Towards model checking Android applications[J]. IEEE Transactions on Software Engineering, 2018, 44(6): 595-612.

[25] MERCALDO F, NARDONE V, SANTONE A, et al. Ransomware steals your phone. formal methods rescue it[M]//Formal Techniques for Distributed Objects, Components, and Systems. Cham: Springer International Publishing, 2016: 212-221.

[26] MERCALDO F, NARDONE V, SANTONE A, et al. Download malware? No, thanks: how formal methods can block update attacks[C]//Proceedings of the 4th FME Workshop on Formal Methods in Software Engineering. 2016: 22-28.

[27] BATTISTA P, MERCALDO F, NARDONE V, et al. Identification of android malware families with model checking[C]//Proceedings of the 2nd International Conference on Information Systems Security and Privacy. 2016: 542-547.

[28] CANFORA G, MARTINELLI F, MERCALDO F, et al. LEILA: formal tool for identifying mobile malicious behaviour[J]. IEEE Transactions on Software Engineering, 2019, 45(12): 1230-1252.

[29] MILNER R. Communication and concurrency[M]. Prentice Hall, 1989.

[30] BARBUTI R, DE FRANCESCO N, SANTONE A, et al. Selective mu-calculus and formula-based equivalence of transition systems[J]. Journal of Computer and System Sciences, 1999, 59(3): 537-556.

[31] SURHONE L M, TENNOE M T, HENSSONOW S F, et al. Jimple[M]. Betascript Publishing, 2010.

[32] SHEN F, VECCHIO J D, MOHAISEN A, et al. Android malware detection using complex-flows[C]//Proceedings of IEEE Transactions on Mobile Computing. 2017: 1231-1245.

Android complex information flow analysis method based on communicating sequential process

YUAN Zhanhui1, YANG Zhi1,ZHANG Hongqi1, JIN Shuyuan2, DUXuehui1

1. Information Engineering University, Zhengzhou 450001, China 2. Sun Yat-sen University, Guangzhou 510006, China

Android privacy leak problem is becoming more and more serious. Information flow analysis is a main method to find privacy leak. Traditional information flow analysis methods mainly focus on single accessibility analysis, which is difficult to analyze complex information flow. An information flow analysis method based on communication sequence process was proposed. The formal model of application behavior was established, which can fully describe the information flow of program. The process trace equivalence analysis method could automatically verify complex information flow problems such as information flow association and information flow constraints. This method could detect whether the application program leaks sensitive information. Experimental results show that the accuracy of the proposed method can reach 90.99%.

Android, information flow analysis, privacy protection, formal analysis, communicating sequential process

TP309

A

10.11959/j.issn.2096?109x.2021086

2021?08?19；

2021?09?23

楊智，zynoah@163.com

國家自然科學(xué)基金（62176265, 61972040）

The National Natural Science Foundation of China (62176265, 61972040)

袁占慧, 楊智, 張紅旗, 等. 基于通信順序進(jìn)程的Android程序復(fù)雜信息流分析方法[J]. 網(wǎng)絡(luò)與信息安全學(xué)報, 2021, 7(5): 156-168.

YUAN Z H, YANG Z, ZHANG H Q, et al. Android complex information flow analysis method based on communicating sequential process[J]. Chinese Journal of Network and Information Security, 2021, 7(5): 156-168.

袁占慧（1997?），男，吉林遼源人，信息工程大學(xué)碩士生，主要研究方向?yàn)橐苿又悄芙K端的信息流控制與隱私保護(hù)。

楊智（1975?），男，河南開封人，博士，信息工程大學(xué)副教授，主要研究方向?yàn)椴僮飨到y(tǒng)安全、云計算安全、隱私保護(hù)。

張紅旗（1962?），男，河北遵化人，博士，信息工程大學(xué)教授、博士生導(dǎo)師，主要研究方向?yàn)榫W(wǎng)絡(luò)安全、風(fēng)險評估、等級保護(hù)和信息安全管理等。

金舒原（1974?），女，吉林白城人，博士，中山大學(xué)教授、博士生導(dǎo)師，主要研究方向?yàn)殡[私保護(hù)、漏洞分析等。

杜學(xué)繪（1968?），女，河南新鄉(xiāng)人，博士，信息工程大學(xué)教授、博士生導(dǎo)師，主要研究方向?yàn)榭臻g信息網(wǎng)絡(luò)、云計算安全。