汇编与 EVM 课程 - Gas 2

视频 AI 总结： 该视频主要讲解了如何使用 Certora 工具对智能合约进行形式化验证，特别是针对 Gas 优化后的合约进行等价性验证。视频通过一个 NFT 市场的例子，展示了如何定义 ghost 变量、使用 hooks 监控合约状态变化、编写 invariants 来验证合约行为，以及如何利用 method summaries 和 prover arguments 来解决验证过程中遇到的问题，最终实现对 Gas 优化合约的功能等价性证明。 视频中提出的关键信息包括： 1. **Ghost 变量：** 用于在形式化验证中追踪合约状态，但不会影响合约的实际执行。 2. **Hooks：** 用于在特定 EVM 操作码执行时触发自定义逻辑，例如更新 ghost 变量。 3. **Invariants：** 用于声明合约状态必须满足的条件，Certora 会尝试找到违反这些条件的执行路径。 4. **Method Summaries：** 用于简化或替换合约中的函数行为，例如使用 `dispatcher` 关键字来限制外部调用的影响。 5. **Prover Arguments：** 用于配置 Certora 的行为，例如使用 `optimistic fallback` 来假设外部调用不会对合约状态产生任意修改。 6. **Parametric Rules：** 允许验证具有未定义方法变量的规则，用于比较不同合约在相同输入下的行为。 7. **Vacuity Checks：** 用于检测规则是否过于严格，以至于没有输入可以满足所有前提条件。 8. **等价性验证：** 通过比较 Gas 优化前后合约的 getter 函数返回值，证明它们在功能上是等价的。

汇编与 EVM 课程 - NFT 市场 gas 优化

**视频 AI 总结：** 该视频是 Assembly EVM Op Codes 和 Formal Verification 课程的最后一部分，旨在帮助学习者掌握汇编和形式化验证技术。视频的核心内容是演示如何使用形式化验证工具 Certora 来验证一个用 Solidity 编写的 NFT 市场合约和一个用汇编重写的、更节省 Gas 的版本是否等价。通过这个过程，学习者可以学习到如何确保汇编代码在功能上与 Solidity 参考实现一致，从而构建更高效的智能合约。 **视频中提出的关键信息：** * **CodeHawks 平台：** 学习者可以在完成课程后参与 codehawks 上的形式化验证竞赛，并有机会获得报酬。 * **Gas Bad NFT Marketplace 项目：** 该项目包含一个用 Solidity 编写的 NFT 市场合约（`nft_marketplace.sol`）和一个用汇编重写的版本（`gas_bad_nft_marketplace.sol`），汇编版本旨在节省 Gas 费用。 * **形式化验证目标：** 视频将演示如何使用 Certora 验证以下两点： * 每当映射（mapping）被更新时，都会发出一个事件（event）。 * Gas Bad NFT Marketplace 和 NFT Marketplace 在调用任何函数后，最终状态是相同的（除了 Gas 消耗的差异）。 * **Certora 的使用：** 视频将从头开始编写 Certora 的配置文件和规范文件，并介绍以下概念： * **Ghost 变量：** 用于在验证过程中定义额外的变量，以便在规则和Hook之间传递信息。 * **Hooks（Hook）：** 用于在特定的底层操作（如存储变量的加载和存储）上附加 CVL 代码。 * **Init State 和 Axiom：** 用于初始化 Ghost 变量，并确保初始状态始终为真。 * **参数化规则：** 包含未定义方法变量的规则，允许对多个方法进行验证。 * **NFT Mock 合约：** 视频首先使用一个简单的 NFT Mock 合约进行热身，验证总供应量（total supply）永远不会为负，以及铸造（mint）函数总是铸造一个 NFT。 * **乐观循环（Optimistic Loop）：** 在某些情况下，需要启用乐观循环来避免循环展开问题。 * **代码仓库：** 视频提供了与课程相关的 GitHub 代码仓库[链接](https://github.com/Cyfrin/assembly-evm-opcodes-and-formal-verification-course)，学习者可以在其中找到项目代码和资源。

汇编与 EVM 课程 - 形式化验证与 Halmos 和 Certora 工具

视频 AI 总结： 该视频是关于使用形式化验证和符号执行来审计智能合约，特别是针对一个名为 "Math Master" 的代码库。该代码库包含用于定点数运算的算术库，包括 `molwod`、`molwodUp` 和 `sqrt` 函数，这些函数都大量使用了汇编代码。视频强调了形式化验证在发现模糊测试无法找到的 bug 方面的作用，并介绍了 Halmos 和 Certora 等工具。 关键信息： * **核心内容：** 介绍使用形式化验证工具 Halmos 和 Certora 审计 Math Master 代码库，寻找汇编代码中的 bug。 * **关键信息：** * Math Master 代码库包含 `molwod`、`molwodUp` 和 `sqrt` 三个函数，用于定点数运算。 * 形式化验证可以发现模糊测试无法找到的 bug。 * 介绍了 Halmos 和 Certora 两种形式化验证工具。 * 强调了理解代码库属性和编写正确断言的重要性。 * 演示了如何使用 Halmos 和 Certora 查找 Math Master 代码库中的 bug，包括版本问题、内存指针覆盖和函数选择器错误。 * 讨论了形式化验证的局限性，例如路径爆炸问题。 * 介绍了模块化验证的概念，将复杂问题分解为更简单的子问题。 * 强调了代码审计中手动审查和工具辅助相结合的重要性。

汇编与 EVM 课程 - YUL 与 Huff

视频 AI 总结： 该视频主要讲解了以太坊虚拟机（EVM）的底层编程，包括 YUL 语言和 Huff 语言，以及如何使用它们来编写更高效的智能合约。视频通过一个 HorseStore 合约的例子，展示了如何将 Solidity 代码转换为 YUL 和 Huff 代码，并进行测试。强调了理解 EVM 底层原理对于优化智能合约和进行安全分析的重要性。 关键信息： 1. YUL 是一种内置于 Solidity 的低级语言，可以实现对 EVM 的细粒度控制。 2. Huff 是一种更底层的语言，直接操作 EVM 的操作码，可以实现更高的 gas 效率。 3. 可以使用 HuffMate 工具来简化 Huff 编程，例如处理映射（mapping）的存储和读取。 4. 通过将 Solidity 代码转换为 YUL 和 Huff 代码，可以更好地理解 EVM 的工作原理。 5. 可以使用 Foundry 的 forge snapshot 命令来比较不同语言编写的智能合约的 gas 消耗。 6. 强调了理解 EVM 底层原理对于优化智能合约和进行安全分析的重要性。 7. 介绍了 Metadeck 工具，可以帮助分析以太坊上的智能合约。

汇编与 EVM 课程 #3 - EVM 操作码及编译器工作原理

视频 AI 总结： 本视频的核心内容是深入解析 Solidity 智能合约在二进制层面的运作方式，通过逐行分析 Solidity 代码编译后的 EVM 操作码，揭示编译器背后的工作原理。视频旨在帮助开发者理解 Solidity 编译器的行为，掌握智能合约底层运作机制，从而编写更高效、更优化的智能合约代码。 视频中提出的关键信息： 1. Solidity 智能合约编译后包含三个主要部分：合约创建代码、运行时代码和元数据。 2. 合约创建代码负责将运行时代码部署到区块链上。 3. 运行时代码是合约实际执行的逻辑，是所有外部调用的入口点。 4. Solidity 使用“空闲内存指针”来管理内存，确保变量存储在未使用的内存区域。 5. Solidity 编译器会自动添加一些安全检查，例如检查消息值（msg.value）和调用数据大小（calldata size），以防止潜在的安全问题。 6. 函数分发器（function dispatcher）负责根据调用数据中的函数选择器（function selector）来执行相应的函数。 7. 可以通过反编译器将智能合约的字节码转换回 Solidity 代码，尽管反编译的结果可能不完全准确。 8. 预编译合约（precompiles）是 EVM 中预先部署在特定地址的特殊合约，用于执行特定的操作，例如椭圆曲线恢复（EC recover）。

汇编与EVM 课程 #2 -通过 HorseStore 学习 Huff & Opcodes

视频 AI 总结： 本视频主要讲解了以太坊虚拟机（EVM）和操作码（Opcodes）的基础知识，并通过使用 Huff 语言重写一个简单的存储合约（HorseStore）来深入理解智能合约在最低层面的工作原理。视频强调了理解操作码对于优化智能合约和进行形式化验证的重要性，并介绍了如何使用 Foundry 进行测试和调试。 关键信息： 1. **核心内容：** 智能合约本质上是一系列操作码的组合，EVM 通过执行这些操作码来处理交易和存储数据。 2. **操作码（Opcodes）：** EVM 的基本指令，每个操作码由一个字节表示，用于执行特定的操作，如数据存储、算术运算等。 3. **Huff 语言：** 一种低级语言，允许开发者直接编写操作码，从而更好地理解智能合约的底层机制。 4. **数据存储位置：** EVM 中有三种主要的数据存储位置：栈（Stack）、内存（Memory）和存储（Storage），栈用于临时计算，内存用于临时存储，存储用于持久化数据。 5. **Calldata：** 发送到智能合约的数据，包括函数选择器和参数。 6. **函数分发（Function Dispatching）：** 智能合约根据 Calldata 中的函数选择器来确定要调用的函数。 7. **测试和调试：** 使用 Foundry 框架进行智能合约的测试和调试，包括使用调试器逐行查看操作码的执行过程。 8. **Differential Testing：** 通过比较 Solidity 和 Huff 编写的合约的输出来验证它们的行为是否一致。 9. **Gas 优化：** 通过直接编写操作码，可以实现更高效的 Gas 消耗。

汇编与形式化验证 EVM #1 课程介绍

视频 AI 总结： 本视频是关于 EVM 汇编操作码和形式化验证智能合约的课程介绍，旨在帮助开发者和安全研究人员达到区块链知识的顶尖水平。课程内容包括反汇编智能合约、学习字节码、优化合约 Gas 消耗、使用 Yul 和 Huff 编写智能合约，以及形式化验证。通过三个项目实践，深入学习 Halmos 和 Certora 等工具，掌握形式化验证和 Fuzzing 的使用场景，提升智能合约开发和安全能力。 关键信息： * 课程目标：成为区块链知识顶尖的开发者和安全研究人员。 * 课程内容： * 智能合约反汇编和字节码学习。 * 使用 Yul 和 Huff 编写 Gas 优化合约。 * 形式化验证工具 Halmos 和 Certora 的使用。 * Fuzzing 和形式化验证的结合应用。 * 目标学员：已经熟悉 Solidity 或 Vyper 的开发者，希望提升到更高水平。 * 课程特点：深入、高级、项目驱动，强调实践和工具使用。 * Vyper 和 Solidity 的比较：Vyper 和 Solidity 都是高级语言，可以保护开发者免于出错，例如 calldata 大小和意外发送 E 以及安全数学。而且它们都是很棒的语言。所以选择任何一个并享受乐趣。Huff 和 Yul 是很棒的语言，如果你需要非常具体的性能代码，或者你希望了解更多关于 EVM 的信息。我不建议将这些语言用于所有生产代码。但我认为它们对于学习和理解来说非常棒。

智能合约审计、DeFi安全课程 | Tswap 重新审计（续）

视频 AI 总结： 该视频主要讲解了在智能合约安全审计中如何利用模糊测试（Fuzzing）和不变性测试（Invariant Testing）来发现漏洞，并以 TSWAP 协议为例，展示了从无到有构建测试套件的过程。视频强调了理解协议核心不变性的重要性，并介绍了无状态模糊测试、有状态模糊测试（包括 open 方法和 handler 方法）等不同测试策略。通过实例演示，说明了如何编写测试代码，以及如何解读测试结果，最终成功发现 TSWAP 协议中的一个漏洞。 视频中提出的关键信息包括： 1. **模糊测试（Fuzzing）**：通过向系统输入随机数据来尝试破坏它，分为无状态和有状态两种。 2. **不变性测试（Invariant Testing）**：验证系统中的某些属性是否始终成立，即使在随机输入下。 3. **无状态模糊测试**：每次测试都从头开始，不保留之前的状态。 4. **有状态模糊测试**：每次测试都基于前一次测试的状态，模拟更复杂的交互场景。 5. **Handler 方法**：通过创建一个 Handler 合约来限制模糊测试的范围，使其更贴近实际使用场景。 6. **核心不变性**：协议中必须始终保持的属性，例如 TSWAP 协议中的 x * y = k。 7. **WEIRD ERC20s**：具有非标准行为的 ERC20 代币，可能导致协议出现漏洞。 8. **代码覆盖率**：使用 Foundry 提供的工具来检查测试覆盖率，确保测试充分。 9. **工具链**：Slither、Adarin 等静态分析工具可以辅助发现潜在问题。 10. **手动代码审查**：即使有自动化工具，也需要进行手动代码审查，以发现逻辑错误和潜在风险。 11. **报告撰写**：清晰地描述漏洞、影响、复现步骤和修复建议。

智能合约审计、DeFi安全课程 | AMM 是如何运作的 ？

视频 AI 总结： 该视频主要讲解了去中心化交易所（DEX）中自动做市商（AMM）的工作原理，并将其与传统的订单簿模式进行对比。AMM 通过资金池和池中资产的比例来确定价格，用户通过向一个池子放入相应比例的资产来从另一个池子取出资产，从而完成交易。视频还提到了 Uniswap 的不同版本，并强调了安全研究员在理解新协议时应积极提问和实践的重要性。 关键信息： * 传统订单簿模式的交易需要在订单簿中匹配买卖双方，DeFi 中交易成本高昂。 * AMM 使用资金池和池中资产的比例来确定价格，降低了交易成本。 * 用户通过向一个池子放入相应比例的资产来从另一个池子取出资产，从而完成交易。 * 流动性提供者通过提供资金池来赚取交易手续费。 * 安全研究员应积极提问、查阅资料、甚至亲自测试来理解新协议。

智能合约审计、DeFi安全课程 | 流动性提供者

视频 AI 总结： 该视频解释了自动化做市商（AMM）中流动性提供者（LP）如何通过交易手续费获得收益。视频详细讲解了LP如何将资金存入资金池，获得LP代币作为所有权凭证，并根据其在资金池中的份额获得交易手续费。通过一个具体的交易示例，展示了手续费的累积如何使LP在提取资金时获得略高于初始投资的回报。视频强调了LP通过提供流动性来赚取收益的机制，以及手续费在其中的作用。 关键信息： 1. **交易手续费：** 每次在AMM中进行交易时，都会收取一定比例的手续费（例如0.03%），这些费用不会被“无限套娃”利用，而是用于奖励流动性提供者。 2. **流动性提供者（LP）：** LP将资金（例如USDC和WEF）存入资金池，以提供交易所需的流动性。 3. **LP代币：** 作为回报，LP会收到LP代币，代表其在资金池中的所有权份额。 4. **收益机制：** LP通过交易手续费获得收益，手续费会累积在资金池中，LP在提取资金时可以获得略高于初始投资的回报。 5. **资金池价值累积：** 交易手续费会使资金池的价值缓慢增加，LP可以根据其LP代币的份额分享这些收益。