一種基于進(jìn)程代數(shù)的Android組件行為形式化描述方法

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

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

1 引 言

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

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

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

2 Android應(yīng)用到進(jìn)程代數(shù)的映射

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

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

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

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

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

3 Android組件行為描述和分析

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

3.1 基本語義

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

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

(1)

1)“π.P”表示進(jìn)程中成功執(zhí)行動(dòng)作π后轉(zhuǎn)換到P，“.”為前綴算子，表明π和P存在先后關(guān)系，是順序算子的一種表現(xiàn)形式.動(dòng)作π定義如下：

(2)

π.P表示π是組件進(jìn)程P的動(dòng)作前綴，將其稱為衛(wèi)式表達(dá)式，稱P被π護(hù)衛(wèi).型如P=a.P的衛(wèi)式表達(dá)式稱為遞歸衛(wèi)式.若P=a.P1和P1=b.P2，且P和P1不是遞歸衛(wèi)式，若P=a.b.P2也不是遞歸衛(wèi)式，則兩者可約簡(jiǎn)表示為P=a.b.P2.表達(dá)式P=a.Q、Q=b.R和R=c.P均不是遞歸衛(wèi)式，但三者嘗試約簡(jiǎn)后得到的結(jié)果P=a.b.c.P是遞歸衛(wèi)式，故不適用約簡(jiǎn).

2)“P1+P2”表示從組件進(jìn)程P1和P2中選擇一個(gè)執(zhí)行，“+”為選擇算子.具體結(jié)果根據(jù)上下文動(dòng)作來確定，為不確定選擇操作.

3)“P1|P2”表示組件P1和P2并發(fā)執(zhí)行，“|”為并發(fā)算子.如果并發(fā)過程中有衛(wèi)式結(jié)構(gòu)出現(xiàn)，則具體執(zhí)行過程由上下文動(dòng)作及相應(yīng)規(guī)則確定.

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

5)“!P”表示構(gòu)造組件P的一個(gè)副本，“!”為復(fù)制算子.

6)“0|√”表示組件進(jìn)程結(jié)束的兩種方式，“0”表示被強(qiáng)制終止，“√”表示正常結(jié)束.

3.2 演化規(guī)則

前綴(Prefix)算子規(guī)則：

選擇(Choice)算子規(guī)則：

上述部分對(duì)內(nèi)部動(dòng)作τ同樣成立.

并行(Parallel)算子規(guī)則：

3.3 組件行為定義和描述

應(yīng)用交互時(shí)隨動(dòng)作數(shù)量的增加，行為跡規(guī)模呈現(xiàn)幾何級(jí)增長(zhǎng)，不利于進(jìn)一步的分析和研究.在組件層次研究Android應(yīng)用行為時(shí)，內(nèi)部動(dòng)作τ對(duì)組件遷移的影響微乎其微，因此忽略內(nèi)部不可見動(dòng)作，以用戶可觀察的、能引發(fā)組件交互的動(dòng)作進(jìn)行描述.將Android組件交互和通信的命令抽象為動(dòng)作來描述應(yīng)用和組件的行為，部分ICC命令如表2所示.

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

3.3.1 Activity組件

Activity是與用戶交互的可視化接口，有運(yùn)行(Running)、暫停(Paused)、停止(Stopped)、銷毀(Destroyed)4種狀態(tài)，由生命周期函數(shù)實(shí)現(xiàn)相應(yīng)狀態(tài)的轉(zhuǎn)換，描述如下：

頁(yè)面作為信息載體和用戶操作界面，使用Intent封裝數(shù)據(jù)實(shí)現(xiàn)信息交換.Activity組件間交互時(shí)，即可作為交互動(dòng)作的發(fā)起者，也可作為接受者，包括活動(dòng)的發(fā)起、接受和結(jié)果的返回、接收，以及Activity的關(guān)閉，定義如下：

startActivity(y).Activity；

setResult(n).Activity；

finish.Activity.

Activity的狀態(tài)根據(jù)行為模式的不同亦會(huì)有相應(yīng)改變，具體過程描述如下：

Activitydestroyed；

兩個(gè)Activity的一個(gè)典型交互過程為“從頁(yè)面A1切換到目標(biāo)頁(yè)面A2，在時(shí)長(zhǎng)t內(nèi)執(zhí)行若干動(dòng)作e后關(guān)閉頁(yè)面A2并返回?cái)?shù)據(jù)到頁(yè)面A1進(jìn)行處理”.此過程的行為描述如下：

頁(yè)面A1切換到頁(yè)面A2后，A1處于停止?fàn)顟B(tài)，A2處于運(yùn)行狀態(tài)，此過程描述及頁(yè)面狀態(tài)轉(zhuǎn)換如下：

A1stopped|{x/y}A2running；

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

onStop.A1stopped.

經(jīng)過時(shí)長(zhǎng)t后，關(guān)閉A2返回?cái)?shù)據(jù)到A1處理，最終A1處于運(yùn)行狀態(tài)，A2被銷毀，此過程描述以及頁(yè)面狀態(tài)轉(zhuǎn)換如下：

A2destroyed|{m/n}A1running；

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

A1running).onStop.onDestroy.A2destroyed.

若調(diào)用Activity的組件為Activity之外的其它組件，則組件交互過程描述以及Activity的狀態(tài)轉(zhuǎn)換如下：

onCreate.onStart.onResume.Activityrunning.

3.3.2 Service組件

Service組件提供用戶和業(yè)務(wù)邏輯所需的服務(wù)，有運(yùn)行(Running)和銷毀(Destroyed)兩種狀態(tài)，狀態(tài)轉(zhuǎn)換如下：

啟動(dòng)方式開啟Service：

綁定方式開啟Service：

銷毀Service：

Service組件有啟動(dòng)和綁定兩種使用方式，用于響應(yīng)服務(wù)請(qǐng)求，包括開啟、綁定、解除綁定、停止，行為定義如下：

startS(y).Service；

stopS(y).Service；

bindS(y).Service；

unbindS(y).Service.

(vclients)Service；

clients(a).Service；

stopSelf.Service.

組件利用Intent實(shí)現(xiàn)數(shù)據(jù)封裝與Service通信實(shí)現(xiàn)信息交換.Service以startService()方式啟動(dòng)后，若要停止服務(wù)需調(diào)用stopService()或stopSelf().StartService()的回調(diào)方法是onStartCommand()，如果服務(wù)不存在則先用onCreate()創(chuàng)建實(shí)例再執(zhí)行回調(diào)方法，如果已存在則只執(zhí)行回調(diào)方法.組件開啟/關(guān)閉服務(wù)的行為描述及Service狀態(tài)轉(zhuǎn)換如下：

Componet|{x/y}Servicerunning；

onCreate.onStartCommand.Servicerunning；

Componet|Servicedestroyed；

onDestroy.Servicedestroyed；

onDestroy.Servicedestroyed.

Service以bindService()啟動(dòng)后需調(diào)用unbindService()或調(diào)用對(duì)象被銷毀才會(huì)停止.BindService()將調(diào)用者和服務(wù)綁定并建立通道，如果服務(wù)未運(yùn)行則先執(zhí)行onCreate()創(chuàng)建Service實(shí)例再執(zhí)行onBind()，若已運(yùn)行則執(zhí)行onRebind().所有綁定的client都解除綁定后才可銷毀Service對(duì)象，組件綁定/解綁服務(wù)以及服務(wù)組件狀態(tài)轉(zhuǎn)換過程如下：

Componet|clients(x).Servicerunning；

onCreate.onBind.Servicerunning；

[clients=?]Servicedestroyed)；

onUnbind.([clients≠?]Servicerunning+

[clients=?]onDestroy.Servicedestroyed).

若Service同時(shí)調(diào)用startService()和bindService()，根據(jù)調(diào)用順序組件行為有所差異.一般先用startService()開啟服務(wù)，再按需調(diào)用bindService()進(jìn)行服務(wù)的綁定，組件行為過程描述及Service狀態(tài)轉(zhuǎn)換如下：

Componet|{x/y}Servicerunning；

Componet|clients(m).Servicerunning；

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

先調(diào)用bindService()以綁定方式啟動(dòng)Service，再調(diào)用startService()的過程描述及Service狀態(tài)轉(zhuǎn)換如下：

Componet|{m/n}Servicerunning；

Componet|clients(x).Servicerunning；

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

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

Componet|[clients=?]Servicedestroyed.

3.3.3 Broadcast Receiver組件

Broadcast Receiver 是Android廣播中的廣播接收者，負(fù)責(zé)響應(yīng)系統(tǒng)和組件的廣播，行為定義如下：

sendBroadcast(y).BroadcastReceiver.

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

BroadcastReceiver+[timeCost>timeOut]0).

3.3.4 Content Provider組件

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

insertCP(u).ContentProvider；

deleteCP(u).ContentProvider；

updateCP(u).ContentProvider；

queryCP(u).ContentProvider.

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

式中，τ(r)是調(diào)用者建立Content Resolver類實(shí)例r的內(nèi)部動(dòng)作RegistContentResolver(r)，由r調(diào)用相應(yīng)方法操作數(shù)據(jù).將其抽象為組件的動(dòng)作，簡(jiǎn)化組件行為描述如下：

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

3.3.5 組件與數(shù)據(jù)庫(kù)的交互

insertDB(data).DataBase；

deleteDB(data).DataBase；

queryDB(data).DataBase；

updateDB(data).DataBase.

3.4 案例應(yīng)用

以應(yīng)用市場(chǎng)中一個(gè)存在隱私泄露行為的App為例，應(yīng)用使用手機(jī)號(hào)進(jìn)行注冊(cè)，注冊(cè)時(shí)需賦予應(yīng)用讀取手機(jī)通訊錄和發(fā)送短信的權(quán)限，組件交互情況如圖1所示.

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

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

setResult(info).LoginActivity；

startActiviy(regist).RegistActivity；

startActiviy(login).MainActivity；

startActiviy(modify).ModifyActivity；

MusicService、MyRecevier、ProvideroutSide沒有發(fā)起交互，僅用于響應(yīng)其它組件的交互，行為如下：

startS(music).MusicService；

stopS(music).MusicService；

sendBroadcast(msg).MyRecevier；

queryCP(phoneBook).ProvideroutSide.

LoginActivity中根據(jù)用戶選擇choice可發(fā)起與注冊(cè)頁(yè)面和主界面的交互.以isChecked表示登錄驗(yàn)證結(jié)果，驗(yàn)證通過登錄主界面，否則重新登錄.組件行為描述如下：

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

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

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

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

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

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

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

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

queryCP(phoneBook).ProvideroutSide).

MainActivity|stopS(music).MusicService).

ModifyActivity中可修改登錄用戶的個(gè)人信息，確認(rèn)后進(jìn)行更新，取消操作則關(guān)閉當(dāng)前頁(yè)面，組件行為描述為：

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

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

4 基于行為等價(jià)-弱模擬的行為判定

預(yù)期行為是為實(shí)現(xiàn)應(yīng)用功能、滿足用戶需求所需的動(dòng)作序列及組合，根據(jù)應(yīng)用行為是否是預(yù)期行為做如下分類.

1)可信行為.行為可被監(jiān)測(cè)識(shí)別，并且是預(yù)期行為.

2)有害行為.行為可被監(jiān)測(cè)識(shí)別，并且是非預(yù)期行為.

3)可疑行為.行為可被監(jiān)測(cè)，但無法被完全識(shí)別為預(yù)期行為或是非預(yù)期行為，只能被部分識(shí)別.

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

4.1 行為等價(jià)-強(qiáng)模擬和弱模擬

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

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

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

強(qiáng)互模擬也稱強(qiáng)等價(jià)，但“P強(qiáng)等價(jià)于Q”和“P強(qiáng)模擬Q且Q強(qiáng)模擬P”不是相等的條件.前者表示P和Q強(qiáng)互模擬，蘊(yùn)含了后者，前者是一個(gè)更嚴(yán)格的條件.考慮進(jìn)程P和Q的相似性，都包含兩個(gè)動(dòng)作a和b，如圖2所示.

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

先給出結(jié)論：“P強(qiáng)模擬Q，且Q強(qiáng)模擬P，但P和Q不是強(qiáng)互模擬的”.

證明：

1)首先證明P強(qiáng)模擬Q.

由強(qiáng)模擬定義可知P強(qiáng)模擬Q.

2)然后證明Q強(qiáng)模擬P.

由強(qiáng)模擬定義可知Q強(qiáng)模擬P.

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

由強(qiáng)互模擬定義可知，P和Q不是強(qiáng)互模擬的.

綜上所述即可得出前文結(jié)論.

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

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

弱互模擬也稱觀察等價(jià)或弱等價(jià).強(qiáng)互模擬、強(qiáng)模擬、弱互模擬和弱模擬的條件強(qiáng)度是遞減的，可根據(jù)實(shí)際需求選擇相應(yīng)的模擬機(jī)制進(jìn)行研究.將圖2中的兩個(gè)進(jìn)程用式(1)和式(2)的形式描述，以f表示選擇算子的條件，忽略行為中的中間狀態(tài)簡(jiǎn)化結(jié)構(gòu)，描述如下：

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

Q=a.b.q2.

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

在3.4節(jié)案例中，主界面已有讀取手機(jī)通訊錄的權(quán)限，若ModifyActivity有發(fā)送短信的權(quán)限，那么應(yīng)用存在信息泄露的隱患.忽略主界面和ModifyActivity的中間狀態(tài)以及與其它組件的交互，信息泄露行為如下：

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

ModifyActivity.

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

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

針對(duì)應(yīng)用中的可疑行為和不確定行為進(jìn)行分析和判定時(shí)，弱模擬的范疇已經(jīng)滿足需求，因此采用弱模擬并基于行為等價(jià)機(jī)制給出行為的判定規(guī)則.

4.2 基于弱模擬的行為判定規(guī)則

規(guī)則1.可信行為判定

若預(yù)期行為Q弱模擬實(shí)體行為P，則P是可信行為.

規(guī)則2.有害行為判定

實(shí)體行為P弱模擬非預(yù)期行為R，則P是有害行為.

規(guī)則3.可疑行為判定

若實(shí)體行為P弱模擬預(yù)期行為Q，或非預(yù)期行為R弱模擬實(shí)體行為P，則P是可疑行為.

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

推論1.如果實(shí)體行為P弱互模擬預(yù)期行為Q，則P是可信行為.

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

如果實(shí)體行為和預(yù)期行為弱等價(jià)，表明兩者具有相似行為，判定實(shí)體行為是可信的.如果實(shí)體行為和非預(yù)期行為弱等價(jià)，表明兩者具有相似行為，判定實(shí)體行為是有害的.

對(duì)應(yīng)用行為的性質(zhì)判定時(shí)，需先采用式(1)形式構(gòu)建應(yīng)用和組件的預(yù)期行為和非預(yù)期行為的形式化描述，形成先驗(yàn)的規(guī)則庫(kù)，然后根據(jù)規(guī)則進(jìn)行判定，流程如下：

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

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

3)應(yīng)用或組件行為中存在可疑行為，則判定是可疑的，需用弱模擬和弱互模擬規(guī)則進(jìn)一步判定；

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

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

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

5 結(jié) 論

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