面向移动应用软件信息泄露的模型检测研究
移动平台上的应用软件私密信息泄露漏洞关注违背用户意愿的接口或数据暴露，而泄露形式和内容的复杂性增添了该类漏洞的检测难度。现有方法主要利用传统的静态数据流分析及动态监控等技术，易发生漏报和误报，且无法处理隐式信息泄露问题。该文首次将基于线性时序逻辑（Linear Temporal Logic，LTL）的模型检测技术应用于移动软件信息泄露检测上，提出了一种基于安全要素语句插装的泄露检测方法。文章首先针对代码中的安全要素提出一种信息泄露抽象关系模型；其次设计驱动生成规则和插装算法，在目标应用上生成可规约系统；继而设计具有通用意义的 LTL 泄露检测属性并利用符号执行技术优化检测算法；最后构建支持移动平台的模拟方法库，开发了原型检测系统（Leakage Finder of Android，LFDroid）。公开数据集实验及对比分析表明，该文方法可以为含有隐式信息泄露数据集提供更为精确的漏洞检测，相较于传统方法准确率和召回率均具有明显优势，除此之外亦发现了3个真实移动应用的5个隐式泄露漏洞威胁。
模型检测、移动应用软件、信息泄露、线性时序逻辑、漏洞检测
39
TP311(计算技术、计算机技术)
．本课题得到国家自然科学基金61402264;天津市科学技术委员会项目12JCZDJC20800;国家科技支撑计划2013BAH01B05资助．
2016-11-30（万方平台首次上网日期，不代表论文的发表时间）
共20页
2324-2343
