arXiv:2504.00521v1 公告类型: cross 摘要: 中断驱动程序中的原子性违规对关键系统中的软件安全性构成重大威胁。这些违规行为发生在共享资源的操作执行序列被异步中断打断时。由于程序状态空间庞大、应用程序级别的代码依赖关系以及复杂的领域特定知识，检测原子性违规具有挑战性。我们提出了一种名为Clover的混合框架，该框架结合了静态分析和大型语言模型（LLM）代理，以检测实际程序中的原子性违规。Clover首先进行静态分析以提取关键代码片段和操作信息。然后启动一个多代理过程，在此过程中，专家代理利用领域特定知识检测原子性违规，随后由裁判代理进行验证。在RaceBench 2.1、SV-COMP和RWIP上的评估表明，Clover的精确度/召回率分别为92.3%/86.6%，其在F1分数上的性能比现有方法高出27.4%-118.2%。