[论文分享]Sailfish: Vetting Smart Contract State-Inconsistency Bugs

旗鱼：秒级审查智能合约的状态不一致缺陷

本文由来自UCSB的Priyanka Bose等作者发表于S&P ’22。文中提出了一种可扩展的状态不一致（State Inconsistency, SI）缺陷分析器，具体过程包括：一个轻量的探索阶段，可以有效降低分析的指令数，和一个精确化的阶段，使用了符号求解。文章检测两类缺陷：重入和顺序依赖。

Intro

智能合约的安全问题在工业和学术上都具有较高的关注度。这篇文章中作者关注集中在SI的检测上，这一类缺陷可能使攻击者有机会通过恶意修改交易顺序或单个交易中的控制流，进而操纵全局状态变量。现有分析这类缺陷缺陷的工作，有些过趋近于交易执行，而产生假阳性，或者有些会精细地枚举，并符号追踪整个合约，这让它很难适用于分析规模较大的多路径的程序。动态工具能比较好地扩展，但只适用在出现活跃攻击的时候。而且，现行工具采用的语法导向的模式匹配可能会漏报，因为支持的攻击模型有限。

作者认为设计SI静态分析器主要的难点在于：

1.单个智能合约对外提供的可进入的调用点比较多，而且允许外部调用任意方法、任意顺序、任意多次。而这些方法都有可能影响状态，而使分析更复杂。2.智能合约之间允许存在复杂的调用关系，这些跨合约调用可以被攻击者细心地设计穿插，而使得多次执行的结果更加复杂，分析难以拓展。

旗鱼使用了混合处理方式：

•EXPLORE：整个合约会被转换成一个储存依赖关系图（Storage dependency graph, SDG），图中会总结所有执行的读-写依赖。这些SI缺陷就可以通过对这个图进行访问来得到，缺陷对应SDG的子图。因为静态分析的过近似，这种方法可能会产生假阳性，旗鱼剪枝这些假阳的方法就是使用第二阶段REFINE。•REFINE：这里基于符号验证，传统符号执行可能会将储存变量初始化为’无限制的‘（unconstraint）。但这会使得很多不可行的路径减不掉。为了应对这个问题，作者使用了一种轻量的值汇总分析方法（value-summary analysis, VSA），作为符号执行的预先条件。

SI

这里给出对SI的定义：当一个进度（schedule）中的事件（events）在初始状态下执行，当执行结束时会进入一个新的状态。然后由于一些非确定性的因素存在，新状态不总是可以预估的。比如说，两个交易不能保证按照他们预计的顺序被处理，同时一个从合约内部发出的外部调用可能推翻原有的执行流程（比如通过任意的公开函数入口重入合约）。记没有发生任何上非确定性行为的schedule为H1，任意出现上述影响为H2。若H1和H2导致了不同的结束状态，即为这个合约存在SI。

Root cause of SI

SI发生的两个条件：

1.多个交易涉及了同一个储存状态2.叠加以下任意一种情况：

Stale Read(SR) 攻击者交易会使被攻击交易从存储中读一个旧值，同时被攻击交易的执行流还未来得及更新存储。 

Destructive Write(DW) 攻击者进程抢先写了储存，而被攻击进程还未来得及在执行流中读这块存储。

两个简易的例子来理解：

Design

Overview

Explorer

Figure 2 中的重入bug跨越了两个函数，攻击者可以利用两次访问splits[id]来实现双花攻击。Explorer找到的反例是：11->12->16->4->5。同样Figure 3 中的withdrawBalance可以和transfer组合作为一个跨函数的攻击。旗鱼检测第10行的写和19行的读有潜在风险。对应的反例是4..9->17..19，但是我们可以看到这些标记是不正确的，因为有mutex的保护，这里引入refiner。

Refiner

虽然反例中所讲的问题只覆盖了两个函数P1 P2，但分支条件可能会涉及一些其他函数，比如在重入中，攻击者可以在外部调用之后再调用其他的P*来修改其他状态变量。如Figure3，Refiner可以保守地认为mutex在第九行之后是没有限制的，因为这里缺少value summary，使得这个攻击可以实现。然而summary会告诉符号执行，所有可能的程序流都需要mutex被置为false。这种和预先条件相违背的程序状态，是不存在的，因此可以被剪枝。

Evaluation

RQ1.旗鱼的有效性 

RQ2.旗鱼的可扩展性 

RQ3 REFINER剪枝的能力

作者使用了Etherscan上的91k合约，其中去除编译器版本较老或不可用的，共89k参与了实验。

Bug finding

Manual determination

Analysis time

Abloation study

Ending

作者认为这个工作主要的限制在于

1.依赖源代码。事实上这个工作并不依赖丰富的语义，所以引入源码只是为了方便分析，而且作为定位面向开发者的工具，也是合理的。2.潜在的unsoundness。这里检测重入和TOD都没有soundness的保证，因为solidity本身并不是表达能力特别强的语言，所以异常传播，交易恢复，超出gas等都没有被建模。这也是Refiner并不能提供soundness保证的原因。同时由于call graph建立中的一些不精确的地方，也会影响旗鱼。

原文始发于微信公众号（COMPASS Lab）：[论文分享]Sailfish: Vetting Smart Contract State-Inconsistency Bugs