形式化验证

infiniFi 是一个 DeFi 平台，旨在优化收益，但其 iUSD 赎回机制存在漏洞，可能导致用户在赎回队列中被跳过，从而面临不公平的惩罚。Certora Prover 发现了这一问题，并通过形式化验证确保了修复后的系统符合 FIFO 原则，维护了用户信任和 DeFi 协议的公平性。

本文探讨了如何通过形式化验证（FV）竞赛来提高智能合约代码的安全性，并量化安全服务的有效性。文章强调了形式化验证的关键优势，包括可衡量的覆盖率指标、持续的安全研究参与，以及通过社区合作加速验证过程。形式化验证通过mutation测试等方式量化代码覆盖率，从而改进代码安全性，并能在短时间内提供可衡量的代码安全性提升。

随着Web3应用的持续加速，越来越多的中央银行和机构正在开发数字资产产品，稳定币便是重点方向之一。在严格的合规框架之下，形式化验证被认为是一种极具前景的方法论，助力稳定币项目更有效地满足《GENIUS法案》的合规要求。

Silo Finance 的一个新杠杆合约模块在测试阶段遭到攻击，由于过于宽泛的批准设置导致借款操控漏洞。该模块与核心Silo协议隔离，因此核心协议、金库、市场或用户资金未受影响。Certora 此前对该合约进行了安全审查，但未发现此漏洞，事后进行了风险评估和补救措施，并确认现有Silo代码是安全的。

本文档是Dedaub公司提供的软件服务的使用协议条款。该服务主要针对EVM区块链协议，通过静态分析、形式化验证等技术检测智能合约的安全漏洞。协议规定了服务的使用范围、费用支付、知识产权、数据处理、责任限制以及争议解决方式等内容，用户使用该服务需要同意这些条款。

CertiK完成了针对CosmosSDK形式化验证。形式化验证是一项运用数学逻辑来确保系统符合规范，使其在所有可能的输入和条件下都如预期表现的技术。本文将介绍形式化验证CosmosSDKBank模块的具体步骤，以及一些验证结果。

infiniFi 是一个 DeFi 平台，通过管理 Pendle、AAVE 和 Ethena 等协议上的存款来优化收益。

本文介绍了Certora团队开发的一款用于验证编译器优化的等价性检查工具，该工具通过比较优化前后程序的行为来检测编译器bug。文章还分享了该工具在Vyper编译器中发现的一个优化bug，该bug导致局部变量被错误地映射到相同的堆栈位置，从而改变了程序的行为。该bug已在Vyper 0.4.2版本中修复。

RISC Zero正与Veridise合作，使用Picus工具对zkVM的组件进行形式化验证，以提升ZK安全性。通过数学方法证明电路的确定性，从而消除约束不足的错误，已成功验证Keccak加速器电路的确定性，并正在验证RISC-V电路。此举旨在创建一个既快速又安全zkVM，使开发者无需在性能和安全性之间妥协。

近日，CertiK联合创始人、哥伦比亚大学教授顾荣辉接受全球知名财经媒体CNBC阿拉伯频道专访，围绕形式化验证的行业应用、AI在区块链安全中的角色，以及新兴技术风险等议题，分享了其对Web3.0安全未来的深刻洞察。

Aztec 团队的 Michael Klein 和 Veridise 的 Jon Stephens 展开了一场炉边谈话，深入探讨了 Aztec 网络的关键组成部分——Noir 编程语言。讨论涵盖了 Noir 的设计决策、开发者体验、工具生态以及安全相关主题，还讨论了 Noir 与其他 ZK DSL 的比较、隐私考虑、元编程、Noir 和 zkVM 的区别以及形式化验证的作用。

Veridise 与 Succinct 合作，使用 Veridise 的工具 Picus 来验证 Succinct 的 RISC-V zkVM，SP1 电路的确定性。通过将 Plonky3 电路转换为 LLZK，成功验证了多个 SP1 电路的确定性。同时，也发现了 Plonky3 到 LLZK 转换管道的局限性，并提出了改进方向，未来计划扩展 Picus 以验证 SP1 中的所有电路。

文章讨论了Web3安全审计的重要性，强调了智能合约审计在防止黑客攻击和漏洞利用方面的关键作用。文章还探讨了审计师的角色，有效的审计流程，以及未来审计在安全设计咨询、实时监控、形式化验证和安全教育等领域的发展方向。