Browse all Smart Contract Security articles.
10 min read
在不变量中约束幽灵变量 在上一章中，我们看到了未受约束的幽灵变量会如何导致误报。我们还学习了如何使用语句来有效地约束……
9 min read
ERC-721 中的 SafeMint 和 SafeTransfer 规则简介 本章是我们对 OpenZeppelin 的 ERC-721 CVL 规范代码解析的第四部分（4/5），重点关注形式化验证……
7 min read
理解 Certora CVL 中的 Spec File 在上一章中，我们了解到，要使用 Certora Prover 进行形式化验证，我们需要向 Prover 提供以下关键项：智能...
8 min read
方法属性简介 简介 在上一章中，我们学习了参数化规则，这些规则使我们能够形式化验证预期成立的属性，无论哪个……
8 min read
参数化规则简介 到目前为止，在前面的章节中，我们已经编写了规则来验证特定方法的行为及其对合约状态的影响。例如：在第 2 章中，...
5 min read
在 CVL 中测试 msg.sender 和 msg.value 简介 在本章中，我们将介绍 CVL 中的变量，这使我们能够为依赖于 、 以及……中的其他全局变量的函数制定规则。
6 min read
形式化验证 Counter 在上一章中，我们学习了形式化验证的理论知识，包括它的概念以及它是如何工作的。在本模块中，我们将超越理论，进一步学习...
13 min read
Certora Require、Assert 和 Satisfy 在上一章中，我们了解到规范是一段用 CVL 编写的代码，用于描述智能合约的预期行为。一个……
10 min read
形式化验证简介 形式化验证是通过数学方法证明程序符合规范的过程。本文将从概念上介绍形式化验证是如何……
4 min read
形式化验证 Initializable.sol 本文介绍了 Certora 如何对 OpenZeppelin 的 Initializable.sol 合约进行形式化验证。我们假设读者已经熟悉该合约如何……
6 min read
形式化验证地址余额 在上一章中，我们介绍了如何在 CVL 中对环境依赖型函数进行推理，重点关注了非 payable 上下文。在这些示例中，访问......
7 min read
在 Certora 中测试 Revert 调用 在本章中，我们将学习如何使用方法标签（和）以及 CVL 中的特殊变量，来验证智能合约执行中预期的 revert。准备工作...