登录 后可观看高清视频

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

5次播放
2小时前

视频 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，包括版本问题、内存指针覆盖和函数选择器错误。
    • 讨论了形式化验证的局限性，例如路径爆炸问题。
    • 介绍了模块化验证的概念，将复杂问题分解为更简单的子问题。
    • 强调了代码审计中手动审查和工具辅助相结合的重要性。