构造形式化证明，解决智能合约安全问题——你的合约亟待证明

SECBIT实验室 安比技术社区 2018-07-07 19:07

安比（SECBIT）实验室与 Consensys 中国、轻信科技等团队联手，在智能合约安全的形式化证明领域开展深度合作。

智能合约安全问题始终是萦绕在区块链的各个项目方、开发者和投资者心头的一颗定时炸弹。越来越多的安全团队积极参与，试图通过更完备手段来解决合约安全问题。安比（SECBIT）实验室认为，形式化验证与传统的“测试+审计”方式相结合，将会是保证智能合约安全强有力的手段。

7月7日，安比（SECBIT）实验室联合 ConsenSys 正式发布 ERC20 合约的形式化证明源码。该合约代码来源于 ConsenSys 官方提供的 ERC20 合约模板，形式化证明代码已上传至 Github 仓库（tokenlibs-with-proofs），地址如下：

https://github.com/sec-bit/tokenlibs-with-proofs

ConsenSys 官方源码地址：

https://github.com/ConsenSys/Tokens/blob/master/contracts/eip20

我们针对 ERC20 合约常见问题和特性展开了证明，证明性质分为以下几个部分

  • 漏洞溢出

  • 合约中 Token 总量

  • 转账操作对任意账户的影响

我们希望以本项目为切入点，展示形式化验证是如何应用到智能合约领域的，进而帮助更多的技术人员学习或参与到智能合约的形式化验证中。

我们也希望利用形式化证明，剔除漏洞合约，为大家筛选出更多较为安全的合约模板。

同时，安比实验室也将致力于使用形式化验证的方法，从业务实现，技术安全和经济学等维度，构建更加可信安全的智能合约。

什么是形式化验证？

下面是来自维基百科的一个形式化验证的定义：

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.

The verification of these systems is done by providing a formal proof on an abstract mathematical model of the system, the correspondence between the mathematical model and the nature of the system being otherwise known by construction. Examples of mathematical objects often used to model systems are: finite state machines, labelled transition systems, Petri nets, vector addition systems, timed automata, hybrid automata, process algebra, formal semantics of programming languages such as operational semantics, denotational semantics, axiomatic semantics and Hoare logic.

从上述定义，我们可以看到，形式化验证事实上包含了各种不同的验证理论技术。但是，万变不离其宗，形式化验证简单说就是一个基于数学模型的验证。验证的过程是为了保证这个数学模型满足一定的性质。

本文后面所采用的形式化验证理论技术，是将智能合约语言编写的代码作为数学模型，将智能合约所需要满足的要求作为性质进行证明。通俗的来讲，就是使用数学语言来描述合约代码，并证明其具有一些好的性质，例如不存在整数溢出漏洞。

更深一步讲，我们是通过形式化的程序逻辑(Program Logic)，来证明一个智能合约程序（Code）是否满足已给定的形式化规范（Formal Specification），然后，在规范的基础上，证明智能合约的行为始终满足一些高层性质（High-level Property），并且通过显式的证明（Proof Object）来使用户确信验证结果的正确性。

当我们在讨论任何形式化验证理论或者技术时，都绕不开下面三个关键点：

  1. 任何证明都是在一定的前提假设下的证明；

  2. 证明过程是依赖形式化逻辑理论的正确推理；

  3. 证明的最终结果（定理）是大家能够取得共识的结论；

安比实验室（SECBIT）所采用的形式化验证方法中，第一点需要保证一些基本的定义是正确的；第二点需要保证证明过程的合法性，这里我们采用流行的证明辅助工具 Coq 来表示证明和检查证明；第三点我们证明的结论正确表达了大家共同关心的 ERC20 性质。

注意：这三点内容是形式化证明的前提条件，是我们对保证合约安全的必须信任的前提条件，是智能合约形式化证明的信任基础（Trusted Computing Base）。任何安全都必须基于一定的信任基础，一个系统的信任基础越小，那么它就越安全。本文所采用的形式化证明方法将信任基础降到了最小集合。

智能合约为何需要形式化证明

以比特币为首的区块链技术将智能合约的构想落地，随之以太坊将智能合约发扬光大。以太坊将比特币交易中的脚本变成了一种通用的图灵完备的编程语言。（注：所谓图灵完备是指编程语言的表达能力得到了最大程度的释放），但是过于自由的以太坊智能合约编程语言也使智能合约会和传统软件一样，被无处不在的安全漏洞和Bug所困扰。自从以太坊正式上线以来，由于智能合约漏洞/缺陷所带来的经济损失数以亿记。

安比实验室目前已经对以太坊上所有部署的 Token 合约进行扫描，将已披露的合约漏洞与安全风险进行了全景分析，披露问题合约的总数量达到 4,172 个，其中被 CoinMarketCap 收录的合约数量达 101 个。问题合约列表被 ConsensysLabs 收录到推荐开发者工具列表中。

推荐开发者工具列表地址：

https://github.com/ConsenSysLabs/ethereum-developer-tools-list

安比实验室在审计过大量的智能合约之后，发现相比传统软件而言，智能合约的安全问题更加棘手，现实情况也更加严峻：

  1. 智能合约的可信度是来源于不可篡改性，以太坊的智能合约一旦部署上线后就无法再修改。一旦合约存在安全漏洞，任何人都可以发起攻击，并且在攻击发生后，假如合约没有一定的防御措施，将会无法阻止安全问题的进一步恶化。这无论是对合约本身的经济价值（如Token）还是公众对项目的信任，都会造成严重的损害。

  2. 智能合约部署上线后，一部分项目会公开合约源码。源码的公开一方面是增强用户对合约的信任度，但是另一方面也大幅度降低了黑客攻击的成本，代码中的任何一个小问题都有可能被黑客捕捉到并且加以利用。

  3. 智能合约开发过程涉及的问题更是方方面面，而智能合约发展时间比较短其本身还存在很多的不足；同时市面上专业的技术人员严重缺乏，无法避免人为因素引起的漏洞，因此稍有不慎就有可能留下致命的安全隐患。

目前针对智能合约安全问题的应对方式主要有两种：合约代码的测试和审计。这两种方式能够在一定程度上有效的规避大部分的安全问题，是保证合约安全的必要手段，但是同时也存在着一定的局限性。

  • 合约测试

    安全团队开发自动化测试工具，自动生成大量的测试用例执行合约来进行测试，检测在尽量多的条件下，合约是否能够正确执行。但由于测试用例无法保证100%覆盖所有的情况，所以，即使测试结果没有发现问题，也不能保证合约的实现一定没有漏洞。

  • 合约审计

    安全审计人员对合约源码从代码实现和业务逻辑等多个角度进行审计。安全团队通过专业的手段检查出大部分的合约漏洞和隐患，并在业务逻辑的实现上给与项目方指导或者建议。尽管安全审计可以发现并规避大部分常见的漏洞和风险，但由于审计工作在一定程度上依赖于审计人员的自身经验和主观判断，并不能100%完全杜绝安全风险和漏洞。

而形式化证明是通过形式化逻辑的方式来表示合约代码，并加以严格地推理证明。这个过程依赖于数学逻辑推理的严密性，保证 100% 覆盖到到代码的运行期行为，可以明确保证在一定范围内的绝对正确，能弥补以上两种传统方式的局限。因此形式化证明在一些安全攸关的领域，如航天、高铁、核电、航空，已经逐步得到应用，并且取得了非常好的效果。

而智能合约代码，同样也是对安全要求极高，一旦出现问题，造成的经济损失更是不可估量。另外一些较为复杂的业务逻辑以及更高阶的性质，如经济学，博弈论范畴的问题，通过测试或者审计的方式更是难以有效验证。因而对于规模相对较小而设计复杂的智能合约而言，形式化程序验证无疑是保证其安全可靠的有效方法之一。

如何为智能合约构造形式化证明

尽管形式化验证是保证智能合约安全极其有效的手段，但目前相关的研究还比较匮乏，也缺少相应的工具支撑。安比实验室发布了 ERC20 合约的形式化证明，一方面希望能够为大家筛选出一份安全的合约模板；另一方面也希望能够借此让更多的人了解并学习形式化验证，共同参与到智能合约的形式化验证领域中来。

证明结构

Token形式化证明大致可以分为四个部分：合约源码，代码规范，合约性质，证明。

Image

形式化验证需要按照形式化方法的步骤来实现。

  • 合约源码：Solidity 源码即我们要证明的代码

  • 代码规范：代码规范定义每一个合约函数的预期行为。

  • 合约性质：合约的性质是形式化证明最终需要保证的性质，如Token发行总量保持不变。

  • 证明：基于代码规范，对合约特定的性质进行证明。

到底证明了哪些性质

Token 合约主要包含以下几种性质的证明过程：

  • nat_nooverflow_dsl_nooverflow：transfer() 和 transferFrom() 操作不存在溢出漏洞

    Lemma nat_nooverflow_dsl_nooverflow:
      forall (m: state -> a2v) st env msg,
        (_from = _to \/ (_from <> _to /\ (m st _to <= MAX_UINT256 - _value)))%nat ->
        ((from == to) ||
         ((fun st env msg => m st (to st env msg)) <= max_uint256 - value))%dsl st env msg = otrue.

  • Property_totalSupply_equal_to_sum_balances：在合约中，任意执行完成一步后，合约中 totalSupply 的值与所有账户的余额的总和相等

    (* Prop #1: total supply is equal to sum of balances *)
    Theorem Property_totalSupply_equal_to_sum_balances :
    forall env0 env msg ml C E C' E',
      create env0 msg C E
      -> env_step env0 env
      -> run env C ml C' E'
      -> Sum (st_balances (w_st C')) (st_totalSupply (w_st C')).

  • Property_totalSupply_fixed_transfer : 合约执行完成 transfer() 转账操作以后，token 总量不变

    (* Prop #2: total supply is fixed with transfer *)
    Theorem Property_totalSupply_fixed_transfer:
    forall env C C' E'  msg to v spec preP evP postP,
      spec = funcspec_transfer to v (w_a C) env msg
      -> preP = spec_require spec
      -> evP = spec_events spec
      -> postP = spec_trans spec
      -> preP (w_st C) /\ evP (w_st C) E' /\ postP (w_st C) (w_st C')
      -> (st_totalSupply (w_st C)) =  (st_totalSupply (w_st C')).

  • Property_totalSupply_fixed_after_initialization : 合约初始化完成后，token 总量不变

    (* Prop #3: total supply is fixed after initialization *)
    Theorem Property_totalSupply_fixed_after_initialization:
    forall env0 env msg C E C' E',
      create env0 msg C E
      -> step env C msg C' E'
      -> (st_totalSupply (w_st C)) =  (st_totalSupply (w_st C')).

  • Property_totalSupply_fixed_delegate_transfer ： 合约执行完成 transferFrom() 转账操作以后，token 总量不变

    (* Prop #4: total supply is fixed with delegate transfer *)
    Theorem Property_totalSupply_fixed_delegate_transfer1:
     forall env C C' E' from  msg to v spec,
      spec = funcspec_transferFrom_1 from to v (w_a C) env msg
      -> (spec_require spec) (w_st C) /\ (spec_events spec) (w_st C) E' /\ (spec_trans spec) (w_st C) (w_st C')
      -> (st_totalSupply (w_st C)) =  (st_totalSupply (w_st C')).

    Theorem Property_totalSupply_fixed_delegate_transfer2:
     forall env C C' E' from  msg to v spec,
      spec = funcspec_transferFrom_2 from to v (w_a C) env msg
      -> (spec_require spec) (w_st C) /\ (spec_events spec) (w_st C) E' /\ (spec_trans spec) (w_st C) (w_st C')
      -> (st_totalSupply (w_st C)) =  (st_totalSupply (w_st C')).

  • Property_from_to_balances_change : 转账操作后，合约中仅余额转出和转入的账户发生改变，其它账户不变

    (* Prop #5: only balances of from and to changed by transfer*)
    Theorem Property_from_to_balances_change_only:
    forall env C C' E' to addr msg v spec,
      spec = funcspec_transfer to v (w_a C) env msg
      -> (spec_require spec) (w_st C) /\
         (spec_events spec) (w_st C) E' /\
         (spec_trans spec) (w_st C) (w_st C')
      -> m_sender msg <> to
      -> m_sender msg <> addr
      -> to <> addr
      -> (st_balances (w_st C') to = (st_balances (w_st C) to) + v)
         /\ (st_balances (w_st C') (m_sender msg) = (st_balances (w_st C) (m_sender msg)) - v)
         /\ st_balances (w_st C') addr = st_balances (w_st C) addr.

证明过程简述

  1. 合约solidity源码

    ERC20 的合约代码，为标准的 ERC20 合约。包含六个函数：构造函数，transfer()，transferFrom()，balanceOf()，approve()，allowance()。

  2. 合约规范

    A specification language is a formal language in computer science used during systems analysis, requirements analysis and systems design to describe a system at a much higher level than a programming language, which is used to produce the executable code for a system.

    Spec.v 文件中定义了 ERC20 合约的六个函数的规范。

    每个函数的执行都可能涉及多种情况，函数在一类情况下的行为可以通过一条规则描述，所以通常函数的规范由一条或者多条规则组成。以 transferFrom() 函数的规范的为例，它由两条规则 funspec_transferFrom_1 和 funcspec_transferFrom_2 组成，分别对应允许转账额度小于 2**256-1 和等于 2**256-1 的情况。

    以 funcspec_transferFrom_1 为例，每条规范规则由以下几个部分组成。

    • spec_require 定义了在该类情况下执行该函数前必需满足的条件：

      Image

    • spec_events 定义了函数成功执行所产生的所有事件：

      Image

      其中，

      • ev_Transfer 对应 Transfer 事件；

      • ev_return 是一个伪事件，用于标记函数的返回以及返回值。

    • spec_trans 定义了函数成功执行对合约状态的改变，例如哪些 storage 变量发生的改变：Image

      • 即，balances 和 allowed 的相应项发生了预期的变化，而其它 storage variable 保持不变。

  3. 证明合约满足规范

    证明高层性质的过程是基于以上定义的规范完成的，但在性质证明之前，我们需要保证 Solidity 源码本身需满足我们定义的规范。首先我们要将合约的 Solidity 实现表示在 Coq 中。为此我们在 Coq 中实现了一个 Domain Specific Language (DSL)，用于在 Coq 中表示 Solidity 代码。例如 ERC20 中的 transfer() 的实现在 DSL.v 中被表示成如下形式：

    Image

    然后，我们需要证明以 DSL 表示的各个合约函数满足对应的合约规范。例如，transfer() 满足规范 funcspec_transfer 可由 DSL.v 中的如下引理证明：

    Image

  4. 高层性质的定义和证明

    上述规范描述了合约中单个函数的单次执行的行为。高层性质描述的是合约作为一个整体，在接受任意的 message call 的情况下，仍然具备的性质。例如 Prop.v 中定义的 ERC20 中所有账户不会存在 token 丢失，个账户 token 总量始终和总发行量一致 的性质：

    Image

  5. 包括该性质在内的所有高层性质的详细定义和证明过程，请参见 Spec.v。

未来的计划

与传统的安全问题不同，智能合约的安全问题危害更严重，波及范围更广，造成的经济损失更大。形式化验证无疑是解决智能合约安全问题的一把利剑。

在一定的边界条件内，形式化验证可以保证代码的绝对安全可信，根本上杜绝了某一类漏洞问题。本仓库对以ERC20 token 合约的几个简单性质为例，初步介绍了形式化验证如何应用在智能合约领域，但仅此还不足以突显形式化验证的巨大价值。但随着智能合约应用范围的扩大，业务逻辑复杂度进一步增加，更甚者当涉及更深层次的经济学，博弈论问题，借助于形式化验证背后完备的数学理论和哲学思想，加以验证和证明，必将带来更多的惊喜。

尽管形式化证明是保证智能合约安全极其有效的手段，但目前国内这一领域专业人才较少，相关的研究还比较匮乏，也缺少相应的工具支撑。安比（SECBIT）实验室成员依托形式化验证领域十余年的研究经验，致力于把该项技术更广泛应用于智能合约安全。

  • 我们将会证明更多的通用性质，规避常见漏洞和风险

  • 我们将证明功能更加丰富的 Token 合约，如冻结、升级、权限管理、增加控制等。

  • 我们将研究如何证明一些博弈论相关的高层性质，如公平性，最优策略与纳什均衡等。

同时我们更希望越来越多的技术爱好者可以参与进来，共同为形式化验证和智能合约的发展贡献一份力量。如果有任何问题或者想法，欢迎加入我们的 Gitter 进行讨论。

Gitter地址: https://gitter.im/sec-bit/Lobby

致谢：特别感谢 Yi Tang（consensys中国），Yuhui Wu（轻信科技）和 Zhong Zhuang（dex.top）等人对本文提出了宝贵的建议

参考文献

  • [1] DSLs for Ethereum Contracts https://www.michaelburge.us/2018/05/15/ethereum-chess-engine.html

  • [2] Formal verification https://en.wikipedia.org/wiki/Formal_verification

  • [3] Domain-specific language https://en.wikipedia.org/wiki/Domain-specific_language

  • [4] 安⽐（SECBIT）实验室携⼿路印（Loopring）共同发布智能合约风险列表 https://mp.weixin.qq.com/s/XbXlrmt0fi9IgxicmdAF0w

  • [5]【推荐】王健：说说形式化验证（Formal Verification）吧 http://chainb.com/?P=Cont&id=1957

  • [6] C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 26(1):53-56, Jan. 1983.

  • [7] L. Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering SE-3, 2 (March 1977), 125-143.

  • [8] G. Necula. Proof-carrying code. In Proc.24th ACM symposium on Principles of programming languages (POPL’97). pages 106-119, New York, Jan. 1997.

  • [9] Inria: The Coq Proof Assistant. https://coq.inria.fr/

  • [10] Cadar, C., Dunbar, D., Engler, D.R., et al.: Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI. Volume 8. (2008) 209–224

  • [11] Gaudel, M.C.: Testing from formal specifications, a generic approach. In: International Conference on Reliable Software Technologies, Springer (2001) 35–48

  • [12] Nielson, F., Nielson, H.R., Hankin, C.: Principles of program analysis. Springer (2015)

  • [13] Gaudel, M.C.: Testing from formal specifications, a generic approach. In: International Conference on Reliable Software Technologies, Springer (2001) 35–48

  • [14] Inria: The Gallina specification language. https://coq.inria.fr/distrib/current/refman/language/gallina-specification-language.html

  • [15] 基于逻辑的形式化验证方法:进展及应用  http://xbna.pku.edu.cn/html/2016-2-363.htm

合作交流请联系info@secbit.io。

安比（SECBIT）实验室


安比（SECBIT）实验室专注于区块链与智能合约安全问题，全方位监控智能合约安全漏洞、提供专业合约安全审计服务，在智能合约安全技术上开展全方位深入研究，致力于参与共建共识、可信、有序的区块链经济体。


安比（SECBIT）实验室创始人郭宇，中国科学技术大学博士、耶鲁大学访问学者、曾任中科大副教授，后担任知名金融科技公司副总裁。专注于形式化证明与系统软件研究领域十余年，具有丰富的金融安全产品研发经验，是国内早期关注并研究比特币与区块链技术的科研人员之一。研究专长：区块链技术、形式化验证、程序语言理论、操作系统内核。


SECBIT技术社区

info@secbit.io

Image


Modified on 2018-09-10

Scan to Follow