引用本文：郑忠斌,王朝栋,蔡佳浩.智能合约的安全研究现状与检测方法分析综述[J].信息安全与通信保密,2020(7):93-105.
摘要
随着密码学和通信技术的发展，传统的纸质合约迎来了革命性的改变，基于密码学这种高科技上的数字化合同逐渐崭露头角，智能合约通过程序代码规定合约条款和触发条件，一旦满足出发条件合约便会自行执行。基于对智能合约存在的重入漏洞、整数溢出漏洞、拒绝服务攻击漏洞和时间戳依赖漏洞等安全漏洞进行的总结分析，提出了针对智能合约漏洞的形式化验证、符号执行、静态分析和污点分析等检测方法，并进行了相关的实验分析，最后提出了总结与展望。
关键词：智能合约；安全漏洞；检测方法；实验分析
内容目录：
0 引 言
1 智能合约的安全问题
1.1 重入漏洞
1.1.1 重入漏洞原理
1.1.2 重入漏洞场景
1.1.3 重入漏洞防守
1.2 整数溢出漏洞
1.2.1 整数溢出漏洞原理
1.2.2 整数溢出场景
1.2.3 整数溢出漏洞防守
1.3 拒绝服务攻击漏洞
1.3.1 拒绝服务攻击漏洞原理
1.3.2 拒绝服务攻击漏洞场景
1.3.3 拒绝服务攻击漏洞防守
1.4 未检查 call 调用返回值漏洞
1.4.1 未检查 call 返回值漏洞原理
1.4.2 未检查 call 返回值漏洞场景
1.4.3 未检查 call 返回值漏洞防守
1.5 短地址/参数攻击漏洞
1.5.1 短地址/参数攻击漏洞原理
1.5.2 短地址/参数攻击漏洞防守
1.6 危险的 Delegatecall 漏洞
1.6.1 危险的 Delegatecall 漏洞原理
1.6.2 危险的 Delegatecall 漏洞防守
1.7 时间戳依赖漏洞
1.7.1 时间戳依赖漏洞原理
1.7.2 时间戳依赖漏洞防守
1.8 以太币冻结漏洞
1.8.1 以太币冻结漏洞原理
1.8.2 以太币冻结漏洞防守
1.9 无气发送漏洞
1.9.1 无气发送漏洞原理
1.9.2 无气发送漏洞防守
1.10 交易顺序依赖漏洞
1.10.1 交易顺序依赖漏洞原理
1.10.2 交易顺序依赖漏洞防守
1.11 区块变量依赖漏洞
1.11.1 区块变量依赖漏洞原理
1.11.2 区块变量依赖漏洞防守
1.12 Tx Origin 依赖漏洞
1.12.1 Tx Origin 依赖漏洞原理
1.12.2 Tx Origin 依赖漏洞防守
1.13 访问控制不当漏洞
1.13.1 访问控制不当漏洞原理
1.13.2 访问控制不当漏洞防守
1.14 签名重放漏洞
1.14.1 签名重放漏洞原理
1.14.2 签名重放漏洞防范
2 智能合约漏洞检测方法
2.1 形式化验证
2.2 符号执行
2.3 静态分析
2.4 污点分析
2.5 模糊测试
3 智能合约实验分析
3.1 检测工具对常见漏洞检测情况分析
3.2 5种工具检测 BEC 溢出漏洞
3.3 ContractGuard、Mythril、链安 VaaS 三个工具实验对比
4 结语
4.1 扩展形式化验证的应用范围
4.2 提取重点路径，缩短路径空间
4.3 改进现有的模糊测试工具
4.4 完善智能合约漏洞库，建立漏洞挖掘工具效率评价方法
引言
1994年计算机科学家、加密大师尼克·萨博 (Nick Szabo) 提出“智能合约 (Smart contract)” 的定义为：“一个智能合约是一套数字形式定义的承诺，包括合约的参与方可以在上面执行这些承诺的协议。”他描述了自动售货机在物理设定下，将产品直接给付过款的用户的场景， 认为可以使用计算机代码代替机械设备来完成更为复杂的交易。
然而当时缺少可信的执行环境，缺乏支持可编程合约的数字系统和技术，智能合约并未被应用于实际产业中。直到区块链技术的兴起使得该问题得以解决，区块链不仅能够支持可编程合约，并具有去中心化、不可篡改、过程透明、可追踪等优势，为智能合约提供了一个完美的解决信任问题的机制。2013年底，Vitalik Buterin发布的以太坊白皮书《以太坊：下一代智能合约和去中心化应用平台》将智能合约引入了区块链，拓展了区块链在货币领域之外的应用，引领了区块链 2.0 时代的到来。
简而言之，智能合约是一份基于密码学这种高科技上面的数字化合同，与传统的纸质合同的差异就是：自动售货机相当于智能合约，售货员相当于纸质合同。智能合约程序代码规定了合约条款，包含一些触发条件，一旦满足触发条件合约便会自行执行。
1、智能合约的安全问题
1.1 重入漏洞
1.1.1 重入漏洞原理
以太网智能合约的重要特点之一就是调用和利用其他外部的合约。通常在合约中会发生一些将以太币发送给外部用户账户的行为，而转账和调用外部合约的操作需要智能合约的外部调用，若这些外部调用操作不慎，则极其容易被攻击者利用，通过回退函数或者回调攻击合约自身来进行攻击和一些不当操作，从而造成用户的损失。比如之前引起以太币市场剧烈波动的THE DAO被攻击事件就是这种漏洞极为典型的例子。可重入性通常表现为一个函数的同时多次调用，恶意合约在调用其他函数完成之前多次调用被攻击函数，在被攻击合约中“重新输入”了代码执行，从而实现攻击，这可能会造成巨大的破坏。
1.1.2 重入漏洞场景
如表1所示简单实现了存款和取款的操作。用户可以进行存钱，合约会记录每个用户的存款额度，同时用户可以通过 withdraw 函数取出自己的存款。这段代码似乎在逻辑上没有漏洞，但是问题出现在第 9 行，在进行存款回收转账时的 call.value() 函数上。以太坊中 send() 和transfer() 函数只有 2300gas 处理转账操作，call. value() 函数会将合约剩余的所有 gas 全部用于外部调用。若转币时目标地址是一个合约，那么会自动调用合约中的 fallback 函数，若攻击者在部署一个恶意递归调用转账操作的合约，则会将公共钱包合约里的余额全部提出来，对被攻击合约造成巨大损失。
1.1.3 重入漏洞防守
为了避免重入漏洞的产生，在进行转账操作时，应该注意以下 3 点：
（1）尽量使用 send()、transfer() 函数。
（2）如果使用像 call() 函数这样的低级调用函数时，应该先执行内部状态的更改，然后再使用低级调用函数。
（3）编写智能合约时尽量避免外部合约的调用。
1.2 整数溢出漏洞
1.2.1 整数溢出漏洞原理
在合约中，一个整型变量只能有一定范围的数字表示区间。比如 uint8 只能存储范围在 0 到255 的数字，若尝试存储 256 则会上溢导致错误存储为 0，同样 (uint8)0-1 将导致下溢被错误存储为 (uint8)255。这是因为以太坊虚拟机为整数指定了固定的大小，当在操作数据时超出了数据范围会出现溢出错误或 gas 不足，这会使得攻击者有机会滥用代码并创建不合理的逻辑流程。
1.2.2 整数溢出场景
如表 2 所示第 7 行存在一个明显的溢出漏洞，该代码段中的 withdraw() 函数实现的功能为：当账户余额大于取款金额时，就给该账户转入对应的取款金额，然后修改账户余额。因为 uint256 的存储范围在 0 到 2^256-1 的数字，当账户余额小于取款金额时，会发生整数下溢，从而产生一个较大的数值，满足第 7 行的条件，从而可以取出大于账户余额的金额，因此利用该漏洞，攻击者可以存入很少的金额，但能够取出大于存入的金额。
1.2.3 整数溢出漏洞防守
编写智能合约代码时，在进行所有算术运算时，可以注意以下两点：
（1）可以在算术逻辑前后进行验证；
（2）可以直接使用由 OpenZeppelin 建立SafeMath 库来处理算术运算逻辑。
1.3 拒绝服务攻击漏洞
1.3.1 拒绝服务攻击漏洞原理
拒绝服务攻击即 DOS，通常是使得原来的代码逻辑无法运行，导致以太币和 gas 的消耗，使得合约无法正常运行。
1.3.2 拒绝服务攻击漏洞场景
产生拒绝服务攻击漏洞的主要有以下 3 种方式：
（1）一些细微的智能合约编码方式或逻辑都极有可能被攻击者利用造成 DOS 攻击。触发报错操作，从而中止合约服务。
（2）另一种容易造成 DOS 漏洞的情况是将代码控制权集中在某一个变量上，这极易造成某一个用户的控制权垄断，当其不活动或者出现丢失密钥的情况下，会造成整个智能合约的瘫痪，无法继续运行。
（3）还有一种 DOS 漏洞出现在数组循环中，因为在以太坊中的每个区块的 gas limit 是有上限的，攻击者通过外部操控数组，使得 gas 枯竭，造成合约中的交易无法继续运行。
1.3.3 拒绝服务攻击漏洞防守
在第一个和第二个出现漏洞的情况中，可以引入时间机制，允许用户在一定时间内完成操作。要考虑到用户操作失败的情况，若超时或操作失败时则采用一定的策略来让合约继续运行下去，而不是被锁在失败的地方。
在出现漏洞的第三种情况中，最好采用 pull 而不是 push 机制，让每个用户自己去 pull 自己的资产，而不是通过循环一个极易被外部操纵的数据结构去分别 push。
1.4 未检查 call 调用返回值漏洞
1.4.1 未检查 call 返回值漏洞原理
Solidity 的消息调用函数中，send() 函数和底层调用函数 call()、Delegatecall()，callcode() 发生异常时，只返回 false，而不会抛出异常，因此在进行外部调用时，若未对函数的返回值进行检查，即使被调用的合约抛出异常，只会返回false，交易将会继续执行，可能会导致合约中出现逻辑错误。
1.4.2 未检查 call 返回值漏洞场景
如表 3 所示的代码段中的第 7 行中通过调用 send() 函数进行转账操作，如果该操作发生异常，交易会继续执行，即会进行第 9 步操作， 从而会导致合约中出现逻辑错误。
1.4.3 未检查 call 返回值漏洞防守
在智能合约的编写中，最好将外部的发送功能与智能合约内部的其他功能进行分离，采取 pull 模式，让用户自己去调用撤销的操作，而不是合约主动去向外部发送。这样可以让用户独立处理失败后的后果，从而不会导致智能合约的错误运行。
尽可能在转账操作中使用 transfer() 函数替换 send() 函数。同时在每次调用之后都要检查返回值以便及时处理可能存在的错误。
1.5 短地址/参数攻击漏洞
1.5.1 短地址/参数攻击漏洞原理
短地址/参数攻击主要出现在基于ERC20类型的代币合约中，在 EVM 层面中，交易的消息输入由一串16进制的字节码组成，该字节码分为三部分：方法名哈希值占 4 个字节、交易目标地址占 32 个字节、转账金额占 32 个字节。在调用 ERC20 代币合约中的转发代币函数时，如果没有对账户地址长度进行输入验证，可能会导致传送给智能合约转账函数的参数异常，从而导致转账金额会出现错误，从而攻击者可以极易盗取代币中的交易账户的代币金额。
1.5.2 短地址 / 参数攻击漏洞防守
通过了解该漏洞的具体内容，该问题较容易避免，只需在客户端开发时，确保对用户的输入数据进行有效性检查。
1.6 危险的 Delegatecall 漏洞
1.6.1 危险的 Delegatecall 漏洞原理
Delegatecall 操作是消息调用有一个特殊的变种，它与消息调用相同，不同之处在于目标地址上的代码是在调用合约的上下文中执行的，并且msg.sender 和msg.value 的值也会保持不变。这意味着合约可以在运行时从其他地址动态加载代码，这样可以通过这种“库合约函数”来实现对代码的复用。但是这种新特性也存在一些问题，当“库合约函数”即被调用函数中的状态变量发生改变时，相应的会修改调用函数中的变量，从而会产生一系列的问题。
1.6.2 危险的 Delegatecall 漏洞防守
谨慎使用 Delegatecall，并且确保不要调用不受信任的合约。如果目标地址需要用户输入，需要根据受信任合约的白名单来检查目标地址。
1.7 时间戳依赖漏洞
1.7.1 时间戳依赖漏洞原理
当智能合约使用区块时间戳作为执行关键操作（例如发送以太币）的条件的一部分或是作为产生随机数的熵源时，会产生时间戳依赖漏洞。在像区块链这样的分布式系统中，矿工可以在短时间间隔（小于900秒）内自由设置区块的时间戳。但是，如果基于时间戳的合约传输以太币，攻击者可以根据操纵区块时间戳来利用此漏洞。
1.7.2 时间戳依赖漏洞防守
开发人员在编写智能合约时，应当意识到区块时间戳和实际时间戳是可以有一定的差异的，并且区块时间戳可以被人为控制，因此可以考虑使用外部源作为时间戳来源。
1.8 以太币冻结漏洞
1.8.1 以太币冻结漏洞原理
如果合约可以接收以太币并且也可以通过Delegatecall 调用其他合约中的转账函数发送以太币，但是合约本身却没有转账功能，则该合约可能会产生以太币冻结漏洞，因为如果提供转账功能的合约执行 suicide 或 self-destruct 操作销毁该合约时，通过 Delegatecall 调用转账函数的合约就可能出现以太币被冻结的情况。
1.8.2 以太币冻结漏洞防守
如果一个合约通过在函数中添加“payable” 关键字来接收以太币，则必须至少提供一个将以太币发送出去的函数，如使用call()、send()、transfer() 等函数，否则，必须从合约函数中删除所有“payable”关键字。
1.9 无气发送漏洞
1.9.1 无气发送漏洞原理
无气发送漏洞是由于使用 send() 函数时，调用接收方合约的回退函数，并且会消耗固定的gas 值（gas 为回退函数中的变量值）。通常，回退函数的 gas 限制为 2300。因此，如果接收方合约中的回退函数中有复杂的操作需消耗大量的 gas，则以太币的发送方将会得到一个 out- of-gas 异常。如果不适当地检查和传播此类异常，恶意发送者可能会不当地收到以太币。
1.9.2 无气发送漏洞防守
因为 transfer() 函数如果出现异常会导致转账失败，抛出异常，所以建议在进行转账操作时， 用 transfer() 函数代替 send() 函数。
1.10 交易顺序依赖漏洞
1.10.1 交易顺序依赖漏洞原理
一个区块包含一组交易，因此区块链状态在每个纪元中会更新几次。如果存在这样一个场景：区块链处于状态 σ，新区块包括两个调用同一合约的交易（例如，Ti、Tj）。在这样的场景中，用户在执行各自的调用时不确定合约处于哪个状态。因此，用户可能要调用的合约状态与相应执行时的实际状态之间存在差异，只有矿工才能决定这些事务的顺序，从而决定更新的顺序。因此，合约的最终状态取决于矿工如何命令调用它的事务。我们称这种合约为交易顺序依赖（或 TOD）合约。如果有并发调用，即使对合约的良性调用也可能会给用户带来意外的结果。此外，攻击者可以利用 TOD 合约获取更多利润，甚至窃取用户的资金。
1.10.2 交易顺序依赖漏洞防守
为了避免交易顺序依赖漏洞，可以使用哈希存储提交的信息，哈希中存储编号、账户地址、问题的正确答案。通过提交哈希值信息，判断两个交易的哈希值是否匹配，如果匹配，则合约账户会给提交正确答案的账户所得的奖励金额。
1.11 区块变量依赖漏洞
1.11.1 区块变量依赖漏洞原理
基于区块链的应用中有很多场景都需要产生随机数，在官方不提供直接访问随机数的背景下，公共链上的开发人员根据可使用的各种区块变量独立开发伪随机数生成器（简称“PRNG”），而这些伪随机数生成器严重依赖于block. number、block.coinbase、block.difficulty、block. gaslimit、block.timestamp 等区块变量，矿工可以通过操控这些区块变量使生成的随机数变得可预测。
1.11.2 区块变量依赖漏洞防守
为了避免区块变量依赖漏洞，应避免依赖区块变量来产生随机数，尽量通过 Oracles 使用外部随机源，例如可以通过 Oraclize 第三方服务来生成随机数。
1.12 Tx Origin 依赖漏洞
1.12.1 Tx Origin 依赖漏洞原理
Tx.Origin 和 msg.sender 是 solidity 中的全局变量，Tx.Origin 返回原始发送交易的账户地址、msg.sender 是当前的直接的消息发送者。如果通过 Tx.Origin 变量授权的账户调用恶意合约，则可能会使该合约易受攻击，因为 Tx.Origin 返回的是原始发送者的地址，即授权账户的地址，因此可以通过授权账户向攻击账户进行转账。
1.12.2 Tx Origin 依赖漏洞防守
为了避免 Tx.Origin Dependency 漏洞，尽量使用 msg.sender 代替 Tx.Origin。
1.13 访问控制不当漏洞
1.13.1 访问控制不当漏洞原理
Solidity 语言对函数的 4 种可见性修饰分别为：public、internal、private、external。如果在编写智能合约时没有指定可见性修饰符，则函数默认可见性为 public；如果转账等重要函数缺少访问控制或访问控制不足，恶意方则可以从合约账户中提取部分或全部以太币。同时，智能合约中的构造函数会执行一些初始化等关键操作，如果错误地命名构造函数，则该函数就会成为普通函数，并且任何人都可以调用它来重新初始化，会产生严重损失。
1.13.2 访问控制不当漏洞防守
为了避免访问控制不当漏洞，需做到以下两点：
（1）因为 Remix 编译器规范了构造函数的写法，因此需要按照该规范编写构造函数。
（2）为函数添加正确的可见性修饰符， 并对一些重要的转账操作进行严格的权限检查。
1.14 签名重放漏洞
1.14.1 签名重放漏洞原理
有些智能合约会通过交易的签名信息进行交易的有效性验证，但假如合约的签名验证过程不够严谨，会导致签名信息被重复利用。例如，对于这样一个场景：A 账户有两种数字资产TokenX 和 TokenY，这两种数字资产都可以通过A 账户的签名信息转移 A 账户的数字资产到 B 账户，其核心代码片段如表 4 所示：
假如 A 账户希望转给 B 账户一笔 TokenX， 需要告诉 B 那笔转账交易的签名信息（_value, _ fee, _v, _s, _r), B 账户然后利用其签名信息调用transferProxy, 从而转移A 账户中的TokenX 到B， 而对于这样的签名信息，在区块链上是可以被公开获取的，这样这些签名信息可以同样被应用到 TokenY 合约的转账代码，从而在没有被 A 明确授权的情况下，B 账户获得了同样数量的TokenY。
1.14.2 签名重放漏洞防范
（1）尽量避免使用和 transferProxy() 类似的功能。
（2）确保当前签名信息只能在本合约中使用一次，例如在keccak256() 函数中添加当前合约地址 address(this)。
2、智能合约漏洞检测方法
2.1 形式化验证
形式化验证是用逻辑语言对智能合约文档和代码进行形式化建模，通过严密的数学推理逻辑和证明，检查合约的功能正确性和安全属性。对于规模相对较小而设计复杂的智能合约而言，形式化程序验证无疑是保证其安全可靠的有效方法之一。形式化验证包括模型检验和定理证明。模型检验是列举出系统所有可能的状态并逐一进行检验，这种方法全自动化却只适用于小型系统；而定理证明首先把系统代码提取成抽象的数学模型，然后对定理进行证明，这种方法能够适应大规模系统，但需要将系统的运作方式转换成验证系统能够理解的语言。
2.2 符号执行
符号执行将程序变量的值表示为输入符号值的符号表达式。每个符号路径都有一个路径条件，该条件是通过累加这些输入必须满足的约束来建立符号输入上的公式，以便执行该路径。如果路径条件不可满足，则路径是不可行的。否则，这条路是可行的。符号执行包括动态分析和静态分析。
借助符号执行检测智能合约漏洞的一般过程为：首先按需将智能合约中不确定值的变量符号化，然后逐条解释执行程序中的指令，在解释执行过程中更新执行状态、搜集路径约束， 并在分支节点处做 fork 执行，以完成程序中所
有可执行路径的探索，发现安全问题。约束求解技术能够对符号执行中搜集的路径约束进行求解，判断路径是否可达，并在特定的程序点上检测变量的取值是否符合程序安全的规定或者可能满足漏洞存在的条件。
2.3 静态分析
静态分析检测智能合约漏洞的主要过程为：首先分析合约的源代码或编译的合约的反汇编码。然后，将合约代码转换为内部表示来分析和检测合约中的漏洞。
slither 是一个静态分析框架，该框架具有四个功能：自动漏洞检测、自动优化检测、代码理解、辅助代码评审。slither 以 Solidity 编译器从合约源代码生成的 Solidity 抽象语法树（AST） 作为初始输入。
2.4 污点分析
污点分析是对污点变量的数据流分析。污点分析的过程是：首先识别智能合约中污点信息的产生点并标记；然后根据实际需要和污点传播规则分析前后向的数据依赖关系，得到数据依赖和污点依赖的指令集，检查一些关键的程序点，关键操作是否受到污染信息的影响。
Mythril是用于 EVM 字节码的安全分析工具。Mythril 集成了混合符号执行、污点分析和控制流检查，可以检测出大部分常见的安全漏洞，但无法检测出智能合约的业务逻辑问题，且极易产生误报。
2.5 模糊测试
模糊测试是一种安全测试方法，它将无效或随机的输入注入到程序中，以获得意外行为并识别错误和潜在漏洞。符号测试相对于其他漏洞检测方法，其主要特点就是简单、高效，只需通过生成测试用例动态执行合约代码，就可以检测出合约中的漏洞，并且有利于检测出合约中更深层的漏洞，同时误报率很低。
3、智能合约实验分析
3.1 检测工具对常见漏洞检测情况分析
针对常见的 15 种漏洞，链安 VaaS 可以检测出 12 种漏洞、洛飞可以检测出 9 种漏洞、oyente 可以检测出 6 种漏洞、slither 可以检测出 8 种漏洞、Mythril 可以检测出 11 种漏洞、ContractGuard 可以检测出 10 种漏洞，由此可知：
（1）目前常见的工具 中，链安 VaaS、Mythril 和 ContractGuard 对常见的漏洞检测的效果较好，oyente 检测的漏洞类型较少。
（2）常见的工具大多数支持 Reentrancy、Danger、 Delegatecall、Uncheck call return value、Integer overflow/underflow、TX.Origin Dependency、Timestamp Dependency、Block Gas Limit 这7 种漏洞。
（3）目前 Gasless Send、Freezing Ether、Unexpected Ether Balance、短地址 / 参数攻击、Transaction Order Dependency 这 5 种漏洞大部分工具是无法检测的， 其中Gasless Send 漏洞只有 Contract Guard 可以检测，Transaction Order Dependency 漏洞只有 oyente 可以检测，因此可以考虑给现有的工具添加以上几种漏洞。
3.2 5 种工具检测 BEC 溢出漏洞
针对BEC溢出漏洞，利用链安 VaaS、Mythril、ContractGuard、oyente、slither 检测的情况如表 5 所示：
由表 5 分析可知：
（1）slither 工具无法检测出该漏洞，其余四个工具均可检测出该漏洞。
（2）因为链安 VaaS 工具使用的是形式化验证的方法，因此该工具无法生成测试用例， Mythril、oyente、ContractGuard 三个工具因为使用需要动态执行合约代码，因此可以生成相应的测试用例，生成的漏洞测试用例可便于之后更深入的研究，同时，ContractGuard 工具生成的漏洞测试用例中，可以计算出payable函数所接收到的以太币的值。
（3）ContractGuard 在检测该漏洞时，不会产生误报，其余三个工具的检测结果中都会出现误报，同时 Mythril 工具的检测时间最长，大约需要 5 分钟左右。
3.3 ContractGuard、Mythril、链安 VaaS 三个工具实验对比
根据 swc 和 secbit 实验室整理的 2018 年的buggy contracts，整理出了 200 个测试合约，通过检测，三者可以共同检测的漏洞类型有 8 种，共 150 个错误，ContractGuard 命中 137 个， 误报 3 个、Mythril 命中 124 个，误报 31 个、链安VaaS 命中 144 个，误报 26 个。
如图 1 所示，ContractGuard、Mythril、链安 VaaS 的检测精度分别为91.3%、82.7%、96%。如图2 所示，三个工具的误报率分别为 2.1%、20%、16.3%。
图 1 三个工具的命中率
图 2 三个工具的误报率
其中 , 命中率和误报率的计算公式为：
命中率 = 命中个数 / 总问题个数
误报率 = 误报个数 / ( 误报个数 + 命中个数 )
三个工具对 150 个检测项的具体检测情况
如表 6 所示：
4、结语
4.1 扩展形式化验证的应用范围
对于目前学术界颇为关注的形式化验证方法，用数学推演来验证复杂系统，安全有效但难度很高。未来的研究应针对不同的业务目标定制对应的验证规范描述，突破成本昂贵、不适应大规模合约等技术限制，并扩展形式化验证的应用范围，从验证一般功能属性和安全属性、检测常见漏洞到逐步实现经济学、博弈论范畴中复杂业务逻辑及公平性等高阶性质的证明。
4.2 提取重点路径，缩短路径空间
基于攻击者目标是非法窃取加密货币的假设，结合现有智能合约审计经验和已曝漏洞分析，寻找智能合约中易产生漏洞的高危指令，如 SUICIDE、CALL、ORIGIN、ASSERT_FAIL 等，定义涉及这些操作码的路径为重点路径。为了提高漏洞挖掘效率，实践中不必对所有可能的执行路径进行检查，仅符号执行关注的重点路径并进行漏洞验证，可以有效地缩减路径空间。
4.3 改进现有的模糊测试工具
首先可以改进现有的模糊测试工具中测试用例生成算法，例如可以考虑用多目标优化算法，同时，可以结合其他检测方法提高检测效率，可以采用静态方法、符号执行、模糊测试三者相结合的策略，可以使用静态方法分析并提取关键路径，然后使用符号执行，生成种子测试用例，输入到模糊测试种，从而可以极大地提高模糊测试的效率。
4.4 完善智能合约漏洞库，建立漏洞挖掘工具效率评价方法
当前关于智能合约的测试尚未有标准的案例集，因此，为了验证智能合约漏洞挖掘工具的有效性，同时给智能合约的安全开发提供参考，下一步工作需要根据已爆发的安全事件以及合约审计经验，总结归纳出涵盖类型完善的智能合约漏洞库。综合考虑漏报率、误报率、检测时间、支持漏洞类型和漏洞的危害等级等因素，建立漏洞挖掘工具效率的综合评价指标， 将市面上的相关工具进行对比分析，验证其有效性，并为新工具的研发和改进提供指导。
作者简介
郑忠斌（1979—），男，硕士，高级工程师，主要研究方向为移动通信、无线接入和设备网络管理等；
王朝栋（1981—），男，硕士，主要研究方向为网络与信息安全战略规划、政策标准制定、技术产业开发；
蔡佳浩（1996—），男，上海大学硕士在读，主要研究方向为窄带物联网的性能分析。
选自《信息安全与通信保密》2020年第七期（为便于排版，已省去原文参考文献）
声明：本文来自信息安全与通信保密杂志社，版权归作者所有。文章内容仅代表作者独立观点，不代表安全内参立场，转载目的在于传递更多信息。如有侵权，请联系 anquanneican@163.com。
