减少静态污点分析虚警：一种面向Android应用的验证方法

本文主要探讨了面向Android应用的静态污点分析结果的正确性验证问题，旨在解决静态分析过程中产生的大量虚警问题，提出了一种上下文敏感、路径敏感和域敏感的半自动程序分析方法。 在Android应用程序中，静态污点分析是一种常见的方法，用于检测潜在的隐私泄露漏洞。然而，这种方法往往会产生很多虚假警报（虚警），这给开发者带来额外的工作负担，因为需要手动检查每个警报以确定其真实性。为了解决这个问题，作者提出了一个创新的分析框架，它能够通过减少需要检查的执行路径数量，有效地验证污点分析结果的正确性。 首先，该方法涉及在目标应用中插入桩代码，以生成一条包含源（Source）和汇（Sink）的种子Trace。源通常代表敏感数据的起点，而汇是可能泄露这些数据的位置。如果种子Trace中存在从源到汇的污点传播路径，那么就表明存在真实的隐私泄露漏洞。 接下来，利用基于Trace的污点分析，对这条Trace进行检查，以验证是否存在污点传播路径。如果存在，那么漏洞就被确认为真实；若不存在，则进一步收集Trace的条件集合和污点信息。结合活变量分析（Live Variable Analysis），该方法可以识别出与污点传播无关的变量，从而减少需要考虑的路径。同时，通过条件反转的程序变换技术，设计了一种约束选择策略，能够删除大部分不涉及污点传播的执行路径。 最后，通过对剩余的执行路径进行遍历和分析，进一步验证漏洞是否为虚警。实验中，作者基于FlowDroid实现了这个原型系统，并在DroidBench的75个应用和10个真实应用上进行了验证。结果显示，平均只需要遍历15.09%的路径，虚警率就能平均降低58.17%，证明了该方法在减少静态分析虚警方面的高效性。 关键词：程序验证、污点分析、活变量分析、程序变换、路径敏感。 这篇研究论文属于程序验证和安全分析领域，主要关注如何提高Android应用安全检测的准确性，对于减少误报和提升静态分析工具的实用性具有重要意义。通过引入更精细的上下文、路径和域敏感性，以及优化的路径处理策略，该方法有助于提升静态污点分析的效率和可靠性。