HornDroid：基于SMT求解的Android应用实用且可靠的静态分析
密码学与安全
2017-07-26 v1
摘要
我们提出HornDroid，一个用于Android应用信息流属性静态分析的新工具。HornDroid背后的核心思想是使用Horn子句来可靠地抽象Android应用的语义，并将安全属性表达为一组证明义务，由现成的SMT求解器自动解除。这种方法使得在仍使用现成验证工具的同时，通过微调分析来实现高度精确性成为可能，从而利用该领域的最新进展。事实上，HornDroid在社区提出的基准测试上优于最先进的Android静态分析工具。此外，HornDroid是首个附带可靠性形式化证明的Android静态分析工具，该证明覆盖了分析技术的核心：除了提供正确性保证外，该证明还使我们识别出一些影响先前某些Android静态分析工具所提供的可靠性保证的关键边界情况。
引用
@article{arxiv.1707.07866,
title = {HornDroid: Practical and Sound Static Analysis of Android Applications by SMT Solving},
author = {Stefano Calzavara and Ilya Grishchenko and Matteo Maffei},
journal= {arXiv preprint arXiv:1707.07866},
year = {2017}
}
备注
In Proceedings of 1st IEEE European Symposium on Security and Privacy (IEEE EuroS&P 2016)