从 AI 粗放式测试到形式化验证：随着 AI 的普及，我们正在改变漏洞赏金计划的运作方式

Nym 即将启动下一轮年度安全审计，并正朝着对所有核心组件进行形式化验证以及实施持续的 AI 驱动安全审计的目标迈进。作为准备工作，我们将暂停当前形式的漏洞赏金计划。

2026年7月24日1 分钟读完

从下个月开始，Nym 将进入代码冻结期，为下一次年度安全审计做准备。我们正在整个网络和应用程序中全面推广后量子密码学，并采用新的流量掩护方案，因此有必要进行一次新的安全审计。每年，我们都会对我们的应用程序和代码进行独立审查，以确保我们兑现了对网络用户所作的隐私和安全承诺。

此次审核之后，我们将进一步推进正式验证工作。目前，像 Claude Fable 这样的 AI 模型使得发现攻击变得更加容易，而我们发现，由于人们试图对我们的代码进行 AI 安全审计，我们当前的漏洞赏金计划主要吸引的是“AI 粗制滥造”的报告。

在 Nym，我们已开始持续使用 Claude Fable 对我们的代码进行检测，以发现真正的漏洞。与 ZCash Ironwood 升级类似，要确保我们的代码免受可能被人工智能发现的漏洞影响，唯一的方法就是对 Nym 使用的每个基本组件和协议进行形式化验证。

漏洞赏金计划：有哪些变化

为准备下一次安全审计以及向形式化验证的范式转变，我们将停止当前形式的漏洞赏金计划。

这意味着我们将停止迄今为止运行的奖励发放系统——该系统根据报告问题的严重程度分级，按固定比例发放 $NYM 代币。 Nym 今后将仅针对严重且重要的发现结果酌情支付报酬。我们仍在接收报告，研究人员可以且应当继续将发现的任何问题发送给我们。我们的安全港政策和负责任披露规则仍然有效。

最新指南请随时访问 nym.com/vdp-bbp。

我们为何要这样做

Nym 的代码是开源的，且每年都会经过独立审查，而非仅凭信任。

这次的不同之处在于方法。即将进行的审计将由一家外部安全公司负责，这要求我们在审计开始前冻结代码库，因此我们现暂停漏洞赏金发放。归根结底，漏洞赏金计划与深度审计存在重叠之处，而正在进行的审计中已发现的漏洞报告并不会带来太多额外价值。将我们的安全工作重点放在审计以及随后的形式化验证上，是更合理的资源利用方式。

下一站：形式验证

此次审计结束后，我们将与合作伙伴 Cryspen 共同推进 正式验证 工作。与通过测试和审查来查找缺陷的漏洞赏金计划和传统审计不同，形式化验证会生成代码行为的数学证明，以表明系统的关键部分完全按照预期运行，并且根本无法执行某些操作。这是安全工程领域最高标准的保障，也是像我们这样的隐私基础设施应当努力的方向。

当然，直到最近，对于像 Nym 这样的大型代码库而言，这项工作还过于耗时，但如今借助 AI 工具，已经可以对 Nym 的核心加密原语和协议进行大规模形式化验证了。

如需进一步了解形式验证，请阅读由我们的首席执行官哈里·哈尔平（Harry Halpin）撰写的《高可信度密码学路线图》（https://inria.hal.science/hal-01673294/file/paper.pdf）。该文写于 2017 年他在巴黎国家信息与自动化研究所（Inria de Paris）工作期间，当时他与 卡尔蒂克·巴尔加万合作期间撰写的《高可信度密码学路线图》（）。巴尔加万曾领导对支撑整个互联网运行的协议（如 TLS 1.3 和 Signal）进行形式化验证。随着 Karthk Bhargavan 现已加入 Cryspen，我们将与他的团队合作，对 Nym 的核心密码学和协议进行正式验证。

迄今为止的审计情况

自网络早期以来，Nym 和 NymVPN 一直由领先的公司和密码学家进行独立审计和审查。该记录已发布在我们的信任中心：

Cure53 (2024年7月)。 由丹尼尔·布莱亨巴赫（Daniel Bleichenbacher）博士领导的团队对 Nym 的移动端和桌面端应用、VPN、网络基础设施以及加密技术进行了全面审计。请参阅 Cure53 审计报告。
Oak Security (2023年1月)。 两项审计：一项针对 Nym 混网和锁定合约，另一项针对 Nym 钱包。
JP Aumasson 博士 (2021年9月)。 由该领域最著名的密码学家之一对该网络进行的早期安全审查。
Cryspen 技术评审（2023–2024）。 由 Karthikeyan Bhargavan 博士及其同事领导，采用形式化方法对 Nym 的分布式密钥生成和 Outfox 数据包格式进行的密码学评审。