speca

SPECA 是一个将自然语言规范转化为检查清单的安全审计框架。它通过从自然语言规格说明中提取明确的、类型化的安全属性，并基于这些属性对实现进行结构化证明尝试推理来审计软件。该项目采用Python编写，支持Python 3.11及以上版本。SPECA的核心功能包括：依赖于规格说明的检测能力、跨实现比较以及可追溯到根源的误报分析。这使得它特别适用于协议栈、共识实现和加密库等需要遵循特定规范的系统安全性验证场景，尤其在处理由规范而非代码本身引起的漏洞时表现出色。