概率式Datalog分析中的冲突提取
Conflict Extraction in Probabilistic Datalog Analyses
浏览论文内容
中文总结 AI 辅助
针对概率式Datalog分析中告警间的矛盾问题，提出专门的冲突提取器PPProbe，利用Datalog推导图结构提升搜索效率，在70个基准测试上实现更高吞吐量并减少47.7%的矛盾告警
中文摘要 AI 辅助
Datalog的概率扩展使指针分析、数据竞争检测、侧信道分析等静态分析能够根据可能性对告警进行排序，但这种额外的表达能力也带来了确定性分析中不存在的新挑战：最终输出可能包含各自看似合理但相互矛盾的告警，因为边际概率无法保证联合可满足性。因此，开发者可能会花费精力调查在任何可能世界中都永远不会同时出现的告警组合。我们通过将此类矛盾形式化为最小不可满足子集（MUS）并引入专门针对概率式Datalog分析的冲突提取器PPProbe来解决该问题。PPProbe不改进通用的MUS枚举，而是利用Datalog推导图的结构引导搜索指向可能的冲突，并通过自底向上的UNSAT推理剪枝搜索空间。我们在来自功耗侧信道分析、数据竞争检测、语义差异分析和贝叶斯网络推理的70个基准测试上对PPProbe进行评估。结果显示，PPProbe的吞吐量比最先进的MUS枚举器高2.5至24倍，且其识别出的冲突可实现假阳性减少的保守估计，平均过滤掉47.7%的相互矛盾的告警。
英文摘要
Probabilistic extensions of Datalog enable static analyses such as pointer analysis, data race detection, and side-channel analysis to rank alarms by likelihood, but this added expressiveness also introduces a new challenge absent from deterministic analyses: the final output may contain alarms that are individually plausible yet mutually inconsistent, because marginal probabilities do not guarantee joint satisfiability. As a result, developers may spend effort investigating combinations of alarms that can never co-occur in any possible world. We address this problem by formalizing such inconsistencies as minimal unsatisfiable subsets (MUSes) and introducing PPProbe, a conflict extractor specialized for probabilistic Datalog analyses. Rather than improving MUS enumeration in general, PPProbe exploits the structure of Datalog derivation graphs to guide the search toward likely conflicts and prune the search space through bottom-up UNSAT inference. We evaluate PPProbe on 70 benchmarks from power side-channel analysis, data race detection, semantic diffing, and Bayesian-network inference. The results show that PPProbe achieves 2.5 to 24 times higher throughput than state-of-the-art MUS enumerators, and that the conflicts it identifies yield a conservative estimate of false-positive reduction, filtering out an average of 47.7% of mutually inconsistent alarms.
