基于通信順序進程的Android程序復雜信息流分析方法

袁占慧，楊智，張紅旗，金舒原，杜學繪

基于通信順序進程的Android程序復雜信息流分析方法

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

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

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

安卓；信息流分析；隱私防護；形式化分析；通信順序進程

1 引言

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

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

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

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

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

形式化檢測的關鍵是能夠用形式化語言準確、全面地描述代碼行為，并建立行為模型。模型檢查過程通過數學推導由形式化工具實現自動化。然而，現有的形式化信息流分析方法存在不足。例如，文獻[28]中的LEILA系統，無法處理虛擬調用和反射調用的混淆。此外，數據流沒有被考慮，因為它沒有對賦值語句建模。

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

本文的主要貢獻如下。

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

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

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

圖1 整體工作流程系統框架

Figure 1 The framework of the work process system

2 系統設計

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

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

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

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

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

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

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

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

3 CSP形式化建模

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

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

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

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

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

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

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

3.1 數據流行為建模

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

圖3 數據流行為建模

Figure 3 Modeling for data flow

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

3.2 過程內控制流行為建模

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

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

圖4 過程內控制流行為建模

Figure 4 Modeling for intraprocedural control flow

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

3.3 過程間控制流行為建模

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

3.3.1 函數調用建模

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

圖5 函數調用行為建模

Figure 5 Modeling for function call

對于InvokeStmt調用語句，當被調用的method有參數和返回值時，CSP模型中的param.method!arg0、param.method!1等表示向method依次傳遞實參的事件，retval.method?val表示從method接收val的事件，call.method和return.method分別表示method調用開始和結束的事件。當被調用的方法沒有參數或返回值時，在進程表達式中去掉相應的事件，通過IdentityStmt語句進行實參接收。

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

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

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

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

圖6 系統的調用同步機制

Figure 6 System call synchronization mechanism

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

圖7 InvokeStmt及被調用方法之間的同步

Figure 7 Synchronization between invokeStmt and the called method

3.3.2 反射行為建模

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

圖8 反射行為中的方法調用示例

Figure 8 Example of method calls in reflection

forName方法的調用，在allclasses數組中查找名稱為cla的值的類，并將其索引allclasses_ index(cla)賦值給，對應的CSP進程如圖9(a)所示。

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

invoke方法的調用，主要負責反射調用的具體執(zhí)行，CSP進程如圖9(c)所示。

圖9 反射行為建模

Figure 9 Modeling for reflection

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

圖10 構造反射過程

Figure 10 Constructing for reflection

3.3.3 虛函數建模

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

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

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

圖11 虛函數建模

Figure 11 Modeling for virtual function

4 信息流性質刻畫與驗證

4.1 信息流性質刻畫

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

為了簡化FDR模型檢測的復雜程度，對CSP模型中與信息流傳播不相關的代碼行為進行隱藏，流程為：uselessevents={|transfer,calldeal, api.normalx|}，SAFE_SAMPLE=SAMPLE uselessevents。接下來定義信息流發(fā)生泄露的性質為PROPERTY=source.taint->sink.taint->STOP。基于對簡化信息流CSP模型和信息流泄露性質的定義，得出在CSP模型中發(fā)現信息流泄露路徑的方式為assert SAFE_SAMPLE [T= PROPERTY。

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

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

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

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

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

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

形如上述類型的復雜信息流分析模型，都能夠轉化為以CSP模型描述的信息流性質，進而應用到模型檢測中實現信息流分析挖掘功能。

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

4.2 信息流性質驗證

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

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

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

5 實驗評估

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

5.1 功能測試

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

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

表1 FlowDroid參數配置

圖12 良性和惡意軟件應用程序的行為比較

Figure 12 Behavior comparison between benign and malicious applications

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

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

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

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

表2 InsecureBankv2信息流泄露路徑檢測結果

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

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

表3 DroidBench2.0信息流泄露檢測結果

FlowDroid和本文方法都漏掉了14條路徑，主要是因為一些特殊代碼沒有被跟蹤，包括在獨立組件（Singletons1/ICC）、ICC處理程序（ServiceCommunication1/ICC）、靜態(tài)初始化方法（StaticInitialization1/General java）、格式化程序（StringFormatter1/General java）、文件系統訪問（PrivateDataLeak3/AndroidSpecific）、無目標類的類型信息的方法反射調用（Reflection3/ Reflection）中的污點傳播等情況。

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

5.2 性能測試

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

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

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

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

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

表4 性能測試結果

6 結束語

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

國家自然科學基金（62176265, 61972040）

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

袁占慧, 楊智, 張紅旗, 等. 基于通信順序進程的Android程序復雜信息流分析方法[J]. 網絡與信息安全學報, 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?），男，吉林遼源人，信息工程大學碩士生，主要研究方向為移動智能終端的信息流控制與隱私保護。

楊智（1975?），男，河南開封人，博士，信息工程大學副教授，主要研究方向為操作系統安全、云計算安全、隱私保護。

張紅旗（1962?），男，河北遵化人，博士，信息工程大學教授、博士生導師，主要研究方向為網絡安全、風險評估、等級保護和信息安全管理等。

金舒原（1974?），女，吉林白城人，博士，中山大學教授、博士生導師，主要研究方向為隱私保護、漏洞分析等。

杜學繪（1968?），女，河南新鄉(xiāng)人，博士，信息工程大學教授、博士生導師，主要研究方向為空間信息網絡、云計算安全。