一种基于进程代数的Android组件行为形式化描述方法  

Formal Description Method of Android Component Behavior Based on Process Algebra

作　　者：梁东魁[1,2] 申利民 马川[1,2] 冯佳音[1] 陈真 LIANG Dong-kui;SHEN Li-min;MA Chuan;FENG Jia-yin;CHEN Zhen(Yanshan University,School of Information Science and Engineering,Qinhuangdao 066004,China;Yanshan University,Engineering Training Center,Qinhuangdao 066004,China)

机构地区：[1]燕山大学信息科学与工程学院,河北秦皇岛066004 [2]燕山大学工程训练中心,河北秦皇岛066004

出　　处：《小型微型计算机系统》2021年第7期1561-1568,共8页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(61772450)资助;河北省自然科学基金项目(F2019203287)资助;河北省自然科学基金项目(F2017203307)资助;河北省高等学校科学技术研究项目(QN2020183)资助;河北省博士后科研项目(B2018003009)资助。

摘　　要：已有多种技术和方法用于Android恶意应用的检测,但关于应用行为形式化描述的研究仍有待完善.本文基于π演算提出一种使用进程代数从组件层次描述Android应用及组件行为的形式化描述方法.首先给出组件行为的基本语义和组件行为的定义,并给出了组件行为相应的演化规则,然后给出了组件交互行为的形式化描述,并应用于一个案例表明了方法的正确性和有效性,最后给出了基于模拟机制的行为判定规则,为应用行为的分析和判定提供有效支持.Many technologies and methods have been applied to detect the malicious application in Android,but the research on formal description of application behavior needs to be improved.Based onπ-calculus,the paper proposes a formal description method of Android application and component behavior at component level using process algebra.Firstly,the basic semantics of component behavior and the definition of component behavior are given,and the corresponding evolution rules are proposed.Then,the formal description of component interaction behavior is given,which is applied to a case to show the correctness and effectiveness.Finally,the behavior judgment rule based on simulation mechanism is given,which can provide effective support for the analysis and determination of application behavior.

关 键 词：恶意应用 组件行为 进程代数 Π演算 形式化描述 模拟机制 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]