Certora 发布了一款名为 Concordance 的开源工具,它利用 LLM 自动简化复杂的智能合约代码,同时使用 Concord 等价性检查器来保证代码行为不变。Concordance 通过迭代地简化代码,并使用 Concord 验证 LLM 提出的修改方案,从而帮助开发者更容易地理解和审计复杂的智能合约。
Certora举办了首次针对Rust的形式化验证竞赛,并与Code4rena和Cantina合作,为Soroban智能合约举办了两次社区竞赛。文章介绍了如何使用Certora的工具(如Sunbeam)和Rust库(如CVLR)进行形式化验证,并通过Blend v2和Aquarius两个竞赛的例子展示了形式化验证在发现智能合约漏洞中的应用。
本文是 Certora 对 Aquarius 项目进行的形式化验证竞赛报告,通过引入代码突变来评估参赛者编写的规范质量。报告详细列举了在 AccessControl、FeesController 和 Upgrade 等合约中发现的突变,展示了参赛者提交的高质量属性,并强调了发现的真实漏洞,如 Pending Upgrade 的 Code Hash 未被清除等问题。
Coinbase 遭受了一起数据泄露事件,起因是不良行为者收买海外客服人员出售客户数据,攻击者利用获取的信息进行进一步的社会工程攻击。文章强调了零信任架构的重要性,以及数据分类和权限管理在保护敏感数据方面的作用。Web3 技术需要采用更严格的安全措施,才能吸引传统机构和主流投资者。
Certora Prover v8.1.0 版本发布,引入了多项重大变更,包括最低 Java 和 Python 版本要求提升、默认启用健全性检查、requireInvariant 语义更新、Solana 和 Soroban 验证需使用专用命令、默认报告链接改为私有、CVL 函数支持 revert 处理等。
本文讨论了Web3应用安全问题,特别关注智能合约的形式化验证。Certora通过形式化验证技术确保智能合约安全,并总结了五个Rust智能合约开发最佳实践,包括保持代码模块化、利用编译器检查、简化数据结构、减少trap value状态以及分离核心逻辑与副作用,以提高代码的可验证性和安全性。
infiniFi 是一个 DeFi 平台,旨在优化收益,但其 iUSD 赎回机制存在漏洞,可能导致用户在赎回队列中被跳过,从而面临不公平的惩罚。Certora Prover 发现了这一问题,并通过形式化验证确保了修复后的系统符合 FIFO 原则,维护了用户信任和 DeFi 协议的公平性。
本文介绍了Certora团队开发的一款用于验证编译器优化的等价性检查工具,该工具通过比较优化前后程序的行为来检测编译器bug。文章还分享了该工具在Vyper编译器中发现的一个优化bug,该bug导致局部变量被错误地映射到相同的堆栈位置,从而改变了程序的行为。该bug已在Vyper 0.4.2版本中修复。
infiniFi 是一个 DeFi 平台,通过管理 Pendle、AAVE 和 Ethena 等协议上的存款来优化收益。
Silo Finance 的一个新杠杆合约模块在测试阶段遭到攻击,由于过于宽泛的批准设置导致借款操控漏洞。该模块与核心Silo协议隔离,因此核心协议、金库、市场或用户资金未受影响。Certora 此前对该合约进行了安全审查,但未发现此漏洞,事后进行了风险评估和补救措施,并确认现有Silo代码是安全的。