程序分析漫游指南，第三部分：基本无害 LLM

LLM 越来越多地用于错误分析，以推理代码并判断是否可以在实际执行上下文中触发潜在错误，最近的工作显示了有希望的实证结果。然而，经验有效性并不能使模型生成的合理理由足以发出警告。这种区别对于无错误决策尤其重要：驳回报告或警告需要确定所报告的错误状态在正在分析的程序上下文中无法到达，而不仅仅是提供一个合理的解释来解释为什么它可能不会发生。我们认为程序行为推理应该基于形式分析，而不是直接由 LLM 执行。我们提出了 Evident，一个错误分析系统，它将 LLM 辅助与程序行为推理分开，将后者委托给后端分析。给定指定报告位置和数据流的警告，Evident 仅使用 LLM 来构建特定于警告的分析工具。然后，Evident 在调用后端之前验证该工具。后端执行与Harness相关的检查：在构建的Harness及其假设下，报告的错误状态是否无法到达。我们对来自两个现有静态检测器的 200 个真实 Android 内核驱动程序警告进行 Evident 评估。 Evident 对 151 个案例（76%）进行了正确分类，包括发出 111 个误报，但没有发出数据集中任何已确认的错误；其余情况要么未解决，要么作为潜在错误保守保留。 Evident 还重新发现了先前基于 LLM 的过滤和手动分类所忽视的已确认漏洞。