26在线检测ECF对象的智能合约应用
26.1引用
Shelly Grossman , Ittai Abraham , Guy Golan-Gueta , Yan Michalevsky , Noam Rinetzky , Mooly Sagiv , Yoni Zohar, Online detection of effectively callback free objects with applications to smart contracts, Proceedings of the ACM on Programming Languages, v.2 n.POPL, January 2018 [doi>10.1145/3158136]
26.2介绍
本文的主题是实现封装状态的对象的正确性的模块化推理。这是受Ethereum平台的启发，这些平台在基于区块链的分布式账本的基础上，促进了智能合约的执行。Ethereum智能合约中的一个关键特征是缺少全局可变共享状态，这与常见的标准编程环境(如C和Java)形成了对比。智能合约类似于具有封装状态的对象。
然而，Ethereum区块链和许多其他动态环境使用回调实现事件驱动编程。这些回调对于功能来说是必要的，但是可能会损害安全性。例如，DAO合约中的著名bug被人加以利用回调，被窃取1.5亿美元。
我们的实验可以被概括为：
我们为对象(sECF)和执行(dECF)定义了一个称为ECF的通用安全属性。我们的定义受到区块链环境的启发，但它也可能适用于其他具有封装状态的环境，比如微服务。
结果表明，在满足ECF的前提下，采用模块化推理方法可以很好地验证具有封装数据的对象
基于冲突等价的ECF概念更加强大，能够在实际环境中有效地验证dECF，并且sECF可用于具有有限状态和无界堆栈的程序。
在一个以太坊客户端建立了一个多项式时间和空间算法的在线检查dECF和原型实现作为动态监测dECF
对Ethereum区块链(包括主分支和经典分支，请参见第9节)整个历史上算法的评估。根据这个结果，可以推断，在实践中，大多数Non-ECF执行都对应于错误的执行。我们还展示了我们的监视器有一个非常小的运行时开销。通过对可用历史运行dECF 监视器，我们能够证明它在防止利用DAO中的漏洞方面的有效性，更重要的是，在其他应用程序中利用它的可行性，例如，简化模块化合约验证。 26.3综述
这一部分提供了一些必要的概念和我们的方法的综述。
26.3.1DAO漏洞
图26-1显示了演示dao中的漏洞的伪代码。合约为每个对象存储一个信用，以及当前余额。信贷代表每个项目的个人投资。为了符合以太坊的术语，用信用和余额表示的货币单位称为以太。合同保持不变的表示形式，其中贷方总额等于当前余额，即
图26-1 说明DAO bug的合约。恶意合约的回调可能违反表示不变式。第2.5行修复了错误
图26-2 使用DAO对象的正常和恶意客户机
该合同提供了两种操纵国家的方法:存款用于存款，取款用于提取特定对象的所有可用资金。
图26-2a显示了一个简单的客户机，演示了DAO对象的预期用法。
图26-3 说明对DAO的攻击的调用的回溯。节点由局部更改状态标记，边缘由操作和原始回溯中相应的顺序标记。D表示DAO, G表示一个好的客户机，a是一个攻击者对象。w表示取款操作，p表示支付操作。b是余额的简写，c是贷方的简写，s是停止的简写。
图26-4 调用的两个回溯说明了对DAO的ECF版本的一次失败攻击的原始版本和无回调版本。
26.3.2Effectively Callback Free合约
原则上，可以使用半自动程序验证和抽象解释来验证攻击者对象中是否存在恶意攻击。然而，这需要对整个代码进行推理。本文通过探索模块化，提出了一种不同的解决方案。 这个想法是要求合同中有更强的条件，这样就根本不需要对其他对象进行推理。
具体来说，我们定义了effectively callback free对象(ECF)的概念。我们的定义受到区块链合约的启发，但适用于在其他具有本地状态的环境中强制模块化。
我们说，具有初始状态s0和最终状态s的对象的执行是dECF，当存在“等效的”不回调合约执行时，它以相同的初始状态s0开始，并达到最终状态s。
26.3.3在线ECF检测
通过记录回溯并在执行结束时通过枚举所有可能的排列检查ECF属性，可以以一种简单的方式检查执行是否为ECF。然而，这在空间和时间上都是昂贵的，因为排列的数量随着回溯的大小呈指数增长。特别是，很难看到这样的解决方案是否可以集成到虚拟机中。
为了得到一个可行的在线算法，我们检验了一个比ECF更强的要求，这是受数据库事务冲突串行性的启发。其主要思想是探索操作的可交换性，以便有效地在线检查保证无回调回溯结果与原始回溯处于相同状态的正确性条件。
我们将此算法集成到EVM (Ethereum虚拟机)中，并将其应用于区块链中所有可用的执行。结果总结在第26.10节。它们表明，绝大多数Non-ECF执行来自错误的合同。它们还表明，我们的检测的运行时开销是可以忽略的。从这些令人鼓舞的结果中，我们得出结论，如果ECF检查是Ethereum协议的一部分，就可以防止DAO中的漏洞被利用。它显然受益于Ethereum这样的环境，Ethereum处理敏感的金融事务，而且代码几乎不可能升级。
26.3.4识别ECF合约
我们还研究了在编译时验证合约是ECF (sECF属性)的可能性。一般来说，这是无法判定的，比如solidity语言。然而，我们证明了对于有限局部状态的合约，检查ECF是可判定的。这个结果很重要，因为模型允许无限制的堆栈长度。所设计的决策过程提供了关于在实践中检查ECF的其他技术的见解。
图26-5 语法
26.3 验证ECF合约的属性
在本文中，我们证明了关于ECF合约的推理可以以模块化的方式执行。ECF合约的本地可达状态只受合约代码的影响，不能被外部合约更改。
这对于程序验证和程序分析非常有用，将外部调用视为可能返回任意值但不能更改本地状态的非确定性操作。我们使用Dafny [Leino 2010]来使用这个属性来验证图1中修改后的DAO对象的正确性(包括第2.5行，不包括第5行)。在第7节中，我们将更深入地讨论如何使用Dafny验证这个示例。
26.4 编程语言
26.4.1语法
图26-5定义了语法SMAC.我们假设有限语法域 k ∈ Cnt,f 属于 Fld, 并且 x∈ Var 合约定义，名称和变量定义。 一个合约 K游一个合约定义器k,并且包括一个序列的定义 f和一个无名称的方法。这个合约由一系列变量定义
和命令C ∈Cmd. C也许是一个原始定义 c ∈ PCmd 或者一个复合命令，比如一个循环等。一个原始定义 c ∈PCmd 也许可以是一个表达式e的任务到一个本地变量x,一个本地变量x的值到一个域F(F:=x),一个域F到本地变量x（x:=F),或一个潜入命令（assert(b)),一个用单一参数e对合约方法的调用,用x存储返回值（x:=o(e)）或者一个skip命令。.每个合约都有一个单独的方法，因此没有指定方法的名称，可以使用它们的合约名称来引用它们。
在不损失通用性的前提下，我们假定没有两个合约包含具有相同名称的字段。在下面，我们可以互换使用术语合约和对象。
图26-6 语义域
图26-7 具有上下文的操作语义
26.4.2语义
26.5等效执行
我们定义了两个关于给定(任意)对象o的运行等价(完整执行序列)的概念:最终状态等价和冲突等价。
26.5.1最终状态等价
26.5.2对象冲突等价
冲突。两个原始命令a和a’,表示为Conflict(a, a ‘)，如果这两个访问相同的字段，并且至少其中一个访问是写。
注意事项4.3 回想一下，我们假设对象状态由整数类型的数据成员(字段)组成;因此，可以从它们执行的(语法)基本命令中检测它们访问的堆位置。此外，请记住，不同的对象包含不同的字段，并且一个对象不能直接访问另一个对象的字段;因此，如果两个基本命令冲突，那么它们必须由同一个活动对象执行。
模块化的格式良好的执行。我们将格式良好的执行的定义扩展为模块格式良好的执行，它允许替换方法调用导致的子迭代x ：=o ′(e)通过任意值赋给x。我们将这种(隐含的)转换称为破坏性转换。直观地说，严重破坏转换允许安全地过度估计对象o在调用对象o‘上的方法时可能观察到的惟一效果。
定义 4.4. 过度转换，是一个状态对s ⟨s,s ′ ⟩ ∈ State × State，s = ⟨(o, x B o ′ (e), ρ) · Γ, σ⟩ 并且 s ′ = ⟨(o, done, ρ[res → n]) · Γ, σ⟩对于任何值 o,o’,e,ρ, Γ, σ 和 n。
定义 4.5 模块化结构良好的执行是一个有限序列的转换来自Tr比如对于任何连续转换τ1τ2，它包含最大的状态τ1和源状态τ2。通过符号的滥用,我们使用π表示模块化格式良好的执行。一系列转换π是一个完整的模块化结构良好的运行,如果它是模块化的格式良好的,第一个和最后一个状态是静止的。此外，如果所有其他状态都处于活动状态，则此类运行是完全模块化的、格式良好的执行。
定义 4.6。假设π是一个执行，程序执行π在o上，表示为π |o，是π的子序列，由激活对象为o的转换构成
引理 4.7 对于任何执行π和对象o,它表示为T (π |o ) = T (π)|o .
命题 4.8 让κ ⊢ π是一个模块化的格式良好的执行,所有转换都有相同的活动对象o。然后，有一个上下文k’，比如κ ′ (o) = κ(o)并且一个执行κ ′ ⊢ π ′，T (π)是一个T (π ′ )的子序列并且κ ′ ⊢ π ′是完备定义的。
最后，给出了对象o的执行冲突等价性的定义。
定义 4.9 κ1 ⊢ π1 和 κ2 ⊢ π2 是模块化的完备定义的运行，并且T1 = T (π1 |o )和T2 = T (π2 |o )是他们分别的回溯。o. κ1 ⊢ π1 和 κ2 ⊢ π2是对象冲突等价，对于对象o，表示为
，如果：
26.6正确性条件
一般来说，ECFc需要找到一个无回调的执行，它与使用回调的执行是冲突的。冲突等价要求无回调执行的回溯是原始执行回溯的置换。因此，从对执行的合法排列的特征描述开始是有用的。首先，这种排列可能不会破坏合约代码的程序顺序。也就是说,排列必须保留的排序事件的转换是相同的一部分调用π,和他们的状态有相同的深度(π)。其次，我们希望允许将回调调用从其原始调用位置移除的排列，并将它们设置为在静态状态下执行，同时仍然接收模块形式良好的执行。
当我们对一个回溯进行置换，使回调调用从原来的位置删除时，我们将导致回调的调用转换替换为破坏性转换。图8中可以看到一个示例，它显示了一个回溯的所有合法排列，该回溯具有无回调执行和严重转换。
注意事项 5.2 混乱的转换不是排列回溯的一部分;它只是用来证明执行不再像我们前面定义的那样格式良好。
26.7可判定性
图26-9 两个对象A和B的代码表明是不可判定的，一个图表显示了系统可能的流程
图26-10 自动化Ao和的构造，由符号-->到表示一个命令在代码o被另一个替换
引理 6.2 o是一个对象，假设a是一个有限域对于变量来说，然后有一个算法可以决定o是否是
引理 6.3 用表示所有执行的集合。有一个M的自动机π ∈ Π，在接收状态时结束，如果π≠，否则会进入拒绝状态。
图26-11 M的代码来接收π的一次的执行并且辨别是否是
推论 6.4 检查是否所有的执行是是可判定的。
引理 6.5 一个对象o是如果所有的的执行都是
由推论6.4和引理6.5可以直接得到以下结果:
定理 6.6 设o是一个对象，假设变量有一个有限域。然后有一个算法决定是否o是。
26.8对象级别分析
虽然ECF属性能够检测不满足它的不需要的执行，但它还可以进一步用于对象的模块化分析。我们将说明，在封装对象的环境中，我们可以只考虑执行单个对象的ECF，以帮助简化对象级别的分析。
定理 7.1 设R为处于静止状态的对象o的所有状态的集合，设R0为MGCo运行时对象o的所有状态的集合。如果o是，那么。
明显的是，这个定理认如果为对象o的所有的状态的集合的是，那么它同样是。
这种分析并不是太不精确，因为在真实的环境中，比如Ethereum，我们可以模拟这样的行为。这尤其正确，因为在Ethereum中对象的存储是可更新的，并且可以向系统添加新对象。
26.9动态鉴别
我们描述了一个动态验证属性的良好过程。更准确地说，对于每个执行，如果只属于该对象(投影执行)的转换的子序s列是，那么它将检查参与执行的每个对象。我们假设存在实现第3节中定义的语义的解释器或虚拟机。下面是算法使用的数据结构的描述，以及对象代码维护这些数据结构的工具。然后我们给出了算法的高级描述，接着是伪代码和复杂度分析。我们使用图26-1中overview部分中的示例来解释这个过程。
26.9.1数据结构
段是一种数据结构，它捕获关于部分执行状态的元数据。这部分由一系列相邻的转换组成，它们的顶层堆栈帧具有相同的活动对象。也就是说，对不同对象的调用标志着新段的开始，以及从调用返回到调用者调用，调用者调用在不同对象的上下文中执行。
例 8.1 1. 在第2节的DAO合约示例中，攻击执行由6个部分组成:(1)第一次调用withdrawAll，第1-3行;(2)调用pay，第3-5行;(3)第二次调用withdrawAll，第1-3行;(4)完全调用pay，第3-4行，第7行;(5)withdrawAll第二次调用，第5行;(6)withdrawAll的第一次调用，第5行;
定义 8.2(段) 段t表示与同一对象相关的相邻转换的最大序列。段t = (R,W,D, Idx)包含在段中访问的字段的信息，分别表示读写集的R(t)和W (t)。此外，一个段包含关于调用深度的信息(表示为D(t))，它等于转换状态的深度。最后，执行中的索引(表示Idx(t))严格按照段的创建顺序递增。
例 8.3 我们在执行攻击的概览示例中，按照执行时出现的顺序，写下了与DAO对象相关的片段:
执行可以表示为线段的线性序列。此外，我们可以从这些段确定执行包含的调用。
注意事项 8.4 段可以用作执行和调用的另一种表示，它泛化由一系列转换保存的数据。仅在本节中，我们将重新定义执行和调用的概念，以引用段而不是转换。
定义 8.5 (执行、调用和回调)。执行可以使用序列代表的检测段π= (......)。我们可以访问的段执行使用。我们通常有Idx() = j.调用是段I = (，…，)，从而有一个数字d，所有下列条件都适用。
（1）
（2）
（3）
（4）
由于调用中包含的所有段都具有相同的深度d，因此我们用D (I) = d表示调用的深度。我们说一个调用I是一个其他调用I’的回调，如果
注意事项 8.6 与第3节中对调用的定义不同，这里的调用只捕获与第一个转换深度相同的转换，而不是更高深度的转换。这允许为调用I定义D(I)。
例 8.7 在第2节中介绍的攻击执行中，第一次调用withdrawAll是,并且第二次调用是是一个回调：
我们将深度> 1中的每个段与调用者之前或分别进行调用的所有段的前缀集和后缀集关联起来:
定义 8.8 (前缀和后缀段)。让一组表示调用的段，和一个单独的段，其中并且。通过将I中的段划分为执行时索引小于回调段tcb索引的段(前缀)和执行时索引大于回调段tcb索引的段(后缀)，我们为定义了相对于调用者I的前缀和后缀集：
例 8.9 和对的前缀和后缀段为:
插桩过程创建段和调用。我们在图12中显示了插桩过程的伪代码。
定义 8.10 (交换段)。段t1和t2交互,用t1⇄t2,如果:
如果段t1和段t2不交互，我们用t1⇄t2表示。
例 8.11 在第2节中给出的攻击执行中，确实有t2 ⇄t1，即。同样，t3 t1由于credit[o]，即，因此也是t2⇄ t4。然而，t3确实与t4: t3 ⇄t4交互。
26.9.2算法
我们从算法的高级描述开始。每次系统达到静止状态时调用该算法，执行最后一次完整的执行。该算法生成一个调用关系，该关系定义了不同堆栈深度中调用顺序的约束，类似于[Lamport 1978]关系。我们将这种关系命名为调用顺序约束(IOC)图。例如，如果回调调用的一个分段没有与其调用调用，之后我们添加约束,调用者的调用必须发生在回调之前：。因此，调用的IOC关系定义为:
图26-12 检测过程，实现为按调用命令调用的钩子、返回命令和对象变量读/写访问命令。生成执行(它是段列表)和调用(调用标识符到保持调用调用方的调用对象的映射)，以及在相同深度中属于调用的段列表。顶级调用被标识为 TopInvocation
例 8.12 第2节中攻击执行的IOC关系可以通过示例8.9和8.11中给出的前面的元数据轻松计算出来。我们有
，并且对于
。同样，
。
定义IOC关系后，算法考虑该关系所生成的图，并检查其是否没有循环。例如，如果存在回调调用和包含回调调用的调用者调用，则图中可能出现一个循环，对于这两个调用者，都有(1)段不使用其前缀与调用者进行交换;(2)不以其后缀相对于调用者进行交换的段。由于图中的每个顶点都表示调用，拓扑排序返回调用的顺序，即ECFc。我们只关心是否存在这样的拓扑排序，即IOC关系是否不包含循环。
定理 8.13 让π是一个执行,让Inv是调用的段的map。我们表示为
，如果没有循环，那么
。
例 8.14 继续我们运行的例子，很明显，在DAO对象上执行攻击的IOC关系有一个循环:
。因此该算法不能确定攻击执行的是ECFc。但实际上，攻击执行不是ECF，因此不能是ECFc。
26.9.3完整性
26.9.3.1 时间
插桩步骤向运行时添加了一个常量工作因子。为了分析算法，我们首先看预处理步骤。让n表示调用的数量和m片段的数目(n
添加新手交流群：币种分析、每日早晚盘分析
添加助理微信，一对一亲自指导：YoYo8abc
