NyxFoundation/speca

解决的问题

SPECA 克服了传统代码驱动型安全审计工具依赖已知漏洞模式的局限性。它不寻找常见的错误，而是关注实现是否真正符合其预期设计，从而能够发现人类审计员和基于模式的工具常常遗漏的新颖漏洞——包括密码学不变性违规。

工作原理

SPECA 使用代理式流水线执行「以规范为锚点」的审计。它从自然语言规范中推导出明确的、带类型的安全部分属性，然后要求实现通过结构化证明尝试推理来「证明」这些不变性。该过程包含多个阶段：

1. 规范发现：从规范中提取需求。
2. 子图提取：识别系统中相关部分。
3. 属性生成：基于规范创建安全属性词汇表。
4. 代码解析：将这些属性映射到实际代码。
5. 审查：通过门控审查流程验证发现结果。

适用人群

专为需要验证复杂实现（如智能合约或 C/C++ 项目）是否严格遵循其技术规范的安全研究人员、漏洞赏金猎人和软件审计师设计。

主要亮点

• 高检测率：在 Sherlock Ethereum Fusaka 审计竞赛中复现了所有已知漏洞，并发现了开发者确认的新漏洞。
• 高精度：在 RepoAudit C/C++ 基准测试中，使用 Sonnet 4.5 达到 88.9% 的最高公开精度。
• 可解释结果：误报可追溯至特定流水线阶段，而非模型幻觉导致的黑箱结果。
• 可扩展性：仅需提供配置文件（BUG_BOUNTY_SCOPE.json 和 TARGET_INFO.json）即可接入新目标，无需修改核心代码。