Recon 扩展:现在拥有更多 Halmos

  • Recon
  • 发布于 23小时前
  • 阅读 30

Recon Extension 新版本发布,集成了 Halmos,并支持 Vyper。该扩展旨在改进模糊测试工作流程,可以更高效地定义和打破属性。通过使用 Chimera 框架,Recon Extension 可以运行 Halmos, Echidna 和 Medusa,生成报告,并将损坏的测试转换为 Foundry reproducer。

Recon 帮助你构建和运行不变性测试

Recon 扩展:现在有了更多的 Halmos

运行 Halmos、Echidna 和 Medusa,生成报告,并使用 Recon 扩展将损坏的测试转换为 Foundry reproducers。

简介

新版本的 Recon 扩展发布了! 包含 Halmos、Vyper 支持以及更多功能!

我们利用一年多的模糊测试经验创建了 Recon 扩展,以改进我们的工作流程,以便我们可以更快地进入模糊测试最重要的部分:定义和打破属性。

该扩展的第一个版本通过提供以下功能实现了这一点:

  • 搭建你的模糊测试套件(使用 Chimera)

  • 与 Medusa、Echidna 和 Foundry 集成以运行测试

  • 自动为选定的合约生成 mocks

  • 清理模糊测试覆盖率报告,使其仅包含感兴趣的文件

  • 新功能:自动链接你的 Echidna/Medusa 设置中的 libraries

  • 自动为损坏的属性生成 reproducer 单元测试

  • 为模糊测试运行生成 markdown 报告,其中包含有关测试内容的详细信息

  • 新功能:增加了对 Mocks 和 Target Functions 的 Vyper 支持

现在,它已被 CentrifugeCornCredit Coop 等团队以及更多团队使用,下载量超过 300 次,它已证明了自己对任何使用 Chimera 框架 为不变性测试实施模糊测试的人的价值。

现在有了 Halmos

鉴于该扩展在改进工作流程方面取得了当前的成功,我们认为有必要支持其他工具,以通过 Halmos 进行符号执行来更好地进行不变性测试。

Chimera template 已经可以开箱即用地与 Halmos 配合使用,现在使用新的扩展功能,你可以自动:

  • 从扩展运行 Halmos。

  • 自动生成 halmos.toml 文件。

  • 将被 Halmos 破坏的单元测试和不变性测试转换为 Foundry reproducers。

  • 使用该扩展从 Halmos 运行自动生成报告。

运行 Halmos

从 Recon 扩展选项卡中,你可以单击 使用 Halmos 验证 按钮,以在你的 Chimera 套件上运行 Halmos。

Recon Cockpit 公开了核心配置选项,以简化 Halmos 的运行。

运行配置

我们简化了通过扩展运行 Halmos 时的界面,以便在大多数用例中,你只需要担心两个配置选项:目标合约和要执行的循环展开次数。

默认情况下,当使用 Chimera 框架 时,目标合约是 CryticTester 合约,该合约继承了 TargetFunctions 合约中定义的处理程序函数来更改系统状态。 但是,当使用 Halmos 运行时,CryticToFoundry 合约将成为从 TargetFunctions继承的入口点。

因为 Halmos 是一种符号执行工具,所以用于循环评估的符号值需要被限制,以便该工具不会无限期地运行。 因此,Loop 参数允许我们轻松地将循环迭代限制为固定值,以便于评估。

Halmos 配置

与 Foundry 类似,Halmos 使用 toml 配置文件格式。

使用扩展时自动生成的 halmos.toml 配置文件。

现在,当你使用 Recon 扩展运行 Halmos 时,此配置文件会自动生成并预先配置为与 Chimera 框架一起使用。 默认设置检查以 check_invariant_ 为前缀的函数中的断言。

Foundry Reproducers

Chimera 框架的核心理念是,Foundry 是调试 Solidity 合约问题的最简单工具,但其执行高级测试(如不变性测试和符号执行)的能力受到限制。 这就是为什么我们会自动将来自其他工具的 reproducers(这些工具对于测试 invariants(Echidna、Medusa,现在还有 Halmos)更强大)转换为 Foundry reproducer 单元测试,这些单元测试可以使用相同的值重复且快速地运行,以加快调试速度。

如果在通过扩展运行后,Halmos 发现了一个反例,则该扩展现在将自动生成一个 Foundry reproducer,该 reproducer 将添加到 CryticToFoundry 合约中。

create-chimera-app 存储库上的 Halmos 反例生成的 Foundry reproducer。

这些 Foundry reproducers 是为 Halmos 单元测试和不变性测试生成的。

报告生成

使用该扩展运行的所有工具都有一个生成 markdown 报告的选项,该报告允许查看测试了哪些属性以及生成 Foundry 单元测试的任何反例。

使用扩展运行 Halmos 后自动生成的 markdown 报告。

尝试一下

Recon 扩展的最新版本已在 VS Code Marketplace 上发布,或者可以直接从 github 存储库 下载。

  • 原文链接: getrecon.substack.com/p/...
  • 登链社区 AI 助手,为大家转译优秀英文文章,如有翻译不通的地方,还请包涵~
点赞 0
收藏 0
分享
本文参与登链社区写作激励计划 ,好文好收益,欢迎正在阅读的你也加入。

0 条评论

请先 登录 后评论
Recon
Recon
江湖只有他的大名,没有他的介绍。