面向移动应用软件信息泄露的模型检测研究  

Model Checking for Software Information Leakage in Mobile Application

作　　者：过辰楷[1] 许静[1] 司冠南[2] 李恩鹏[1] 徐思涵 

机构地区：[1]南开大学计算机与控制工程学院,天津300350 [2]山东交通学院信息科学与电气工程学院,济南250357

出　　处：《计算机学报》2016年第11期2324-2343,共20页Chinese Journal of Computers

基　　金：国家自然科学基金(61402264);天津市科学技术委员会项目(12JCZDJC20800);国家科技支撑计划(2013BAH01B05)资助~~

摘　　要：移动平台上的应用软件私密信息泄露漏洞关注违背用户意愿的接口或数据暴露,而泄露形式和内容的复杂性增添了该类漏洞的检测难度.现有方法主要利用传统的静态数据流分析及动态监控等技术,易发生漏报和误报,且无法处理隐式信息泄露问题.该文首次将基于线性时序逻辑(Linear Temporal Logic,LTL)的模型检测技术应用于移动软件信息泄露检测上,提出了一种基于安全要素语句插装的泄露检测方法.文章首先针对代码中的安全要素提出一种信息泄露抽象关系模型;其次设计驱动生成规则和插装算法,在目标应用上生成可规约系统;继而设计具有通用意义的LTL泄露检测属性并利用符号执行技术优化检测算法;最后构建支持移动平台的模拟方法库,开发了原型检测系统(Leakage Finder of Android,LFDroid).公开数据集实验及对比分析表明,该文方法可以为含有隐式信息泄露数据集提供更为精确的漏洞检测,相较于传统方法准确率和召回率均具有明显优势,除此之外亦发现了3个真实移动应用的5个隐式泄露漏洞威胁.Program interfaces exposed against user's wishes can lead to private information leakages within mobile applications.However,the complexity of design and context increases the detection difficulties of such leakages.Existing methods mainly rely on traditional static data flow analysis and dynamic monitoring techniques,which suffer from amounts of false negatives and false positives,and can hardly handle implicit information leakage problems.In this paper,the LTL(Linear Temporal Logic)model checking techniques are exploited for the first time to address those problems.Meanwhile,a statement instrumentation method based on the security features is proposed.Firstly,an abstract model of private information leakage is extracted from a targeted mobile application.Secondly,the driven generation rules and the instrumentation algorithm are constructed to generate the executable codes for model checking.Thirdly,a set of universal LTL properties are presented for detecting the information leakage.Besides,an optimal leakage detection algorithm is proposed to improve the detection efficiency.Finally,this paper also builds a mockup library of mobile platform,by which a corresponding prototype systemLFDroid(Leakage Finder of Android)is developed. The experiment results on public benchmarks show that LFDroid can detect the implicit information leakage vulnerabilities smoothly and obtain a higher precision and recall compared to traditional methods.Meanwhile,LFDroid also finds out five implicit flow vulnerabilities within three real-world applications.

关 键 词：模型检测 移动应用软件 信息泄露 线性时序逻辑 漏洞检测 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]