静态分析抽象策略自适配工具Parf
PARF: An Adaptive Abstraction-Strategy Tuner for Static Analysis
-
摘要:研究背景 可靠静态分析工具（如Frama-C/Eva）旨在识别并帮助用户消除潜在的运行时错误（RTE），但通常会产生大量误报。因此，如何在静态分析的精度与效率之间取得平衡是一项关键任务。然而，在给定的时间预算内找到一组高精度的抽象策略（通常编码为工具外部参数）以实现低误报率极具挑战性，主要原因包括：1)参数取值空间庞大：现有静态分析工具通常提供大量参数，其组合空间可能极其庞大甚至无限；2)缺少自动精化手段：寻找高精度结果通常需多次设置参数与分析，而生成的中间信息未能被充分自动化利用以精化下一轮参数设置。因此，静态分析工具的使用仍高度依赖专家知识与经验。目的 我们提出Parf——一种自适应调整静态分析工具抽象策略的工具，旨在给定时间预算内找到一组能使分析器返回最少警报的抽象策略配置。方法 Parf将各类外部参数建模为格结构参数空间上的概率分布随机变量，通过重复采样与分析中间结果，逐步优化概率分布，最终生成高精度抽象策略。Parf基于Frama-C/Eva实现，提供基于Web的用户界面，支持静态分析工具的直观配置与抽象策略动态分布优化的可视化。结果 Parf在Frama-C开源数据集（共37个程序仓库）中的33个（89.2%）上实现了最低误报率，其中11个（29.7%）案例为独占性最优结果。Parf在对复杂大规模实际程序的分析中表现出优异性能。此外，Frama-C在集成Parf后相比于竞赛版本取得两项关键改进：1）完全消除了分析失败案例，2）额外成功验证了39项任务。这证明了Parf能够增强静态分析工具的验证能力。结论 Parf是一种支持抽象策略增量式优化的全自动化方法。与专家策略及Frama-C/Eva官方抽象策略相比，其在大多数测试案例中显著降低了误报率。此外，Parf还能够提高静态分析工具的验证能力。可能未来研究方向包括：扩展Parf以处理参数间依赖关系、基于神经网络的参数初始化，以及集成其他形式化验证工具。Abstract: We launch PARF—a toolkit for adaptively tuning abstraction strategies of static program analyzers in a fully automated manner. PARF models various types of external parameters (encoding abstraction strategies) as random variables subject to probability distributions over latticed parameter spaces. It incrementally refines the probability distributions based on accumulated intermediate results generated by repeatedly sampling and analyzing, thereby ultimately yielding a set of highly accurate abstraction strategies. PARF is implemented on top of FRAMA-C/EVA—an off-the-shelf open-source static analyzer for C programs. PARF provides a web-based user interface facilitating the intuitive configuration of static analyzers and visualization of dynamic distribution refinement of the abstraction strategies. It further supports the identification of dominant parameters in FRAMA-C/EVA analysis. Benchmark experiments and a case study demonstrate the competitive performance of PARF for analyzing complex, large-scale real-world programs.
下载: