Browse all Smart Contract Security articles.
26 min read
Starknet 中的系统调用 在 Solidity 中，读取/写入存储、合约间调用或发送消息等底层操作，都是直接使用 Yul 通过内联汇编来执行的...
6 min read
Native Solana：必要的安全检查 在我们之前的 native Solana 教程中，为了保持示例简短并专注于核心主题，我们跳过了安全检查。在本教程中，我们将介绍……
15 min read
Storage Hooks 与 Ghosts 简介 通常我们需要检查特定存储位置的更改，以证明某个属性或不变量成立，特别是当该存储不...
6 min read
在存储映射中使用 Sload Hooks 简介 在上一章中，我们演示了在验证涉及 mapping 值变化的属性时，hooks 是必不可少的。该 hook 会监控...
8 min read
在规则中约束 Ghost 值 在上一章中，我们学习了 Ghost 变量如何让信息从 hook 流入规则。我们还了解到：在验证开始时……
9 min read
ERC-721 中的 SafeMint 和 SafeTransfer 规则简介 本章是我们对 OpenZeppelin 的 ERC-721 CVL 规范代码解析的第四部分（4/5），重点关注形式化验证……
17 min read
Preserved Block 及其在不变量验证中的作用 不变量是一种在智能合约部署之后及其整个执行过程中必须始终保持成立的属性。乍一看，...
12 min read
Certora 中的不变量简介 到目前为止，我们一直专注于验证单个方法或方法序列的行为——确保特定的函数调用或一组调用......
9 min read
Persistent Ghosts 简介 在之前的章节中，我们使用了幽灵变量（通过 hooks）来记录在智能合约中未被显式追踪的存储值和数量——例如，...
13 min read
形式化验证 Solady WETH 简介 ETH 广泛用于 DeFi 中的兑换、流动性提供、质押和抵押，因此需要一个兼容 ERC-20 的版本，以便协议可以通过...与其进行交互
17 min read
CVL 中的循环：路径爆炸与循环展开 循环是最常见的编程结构之一，但在形式化验证中，对它们进行推理仍然具有挑战性。虽然 Solidity 中的循环...
13 min read
在规则和不变量中使用 “requireInvariant” 到目前为止，我们要么编写一条规则来验证特定的行为，要么编写一个不变量来验证在整个……过程中必须始终成立的属性。