Certora Prover 开源——智能合约安全的未来

我们正在 开源 Certora Prover， 这是针对以太坊 (EVM)、Solana (sBPF) 和恒星 (WASM) 的最先进的形式验证 (FV) 引擎。使用这个工业级工具来 确保你的代码的安全性， 现在它是免费的、透明的，并且由社区驱动。

在我们的 安全投资组合 中发现使用 Certora Prover 进行形式验证的协议。

为什么开源安全性很重要

智能合约的安全性既昂贵又缓慢。DeFi 项目在开发上花费超过一年，并在审计上花费数百万，以确保它们不会成为灾难性漏洞的受害者。尽管关键漏洞变得更加罕见，但确保智能合约安全的高成本和复杂性使 DeFi 成为一个排他性的俱乐部——一个需要在发布一行代码之前就获得巨额资金的俱乐部。

这种模式是不可持续的。 安全性不应该是富有者才能享有的特权；它应该是高效的、可访问的，并且 融入开发过程。

Certora Prover 已开发超过 7 年，并为 Aave、MakerDAO、Uniswap、Lido、EigenLayer、Solana Foundation、Ether.fi、Silo、Safe、Kamino、Squads、Jito、Manifest、Balancer、Morpho 等项目确保了总计超过 $1000 亿 的 TVL。开发者已经编写了 超过 70,000 条规则。与审计和测试不同，形式验证是唯一能通过检测所有漏洞并最终证明其不存在来保证所有形式化规则集安全的方法。

什么是 Certora Prover？

将其视为智能合约的 自动化数学审计员：

1. 输入： 你合约的代码 + 规则（使用类似 Solidity 的开源 Certora Verification Language (CVL) 编写）。
2. 输出： 正确性的证明或显示漏洞的反例。
3. 结果： 确保你的代码是安全的且表现如预期。

示例：

一条规则可以说，即使是恶意用户也不能提取超过他们已经存入和合法赚取的资产。Prover 将检查 所有可能的场景，而不仅仅是几个测试用例。这确保了该协议绝对不可能被漏洞攻击，允许黑客提取超过他们应得的资产。

现实影响：Certora Prover 捕获的漏洞

1. MakerDAO 的 DAI 方程漏洞

• 问题： 一个核心不变性——DAI 的基本方程——自 2018 年以来就数学上不正确。它没有在顶级审计公司的审计中被发现，被 Maker 团队自己错误地证明为数学正确，最后只被 Certora Prover 发现。 具体链接
• 风险： 其稳定性受到破坏，影响了加密市场上最大的稳定币之一。
• 结果： 在部署前修复，避免了系统风险。

2. SushiSwap 的 Trident 池排干

• 问题： 不变性破裂使 攻击者能够排干流动性池。
• 风险： 用户资金损失数百万。
• 结果： 在漏洞发生之前修复。

3. PRBMath 的四舍五入错误

• 问题： signed mulDiv() 函数中的错误四舍五入方向。
• 风险： 排干流动性提供者的资金。
• 结果： 该漏洞在库文档中被高亮显示，并将在新版本中修复。

4. Jito 重新质押储备计算漏洞

• 问题： 储备金额计算使用了错误的单位，
• 风险： 储备池可能过度委托，无法满足所有的提款请求。
• 结果： 在部署前修复。

5. Manifest Vault 转移漏洞

• 问题： 对于 Token-2022，资金从 用户转移到储备池，依据提款指令。
• 风险： 协议意外地消耗用户资金。
• 结果： 在漏洞发生之前修复。

开发者为什么喜欢 Certora

• Shift Left Security： 尽早发现漏洞——就像是代码的拼写检查。
• 审计准备： 通过预验证代码减少 30% 的审计费用。
• 多链支持：支持以太坊、Solana和恒星。
• 自动化安全： 编写一次，在每次更改时运行。
• 安全保障： 享受数学上正确的安心。
• 编译器漏洞检测： 保护防止编译器引入的微妙漏洞，已通过静态分析揭示 Solidity 编译器中的多个漏洞（包括 静默损坏存储、优化器漏洞、分配器漏洞、错误的 calldata 验证、内存隔离违规和 内存损坏）进行保护。
• 免费： Certora Prover 现在是免费的开源工具。

加入形式验证安全运动

形式验证不再仅限于博士。随着 AI 生成的代码和可组合的 DeFi，数学保证是不可谈判的。通过开源 Prover，我们赋予建设者力量：

✅ 在漏洞发生之前预防攻击。

✅ 使用可验证的正确性建立信任。

✅ 使安全性在 Web3 中民主化。

关注我们的 Twitter 并在 GitHub 上给我们点赞。

安全性不是特权——它是一项权利。让防弹智能合约成为常态。

• 如果你是开发者： 注册 并开始验证。
• 安全研究人员： 参加 Certora 的竞赛，帮助保护领先的 DeFi 项目，测试你的技能，并获得奖励。

• 原文链接： certora.com/blog/certora...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～