摘要
静态分析方法被广泛用于Android应用的隐私泄露检测,其以(Source,Sink)对形式检测潜在漏洞,但同时会产生大量虚警。针对该问题,提出一种上下文敏感和域敏感的污点分析方法。对污点传播的操作语义和一致性约束进行形式化定义,保证污点传播的语义正确性,同时分析插桩运行Android应用后产生的Trace片段,验证漏洞是否存在虚警。基于Soot实现原型系统并对DroidBench数据集中的70个应用进行分析,实验结果表明,该方法可成功验证4个虚警并发现8个漏报,表明其能有效判断静态分析结果的正确性。
Static analysis methods are widely used to detect privacy leaks in the Android applications and potential bugs are detected by the form of(Source,Sink),but many false alarms are generated as well.To address the problem,this paper proposes a context-sensitive and field-sensitive taint analysis approach.The operational semantics of taint propagation and the consistent constraints are formally defined to ensure taint propagation to be semantically correct.Trace segments generated after instrumenting and running an Android applications is also analyzed to verify if a potential bug is really true.A prototype system is implemented based on Soot and tested on seventy applications from the DroidBench dataset.Experimental results show that the proposed method can successfully verified four false positives and found eight false negatives,demonstrating that the proposed method is capable of verifying the correctness of static analysis results.
作者
秦彪
郭帆
杨晨霞
QIN Biao;GUO Fan;YANG Chenxia(College of Computer Information Engineering,Jiangxi Normal University,Nanchang 330022,China;Department of Computer Science,Yuzhang Normal University,Nanchang 330105,China)
出处
《计算机工程》
CAS
CSCD
北大核心
2020年第5期157-166,共10页
Computer Engineering
基金
国家自然科学基金(61562040)
江西省教育厅科学技术研究项目(GJJ161305,GJJ151330)。
关键词
污点分析
上下文敏感
域敏感
污点传播
形式化定义
taint analysis
context sensitivity
field sensitivity
taint propagation
formal definition