形式化验证

本文作者分享了使用 Certora Verification Language (CVL) 进行智能合约形式化验证的经验，通过将模糊测试中的不变量思想应用于 CVL，解决了之前在模糊测试中发现的真实漏洞的简化版本。文章详细对比了模糊测试与形式化验证的异同，并展示了使用 Certora 解决各种漏洞的实例，强调了 Certora 在漏洞检测方面的有效性和简洁性。

本文强调了形式化验证（FV）在Web3和DeFi安全中的重要性，指出传统测试方法不足以应对Web3的安全挑战。FV通过数学证明确保代码按预期运行，能预防高危漏洞，并已在多个知名DeFi项目中应用，同时建议将FV尽早集成到开发生命周期中，以提升代码质量和安全性。

本文总结了 Vyper 编译器在过去一年中为提升安全性和稳定性所做的努力，包括增加安全预算、进行多次安全审计、发起漏洞赏金计划、实施合约监控系统等。文章还介绍了 Vyper 团队在测试和形式化验证方面的工作，以及未来的发展计划，强调了社区支持对 Vyper 安全的重要性。

RISC Zero 发布了 R0VM 2.0，这是一个为实时时代构建的 zkVM，它更快、更大、更安全。R0VM 2.0 的证明速度更快，成本更低，内存更大，并支持所有主要的以太坊预编译，目标是在 2025 年 7 月实现实时证明，同时，R0VM 2.0 还非常注重安全性，通过形式化验证来确保系统的可靠性。

本文深入探讨了零知识证明（ZKP）中可能出现漏洞的各个层次，包括电路层、前端层、后端层和集成层。重点介绍了用于检测电路漏洞的安全工具的现状，如静态分析、符号执行、动态分析、模糊测试和形式化验证等技术，并强调了在前端和后端层中发现漏洞的重要性，以及zkSecurity在开发相关安全工具上的努力。

本文探讨了如何形式化验证零知识证明系统中使用的算术电路的特性，如完备性、可靠性和零知识性。文章介绍了使用证明辅助工具和不使用证明辅助工具的不同验证技术，并讨论了形式化验证在零知识电路中的应用，包括问题分解、语义设计以及代码的综合验证，同时概述了当前的研究进展和未来的研究方向。

随着以智能合约（Smart Contract）及区块链应用（DApp）为核心的区块链2.0时代逐渐成为主流，智能合约及区块链应用的安全性也越发成为业界备受关注的焦点。尤其是，在经历过诸如THE DAO、币安被盗等事件，智能合约及区块链应用的安全性究竟应该如何得到验证和保障，业已成为当前区块链业界亟待解决的痛点。

本文介绍了Move语言的诞生背景，它旨在解决Solidity等现有编程语言在资产安全方面的不足。Move通过在语言设计、虚拟机和验证工具三个层面进行创新，例如引入Resource类型、Module系统和所有权系统，从而提高了数字资产的安全性。目前Move主要应用于Aptos、Sui和Starcoin等L1链项目，未来有望在DeFi、SocialFi和GameFi等领域得到更广泛的应用。

“程序测试能证明错误的存在, 但不能证明错误不存在” – Edsger Dijkstra。智能合约是一个对安全性要求非常高的领域，一个不经意的小 bug 很可能会导致不可估量的损失。

近日，以太坊基金会公布了2025年第一季度研究资助名单，CertiK荣获两项研究资助。

本文讨论了智能合约开发的演进，特别是reentrancy重入攻击的风险，以及使用Move语言和SVM（MoveVM）虚拟机来提高智能合约安全性的方案。文章分析了Curve和DAO两次著名的攻击事件，并深入探讨了Move语言的安全机制，包括资源类型、模块系统、线性类型系统、字节码验证和形式化验证。最后，作者展望了MoveVM在EVM社区的未来应用。

本文分析了2025年5月至6月期间发生的多起区块链安全事件，包括Cetus Protocol、Alex Protocol、Cork Protocol和Mobius DAO等项目遭受的攻击，并探讨了ImmuneBytes如何通过其安全策略来预防这些漏洞，强调了安全审计和验证的重要性。

本文详细介绍了Vlad的Casper协议及其在Isabelle/HOL中的形式化验证过程，探讨了异步环境下共识问题的核心挑战，并展示了如何使用形式化方法确保估计的安全性。

Trail of Bits 对 Ockam 的安全通信协议设计进行了密码学设计审查，Ockam 旨在实现跨异构网络的安全通信。审查肯定了 Ockam 设计的优点，并提出了加强系统安全性的建议，包括改进文档、明确安全保证以及进行形式化验证，使用 Verifpal 和 CryptoVerif 等工具来验证 Ockam Identities 的安全性。