探索智能合约安全的新工具：Yools

项目介绍

Yools 是一款实验性的 Yul 语言符号执行引擎，旨在通过将 Yul 程序转化为一组 SMT（ satisfiability modulo theories）约束，并借助 SMT 解决器来检测特定程序状态的可达性。目前，其主要功能是检查程序是否可能引发回滚错误。

项目技术分析

Yools 支持 Yul 的完整语法，但并非所有的 EVM 内置函数都在其中。它采用典型的 BMC (bounded model checking) 风格对循环进行最多指定次数的展开（用户可自定义）。这意味着在存在循环的情况下，结果可能不总是健全的，此时的结果假设循环不会超过给定的界限。

该工具提供了一个名为 symbolic 的子命令，用于实现可用的符号执行功能。用户可以通过命令行输入源文件并调整参数，如循环展开限制和所使用的 SMT 解决器。

例如：

yools symbolic -i switch.yul

对于简单的 Yul 源代码，Yools 可以轻松判断是否存在导致回滚的路径。

项目及技术应用场景

Yools 主要针对想要验证智能合约安全性的人群，尤其是那些希望从编译器级别的代码入手的开发者或安全专家。与直接分析 EVM 字节码或 Solidity 源代码相比，有以下几个优势：

1. 相比于 Solidity，开发和维护 Yul 工具更简单，因为它的高级语言结构和类型变更较少。
2. Yul 包含更多结构化信息，比如函数、循环、条件分支以及存储访问等，这使得代码推理和证明更加直观。
3. 分析 Yul 代码可以避免在字节码层面上的信任问题，虽然最终部署的是 EVM 字节码，但在分析阶段无需考虑编译过程。

尽管如此，Yools 也存在一些限制，比如没有 Solidity 提供的复杂类型和结构化信息，以及无法直接处理已编译的二进制代码。

项目特点

• 灵活性：Yools 允许高度定制化的符号表示法，为不同的内存区域（如 calldata、memory 和 storage）编码提供了多种方式。
• 探索式研究：项目的目标之一是实验不同方法来提高 SMT 约束的生成，以便找到最适合特定 Yul 程序的方法。
• 未完成的功能：包括函数/循环摘要、ABI 编码/解码抽象、并行处理和外部调用等，这些未来的特性将使 Yools 功能更加强大和完善。

贡献者欢迎

如果你对智能合约验证或相关技术感兴趣，Yools 团队热情欢迎你的加入，一起探讨并贡献代码！

总的来说，Yools 作为一个新颖的工具，为智能合约的安全验证带来了新的视角和可能性。无论是开发者还是安全研究人员，都值得尝试并利用它来增强你的合约审核流程。