一種基于進程代數的Android組件行為形式化描述方法

梁東魁，申利民，馬 川，馮佳音，陳 真

1(燕山大學 信息科學與工程學院，河北 秦皇島 066004)2(燕山大學 工程訓練中心，河北 秦皇島 066004)

1 引 言

Android是目前移動智能終端OS市場中占有率最高的操作系統，是惡意攻擊者和黑客的首要目標，Android惡意軟件和惡意行為的檢測一直是國內外的研究熱點.根據分析方式可分為靜態分析、動態分析、動靜態相結合的分析檢測方法[1]，已有多種技術和方法用于惡意軟件的監測，如基于特征碼的檢測[2，3]、基于權限的檢測[4，5]、基于行為的檢測[6，7]、基于機器學習的檢測[8，9]和基于數據挖掘的檢測[10，11]等.傳統的基于簽名的檢測技術對已知惡意代碼有很好的檢出率，但未知惡意代碼的漏報率很高.基于行為的檢測以應用行為作為判斷依據，通過構建惡意行為特征進行分析和判斷，對已知惡意代碼和未知惡意代碼有較好的檢測結果，但在未知攻擊和可疑行為的檢測判定中無法完全避免誤報和漏報.有學者將形式化方法引入Android應用行為的分析檢測研究.Bodei等[12]用π演算推導分析驗證軟件行為的安全性.Chaudhuri等[13]提出了基于語義的Android Apps形式化描述方法幫助理解應用的行為安全.Jia等[14]基于進程代數提出一個面向Android組件的無干擾形式化模型.Dam等[15]基于擴展λ-演算建立了Android Apps的形式化安全模型TreeDroid，可有效約束函數調用及參數傳遞的問題.He X等[16]用高級Petri網對Android權限框架建模，分析不同級別權限及其組合的關系.Wu Z等[17]用進程代數描述信息流控制過程，實現了能跟蹤和控制信息流的原型系統CDroid.馬川等[18]用形式化方法對Android應用組件通信行為建模，用于共謀攻擊的分析和檢測.Shen L等[19]提出一種基于功能和進程代數的應用行為檢測方法，用于Android應用中權限提升攻擊的檢測.

目前Android應用的行為檢測技術已實現對已知惡意代碼的高覆蓋性檢測，但對隱蔽攻擊及多組件協同開展的串謀攻擊和共謀攻擊等缺乏有效的分析和判定技術，在未知攻擊的檢測和判定中存在大量可疑行為和不確定行為，無法提供有效的分析和判定方法.在基于行為的Android惡意應用檢測中，現有分析和判定方法大都基于特征和特例，現有行為形式化的研究也大多針對安全策略，沒有對應用行為進行本質抽象和建模，不能滿足自動化分析和判定的需要，理論上缺乏一種普適的形式化方法對要監控和檢測的行為進行描述和刻畫，為應用行為的分析、推理和判定提供支持.

針對上述問題，本文引入進程代數的概念，建立Android應用元素與進程代數π演算的對應關系，用進程代數方法研究Android應用行為.首先基于π演算，提出了使用進程代數的Android組件行為形式化描述方法，給出組件行為的語義及演化規則；然后給出了各組件的行為定義及交互并發的過程描述，用一個實例表明方法是可行、有效的；最后在文中方法基礎上給出了基于行為等價-弱模擬的應用行為判定規則，為基于行為的Android惡意應用檢測提供支持.

2 Android應用到進程代數的映射

Android Apps由4大組件構成，組件中Content Provider可用Uri操作，其它組件必須借助Intent才能實現交互.Intent用于在Android組件間實現通信，若使用不當容易引發惡意調用、信息泄露、組件劫持等安全問題[20]，已有學者利用Intent進行惡意軟件檢測的研究[21，22].Android應用是由相互協作、并發交互的組件構成的復雜系統，具備高度并發、交互的特征，對應用全部行為的分析是極其龐大和復雜的工作，而形式化是一種公認的能有效減少設計錯誤、提高可靠性的方法，可用于復雜系統行為的抽象和研究.

進程代數的術語“進程(Process)”不同于操作系統的進程，表示系統的行為模式，通過動作的有限集描述系統行為.π演算中一個動作或事件是最小的行為，稱其為原子行為，包含若干動作組合的行為序列稱為進程，軟件行為是軟件執行的一系列動作或事件的總和.引入名字的概念，將消息、事件、動作等映射為名字，將通信端口映射為通道，允許名字在通道之間交流，增加動作前綴來描述并發和交互行為，最終將軟件行為用進程表達式來描述和刻畫.目前惡意攻擊不再局限于單一、孤立的攻擊方式，更多的是多組件開展的協同共謀攻擊，因此對適用于移動并發系統的π演算理論進行擴展并用于Android應用行為的研究.

Android應用行為可用進程中實例化后的組件實例的并發和交互來刻畫.在代碼層面描述行為時，一個基本行為就是一條語句或函數調用，組件行為是一系列程序語句或函數調用的外在表現.將組件的基本行為抽象為動作(Action)，根據是否與組件外部交互分為內部動作(Intra-action)和外部動作(Inter-action).內部動作表達組件的內部演化，獨立于外部環境，關系簡單易推導，外部動作能描述組件內部行為以及與外部環境的交互，行為描述和關系推導復雜.通過引入進程代數的語義和規則，將Android Apps運行于操作系統的同一或不同進程的組件實例建模為π演算的進程，將組件實例的交互映射為進程通信，將程序中的語句以及函數和方法的調用建模為動作，將程序中的變量、參數和運行過程中的數據、消息、事件、實體屬性等信息以及組件交互使用的Intent建模為名字.最終建立Android Apps元素到π演算的映射關系如表1所示.

表1 Android apps到π演算的映射關系Table 1 Mapping relationship from Android apps to π-calculus

目前Android應用研究中的進程代數方法多見于具體問題的模型建模和驗證，本文首次把進程代數用于基于行為的Android惡意應用檢測中應用行為形式化的研究.通過擴展進程代數π演算理論，抽象出Android應用領域的進程代數元素，定義相關算子和規則實現組件行為的形式化描述，使用進程代數作為抽象語言來描述應用行為.將Android應用中實體的交互行為用進程表達式和算子描述，并與實體間的并發行為復合，利用進程代數的推理和演算機制為基于進程等價實現應用行為的分析和判定提供支持，為基于行為的Android惡意應用檢測提供理論支撐.

3 Android組件行為描述和分析

將Android應用中的組件視為行為的主體和客體，用行為主體、行為客體、行為動作、主體輸入、客體輸出以及此過程中組件的狀態變化來刻畫和描述組件行為.通過實現組件行為的形式化描述，為應用中的串謀攻擊、共謀攻擊等惡意行為的分析和判定提供支持.

3.1 基本語義

定義5.組件行為(Component Behavior).組件行為的語法與語義由名字和一些符號按照下述語法(BNF)構成：

P∷=π.P|P1+P2|P1|P2|newaP|!P|0|√

(1)

1)“π.P”表示進程中成功執行動作π后轉換到P，“.”為前綴算子，表明π和P存在先后關系，是順序算子的一種表現形式.動作π定義如下：

(2)

π.P表示π是組件進程P的動作前綴，將其稱為衛式表達式，稱P被π護衛.型如P=a.P的衛式表達式稱為遞歸衛式.若P=a.P1和P1=b.P2，且P和P1不是遞歸衛式，若P=a.b.P2也不是遞歸衛式，則兩者可約簡表示為P=a.b.P2.表達式P=a.Q、Q=b.R和R=c.P均不是遞歸衛式，但三者嘗試約簡后得到的結果P=a.b.c.P是遞歸衛式，故不適用約簡.

2)“P1+P2”表示從組件進程P1和P2中選擇一個執行，“+”為選擇算子.具體結果根據上下文動作來確定，為不確定選擇操作.

3)“P1|P2”表示組件P1和P2并發執行，“|”為并發算子.如果并發過程中有衛式結構出現，則具體執行過程由上下文動作及相應規則確定.

4)“newaP”表示名字a受限于組件進程P內部，僅能在P中發生，“new”為限制算子，a為受囿名，可用(newa)P、new (a) P、(vx)P、v (x) P表示.

5)“!P”表示構造組件P的一個副本，“!”為復制算子.

6)“0|√”表示組件進程結束的兩種方式，“0”表示被強制終止，“√”表示正常結束.

3.2 演化規則

前綴(Prefix)算子規則：

選擇(Choice)算子規則：

上述部分對內部動作τ同樣成立.

并行(Parallel)算子規則：

3.3 組件行為定義和描述

應用交互時隨動作數量的增加，行為跡規模呈現幾何級增長，不利于進一步的分析和研究.在組件層次研究Android應用行為時，內部動作τ對組件遷移的影響微乎其微，因此忽略內部不可見動作，以用戶可觀察的、能引發組件交互的動作進行描述.將Android組件交互和通信的命令抽象為動作來描述應用和組件的行為，部分ICC命令如表2所示.

表2 ICC命令示例Table 2 ICC command example

3.3.1 Activity組件

Activity是與用戶交互的可視化接口，有運行(Running)、暫停(Paused)、停止(Stopped)、銷毀(Destroyed)4種狀態，由生命周期函數實現相應狀態的轉換，描述如下：

頁面作為信息載體和用戶操作界面，使用Intent封裝數據實現信息交換.Activity組件間交互時，即可作為交互動作的發起者，也可作為接受者，包括活動的發起、接受和結果的返回、接收，以及Activity的關閉，定義如下：

startActivity(y).Activity；

setResult(n).Activity；

finish.Activity.

Activity的狀態根據行為模式的不同亦會有相應改變，具體過程描述如下：

Activitydestroyed；

兩個Activity的一個典型交互過程為“從頁面A1切換到目標頁面A2，在時長t內執行若干動作e后關閉頁面A2并返回數據到頁面A1進行處理”.此過程的行為描述如下：

頁面A1切換到頁面A2后，A1處于停止狀態，A2處于運行狀態，此過程描述及頁面狀態轉換如下：

A1stopped|{x/y}A2running；

((onPause.A1paused).onCreate.onStart.onResume.A2running).

onStop.A1stopped.

經過時長t后，關閉A2返回數據到A1處理，最終A1處于運行狀態，A2被銷毀，此過程描述以及頁面狀態轉換如下：

A2destroyed|{m/n}A1running；

((onPause.A2paused).onRestart.onStart.onResume.

A1running).onStop.onDestroy.A2destroyed.

若調用Activity的組件為Activity之外的其它組件，則組件交互過程描述以及Activity的狀態轉換如下：

onCreate.onStart.onResume.Activityrunning.

3.3.2 Service組件

Service組件提供用戶和業務邏輯所需的服務，有運行(Running)和銷毀(Destroyed)兩種狀態，狀態轉換如下：

啟動方式開啟Service：

綁定方式開啟Service：

銷毀Service：

Service組件有啟動和綁定兩種使用方式，用于響應服務請求，包括開啟、綁定、解除綁定、停止，行為定義如下：

startS(y).Service；

stopS(y).Service；

bindS(y).Service；

unbindS(y).Service.

(vclients)Service；

clients(a).Service；

stopSelf.Service.

組件利用Intent實現數據封裝與Service通信實現信息交換.Service以startService()方式啟動后，若要停止服務需調用stopService()或stopSelf().StartService()的回調方法是onStartCommand()，如果服務不存在則先用onCreate()創建實例再執行回調方法，如果已存在則只執行回調方法.組件開啟/關閉服務的行為描述及Service狀態轉換如下：

Componet|{x/y}Servicerunning；

onCreate.onStartCommand.Servicerunning；

Componet|Servicedestroyed；

onDestroy.Servicedestroyed；

onDestroy.Servicedestroyed.

Service以bindService()啟動后需調用unbindService()或調用對象被銷毀才會停止.BindService()將調用者和服務綁定并建立通道，如果服務未運行則先執行onCreate()創建Service實例再執行onBind()，若已運行則執行onRebind().所有綁定的client都解除綁定后才可銷毀Service對象，組件綁定/解綁服務以及服務組件狀態轉換過程如下：

Componet|clients(x).Servicerunning；

onCreate.onBind.Servicerunning；

[clients=?]Servicedestroyed)；

onUnbind.([clients≠?]Servicerunning+

[clients=?]onDestroy.Servicedestroyed).

若Service同時調用startService()和bindService()，根據調用順序組件行為有所差異.一般先用startService()開啟服務，再按需調用bindService()進行服務的綁定，組件行為過程描述及Service狀態轉換如下：

Componet|{x/y}Servicerunning；

Componet|clients(m).Servicerunning；

(onCreate.onStartCommand.Servicerunning).onBind.Servicerunning.

先調用bindService()以綁定方式啟動Service，再調用startService()的過程描述及Service狀態轉換如下：

Componet|{m/n}Servicerunning；

Componet|clients(x).Servicerunning；

(onCreate.onBind.Servicerunning).onStartCommand.Servicerunning.

無論startService()和bindService()的調用順序如何，要停止服務需要同時使用unbindService()和stopService()，保證onUnbind()和onDestroy()的執行.組件行為如下：

Componet|[clients=?]Servicedestroyed.

3.3.3 Broadcast Receiver組件

Broadcast Receiver 是Android廣播中的廣播接收者，負責響應系統和組件的廣播，行為定義如下：

sendBroadcast(y).BroadcastReceiver.

應用的組件都可作為發送者發起廣播，由相應接收者在onReceive()中處理.一個廣播的生命周期很短，從創建開始到抵達目標執行完畢或超時被終止.以timeCost表示廣播存在時間，以timeOut表示超時時限，則組件行為如下：

BroadcastReceiver+[timeCost>timeOut]0).

3.3.4 Content Provider組件

Content Provider 用于存儲數據并提供數據共享，若要被外部進程訪問則需設置android：exported="true".其它組件通過Content Resolver類提供的方法操作Content Provider的數據，行為定義如下：

insertCP(u).ContentProvider；

deleteCP(u).ContentProvider；

updateCP(u).ContentProvider；

queryCP(u).ContentProvider.

其它組件通過建立Content Resolver類的實例作為客戶端，使用客戶端提供的insert()、delete()、update()和query()方法以Uri的形式實現Content Provider中數據的增加、刪除、更新和查詢.組件添加數據的行為描述如下：

式中，τ(r)是調用者建立Content Resolver類實例r的內部動作RegistContentResolver(r)，由r調用相應方法操作數據.將其抽象為組件的動作，簡化組件行為描述如下：

組件Content Provider中數據的刪除、更新和查詢過程和添加過程類似，在此不再贅述.

3.3.5 組件與數據庫的交互

insertDB(data).DataBase；

deleteDB(data).DataBase；

queryDB(data).DataBase；

updateDB(data).DataBase.

3.4 案例應用

以應用市場中一個存在隱私泄露行為的App為例，應用使用手機號進行注冊，注冊時需賦予應用讀取手機通訊錄和發送短信的權限，組件交互情況如圖1所示.

圖1 組件交互示意圖Fig.1 Component interaction diagram

應用啟動頁面為登錄界面，新用戶注冊后給出信息提示并返回用戶信息至登錄頁面，已有用戶可直接登錄，登錄主界面后開始播放背景音樂，同時提供用戶信息變更和其它功能.組件實例中LoginActivity、RegistActivity、MainActivity、ModifyActivity均可發起組件交互，能作為交互行為的主體和客體，行為如下：

setResult(info).LoginActivity；

startActiviy(regist).RegistActivity；

startActiviy(login).MainActivity；

startActiviy(modify).ModifyActivity；

MusicService、MyRecevier、ProvideroutSide沒有發起交互，僅用于響應其它組件的交互，行為如下：

startS(music).MusicService；

stopS(music).MusicService；

sendBroadcast(msg).MyRecevier；

queryCP(phoneBook).ProvideroutSide.

LoginActivity中根據用戶選擇choice可發起與注冊頁面和主界面的交互.以isChecked表示登錄驗證結果，驗證通過登錄主界面，否則重新登錄.組件行為描述如下：

setResult(info).LoginActivity|startActivity(regist).

LoginActivity|startActivity(login).MainActivity)+[isChecked=Flase]! LoginActivity)).

RegistActivity中用手機號注冊，取消操作則關閉頁面，確認時以isExsited表示用戶是否存在.若不存在則注冊并保存信息，然后給出提示，最后返回用戶名到登錄界面，若已存在則重新填寫注冊信息.組件行為描述如下：

queryDB(phone).DataBase). ([isExsited=False]

DataBase|sendBroadcast(msg).MyRecevier|setResult(info).

LoginActivity)+[isExsited=True] !RegistActivity)+[operate=Cancel]finish.RegistActivity.

MainActivity中登錄后播放背景音樂、獲取并顯示用戶信息，可以讀取手機通訊錄，并提供用戶信息修改及其它功能，主界面關閉時結束背景音樂.組件行為描述如下：

startS(music).MusicService|queryDB(phone).

queryCP(phoneBook).ProvideroutSide).

MainActivity|stopS(music).MusicService).

ModifyActivity中可修改登錄用戶的個人信息，確認后進行更新，取消操作則關閉當前頁面，組件行為描述為：

ModifyActivity|updateDB(newInfo).DataBase+[confirm=No]finish.ModifyActivity).

對應用組件的行為形式化描述后即可利用文中的演化規則做進一步的分析和行為判定研究.通過分析應用得到應用組件的實例和行為定義，使用式(1)形式建立各組件行為的形式化表達式，利用演化規則對組件行為進行推理，并利用進程等價機制對Android應用行為和惡意行為的行為相似性進行分析，用模擬關系判定應用行為是否為惡意行為，實現Android惡意應用的檢測.

4 基于行為等價-弱模擬的行為判定

預期行為是為實現應用功能、滿足用戶需求所需的動作序列及組合，根據應用行為是否是預期行為做如下分類.

1)可信行為.行為可被監測識別，并且是預期行為.

2)有害行為.行為可被監測識別，并且是非預期行為.

3)可疑行為.行為可被監測，但無法被完全識別為預期行為或是非預期行為，只能被部分識別.

Android Apps中存在不符合預期的行為即為惡意應用.如果應用行為都是預期的，即應用行為都是可信的，那么應用是可信的.如果應用中存在非預期行為，即應用行為中存在有害行為，則應用是惡意的.文中已給出Android應用組件行為的形式化描述，根據應用行為與預期行為或非預期行為的關系，基于行為等價中的模擬機制進行分類和判定.

4.1 行為等價-強模擬和弱模擬

模擬是一個行為對另一行為的單向描述，P模擬Q表明P的行為模式至少和Q一樣豐富.互模擬是行為間的雙向模擬，目的是驗證行為的等價性，P互模擬Q表明兩者在某種程度上是相似的.

定義6.強模擬.行為P強模擬行為Q，當且僅當對于所有的動作a∈Q，a為式(2)中的任一形式，滿足以下條件：

定義7.強互模擬.行為P強互模擬行為Q(記為P～Q)，當且僅當對于所有的動作a∈Q，a為式(2)中的任一形式，滿足以下條件：

強互模擬也稱強等價，但“P強等價于Q”和“P強模擬Q且Q強模擬P”不是相等的條件.前者表示P和Q強互模擬，蘊含了后者，前者是一個更嚴格的條件.考慮進程P和Q的相似性，都包含兩個動作a和b，如圖2所示.

圖2 P和Q的行為示意圖Fig.2 Behavior diagram of P and Q

先給出結論：“P強模擬Q，且Q強模擬P，但P和Q不是強互模擬的”.

證明：

1)首先證明P強模擬Q.

由強模擬定義可知P強模擬Q.

2)然后證明Q強模擬P.

由強模擬定義可知Q強模擬P.

3)最后證明P和Q不是強互模擬的.

由強互模擬定義可知，P和Q不是強互模擬的.

綜上所述即可得出前文結論.

定義8.弱模擬.行為P弱模擬行為Q，當且僅當對于所有的動作a∈Q，a為式(2)中的任一形式，滿足以下條件：

定義9.弱互模擬.行為P弱互模擬行為Q(記為P≈Q)，當且僅當對于所有的動作a∈Q，a為式(2)中的任一形式，滿足：

弱互模擬也稱觀察等價或弱等價.強互模擬、強模擬、弱互模擬和弱模擬的條件強度是遞減的，可根據實際需求選擇相應的模擬機制進行研究.將圖2中的兩個進程用式(1)和式(2)的形式描述，以f表示選擇算子的條件，忽略行為中的中間狀態簡化結構，描述如下：

P=[f]a.p3+[not(f)]a.b.p2；

Q=a.b.q2.

根據上述表達式，由弱模擬定義顯然可知P弱模擬Q，且Q弱模擬P，即P弱互模擬Q，因此行為P和Q有相同的性質分類，同屬可信行為或同屬有害行為.

在3.4節案例中，主界面已有讀取手機通訊錄的權限，若ModifyActivity有發送短信的權限，那么應用存在信息泄露的隱患.忽略主界面和ModifyActivity的中間狀態以及與其它組件的交互，信息泄露行為如下：

startActiviy(i).(newsendMsg)e2.update.

ModifyActivity.

圖3 行為M和行為N的示意圖Fig.3 Schematic diagram of behavior M and behavior N

綜上所述，由弱模擬定義可知應用行為M弱模擬有害行為N，應用行為M是有害行為，3.4的案例中存在惡意行為，因此判定此應用為惡意應用.

針對應用中的可疑行為和不確定行為進行分析和判定時，弱模擬的范疇已經滿足需求，因此采用弱模擬并基于行為等價機制給出行為的判定規則.

4.2 基于弱模擬的行為判定規則

規則1.可信行為判定

若預期行為Q弱模擬實體行為P，則P是可信行為.

規則2.有害行為判定

實體行為P弱模擬非預期行為R，則P是有害行為.

規則3.可疑行為判定

若實體行為P弱模擬預期行為Q，或非預期行為R弱模擬實體行為P，則P是可疑行為.

如果實體行為弱模擬預期行為，僅表明實體行為的跡中包含可信行為的部分序列，但不保證所有跡都可信，不能直接對其給出判定，所以判定為可疑行為.如果非預期行為弱模擬實體行為，表明跡中存在有害行為中的部分或全部動作序列，但并不必然構成有害行為，因此判定為可疑行為.

推論1.如果實體行為P弱互模擬預期行為Q，則P是可信行為.

推論2.如果實體行為P弱互模擬非預期行為R，則P是有害行為.

如果實體行為和預期行為弱等價，表明兩者具有相似行為，判定實體行為是可信的.如果實體行為和非預期行為弱等價，表明兩者具有相似行為，判定實體行為是有害的.

對應用行為的性質判定時，需先采用式(1)形式構建應用和組件的預期行為和非預期行為的形式化描述，形成先驗的規則庫，然后根據規則進行判定，流程如下：

1)應用或組件行為中存在有害行為，則判定是有害的；

2)應用和組件行為全部是預期行為，則判定是可信的；

3)應用或組件行為中存在可疑行為，則判定是可疑的，需用弱模擬和弱互模擬規則進一步判定；

4)應用或組件行為弱模擬非預期行為，或被非預期行為弱互模擬，則判定是有害的；

5)應用和組件行為弱互模擬預期行為，或被預期行為弱模擬，則判定是可信的.

過程中不斷將可疑行為的判定抽象為新的預期行為或非預期行為規則，完善規則庫，后續判定可直接利用規則，此過程是行為判定的難點所在，也是下一步的研究重點.文中通過對應用行為進行分析和抽象，提出了行為的形式化描述方法，能使用相應的演化規則和進程代數的推理、演算機制實現應用行為的分類判定，為基于行為的Android惡意應用檢測提供理論支持.

5 結 論

通過分析Android應用組件，針對其并發、交互特性，基于進程代數提出了一種Android組件行為的形式化描述方法，給出了組件行為的定義和演化規則，從組件層次給出組件的行為定義和交互過程描述，并用一個案例說明方法的可行性和有效性，最后給出了基于行為等價-弱模擬的行為判定規則，可在形式化基礎上進行行為分析和判定.文中方法有助于揭示Android Apps行為的分析和判定規律，為應用行為的分析和研究提供理論支持，特別是對涉及組件協同交互的串謀攻擊和共謀攻擊等惡意行為的分析和檢測有重要作用.后續將結合組件內部動作建立行為規則庫，尋找組件行為的關鍵路徑，開展行為的自動化分析和判定研究.