我们将使用三种独特的测试和程序分析技术：

每种技术都有优缺点，在特定情况下会很有用：

* 如果在没有超时情况下遍历所有路径

Slither 可以在几秒钟内分析合同，但是静态分析可能会导致误报，不太适合复杂的检查（例如算术检查）。 通过用于按钮访问内置检测器的 API 或用于用户自定义检查的 API 运行 Slither。

Echidna 需要运行几分钟，并且只会产生真阳性的测试结果。 Echidna 会检查用户提供的用 Solidity 编写的安全属性。 由于它的随机侦测的特性，它也许会错失一些漏洞。

Manticore 进行的是“最大权重”分析。 像 Echidna 一样，Manticore 会验证用户提供的特性。 它需要更多的时间来运行，但它可以证明某个特性的有效性，并且不会报告误报。

从 Slither 的内置检测器开始，确保现在没有或以后不会引入简单的漏洞。 使用 Slither 检查与继承、变量依赖关系和结构问题相关的属性。 随着代码库的增大，可以使用 Echidna 来测试状态机更复杂的特性。 再次使用 Slither 开发专门用于那些 Solidity 不提供保护的自定义检查，比如防止某个函数被覆盖。 最后，使用 Manticore 对关键安全属性进行有针对性的验证，例如算术运算。

关于单元测试的说明。 单元测试是构建高质量软件的必要条件。 然而，要找出安全漏洞，这些技术并不是最合适的。 它们通常用来测试正向代码行为（例如：代码在正常情况下按预期工作）， 但安全漏洞往往存在于开发者未考虑的边缘情况。 在我们进行的数十次智能合约安全测试研究中，单元测试覆盖率对于我们在客户端的代码中发现的安全漏洞的数量或者严重程度没有影响(opens in a new tab)。

为了有效测试和验证代码，你必须确定需要注意的地方。 因为花费在安全上的资源是有限的，只有划分出代码库中的薄弱和高价值部分，才能优化你的工作。 威胁建模可以提供帮助。 供考虑的审核方法有：

了解要检查的内容也有助于选择正确的工具。

通常与智能合约相关的领域比较广泛，包括：

状态机。大多数合约都可以表示为状态机。 考虑检查以下几点：(1) 不能到达无效状态，(2) 如果状态有效则可以到达，以及 (3) 没有状态会限制合约。

访问控制。如果你的系统有特权用户（例如所有者、监管者等），你必须确保 (1) 每个用户只能执行授权操作，并且 (2) 没有用户可以阻止权限更大的用户的操作。

算术运算。检查算术运算的可靠性至关重要。 在所有地方使用 SafeMath 是防止上溢/下溢很好的做法，但你还必需考虑其他算术缺陷，包括四舍五入和限制合约的缺陷。

继承的正确性。Solidity 合约在很大程度上依赖于多重继承。 因此，很容易出现一些诸如像缺少超级调用的遮蔽函数和曲解了 C3 线性化的顺序之类的错误。

外部交互。这里指合约之间的互动，一些外部合约不应该被信任。 例如，如果你的合约依赖于外部预言机，那么如果现有预言机有一半被泄漏，它是否仍然是安全的？

标准一致性。 以太坊标准（例如 ERC20）记录了他们在设计上的缺陷。 请注意你正在构建的标准的局限性。

其他领域需要根据你的目标进行检查， 但以上囊括的大致重点领域对于所有智能合约系统来说都是一个良好的开端。

我们公开的审计包含了经过验证或测试的属性实例。 请考虑阅读以下报告的自动测试和验证部分，以查看实际安全属性：