一种基于进程代数的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行为的分析和判定规律，为应用行为的分析和研究提供理论支持，特别是对涉及组件协同交互的串谋攻击和共谋攻击等恶意行为的分析和检测有重要作用.后续将结合组件内部动作建立行为规则库，寻找组件行为的关键路径，开展行为的自动化分析和判定研究.