面向 Android 应用静态分析的可靠流敏感堆抽象
密码学与安全
2017-06-13 v2 编程语言
摘要
本文提出首个针对 Android 应用的静态分析，该分析在堆抽象上既是流敏感的，又相对于 Android 平台的丰富形式化模型被证明是可靠的。我们将该分析形式化为一组 Horn 子句，这些子句定义了待分析 Android 应用语义的一个可靠上近似，借鉴了近期性抽象的思想并将其扩展到我们的并发设定中。此外，我们在 HornDroid（一个先进的 Android 应用信息流分析器）中实现了该分析。我们的扩展使得 HornDroid 能够对堆分配数据结构执行强更新，从而在不牺牲其可靠性保证的前提下显著提高其精度。我们在 DroidBench（一个由研究社区开发的流行 Android 应用基准测试集）上测试了我们的实现，结果表明我们对 HornDroid 的修改在仅带来适度的效率代价的同时，提升了该工具的精度。最后，我们评估了该工具在分析真实应用时的可扩展性。
引用
@article{arxiv.1705.10482,
title = {A Sound Flow-Sensitive Heap Abstraction for the Static Analysis of Android Applications},
author = {Stefano Calzavara and Ilya Grishchenko and Adrien Koutsos and Matteo Maffei},
journal= {arXiv preprint arXiv:1705.10482},
year = {2017}
}