Claude开始攻克密码学弱点

Claude不只是在审代码，而是在帮研究者找密码学反例

Anthropic近日披露了一项值得安全行业重视的新进展：Claude已经开始辅助研究人员发现密码学弱点，并参与验证过去高度依赖少数专家的复杂安全问题。

**密码学弱点是指密码协议、数学假设、参数选择或实现方式中，会削弱机密性、完整性、身份认证等安全目标的缺陷。**它不等同于普通的软件漏洞：数组越界通常能在某一行代码附近定位，而密码学问题往往藏在攻击模型、证明前提、随机数使用方式和协议组合关系里，代码即使没有崩溃，系统仍可能是不安全的。

截至2026年7月28日，Anthropic官方研究披露的重点并不是推出一个新的Claude产品版本，而是展示大模型如何进入高难度密码学研究流程。官方页面没有把这项工作包装成一次常规模型发布，也没有给出可供横向比较的统一跑分、固定成功率或完整商业定价，因此现阶段更应该把它看作一项能力验证，而不是成熟的自动化密码审计服务。

这件事的分量在于，密码学研究正在从“模型能否解释论文”，转向“模型能否提出可验证的攻击假设”。前者是知识复述，后者要求模型理解安全目标、追踪多层假设、构造反例，并接受程序、求解器或专家的反复检验。

真正有价值的是候选答案可以被验证

**可验证推理是指模型给出的结论能够由独立程序、数学证明、测试向量或可复现实验进行检查。**这一点决定了Claude在密码学里的价值，也划清了它与普通聊天机器人的边界。

大模型直接说“这个协议存在漏洞”几乎没有意义，因为密码学推理中一个量词、一个概率边界或一个攻击者能力假设写错，结论就可能完全相反。更可靠的流程是让模型生成候选攻击路径，再交给确定性工具和研究人员判断，而不是把模型的自然语言输出当成证明。

一套相对可信的AI辅助密码分析流程通常包含五步：

1. **形式化问题。**明确攻击者能看到什么、控制什么，以及需要证明的安全性质。
2. **生成假设。**让模型寻找边界条件、异常参数、协议组合冲突或证明中的隐含前提。
3. **构造反例。**把怀疑转化为具体输入、消息序列、测试向量或代数关系。
4. **机器验证。**使用测试程序、SMT求解器、证明助手或独立实现复核结果。
5. **人工审查。**由密码学研究者检查攻击模型是否现实，确认问题究竟属于设计缺陷、实现错误还是无效假设。

Claude在这里最适合扮演的角色不是“裁判”，而是高吞吐量的研究助理。它可以同时沿着多条路径搜索，快速阅读协议文档、论文、实现代码和测试记录，把研究人员从大量低命中率的试探中解放出来；最终结论仍应由可复现证据收口。

密码学问题为什么比普通代码审计更难

密码系统的安全性通常不是由某一段代码单独决定，而是由算法、参数、实现和部署环境共同决定。一个加密算法在标准模型中可能是安全的，但如果随机数发生器重复输出、错误信息泄露执行路径，或者两个分别安全的协议被不恰当地组合，整体系统仍会失守。

**侧信道攻击是通过运行时间、功耗、缓存访问或错误信息等间接信号推断秘密数据的攻击方式。**这类问题尤其难以仅靠阅读源代码发现，因为危险可能来自编译器优化、处理器行为和部署环境，而不是源代码表面上的逻辑错误。

**形式化验证是把系统目标和实现行为表示为数学命题，再借助证明助手或自动求解器检查其是否成立的方法。**它能提供比普通测试更强的保证，但成本很高：研究者首先要写对安全性质、环境模型和前置条件，之后才能讨论证明是否正确。

大模型恰好能填补形式化验证最昂贵的一段工作。Claude可以把自然语言协议转换为更结构化的约束，提示缺失的前提，尝试生成证明框架，并在证明失败时寻找反例；但它也可能把错误假设写得非常流畅，因此机器检查不能省略。

| 方法 | 最擅长的问题 | 是否能证明“没有漏洞” | 主要短板 | Claude适合参与的环节 | |---|---|---:|---|---| | 模糊测试 | 崩溃、越界、异常输入 | 否 | 难覆盖复杂协议状态与数学关系 | 生成输入、分析异常、扩展测试语料 | | 静态分析 | 数据流、危险调用、规则匹配 | 通常不能 | 误报较多，依赖预设规则 | 解释告警、关联上下文、编写检查规则 | | 符号执行 | 路径约束、边界条件 | 局部可以 | 容易出现路径爆炸 | 选择路径、简化约束、解释求解结果 | | 形式化验证 | 协议性质、实现正确性 | 在给定模型内可以 | 建模成本高，前提可能写错 | 生成规格、补全证明、寻找反例 | | 人工密码分析 | 新型攻击、模型缺陷、组合问题 | 取决于证据 | 专家稀缺、周期长 | 扩展搜索空间、整理证据、复核假设 |

这不是“Claude证明了某个系统绝对安全”

Anthropic这次展示的是发现弱点和辅助验证的能力，而不是让Claude为密码系统签发安全证书。安全行业最容易犯的错误，是把“模型找到过有效问题”外推成“模型没找到问题就代表系统安全”。

密码学中的证明只在明确模型和假设范围内成立。假设攻击者不能读取内存，那么证明不会自动覆盖内存泄露；假设随机数均匀分布，那么证明不会自动发现随机数生成器熵不足；假设底层原语安全，那么证明也不会替代对底层实现的侧信道分析。

对模型输出的可信度至少可以分成四级：

| 证据等级 | 模型输出 | 可否用于安全决策 | 需要的下一步 | |---|---|---:|---| | L1：直觉 | 自然语言描述“可能存在问题” | 否 | 明确攻击模型和受影响性质 | | L2：候选反例 | 给出参数、输入或消息序列 | 谨慎 | 在独立环境中复现 | | L3：机器验证 | 测试程序、求解器或证明助手确认 | 可以作为技术证据 | 人工检查模型与前提 | | L4：独立复核 | 多方复现并完成影响分析 | 可以进入修复与披露流程 | 持续回归测试和版本跟踪 |

Claude最明显的提升，是把更多问题从L1推进到L2，甚至协助研究者准备L3所需的结构化材料。只有完成机器验证和独立复核，才应该把结果写进正式安全公告。

和Claude Mythos相比，这是另一条能力主线

Claude此次参与密码学弱点研究，不应被简单等同于此前围绕Claude Mythos的漏洞发现叙事。前者关注的是高难度密码学问题能否被模型提出、拆解和验证，后者更多被讨论为面向软件漏洞挖掘和防御性网络安全工作流的受控模型能力。

两者的共同点是都在压缩安全研究的人力瓶颈。传统漏洞挖掘主要搜索程序状态空间，密码分析则还要搜索数学假设、协议状态和攻击模型；大模型的优势不是计算得比专用求解器更精确，而是能在不同表示之间转换，并决定下一步值得调用什么工具。

两者的风险边界也明显不同。普通内存安全漏洞通常对应具体版本和具体触发条件，而密码学弱点一旦涉及通用协议或广泛采用的参数，影响范围可能跨越多个实现；与此同时，披露不完整的攻击思路也可能降低攻击门槛。

因此，Claude进入密码学研究后，访问控制、日志审计和协调披露会比模型跑分更重要。一个能自主尝试攻击假设的Agent，如果同时拥有代码仓库、编译环境、云资源和真实系统访问权限，其风险不再来自单次回答，而来自连续执行能力。

大模型与传统工具不是替代关系

大模型不会取代SMT求解器、证明助手和密码测试套件，因为这些工具提供的是确定性检查能力。Claude擅长提出“应该检查什么”，Z3、Lean、Cryptol和测试程序负责回答“这个命题到底是否成立”。

**SMT求解器是用于判断带约束逻辑公式是否可满足的自动化工具。**它适合验证边界条件、位向量运算和协议约束，但需要有人把现实问题转换成正确公式。

**证明助手是由计算机检查每一步形式化证明是否合法的软件系统。**Lean等工具不会因为论述听起来合理就放行，但它们也无法判断研究者是否一开始证明了错误的问题。

这意味着未来更现实的组合不是“Claude对抗密码学家”，而是“Claude加密码学家加验证工具”对抗复杂系统。模型承担文献阅读、假设生成和工具编排，专用软件承担精确计算，人类负责定义目标、识别现实边界并承担披露责任。

GitHub上的Project Wycheproof已经展示了机器可执行密码测试向量的价值。该项目把已知攻击和边界情况整理成测试集合，使实现者可以自动检查常见错误；Claude一类模型可以进一步帮助研究人员解释失败原因、迁移测试模式，并寻找现有测试集尚未覆盖的变体。

对开发者最直接的影响：安全审查要开始保存推理证据

开发团队不应只保存Claude给出的最终结论，而应保存问题定义、模型输出、工具日志、复现环境和人工复核记录。没有证据链的“AI发现”，既难以进入漏洞披露流程，也无法在模型或代码升级后进行回归验证。

企业可以优先把Claude用于三类低争议、高收益任务：

• 把协议文档、实现代码和测试用例之间的不一致整理出来；
• 根据已知攻击模式生成额外测试向量和边界条件；
• 为Z3、Lean、Cryptol等工具准备候选规格，再由工具和专家检查。

企业暂时不应把Claude单独用于三类高风险决策：

• 宣布某个密码协议“已经被证明安全”；
• 在没有独立复现的情况下公开高影响攻击路径；
• 让安全Agent直接对生产系统执行未经审批的利用验证。

衡量这类系统也不能只看“发现了多少问题”。更合理的指标包括有效反例比例、独立复现率、误报率、每个确认问题所需专家工时，以及从提出假设到完成验证的中位时间；遗憾的是，Anthropic此次公开材料尚未提供一组足够完整、可横向比较的数据。

判断：这比再多一个代码跑分更重要

Claude辅助发现密码学弱点的真正意义，是前沿模型开始触碰专家型研究工作的验证闭环。模型会写一段看似正确的密码学分析早已不稀奇，稀奇的是它能否把分析推进为具体反例，并让独立工具和研究者复核。

这项能力短期内不会让密码学家失业，反而会增加对高水平研究者的需求。候选攻击越多，筛选、建模、复现和协调披露的工作量越大；真正稀缺的人才将从“手工尝试每一条路径”，转向“设计验证体系并判断哪些结论值得相信”。

这项能力长期看会改变安全研究的成本结构。过去只有少数团队有资源持续审查复杂协议，未来模型可以把初步分析扩展到更多开源项目和基础设施，但攻击者也能使用类似方法搜索弱点，防守方的窗口期未必会自动扩大。

Anthropic这次最值得肯定的地方，是把重点放在可验证的高难度问题，而不是继续展示模型生成安全报告的文笔。最需要警惕的地方，则是市场可能把研究演示过早包装成自动化密码审计：在密码学里，流畅答案从来不是证据，能被独立复现的反例才是。

参考来源

• Anthropic Research：《Discovering Cryptographic Weaknesses with Claude》，本次事件的首要研究披露；受文末链接域名限制，此处仅列文献名称。
• Project Wycheproof：由社区维护的密码学测试向量项目，用于检查实现中的已知弱点和边界情况。
• Lean 4：形式化证明助手及编程语言，可用于机器检查数学命题和软件性质。
• Z3 Theorem Prover：微软研究院开源的SMT求解器，适合验证逻辑约束、位向量和程序性质。
• Cryptol：面向密码算法规格与验证的语言和工具链，可用于描述并检查密码学实现。