关于审计技术和工具 101事

• 原文链接： https://secureum.substack.com/p/audit-techniques-and-tools-101
• 译文出自：登链翻译计划
• 译者：翻译小组 校对：Tiny 熊
• 本文永久链接：learnblockchain.cn/article…

1. 审计：是对项目代码库的外部安全评估，通常由项目团队要求并支付费用。

   • 它检测并描述（在报告中）安全问题，包括潜在的漏洞、严重程度/难度、潜在的利用方案和建议的修复。

   • 它还提供了对代码质量、文档和测试的主观见解。

   • 审计报告的范围/深度/格式在不同的审计团队中有所不同，但它们通常涵盖类似的方面。

2. 审计范围：对于基于以太坊的智能合约项目，范围通常是链上智能合约代码，有时也包括与智能合约交互的链下组件。

3. 审计目标：审计的目标是评估项目代码（以及任何相关的规范、文件），并提醒项目团队（通常在启动之前）需要解决的潜在安全相关问题，以改善安全态势，减少攻击面并减轻风险。

4. 非审计目标：无论如何，审计都不是对"无缺陷"代码的安全保证，而是由训练有素的安全专家在合理的时间、理解、专业知识和当然的可判定性限制下进行的最佳努力。

5. 审计目标：安全公司为支付其服务的客户执行审计。因此，审计工作是优先为项目方服务，而不是针对项目用户/投资者。审计的目的不是为了提醒潜在的项目用户任何内在的风险。这不是他们的业务/技术目标。

6. 审计需要：基于智能合约的项目没有足够丰富以太坊智能合约安全专业知识和/或时间来进行内部安全评估，因此依赖于在这些领域拥有领域专业知识的外部专家。即使项目内部有一些专业知识，他们仍然会受益于具有补充/补充技能的无偏见的外部团队，他们可以审查项目假设、设计、规范和实现。

7. 审计类型：取决于项目的范围/性质/地位，但一般分为以下几类：

   • 全新审计：针对正在启动的新项目

   • 重复审计：针对正在修订的现有项目的新版本，有新的/固定的功能

   • 修复审计：审查对当前/以前的审计结果的修复。

   • 维护审计：用于不断审查项目的更新。

   • 事件审计：用于审查漏洞事件，从根本上导致事件的发生，识别潜在的漏洞并提出修复方案。

8. 审计时间表：取决于要评估的项目的范围/性质/状态以及审计的类型。这可能从几天的修复/维护者审计到几周， 全新的/重复的/事件审计而有所不同。

9. 审计工作：通常涉及一个以上的审计师同时进行，以获得独立的、多余的或补充/互补的项目评估专业知识。

10. 审计费用：取决于审计的类型/范围，但通常费用在1万美元/周以上，这取决于项目的复杂性、市场对审计的需求/供应以及审计公司的实力/声誉。

11. 审计的先决条件应包括：

    • 明确界定要评估的项目范围，通常是以github仓库中项目文件/文件夹的具体提交哈希的形式。

    • 公开/私有代码库

    • 公开/匿名团队

    • 规范项目的设计和架构

    • 项目的实现和业务逻辑的文档

    • 威胁模型和具体关注领域

    • 先前的测试，使用的工具，其他审计

    • 时间表、努力和成本/付款

    • 参与动态/提问/澄清的渠道，结果沟通和报告

    • 双方的联络点

12. 审计的局限性：审计是必要的（至少现在是），但不是充分的：

    • 风险有所降低，但由于几个因素，如有限的审计时间/精力、对项目规范/实现的有限洞察力、新的和快速发展的技术中有限的安全专业知识、有限的审计范围、显著的项目复杂性和自动/手动分析的局限性，所以存在残余风险。

    • 并非所有的审计都是等效的 -- 这在很大程度上取决于审计人员的专业知识/经验、相对于项目复杂性/质量所投入的努力以及所使用的工具/流程。

    • 审计提供了一个项目在短暂（通常是几周）期间的安全快照。然而，智能合约需要随着时间的推移不断发展，以增加新的功能，修复错误或优化。依靠每次变化后的外部审计是不现实的。

13. 审计报告：包括范围、目标、努力、时间表、方法、所使用的工具/技术、发现摘要、漏洞细节、漏洞分类、漏洞严重性/难度/可能性、漏洞利用情况、漏洞修复以及关于编程最佳做法的信息建议/意见的细节。

14. 审计结果分类：审计过程中发现的漏洞通常被分为不同的类别，这有助于了解漏洞的性质、潜在影响/严重程度、受影响的项目组件/功能和利用方案。例如，Trail of Bits使用以下分类：

    • 访问控制（Access Controls）：与用户的授权和权利的评估有关

    • 审计和记录：与行动的审计或问题的记录有关

    • 认证（Authentication）：与用户的识别有关

    • 配置（Configuration）：与服务器、设备或软件的安全配置有关

    • 密码学（Cryptography）：与保护数据的隐私或完整性有关

    • 数据暴露（Data Exposure）：与敏感信息的意外暴露有关

    • 数据验证（Data Validation）：与不适当地依赖数据的结构或价值有关

    • 拒绝服务： 与造成系统故障有关

    • 错误报告：与以安全方式报告错误情况有关

    • 补丁：与保持软件的更新有关

    • 会话管理： 与认证用户的识别有关

    • 时间（Timing）：与竞赛条件、锁定或操作顺序有关

    • 未定义的行为（Undefined Behavior）：与程序触发的未定义行为有关

15. 审计发现的可能性/难度。根据OWASP，可能性或难度是对该特定漏洞被攻击者发现和利用的可能性或难度的粗略衡量。OWASP提出了低、中、高三个级别的可能性。例如，Trail of Bits将每一个发现分为四个难度级别：

    • 未确定的（Undetermined）：在这次升级中，不能确定利用的难度

    • 低（Low）：普遍被利用，存在公开工具或可以用脚本来利用这个缺陷

    • 中等（Medium）：攻击者必须编写漏洞，或需要对复杂系统有深入了解

    • 高（High）：攻击者必须有内部访问系统的特权，可能需要知道极其复杂的技术细节，或者必须发现其他弱点才能利用这个问题

16. 审计发现的影响：根据OWASP，这估计了如果漏洞被利用，对系统的技术和商业影响的大小。OWASP提出了三个影响级别：低、中、高。

17. 审计结果的严重程度： 根据OWASP，可能性估计和影响估计被放在一起，以计算该风险的总体严重性。这是通过计算可能性是低、中、还是高来完成的，然后对影响做同样的计算。

    • OWASP提出了一个3x3的严重程度矩阵，将三个可能性级别和三个影响级别结合起来。
    • 严重程度矩阵（可能性-影响=严重程度）。低-低=注意；低-中=低；低-高=中；中-低=低；中-中=中；中-高=高；高-低=中；高-中=高；高-高=关键。
    • Trail of Bits 使用：
      • 信息（Information）: 该问题不构成直接风险，但与安全最佳实践或深度防御有关。
      • 未确定的（Undetermined）：在本次活动中，风险的程度未被确定。
      • 低（Low）：风险相对较小，或不是客户认为的重要风险。
      • 中等（Medium）：个别用户的信息处于危险之中，利用这些信息对客户的声誉不利，对客户有中等程度的财务影响，可能对客户有法律影响。
      • 高（Hight）：大量的用户，对客户的声誉非常不利，或有严重的法律或财务影响
    • ConsenSys 使用：
      • 小（Minor）：问题是主观性的。它们通常是围绕最佳实践或可读性的建议。代码维护者应该使用他们自己的判断来决定是否要解决这些问题。
      • 中等（Medium）：问题在本质上是客观的，但不是安全隐患。除非有明确的理由，否则这些问题应该被解决。
      • 重大（Major）：问题是安全漏洞，可能无法直接利用或需要某些条件才能利用。所有的重大问题都应该被解决。
      • 至关重要的（Critical）：问题是可直接利用的安全漏洞，需要修复。

18. 项目的审计清单（Trail of Bits建议见这里）：

    • 解决容易的问题：1) 启用并处理每一个编译器警告 2) 增加单元和功能测试覆盖率 3) 删除死代码、陈旧的分支、未使用的库和其他不相干的代码。
    • 文档：1）描述你的产品是做什么的，谁在使用它，为什么，以及它是如何交付的。2）在代码中加入关于预期行为的注释。3) 标记和描述你的测试和结果，包括正面和负面的。4) 包括过去的评论和bug。
    • 交付代码： 1) 记录在一台与你的内部网络完全断开的计算机上从头开始创建构建环境的步骤 2) 包括外部依赖关系 3) 记录构建过程，包括调试和测试环境 4) 记录部署过程和环境，包括这个过程的所有外部工具和库的具体版本。

19. 审计技术：涉及不同方法的组合，这些方法被应用于项目代码库，并附有规范和文件。许多是用工具进行的自动分析，有些需要人工协助。

    • 规范分析（手动）

    • 文档分析（手动）

    • 测试（自动）

    • 静态分析（自动化）

    • 摸索（自动化）

    • 符号检查(自动化)

    • 形式验证（自动化）

    • 手工分析（手动）

人们也可以把这些看作是手动/半自动/完全自动，其中半自动和完全自动的区别是需要用户定义属性的工具和除了分流结果外（几乎）不需要用户配置的工具之间的区别。完全自动化的工具往往是直接使用的，而半自动化的工具则需要一些人工协助，因此资源成本较高。

20. 规范分析：规范详细描述了项目及其各个组成部分在功能上应该做什么（有时是为什么），作为其设计和架构的一部分。

    • 从安全的角度来看，它规定了资产是什么，它们被保存在哪里，谁是行为者，行为者的特权，谁被允许访问什么和什么时候，信任关系，威胁模型，潜在的攻击载体，情景和缓解措施。

    • 分析一个项目的规范为审计人员提供上述细节，让他们评估所做的假设并指出任何缺陷。

    • 很少有智能合约项目在其第一个审计阶段有详细的规范。充其量，他们有一些关于实现内容的文件。审计人员花了很多时间从文档/实现中推断规范，这使得他们没有更多的时间进行漏洞评估。

21. 文档分析：文档是对基于设计和架构要求已经实现的内容的描述。

    • 文档回答了 "如何 "设计/架构/实现的问题，但不一定涉及 "为什么 "和设计/需求目标。

    • 文档通常以Github代码库中的Readme文件的形式，描述个别合约的功能，并结合功能NatSpec和个别代码注释。

    • 文档在很多情况下可以替代规范，并提供对项目团队的假设、要求和目标的重要见解。

    • 在查看代码之前了解文档有助于审计人员在推断项目架构、合约交互、项目约束、资产流、行为人、威胁模型和风险缓解措施方面节省时间。

    • 文档和代码之间的不匹配可能表明文档陈旧/贫乏、软件缺陷或安全漏洞。

    • 审计员应鼓励项目组全面记录，这样他们就不需要通过阅读代码来浪费时间来推断。

22. 测试：软件测试或验证是众所周知的软件工程基本原理，以确定软件在以不同选择的输入执行时是否产生预期的输出。

    • 智能合约的测试有类似的动机，但可以说更复杂，尽管与Web2软件相比，它们的规模（以代码行数计）相对较小。

    • 智能合约开发平台（Truffle、Embark、Brownie、Waffle、Hardhat等）相对较新，对测试的支持程度不同。

    • 一般来说，项目在审计阶段很少进行测试。测试与主网合约和状态的集成和可组合性是不容易的。

    • 测试范围和测试案例可以很好地说明项目的成熟度，同时也为审计人员提供有价值的假设/漏洞评估的边缘案例的见解。

    • 审计员应该期待高水平的测试和测试覆盖率，因为这是一个必须具备的软件工程学科，特别是当设计上暴露给区块链上每个人的智能合约最终持有价值数千万美元的资产时。

    • "程序测试可以用来显示错误的存在，但绝不是用来显示错误的不存在！" - E.W. Dijkstra

23. 静态分析：是一种在不实际执行程序的情况下分析程序特性的技术。

    • 这与软件测试相反，在软件测试中，程序被实际执行/以不同的输入运行。

    • 对于智能合约，静态分析可以在Solidity代码或EVM字节码上进行。Slither在Solidity层面进行静态分析，而Mythril分析EVM字节码。

    • 静态分析通常是控制流和数据流分析的结合。

24. Fuzzing：或称模糊测试是一种自动化的软件测试技术，包括向计算机程序提供无效、意外或随机数据作为输入。然后监测程序的异常情况，如崩溃、内置代码断言失败或潜在的内存泄漏。

    • 模糊测试与智能合约特别相关，因为任何人都可以在区块链上用随机输入与之交互，而不一定有有效的理由或期望（任意的拜占庭行为）。

    • Echidna和Harvey是两个流行的智能合约模糊测试工具。

25. 符号检查（Symbolic checking）：是一种检查程序正确性的技术，即证明/验证，通过使用符号输入来表示状态和过渡的集合，而不是单独列举单个状态/过渡。

    • 模型检查或属性检查是一种检查系统的有限状态模型是否符合给定规范的方法（也称为正确性）。

    • 为了在算法上解决这样的问题，系统的模型和它的规范都要用一些精确的数学语言来表述。为此，该问题被表述为逻辑学中的一项任务，即检查一个结构是否满足一个给定的逻辑公式。

    • 一个简单的模型检查问题包括验证一个给定的结构是否满足命题逻辑中的一个公式。

    • 与其一次一次地列举可达状态，有时可以通过在一个步骤中考虑大量的状态来更有效地遍历状态空间。当这种状态空间的遍历是基于一组状态和过渡关系的表示，作为逻辑公式、二进制决策图（BDD）或其他相关的数据结构，模型检查方法是符号化的。

    • 模型检查工具面临着状态空间的组合爆炸，通常被称为状态爆炸问题，要解决大多数现实世界的问题必须解决这个问题。

    • 符号算法避免了明确地构建有限状态机（FSM）的图；相反，它们使用量化命题逻辑的公式隐含地表示图。

26. 形式化验证：是指使用数学的形式化方法，证明或反驳一个系统所依据的预定算法在某种形式化规范或属性方面的正确性的行为。

    • 形式化验证可以有效地检测出人工或使用较简单的自动化工具难以检测的复杂错误。

    • 形式化验证需要被验证程序的规范，以及将规范与实际实现进行转换/比较的技术。

    • Certora的 Prover和ChainSecurity的VerX是智能合约形式验证工具的例子。Runtime Verification Inc的KEVM是一个形式化验证框架，为EVM语义建模。

27. 人工分析：是对使用工具的自动分析的补充，并为智能合约审计中的关键需求服务。

    • 使用工具的自动分析是便宜的（通常是开源的免费软件），快速，确定性和可扩展性（取决于半自动/完全自动的工具），但只有在它意识到的属性中才是好的，这通常仅限于Solidity和EVM相关的约束。

    • 相比之下，人工分析是昂贵的、缓慢的、非决定性的和不可扩展的，因为在智能合约安全方面的具有专业知识依然是罕见的，并且人类通常速度较慢，容易出错和不一致。

    • 然而，人工分析是目前推断和评估业务逻辑和应用层面约束的唯一方法，而这正是大多数严重漏洞被发现的地方。

28. 假阳性：是指表明存在漏洞，但事实上并不存在漏洞的发现。这种假阳性可能是由于不正确的假设或分析中的简化，没有正确考虑实际存在漏洞所需的所有因素。

    • 假阳性需要对发现进行进一步的人工分析，以调查它们确实是假阳性还是真阳性。

    • 大量的假阳性现象增加了人工验证的工作量，降低了对早期自动/人工分析的准确性的信心。

    • 真阳性结果有时可能被归类为假阳性结果，从而导致漏洞被利用而不是被修复。

29. 假阴性：是指遗漏的发现，这些发现本应表明漏洞的存在，但事实上根本就没有报告。这种假阴性可能是由于不正确的假设或不准确的分析，没有正确考虑实际存在漏洞所需的最低因素。

    • 根据定义，假阴性是不会被报告的，甚至不会被意识到，除非不同的分析显示它们的存在或漏洞被利用。

    • 高数量的假阴性降低了人们对早期人工/自动分析有效性的信心。

30. 审计公司（有代表性的；不是详尽的）：ABDK, Arcadia, Beosin, Blockchain Consilium, BlockSec, CertiK, ChainSafe, ChainSecurity, Chainsulting , CoinFabrik, ConsenSys Diligence, Dedaub, G0, Hacken, Haechi, Halborn, HashEx, Iosiro , Least Authority, MixBytes, NCC, NewAlchemy, OpenZeppelin, PeckShield, Pessimistic, PepperSec, Pickle , Quantstamp, QuillHash, Runtime Verification, Sigma Prime, SlowMist, SmartDec, Solidified, Somish, Trail of Bits 和 Zokyo。

31. 智能合约安全工具：在协助智能合约开发者和审计师展示（潜在的）可利用的漏洞，突出危险的编程风格或浮现常见的滥用模式方面至关重要。然而，这些都不能取代人工审查/验证的需要，以评估特定合约的业务逻辑和其他复杂的控制流、数据流和价值流方面。

32. 安全工具的类别：测试工具、测试覆盖率、提示、反汇编、可视化、静态分析、动态分析和智能合约的形式验证。

33. Slither 是一个用Python 3编写的Solidity静态分析框架。它运行一套漏洞检测器，打印关于合约细节的可视化信息，并提供一个API来轻松编写自定义分析。Slither使开发者能够发现漏洞，提高他们的代码理解力，并快速建立自定义分析的原型。它在公开的免费版本中实现了74个检测器（有奖杯，展示了Slither在真实世界合约中的发现）。

34. Slither的特点：

    • 检测脆弱的Solidity代码，误报率低

    • 识别错误条件在源代码中发生的位置

    • 容易集成到持续集成和 Truffle 构建中

    • 内置 "打印" 快速报告关键的合约信息

    • 用Python编写自定义分析的检测器API

    • 能够分析用Solidity >= 0.4编写的合约。

    • 中间表示法（SlithIR）能够进行简单、高精度的分析

    • 正确地解析99.9%的所有公开Solidity代码

    • 每个合约的平均执行时间小于1秒

35. Slither bug和优化检测可以在 Truffle/Embark/Dapp/Etherlime/Hardhat 应用程序或单个Solidity文件上运行。

    • Slither默认运行其所有检测器。要只运行选定的检测器，使用 --detect detector1,detector2。要排除检测器，使用 --exclude detector1,detector2。

    • 要排除具有信息或低严重性的检测器，使用--exclude-informational或 --exclude-low。

    • --list-detectors 列出可用的探测器。

36. Slither 打印 允许使用 --print 和以下选项打印合约信息（合约摘要、人类摘要和继承图用于快速审查，其他如调用图、cfg、功能摘要和vars-and-auth用于深入审查）:

    • 调用图:将合约的调用图导出到一个dot文件中

    • cfg：导出每个函数的CFG

    • 构造函数调用。打印所执行的构造函数

    • 合约摘要：打印合约的摘要

    • 数据依赖性。打印变量的数据依赖性

    • echidna: 导出Echidna的信息

    • evm: 打印函数中节点的evm指令

    • function-id: 打印函数的keccack256签名

    • function-summary: 打印函数的摘要

    • human-summary: 打印合约的可读摘要

    • inheritance：打印合约之间的继承关系

    • 继承图：将每个合约的继承图导出到一个dot文件中

    • 修改器：打印每个函数所调用的修改器

    • require: 打印每个函数的require和assert调用

    • slithir：打印函数的slithIR表示法

    • slithir-ssa: 打印函数的slithIR表示法

    • variable-order: 打印状态变量的存储顺序

    • vars-and-auth: 打印写入的状态变量和函数的授权

37. Slither 可升级性检查有助于使用slither-check-upgradeability工具审查使用delegatecall代理模式的合约，其选项如下：

    • became-constant：不应该是常量的变量

    • function-id-collision：函数ID的碰撞

    • function-shadowing: 函数的阴影

    • missing-calls: 缺少对初始函数的调用

    • 缺少init-modifier：初始化器（）没有被调用

    • 多次调用：初始化函数被多次调用

    • order-vars-contracts: 与v2的vars顺序不正确

    • order-vars-proxy：与代理的变量顺序不正确

    • variables-initialized: 具有初始值的状态变量

    • were-constant: 应该是常量的变量

    • extra-vars-proxy: 代理中的额外变量

    • missing-variables: v2中缺少的变量

    • extra-vars-v2: v2中的额外变量

    • init-inherited: Initializable不被继承

    • init-missing: 缺少可初始化的函数

    • initialize-target: 必须调用的初始化函数

    • initializer-missing: 缺少initializer()

38. Slither 代码相似性检测器 (一个面向研究的工具)使用最先进的机器学习来检测相似的(脆弱的)Solidity函数:

    • 它使用一个来自 etherscan_verified_contracts 的预训练模型，其中有 60,000 个合约和超过 850,000 个函数。
    • 它使用FastText，一种矢量嵌入技术，来生成每个函数的紧凑的数字表示。
    • 它有四种模式：（1）测试--在合约数据集中找到与你自己相似的函数（2）绘图--提供多个采样函数的相似性的可视化表示（3）训练--建立大型合约数据集的新模型（4）信息--检查预训练模型的内部信息或评估代码

39. Slither合约扁平化工具 slither-flat产生一个具有以下特点的扁平化版本的代码库。

    • 支持三种策略。1) MostDerived。导出所有最派生的合约（每个文件都是独立的） 2）OneFile：在一个独立的文件中导出所有合约 3）LocalImport。在一个独立的文件中导出每个合约，并在其前奏中包括导入"..."。
      • 支持循环依赖性
      • 支持所有的编译平台（Truffle, embark, buidler, etherlime, ...）。

40. Slither格式工具slither-format可自动生成补丁。这些补丁与git兼容。补丁在应用前应仔细审查。该工具支持的检测器有:

    • 未使用的状态
    • Solc-version
      • pragma
      • 命名规范
      • 外部函数
      • 常量状态
      • 常量函数

41. Slither ERC一致性工具slither-check-erc对ERC20、ERC721、ERC777、ERC165、ERC223和ERC1820的ERC一致性进行以下检查。

    • 所有的功能都存在

    • 所有的事件都存在

    • 函数返回正确的类型

    • 必须是视图的函数是视图

    • 事件的参数被正确索引

    • 这些函数发出了事件

    • 派生合约不会破坏一致性

42. Slither属性生成工具slither-prop可以生成代码属性（如不变量），可以用单元测试或Echidna测试，完全自动。可以测试的ERC20场景有：

    • 可转账 - 测试正确的代币转账

    • 可暂停的 - 测试可暂停的功能

    • NotMintable - 测试没有人可以铸造代币

    • NotMintableNotBurnable - 测试没有人可以铸造或销毁代币

    • NotBurnable - 测试没有人可以销毁代币

    • Burnable - 测试代币的销毁情况。要求使用 burn(address) returns()函数

43. Slither 新的检测器: Slither的插件架构让你可以整合新的检测器，从命令行运行。一个检测器的骨架有:

    • ARGUMENT：让你从命令行中运行检测器

    • HELP：是从命令行中打印的信息

    • IMPACT：表示问题的影响。允许的值是 INFORMATIONAL|LOW|MEDIUM|HIGH

    • CONFIDENCE：表示你对分析的信心。允许的值是低|中|高

    • WIKI：常数用于自动生成文档。

    • _detect() 是实现检测器逻辑的函数，需要返回一个发现列表。

44. Manticore 是一个用于分析以太坊智能合约的符号执行工具（除了Linux二进制文件和WASM模块）。详见教程。

    • 程序探索: Manticore可以用符号输入来执行一个程序，并探索它所能达到的所有可能状态。

• 输入生成: Manticore可以自动生成导致给定程序状态的具体输入。

• 错误发现: Manticore可以检测二进制文件和智能合约中的崩溃和其他失败情况。

• 工具化: Manticore通过事件回调和指令钩子提供对状态探索的细粒度控制。

• 程序化接口: Manticore通过一个Python API公开了对其分析引擎的程序化访问。

45. Echidna是个Haskell程序，旨在对以太坊智能合约进行模糊化/基于属性测试。它使用复杂的基于语法的模糊测试活动，基于合约ABI来伪造用户定义的谓词或Solidity断言。

46. Echidna的特点:

    • 生成适合你实际代码的输入

    • 可选的语料库收集、突变和覆盖率指导，以发现更深层次的bug

    • 由Slither提供支持，在模糊处理活动之前提取有用的信息

    • 源代码整合，以确定在模糊处理活动后哪些行被覆盖了

    • 复古用户界面，纯文本或JSON输出

    • 自动将测试案例最小化，以便快速分流

    • 无缝集成到开发工作流程中

    • 模糊测试活动的最大Gas使用报告

    • 支持用Etheno和Truffle进行复杂的合约初始化

47. Echidna使用方法（详见教程）。

    • 执行测试运行器: Echidna的核心功能是一个叫做echidna-test的可执行程序。echidna-test接收一个合约和一个不变式（应该永远保持真实的属性）列表作为输入。对于每个不变量，它生成对合约的随机调用序列，并检查该不变量是否成立。如果它能找到一些方法来伪造该不变式，它就会打印出这样的调用序列。如果它不能，你就可以保证合约是安全的。

    • 编写不变式: 不变量可以用 Solidity 函数表达，其名称以 echidna_ 开头，没有参数，并返回一个布尔值。

    • 收集和可视化覆盖率: 在完成一个活动后，Echidna可以将覆盖率最大化的语料库保存在一个由corpusDir配置选项指定的特殊目录中。这个目录将包含两个条目：（1）一个名为coverage的目录，包含JSON文件，可以被Echidna重放；（2）一个名为covered.txt的纯文本文件，是带有覆盖率注释的源代码副本。

48. Eth-security-toolbox是一个预先安装和预先配置了Trail of Bits所有以太坊安全工具的Docker容器。这包括：

    • 基于Echidna属性的模糊测试器

• Etheno集成工具和差分测试器

• Manticore符号分析器和形式化合约验证器

• Slither静态分析工具

• Rattle EVM提升器

• 智能合约库

49. Ethersplay是个二进制Ninja插件，可以实现EVM反汇编器和相关分析工具：
    • 接受原始二进制格式的evm字节码作为输入。

• 渲染所有函数的控制流图

• 显示Manticore覆盖率

50. Pyevmasm是一个用于以太坊虚拟机（EVM）的汇编和反汇编库。它包括一个命令行工具和一个Python API。

51. Rattle是一个EVM二进制静态分析框架，设计用于部署的智能合约（不再活跃开发）。

52. Evm_cfg_builder是一个用于从EVM字节码中提取控制流图(CFG)的工具，被Ethersplay、Manticore和Trail of Bits的其他工具使用。

    • 通过专用的值集分析，从EVM字节码中可靠地恢复控制流图（CFG）。

• 恢复函数名称

• 恢复属性（例如，payable、view、pure）。

• 将CFG输出到一个dot文件

• 库 API

53. Crytic-compile是一个智能合约编译库，用于Trail of Bits的安全工具，支持Truffle, Embark, Etherscan, Brownie, Waffle, Hardhat和其他开发环境。该插件在Crytic工具中使用，包括：
    • Slither

• Echidna

• Manticore

• evm-cfg-builder

54. Solc-select 是一个在Solidity编译器版本之间快速切换的脚本。

    • solc-select: 管理安装和设置不同的solc编译器版本

    • solc: 围绕solc的包装器，根据通过solc-select设置的版本选择正确的版本

    • solc二进制文件从https://binaries.soliditylang.org/，其中包含了许多Linux和macOS的历史和现代solc版本的官方工件。

55. Etheno是的以太坊测试瑞士军刀。它是一个JSON RPC多路复用器、分析工具封装器和测试集成工具。

    • JSON RPC多路复用： Etheno运行一个JSON RPC服务器，可以复用调用一个或多个客户端。1) 用于过滤和修改JSON RPC调用的API 2) 通过向多个以太坊客户端发送JSON RPC序列实现差异化测试 3) 同时部署到多个网络并与之交互

    • 分析工具封装器：Etheno为Manticore等高级分析工具提供了一个JSON RPC客户端 1) 降低了使用高级分析工具的门槛 2) 不需要自定义脚本来设置账户和合约状态 3) 无需Solidity源代码即可分析任意交易

    • 与Ganache和Truffle等测试框架集成：1）用一个命令运行本地测试网络 2）使用Truffle迁移来引导Manticore分析 3）在单元测试中进行符号语义注释

56. MythX是一个强大的安全分析服务，可以在你的开发生命周期中发现你的以太坊智能合约代码中的Solidity漏洞。它是一个基于API的付费服务，在后端使用几个工具，包括静态分析器（Maru）、符号分析器（Mythril）和灰盒模糊器（Harvey）来实现总共46个检测器。Mythril是MythX的开源组件。

57. MythX的过程:

    • 提交你的代码。分析请求是用TLS加密的，你提交的代码只有你自己能访问。同时提交你的智能合约的源代码和编译后的字节码，以获得最佳结果。

    • 启动一整套分析技术： MythX运行的时间越长，越能发现更多的安全弱点。

      • 收到一份详细的分析报告： MythX可以检测到SWC注册表中列出的大部分漏洞。该报告将返回在你的代码中发现的所有弱点的清单，包括问题的确切位置和它的SWC ID。生成的报告只能由你访问。MythX提供3种扫描模式，快速、标准和深入。你可以在这里看到它们的区别。

58. MythX的工具: 当你向API提交你的代码时，它会被多个微服务并行分析，这些工具合作，在提供的执行时间内返回更全面的结果。

    • 一个静态分析器，解析Solidity AST

    • 符号分析器，检测可能的脆弱状态，以及

    • 一个灰盒模糊器，检测脆弱的执行路径

59. MythX的覆盖范围：扩展到SWC注册表中发现的大多数SWC，其中列出了46个检测器这里以及所用分析的类型。

60. MythX基于SaaS（安全即服务）平台，其前提是：

    • 与在本地运行安全工具相比，性能更高

    • 比任何独立的工具有更高的漏洞覆盖率

    • 随着智能合约安全形势的发展，我们的安全分析技术不断改进，有了新的和改进的安全测试，从而受益。

61. MythX对使用其SaaS API提交的智能合约代码的隐私保证。

    • 代码分析请求是用TLS加密的

    • 为了提供全面的报告并提高性能，它在我们的数据库中存储了一些合约数据，包括部分源代码和字节码，但这些数据从未离开他们的安全服务器，也不会与任何外部方共享。

    • 它保留了你的分析结果，所以你以后可以检索它们，但报告只能由你访问。

62. MythX运行时间：快速扫描运行5分钟，标准扫描运行30分钟，深度扫描运行90分钟。

63. MythX的官方集成、工具和库包括：

    • MythX CLI：将MythX作为命令行界面（CLI）使用的统一工具，现在完全支持Truffle项目。

    • MythX-JS：在你的JS或TS项目中整合MythX的类型脚本库。

    • PythX：Python库，将MythX集成到你的Python项目中。

    • MythX VSCode。VSCode扩展，允许你扫描智能合约并直接从你的代码编辑器中查看结果。

64. MythX的收费：

    • 按需（9.99美元/3次扫描）。所有扫描模式和预付费扫描包

    • 开发者（49美元/月）。快速和标准扫描模式；500次扫描/月

    • 专业版（249美元/月）。所有扫描模式；10 000次扫描/月

    • 企业版（自定义定价）。为你的团队的具体需求定制计划；定制验证服务；定制支持的保留费用

65. Scribble是种验证语言和运行时验证工具，可将高级规范翻译成solidity代码。它允许你用属性来注释solidity智能合约（见这里）：

    • 原则/目标： 1）规范易于被开发者和审计者理解 2）规范易于推理 3）规范可以使用现成的分析工具进行有效的检查 4）少量的核心规范结构足以表达和推理更高级的结构

• 将Scribble规范语言中的注释转换为具体的断言

• 有了这些工具化但等价的合约，就可以使用Mythril、Harvey、MythX

66. Fuzzing-as-a-Service：是ConsenSys Diligence最近推出的一项服务，项目可以提交他们的智能合约，以及使用Scribble语言编写的内嵌规范或属性。这些合约通过Harvey模糊器运行，该模糊器使用指定的属性来优化模糊活动。模糊测试的任何违规行为都会从服务中报告出来，供项目修复。

67. Karl是个智能合约的监控器，使用Mythril检测引擎检查安全漏洞。它可以用来实时监控以太坊区块链上新部署的脆弱智能合约。

68. Theo是一个具有类似Metasploit界面的开发工具，让你进入一个Python REPL控制台，在那里你可以使用可用的功能来进行智能合约侦察，检查存储，运行漏洞或针对特定智能合约的frontrun或backrun交易。特点：

    • 自动智能合约扫描，生成可能的漏洞列表

    • 发送交易以利用智能合约

    • 交易池监控

    • Web3控制台

    • 前端交易和后端交易

    • 等待交易清单并发送其他交易

    • 估计交易的Gas意味着只发送成功的交易

    • 禁用Gas估算将发送具有固定Gas数量的交易。

69. Visual Auditor是个Visual Studio Code扩展，为 Solidity 和 Vyper提供安全意识的语法和语义高亮显示：

    • 语法高亮：访问修饰符（external, public, payable, ...），安全相关的内建程序，globals，方法和用户/默许的信息，（address.call(), tx.origin, msg.data, block.*，now），存储访问修改器（内存，存储），注释中的开发者说明（TODO，FIXME，HACK，...），自定义函数修改器，合约创建/事件调用，轻松区分算术与逻辑运算，使构造函数和回退函数更加突出

    • 语义高亮：高亮状态变量（常量，继承），检测并提醒状态变量的遮蔽，高亮函数体中的函数参数

    • 审查功能：审计注释/书签 - @audit - <msg> @audit-ok - <msg>（见下文），导入外部扫描器结果的通用接口 - cdili json格式（见下文），codelens内联动作：图形、报告、依赖关系、继承、解析、ftrace、扁平化、生成单元测试存根、函数签名散列、UML

    • 图形和报告功能：从vscode中访问你最喜爱的Sūrya功能，带有调用流高亮的交互式调用图等，从代码中自动生成UML图，以支持你的威胁建模练习或文档。

    • 代码增强：悬停在以太坊账户地址上可下载字节码、源码或在浏览器中打开，悬停在ASM指令上可显示其签名，悬停在关键字上可显示基本安全说明，悬停在状态变量上可显示声明信息。

    • 视图：Cockpit 与 Outline

70. Surya 通过提供合约结构的信息，帮助审计人员理解和可视化Solidity智能合约，并生成调用图和继承图。它还支持以多种方式查询函数调用图，以帮助人工检查合约。

    • 与Visual Auditor集成

    • 命令：graph, ftrace, flatten, describe, inheritance, dependencies, parse, mdreport

71. SWC Registry ： 智能合约弱点分类注册表（SWC Registry）是EIP-1470中提出的弱点分类方案的实现。

    • 它与通用弱点列举（CWE）中使用的术语和结构松散一致，同时覆盖了智能合约特有的广泛的弱点变体。

    • 本项目的目标如下。1）提供一种直接的方式来对智能合约系统中的安全问题进行分类。2）为描述智能合约系统的架构、设计或代码中的安全问题定义一种通用语言。3）作为训练和提高智能合约安全分析工具性能的一种方式。

    • 该代码库由MythX背后的团队维护，目前包含37个条目

72. Securify：是一个针对以太坊智能合约的安全扫描器，它采用Datalog编写的静态分析，支持38个漏洞。

73. VerX：是一个验证器，可以自动证明以太坊智能合约的时间安全属性。该验证器基于三个想法的精心组合：将时间安全验证简化为可达性检查，一个高效的符号执行引擎用于计算交易中的精确符号状态，以及延迟抽象，将交易结束时的符号状态近似为抽象状态。

74. SmartCheck：是一个可扩展的静态分析工具，用于发现用Solidity编程语言编写的以太坊智能合约中的漏洞和其他代码问题。它将Solidity源代码翻译成基于XML的中间表示，并根据XPath模式对其进行检查。

75. 基于K-Framework的分析、建模和验证工具来自Runtime Verification (RV)：提供KEVM，这是K-Framework中EVM的模型。它是第一个完全通过官方测试套件的EVM的可执行规范，并作为一个平台，用于建立广泛的分析工具和EVM的其他语义扩展。

76. Certora Prover：检查一个智能合约是否满足一套用称为Specify的语言编写的规则。每条规则都在所有可能的交易上进行检查，当然这不是通过明确地列举交易来完成的，而是通过符号技术。

• Certora验证器为用户提供的一组安全规则提供完整的路径覆盖。例如，一个规则可能会检查在ERC20合约中只能铸造一个有限数量的代币。验证器要么保证一条规则在所有路径和所有输入上都成立，要么产生一个测试输入，证明违反了该规则。
• Certora验证器处理的问题是已知的不可判定的，这意味着总会有一些病态的程序和规则，Certora验证器会在没有明确答案的情况下超时。
• Certora验证器将智能合约（作为EVM字节码或Solidity源代码）和一组规则（用Certora的规范语言编写）作为输入。然后，验证器使用两种计算机科学技术的组合自动确定合约是否满足所有的规则：抽象解释和约束解决。

77. DappHub的Hevm：是EVM的一个实现，专门为单元测试和调试智能合约而制作。它可以运行单元测试、属性测试，在显示Solidity源代码的同时交互式地调试合约，或者运行任意的EVM代码。

78. 夺旗竞赛（CTF）：是有趣的教育性挑战，参与者必须入侵不同的（假）智能合约，这些合约中存在漏洞。它们有助于理解围绕漏洞如何在野外被利用的复杂性。流行的包括

    • Capture The Ether：是由Steve Marx创建的一组20个挑战，测试以太坊的合约、账户和数学等概念的知识。
    • Ethernaut：是OpenZeppelin的一个基于Web3/Solidity的战争游戏，在以太坊虚拟机中进行。每个关卡都是一个智能合约，需要被 "黑 "掉。该游戏是100%开源的，所有关卡都是其他玩家的贡献。
    • Damn Vulnerable DeFi v2：是由tinchoabbate创建的一组12个与DeFi相关的挑战。根据不同的挑战，你应该阻止系统工作，尽可能多地偷取资金，或者做一些其他意想不到的事情。
    • Paradigm CFT：是由samczsun在Paradigm创建的一组17个挑战。

79. 智能合约安全工具在协助审计师审查智能合约时非常有用。它们将许多任务自动化，可以编入具有不同覆盖率、正确性和精确度的规则。与人工分析相比，它们是快速、廉价、可扩展和确定性的。但它们也容易受到假阳性的影响。它们目前特别适合于检测常见的安全隐患和在Solidity和EVM层面的最佳实践。在不同程度的人工协助下，它们也可以被编程，以检查应用层面、商业逻辑的限制。

80. 审计过程可以被认为是一个十步的过程，如下:

    • 阅读项目的规范/文件，了解需求、设计和结构

    • 运行快速的自动化工具，如linters或静态分析器，以调查常见的Solidity隐患或缺失的智能合约最佳实践

    • 手动分析代码以了解业务逻辑并检测其中的漏洞

    • 运行较慢但更深入的自动化工具，如符号检查器、模糊器或形式验证分析器，这些工具通常需要事先制定属性/约束条件，在分析过程中手把手地指导，并在运行后对其结果进行一些评估。

    • （与其他审计人员）讨论上述发现，以确定任何假阳性或遗漏的分析。

    • 向项目组传达情况，以澄清业务逻辑或威胁模型方面的问题。

    • 在审计期间反复进行上述工作，留出一些时间来写报告

    • 撰写报告，总结上述内容，并详细说明调查结果和建议

    • 将报告交给项目组，并讨论调查结果、严重程度和可能的修复措施。

    • 评估项目组的修复方案，并验证它们是否确实消除了发现中的漏洞。

81. 阅读规范/文件。对于那些有智能合约设计和架构规范的项目，这是推荐的起点。很少有新项目在审计阶段有规范。他们中的一些人有部分的文件。一些关键点:

    • 规范从项目的技术和业务目标及要求开始。它描述了项目的设计和架构如何帮助实现这些目标。

    • 智能合约的实际实现是目标、要求、规范、设计和架构的功能体现，对其的理解对于评估实现是否确实符合目标和要求至关重要。

    • 文档是对基于设计和架构要求所实现的内容的描述。

    • 规范回答了 "为什么"某些东西需要以它的方式被设计/架构/实现。文件回答了 "如何" 设计/架构/实现的问题，但不一定涉及 "为什么"，而是让审计人员去猜测原因。

    • 文档通常以Readme文件的形式描述单个合约的功能，并结合功能NatSpec和单个代码注释。鼓励项目提供详细的规范和文档，可以为审计人员在理解项目目标/结构方面节省大量的时间和精力，并防止他们做出与实现相同的假设，这是造成漏洞的一个主要原因。

    • 在缺乏规范和文档的情况下，审计人员不得不通过阅读代码和使用Surya和Slither打印机等工具来推断目标、需求、设计和架构。这占用了大量的时间，使得更深入/复杂的安全分析时间减少。

82. 运行静态分析器。自动工具，如linters或静态分析器，有助于调查常见的Solidity隐患或缺失的智能合约最佳实践

    • Slither和MythX等工具在其检测器的背景下对智能合约进行控制流和数据流分析，这些检测器对常见的安全隐患和最佳实践进行编码。

    • 评估他们的发现，通常在几秒钟/几分钟内就可以得到，这是一个很好的起点，可以根据Solidity语言、EVM或以太坊区块链的知名约束/属性来检测常见的漏洞。

    • 在一些检测器的发现中，可能会出现假阳性，如果是真/假阳性，则需要手动验证。

83. 手动代码审查：需要了解业务逻辑并检测其中的漏洞。

    • 自动分析器不了解应用层面的逻辑和它们的约束。他们仅限于Solidity语言、EVM或以太坊区块链的约束。

    • 需要对代码进行人工分析，以检测实现过程中与安全相关的、与规范或文档相关的偏差。

    • 审计员可能需要直接从代码或与项目团队的讨论中推断出业务逻辑及其隐含的约束，然后评估这些约束/属性是否在代码库的所有部分都适用。

84. 运行更深入的自动化工具：如模糊器，如Echidna，符号检查器，如Manticore，工具套件，如MythX，用Scribble或Certora Prover正式验证自定义属性，需要更多的设置和准备时间，但有助于运行更深入的分析，发现应用级属性和数学错误等方面的边缘案例。

    • 鉴于这些需要了解项目的应用逻辑，建议至少在最初的手工代码审查之后，或者有时在与项目团队深入讨论规范/实现之后使用。

    • 分析这些工具的输出需要对工具本身、其特定领域的语言，有时甚至是其内部工作原理有大量的专业知识。

    • 评估假阳性现象有时对这些工具来说是个挑战，但它们发现的真阳性现象是很重要的，即使是最好的人工分析也会错过的极端角落案例。

85. 与其他审计人员进行头脑风暴。Linus's law。"只要有足够的眼球，所有的bug都是浅显的"，如果审计人员对智能合约的实现、假设、发现和漏洞进行头脑风暴，可能也适用。

    • 虽然有些审计公司鼓励主动/被动讨论，但也有一些公司的做法是让审计人员分别进行评估，以鼓励独立思考而不是集体思考。其前提是，集体思考可能会使审计小组偏向于关注某些方面，而忽略一些漏洞。
    • 一种混合的方法可能很有趣，审计小组最初进行头脑风暴，讨论项目的目标、规范/文件和执行情况，但后来又形成防火墙，独立进行评估，最后再一起汇总他们的发现。

86. 与项目组讨论。与项目组有一个开放的沟通渠道，对于澄清规范、文件、实现中的任何假设，或讨论中期发现都是很有用的。

    • 研究结果也可以立即与项目团队在私有代码库上共享，以讨论影响、修复和其他影响。

    • 如果审计跨越了多个星期，每周进行一次同步电话可能会有帮助。与此相对应的是，独立地进行整个评估，以便不被项目团队的投入和意见所偏离。

87. 报告的撰写。审计报告是整个评估的最终汇编，并介绍了审计的所有方面，包括审计范围/覆盖面、时间表、团队/努力、总结、工具/技术、发现、利用场景、建议的修复、短期/长期建议以及任何关于工具和理由的进一步细节的附录。

    • 执行摘要通常对审计报告进行概述，其中包括说明所发现漏洞的数量/类型/严重程度的重点/难点以及对风险的总体评估。它还可能包括对智能合约、（推断的）行动者、资产、角色、权限、访问控制、交互、威胁模型和现有风险缓解措施的描述。

    • 报告的大部分内容集中在审计结果、其类型/类别、可能性/影响、严重程度、这些评级的理由、潜在的利用场景、智能合约的受影响部分和潜在的补救措施。

    • 它还可能涉及代码质量、可读性/可审计性的主观方面，以及与文档、代码结构、功能/变量命名惯例、测试覆盖率等有关的其他软件工程最佳实践，这些方面不构成紧迫的安全风险，但却是影响安全漏洞引入和持续存在的反模式和流程的指标。

88. 报告交付。向项目组交付报告是一个关键的交付物和里程碑。除非分享临时发现/状态，否则这将是项目团队第一次接触到评估的细节。

    • 交付通常是通过一个共享的在线文件进行的，并伴随着宣读，在宣读过程中，审计师向项目组介绍报告的重点，以便讨论和辩论调查结果及其严重性评级。

    • 项目组通常需要一些时间来审查审计报告，并对调查结果、严重程度或建议的修复措施进行反驳。

    • 根据事先的协议，项目组和审计公司可能会公开发布审计报告（在所有要求的修复工作完成后），或者项目可能会因为某些原因决定不公开。

89. 评估修复工作。审计结束后，项目组可以对报告中的发现进行任何必要的修复，并要求审计交易所审查他们的回应。

    • 对大部分的发现进行修复，审查时可能需要确认所应用的修复（可能与审计建议的修复不同）确实减轻了发现所报告的风险。

    • 调查结果可能被认为是不相关的，不在项目的威胁模型之内，或者仅仅被认为是在项目可接受的风险模型之内。

    • 审计公司可以评估所应用的具体修复措施，并确认/否认其风险缓解。除非是修复/维护类型的审计，这一阶段通常不超过一天，因为它通常会在商定的审计期限之外。

90. 人工审查方法： 审计人员有不同的方法来手动审查智能合约代码的漏洞：

    • 从访问控制开始

    • 从资产流开始

    • 从控制流开始

    • 从数据流开始

    • 推断约束条件

    • 理解依赖关系

    • 评估假设条件

    • 评估安全检查表

91. 从访问控制开始。访问控制是最基本的安全基础，它解决了 "谁"对 "什么"的授权访问。（在一个正式的访问控制模型中，"谁"指的是主体，"什么"指的是对象，访问控制矩阵表示主体和对象之间的权限）。

    • 虽然总体理念可能是智能合约是无权限的，但在现实中，它们确实对交互/使用它们的不同行为者有不同的权限/角色。

    • 一般的分类是用户和管理员。为了保护性启动或其他目的，许多智能合约有一个管理员角色，通常是部署合约的地址。管理员通常可以控制关键的配置和应用参数，包括合约资金的（紧急）转移/提取。

    • 从了解智能合约实现的访问控制开始，并检查它们是否正确、完整和一致地应用，是了解访问流和检测违规的好方法

92. 从资产流开始。资产是由智能合约管理的以太币或 ERC20/ERC721/其他代币。鉴于漏洞的目标是有价值的资产，开始评估资产流入/流出/流入/跨越智能合约及其依赖关系是有意义的：

    • 谁：根据应用逻辑，资产应该只被授权/指定的地址提取/存入。

    • 何时：只有在授权的/指定的时间窗口或在授权的/指定的条件下，按照应用逻辑（何时）提取/存入资产。

    • 哪些资产：只有那些被授权/指定的类型，应该按照应用逻辑被提取/存放。

    • 为什么：根据应用逻辑，只有在授权/指定的原因下才可以提取/存入资产。

    • 在哪里：根据应用逻辑，资产应该只被提取/存放到授权/指定的地址。

    • 什么类型：按照应用逻辑，只有授权/指定类型的资产才能被提取/存入。

    • 多少钱：只有授权的/指定的金额的资产，应该按照应用逻辑提取/存入。

93. 评估控制流: 控制流分析控制的转移，即执行顺序，在智能合约之间和内部：

    • 程序间（程序只是函数的另一个名称）控制流通常由调用图表示，它显示了智能合约之间或内部的哪些函数（调用者）调用了哪些其他函数（被调用者）。

    • 程序内（即在一个函数内）控制流是由条件（if/else）、循环（for/while/do/continue/break）和返回语句决定的。

    • 程序内和程序间控制流分析都有助于跟踪智能合约中的执行和数据流。

94. 评估数据流: 数据流分析了智能合约之间和内部的数据转账情况

    • 程序间数据流是通过分析在调用地点作为函数参数参数值的数据（变量/常量）来评估的。

    • 程序内数据流是通过分析（状态/内存/calldata）变量/常量沿函数内控制流路径的分配和使用来评估的。

    • 程序内和程序间的数据流分析都有助于跟踪智能合约中全局/局部存储/内存变化的流动。

95. 推断约束条件。程序约束基本上是程序应该遵循的规则。语言级和EVM级安全约束是众所周知的，因为它们是语言和EVM规范的一部分。然而，应用层面的约束是隐含在所实现的业务逻辑中的规则，可能不会在规范中明确描述，例如，当地址向智能合约存入一定的ERC-20代币时，将铸造ERC-721代币，当它撤回先前的存款时，将其销毁。这种约束可能必须由审计人员在手动分析智能合约代码时推断出来：

    • 推断程序约束的一种方法是评估与特定逻辑相关的大多数程序路径上正在做的事情，并将其视为一种约束。如果这样的约束在一个或极少数程序路径上缺失，那么它可能是一个漏洞的指标（假设该约束与安全有关），或者这些程序路径是约束不需要成立的特殊条件。

    • 程序约束也可以用符号检查器来验证，该检查器沿着执行路径生成反例或证明，这些约束不成立。

96. 了解依赖性。当程序代码的正确编译或运行依赖于其他智能合约的代码/数据时，就存在依赖性，而这些代码/数据不一定是由项目组开发的。

    • 明确的程序依赖性在导入语句和继承层次中被获取。例如，许多项目使用OpenZeppelin社区开发的、经过审计和时间检验的智能合约，用于代币、访问控制、代理、安全等。

    • 通过智能合约与其他协议的对接，预期并鼓励可组合性，这导致了对外部智能合约的状态/逻辑的紧急或隐性依赖，例如，通过预言机。

    • 这在依赖其他相关协议的稳定币、收益率生成、借/贷、衍生品、预言机等的DeFi协议中尤其值得关注/关切。

97. 评估假设: 许多安全漏洞是由错误的假设造成的，例如，谁可以访问什么，什么时候，在什么条件下，出于什么原因等等。识别程序代码所做的假设并评估它们是否确实正确，可以成为许多审计结果的来源。一些常见的错误假设的例子是：

    • 只有管理员可以调用这些函数

    • 初始化函数只被合约部署者调用一次（例如，对于可升级的合约）。

    • 函数将总是按照一定的顺序被调用（正如规范所期望的）。

    • 参数只能有非零值或在一定阈值内的值，例如地址永远不会是零值。

    • 某些地址或数据值永远不能被攻击者控制。它们永远无法到达可以被滥用的程序位置。(在程序分析文献中，这被称为污点分析）。

    • 函数调用总是成功的，因此不需要检查返回值。

98. 评估安全检查表： 检查表是逐项列出的清单，可以快速而有条不紊地遵循（并在之后通过其清单编号进行参考），以确保所有列出的项目都已按照相关领域进行处理。

    • 这种基于清单的方法在《清单宣言（”The Checklist Manifesto. How to Get Things Right“）》一书中得到了普及。Atul Gawande是一位著名的外科医生、作家和公共卫生领导人。马尔科姆-格拉德威尔（Malcolm Gladwell）在他对这本书的评论中写道。"加万德一开始就对无知的错误（因为我们知道得不够多而犯的错误）和无能的错误（因为我们没有适当地利用我们知道的东西而犯的错误）进行了区分。他写道，现代世界的失败实际上是关于这些错误中的第二种，他通过一系列医学的例子告诉我们，外科医生的常规任务现在已经变得非常复杂，以至于这样或那样的错误几乎是不可避免的：对于一个本来有能力的医生来说，太容易错过一个步骤，或者忘记问一个关键问题，或者在当时的压力下，没有为每一种可能的情况做好计划。加万德随后访问了飞行员和建造摩天大楼的人，并带回了一个解决方案。专家们需要核对表--实际上是书面的指南，指导他们完成任何复杂程序中的关键步骤。在这本书的最后一节，加万德展示了他的研究团队如何采用这一想法，开发了一个安全的手术检查表，并在世界各地应用，取得了惊人的成功"。

    • 鉴于快速发展的以太坊基础设施（新平台、新语言、新工具和新协议）的复杂程度令人匪夷所思，以及部署智能合约管理数百万美元的风险，智能合约有许多事情需要正确处理，很容易错过一些检查，做出不正确的假设或没有考虑潜在的情况。因此，智能合约专家也需要检查表。

    • 智能合约安全检查表（如本系列文章）有助于浏览需要记住和应用的大量关键方面。它们有助于有条不紊地浏览逐项的特征、概念、隐患、最佳实践和例子，而不会遗漏任何项目。众所周知，核对表可以提高记忆力，并有更快的回忆。它们还有助于参考感兴趣的具体项目，例如，安全隐患和最佳做法101中的第42条或审计技术和工具101中的第98条。

99. 提出概念验证的漏洞。漏洞利用是指恶意行为者触发漏洞，滥用智能合约，导致资产被盗/冻结等事件。

    • 以代码或假设场景的书面描述呈现此类漏洞的概念证明，通过说明具体的利用路径和证明发现的严重性，使审计结果更加现实和有意义。

    • 漏洞应该始终在测试网中，保持私密性，并负责任地披露给项目团队，不存在任何在实际系统中执行导致资金或访问权实际损失的风险。

    • 描述性的利用方案应该对行动者的角色/权力、他们行动的实际原因以及触发漏洞的事件顺序做出现实的假设，并说明利用的途径。

100. 估计可能性和影响。可能性表示一个漏洞被恶意行为者发现并引发成功利用潜在弱点的概率。影响表示如果漏洞被利用，对系统的技术和业务方面的影响程度。在许多情况下，估计可能性/影响是否低/中/高是不难的。

     • 如果漏洞可以由几个交易手动触发，不需要很多资源/访问（例如不是管理员），也不需要假设很多条件成立，那么可能性被评估为高。需要深入了解系统工作原理、特权角色、大量资源或多个边缘条件才能成立的漏洞被评估为中等可能性。其他需要更难的假设才能成立的，例如矿工串通，链分叉或内部人员串通，被认为是低可能性。

     • 如果有任何资金损失或锁定，那么其影响被评估为高。不影响资金但扰乱系统正常运作的漏洞通常被评估为中等。其他的都是低影响。

     • 许多可能性和影响的评估在审计团队和项目团队之间是有争议和争论的，通常有安全意识的审计团队要求提高可能性和影响，而项目团队则淡化风险。

     估算严重性，根据OWASP，严重性是可能性和影响的组合。有了对这两者的合理评估，从OWASP矩阵中估计严重性应该是很简单的。

101. 总结：审计是一种时间、资源和专业知识的约束，训练有素的专家使用自动和手动技术的组合评估智能合约，以找到尽可能多的漏洞。审计可以显示漏洞的存在，但不能显示其不存在。