SPECA：多实现系统的规范到检查表代理审计——以以太坊客户端为例
SPECA: Specification-to-Checklist Agentic Auditing for Multi-Implementation Systems -- A Case Study on Ethereum Clients
AI总结：
SPECA通过规范到检查表的审计框架，提高了多实现系统审计中跨实现重用的效率，减少假阳性，提升漏洞检测效果。
摘要：
多实现系统越来越多地根据自然语言规范进行审计。差异测试在实现之间存在分歧时表现良好，但在所有实现都收敛于对模糊要求的相同错误解释时提供很少的信号。我们提出了SPECA，一种规范到检查表的审计框架，将规范性要求转化为检查表，将其映射到实现位置，并支持跨实现的重用。我们在一个真实世界的安全审计比赛中实例化了SPECA，针对以太坊Fusaka升级，覆盖了11个生产客户端。在54份提交中，17份被比赛组织者判定为有效。跨实现检查占有效发现的76.5%（13/17），表明由检查表衍生的一对多重用是多实现审计中的实用扩展机制。为了理解假阳性，我们手动编码了37份无效提交，发现威胁模型不一致解释了56.8%（21/37）：依赖于关于信任边界或范围的假设报告，这些假设与审计规则相矛盾。在V1部署中未检测到高或中等发现；遗漏集中在规范细节和隐含假设（57.1%），时间与并发问题（28.6%），以及外部库依赖（14.3%）。我们的改进代理在与竞争审计的地面真相对比中，实现了严格召回27.3%的高影响漏洞，处于人类审计员的前4%之中，并在关键问题上超越了51名参赛者中的49名。这些结果，尽管来自单一部署，表明早期、明确的威胁建模对于减少假阳性并聚焦代理审计努力至关重要。代理驱动的过程使专家验证和提交在平均约40分钟内完成。
英文摘要：
Multi-implementation systems are increasingly audited against natural-language specifications. Differential testing scales well when implementations disagree, but it provides little signal when all implementations converge on the same incorrect interpretation of an ambiguous requirement. We present SPECA, a Specification-to-Checklist Auditing framework that turns normative requirements into checklists, maps them to implementation locations, and supports cross-implementation reuse. We instantiate SPECA in an in-the-wild security audit contest for the Ethereum Fusaka upgrade, covering 11 production clients. Across 54 submissions, 17 were judged valid by the contest organizers. Cross-implementation checks account for 76.5 percent (13 of 17) of valid findings, suggesting that checklist-derived one-to-many reuse is a practical scaling mechanism in multi-implementation audits. To understand false positives, we manually coded the 37 invalid submissions and find that threat model misalignment explains 56.8 percent (21 of 37): reports that rely on assumptions about trust boundaries or scope that contradict the audit's rules. We detected no High or Medium findings in the V1 deployment; misses concentrated in specification details and implicit assumptions (57.1 percent), timing and concurrency issues (28.6 percent), and external library dependencies (14.3 percent). Our improved agent, evaluated against the ground truth of a competitive audit, achieved a strict recall of 27.3 percent on high-impact vulnerabilities, placing it in the top 4 percent of human auditors and outperforming 49 of 51 contestants on critical issues. These results, though from a single deployment, suggest that early, explicit threat modeling is essential for reducing false positives and focusing agentic auditing effort. The agent-driven process enables expert validation and submission in about 40 minutes on average.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
