适用于所有场景的Echidna
TL;DR: 自发布以来，我们为Echidna添加了大量新功能和改进——而且还有更多即将到来。
两年前，我们开源了Echidna，这是我们基于属性的智能合约模糊测试工具。Echidna是我们智能合约评估中最常用的工具之一。根据我们的记录，在过去两年中，Echidna在我们约35%的智能合约审计中被使用。这包括多个知名审计项目，如MakerDAO、0x和Balancer。自Echidna首次发布以来，我们一直在添加新功能并修复错误。以下是我们的工作概览。
新功能
我们通过一系列令人兴奋的新功能扩展了Echidna的能力。其中一些最重要的功能包括：
支持多种编译框架使用crytic-compile：与crytic-compile的集成使Echidna能够测试复杂的Truffle项目，甚至其他语言的智能合约，如Vyper，开箱即用。这对用户完全透明（如果您是Echidna用户，您已经在使用它！），这是我们去年在Echidna中实施的最重要功能之一。
断言测试：Solidity的assert可以用作显式Echidna属性的替代方案，特别是当您检查的条件与函数深处某些复杂代码的正确使用直接相关时。断言测试还允许您检查编译器插入的隐式断言，例如没有显式属性的越界数组访问。在Echidna配置文件中添加checkAsserts: true，它将处理其余部分。
在Vera的MakerDAO示例中发现断言失败
限制模糊测试活动中调用的函数：并非所有智能合约中的函数都是平等的。其中一些在基于属性的测试中没有用，只会减慢活动速度。这就是为什么Echidna可以在模糊测试活动中黑名单或白名单要调用的函数。以下是一个Echidna配置，避免在模糊测试活动中调用“f1”和“f2”方法：
|
|
保存和加载模糊测试活动中收集的语料库：如果启用了覆盖支持，Echidna可以加载和保存以JSON格式收集的完整语料库。如果在模糊测试活动开始时语料库可用，Echidna将立即使用它。这意味着Echidna不会从零开始，这在CI测试期间特别有用，可以加速复杂属性的验证。在Echidna配置中添加coverage: true和corpusDir: "corpus"，并创建一个“corpus”目录来保存Echidna生成的输入。
语料库中交易的漂亮打印示例
检测高Gas消耗的交易：过度的Gas使用对智能合约的开发者和用户来说可能是个痛点。可用于检测大Gas消耗交易的工具很少，特别是如果检测交易需要通过其他交易达到合约的不寻常状态。最近Echidna添加了支持来检测此类问题。在Echidna配置中使用estimateGas: true，将高Gas交易报告到控制台。
发现消耗大量Gas的交易
复杂合约的扩展测试：Echidna还通过两个很酷的功能改进了复杂合约的测试。首先，它允许使用Etheno初始化具有任意交易的模糊测试活动。其次，它可以同时测试多个合约，调用任何测试合约的任何公共或外部函数。在Echidna配置中使用multi-abi: true来同时测试多个合约。
与最新研究保持同步
我们正在关注智能合约模糊测试论文的最新发展，以确保Echidna保持最新。我们的研究人员将开源模糊测试工具与Echidna进行比较，并整合任何被证明对发现故障或生成更有趣输入有效的新方法。事实上，我们不时测试研究论文中提出的示例，以确保Echidna能够非常高效地解决它们！我们还定期参加会议讨论新颖的模糊测试技术，甚至经济支持改进我们工具的新研究论文。
Echidna解决了Harvey论文中提出的示例
展望未来
而且我们没有休息！事实上，我们在不久的将来有一系列改进和新功能即将到来，包括增强的覆盖反馈、数组生成和语料库变异，以及Slither集成。我们还兴奋地分享，我们已经在crytic.io中添加了Echidna支持，这是我们用于智能合约的持续保证平台。
在crytic.io中集成Echidna进行自动断言检查
总结
两年来，Echidna已从一个实验性工具发展成为模糊测试智能合约和识别正确性/安全问题的基本资源。我们继续推动模糊测试智能合约的可能极限，并保持我们的开源工具更新以供社区使用。在我们的Building Secure Contracts培训中了解更多关于使用Echidna测试智能合约的信息。
您有智能合约要用Echidna测试吗？您有兴趣审查您的Echidna脚本或接受关于如何有效使用它的培训吗？给我们留言！Trail of Bits在执行智能合约安全评估方面拥有多年经验，处理从最小化代币到复杂的质押和投票平台的一切。
如果您喜欢这篇文章，请分享： Twitter LinkedIn GitHub Mastodon Hacker News