智能合约的形式化描述、分析和验证

摘要
目前数字经济正在向可编程经济时代演进，智能合约对可编程经济起着重要的推动作用，但其应用却面临着种种问题。随着平台级应用的普遍化，智能合约涉及的金额呈指数级别增长，如果其代码存在漏洞，则可能会遭到攻击，造成巨额损失，为防止类似事件发生，提出了运用形式化方法提高智能合约的安全系数的方法。

一、智能合约简介
智能合约（smart contract）这个术语至少可以追溯到1995年，是由多产的跨领域法律学者尼克·萨博（Nick Szabo）提出来的。他在发表在自己的网站的几篇文章中提到了智能合约的理念。他的定义如下：
“一个智能合约是一套以数字形式定义的承诺（promises），包括合约参与方可以在上面执行这些承诺的协议。”
尼克萨博指出计算机代码可以代替机械设备，进行更复杂的数字财产交易，未来的某一天，这些程序甚至可能取代处理某些特定金融交易的律师和银行，
“ 智能财产可以将智能合约内置到物理实体的方式，被创造出来”。比如，房屋出租商将发现智能合约这种用途很有吸引力，一所房屋的门锁，能由被连接到物联网上的智能合约打开，所有门锁都是连接互联网的。当你为租房进行了一笔交易时，存储在智能手机中的钥匙可以为你打开房屋，并进行自动资金转移。虽然智能合约仍然处于初始阶段，但是其潜力显而易见，因为它把人与法律协议以及网络之间复杂的关系程序化了。
智能合约理念几乎与互联网(world wide web)同时出现，从本质上讲，这些自动合约的工作原理是一种旨在以信息化方式传播、验证或执行合同的计算机协议。允许在没有第三方的情况下进行可信交易，这些交易可追踪且不可逆转。当一个预先编好的条件被触发时，智能合约执行相应的合同条款。智能合约的基本理念是，许多合约条款能够嵌入到硬件和软件中。
在计算机上进行智能合约实际应用时，需要控制实物资产保证有效地执行合约，同时做到在执行合约条款时，能获取到的第三方审核的合约方的信息。总的来说，一个智能合约是一套以数字形式定义的承诺，包括合约参与方可以在上面执行这些承诺的协议。它是能够自动执行合约条款的计算机程序，被部署在分享的、复制的账本上，它可以维持自己的状态，控制自己的资产和对接收到的外界信息或者资产进行回应。承诺指的是合约参与方同意的权利与义务，这些承诺定义了合约的本质和目的。数字形式意味着合约不得不写入计算机可读的代码中。只要参与方达成协议，智能合约建立的权利和义务，是由一台计算机或者计算机网络执行完成的。协议是技术实现，在此基础上，合约承诺被实现，或者合约承诺实现被记录下来。

二、智能合约现状
2016年6月17日，运行在以太坊公有链上的The DAO[1]智能合约遭遇攻击，该合约筹集的公众款项不断被一个函数的递归调用转向它的子合约，涉及总额 300多万以太币，这是一起严重的智能合约被攻击事件。The DAO本质上是个VC（风险投资基金），通过以太坊筹集到的资金会锁定在智能合约中，没有哪个人能够单独动用这笔钱。事件是The DAO智能合约本身的脚本漏洞被利用所引发。因此，智能合约的安全、可信问题引起大家的关注，如何编写具有高可靠性、高安全性的智能合约成为目前亟待解决的问题。
所以，智能合约的生成和执行还存在一些问题，包括：
1）智能合约对保证资产的安全性提出了更高的要求，合约需要验证合约逻辑属性的正确性，重要的是能够自动生成可信的可执行合约代码以节省成本并提高效率；
2）智能合约最终会取代合约文本，因此我们必须保证合约文本与合约代码的一致性。基于上述问题，本文提出将形式化方法应用于智能合约的整个生命周期。

三、形式化方法的引入
形式化方法[2] 是指用数学方法描述和推理基于计算机的系统，直观地说，就是规范语言＋形式推理，在技术上通过精确的数学手段和强大的分析工具得到支持，其表现形式通常有逻辑、离散数学、状态机等，规范语言包括语法、语义以及满足关系等，可以分为4类：抽象模型规范法、代数规范法、状态迁移规范法和公理规范法。形式化方法主要包括形式规约和形式化验证。形式规约使用具有精确语法和语义的形式语言刻画系统的行为和性质，是设计系统的约束和验证系统是否正确的依据；形式化验证则是在形式规约的基础上，建立系统行为及其性质的关系，从而验证系统是否满足期望的关键性质，主要包括模型检测和定理证明。
形式化方法[3] 是描述系统性质的基于数学的技术，用于计算机软件的规范、开发和验证。将形式化方法用于软件设计，是期望能够像其他工程学科一样，使用适当的数学分析以提高设计的可靠性和鲁棒性。其中，形式化方法中很重要的一步就是形式化验证，形式化验证可以以更正式的方式产生程序。例如，可以进行从规范到程序的属性或细化的证明。
近年来，模型驱动的设计与开发方法逐渐受到重视，并被工业界认为是切实可行的重要方法。该方法将模型作为整个系统开发过程的核心元素，在设计阶段就建立系统的体系结构模型，尽早进行验证和分析。同时，模型的重用以及基于模型转换的自动或半自动的逐步求精过程，都有助于降低系统开发时间和成本。然而，模型驱动的设计与开发方法的真正有效使用，需要多方面的支持。首先，需要合适的体系结构建模语言，并要求建模语言对系统的软/硬件结构、运行时环境、功能行为以及非功能属性可表达；其次，为满足系统的需求，形式验证与分析方法是重要的手段；最后，基于经过验证和分析的模型，研究自动代码生成技术，有助于避免手工编码带来的错误，可以进一步提高系统的质量属性。
将形式化方法应用于智能合约整个生命周期的流程包括合约设计、自然语言描述、形式化描述、模型验证、自动代码生成和一致性测试。本文重点探讨形式化描述和形式化验证可以更好地生成和执行智能合约。其中，形式化描述可以克服自然语言描述的缺点，例如二义性。形式化验证可以检查合约中是否存在逻辑错误。

四、形式化验证方法提高智能合约安全性
形式化验证与形式化规约之间具有紧密的联系，形式化验证就是验证已有的程序或系统是否满足其规约的要求，它也是形式化方法所要解决的核心问题。
传统的验证方法包括模拟和测试，它们都是通过实验的方法对系统进行查错。模拟和测试分别在系统抽象模型和实际系统上进行，一般的方法是在系统的某点给予输入，观察在另一点的输出，这些方法花费很大，而且由于实验所能涵盖的系统行为有限，很难找出所有潜在的错误。基于此，早期的形式验证主要研究如何使用数学方法，严格证明一个程序的正确性即程序验证。
目前常见的形式化验证方法主要可分为2类：演绎验证和模型检测。其中，早期的形式化技术主要采用演绎法证明顺序和并发程序正确性，而近期则多采用模型检测方法验证实时和混成系统。
1）演绎验证。演绎验证是早期采用的主要验证技术，它基于定理证明的基
本思想，采用逻辑公式描述系统及其性质，通过一些公理或推理规则来证明系统具有某些性质。
演绎验证的优点是可以使用归纳的方法来处理无限状态的问题，并且证明的中间步骤使用户对系统和被证明性质有更多的了解。缺点是现有的方法不能做到完全自动化，还需与用户交互，要求用户能提供验证中创造性最强部分的工作。因而演绎证明方法的效率较低，很难用于大系统的验证。
2）模型检测也即算法验证。模型检测是对有穷状态系统的一种形式化确认
方法，它基于状态搜索的基本思想，是模拟和测试方法的自然延伸，搜索的可穷尽性有赖于为合约建立有穷状态的模型，这为建模造成一定的难度，但能保证搜索过程终止。
模型检测方法的基本思想是通过状态空间搜索来确认合约是否具有某些性质。即给定一个合约（程序）P和规约Q，生成对应的合约模型Ｍ，然后证明规约公式Q在合约模型M中成立，这样就证明了合约（程序）P 满足规约Q。
将模型检测应用于智能合约以解决合约的可信问题，一般包括以下步骤：
1）建模。通过选择合适的建模语言和建模工具，使用模型检测工具能够接受的形式语言来描述合约。
2）描述。阐明所要验证的合约性质，包括合约的状态可达性、死锁、活锁、有界性等。
3）验证。对合约的状态空间进行搜索，发现合约存在的问题并及时修改，对合约进行迭代验证。
目前形式化描述技术主要分为２种类型：形式化描述模型和形式化描述语
言。通过形式化描述模型，可以获得抽象的合约模型。形式化描述语言总是基于一种或多种形式化描述模型。形式化描述技术已经有几十年的发展，目前有多种形式化描述模型和形式化描述语言。形式化描述语言主要有3种标准：CCITT国际电报电话咨询委员会组织制定的SDL，ISO组织制定的LOTOS和ESTELLE。
模型检测主要适用于有穷状态系统，早期主要用于硬件和协议的验证。
模型检测的优点是完全自动化并且验证速度快，即便是只给出了部分描述的合约，通过搜索也可以提供关于已知部分正确性的有用信息。尤其重要的是，在性质未被满足时，搜索终止可以给出反例，这种信息常常反映出合约设计中的细微失误，因而对于合约排错有极大的帮助。
形式化验证方法可以检查智能合约的很多属性，例如，合约的公平性、可达性、有界性、活锁、死锁、不可达以及无状态二义性等。

五、结论
本文针对智能合约存在的可信与安全问题，将形式化方法应用于智能合约的生命周期验证，从形式化描述和形式化验证方面进行了详细的阐述。一个好的模型检测工具有助于检査和验证智能合约的各项属性。智能合约可以在合约的不同阶段获得不同的状态，当智能合约验证时，SPIN可以随机产生若干种不同的结果。形式化方法可以在智能合约的建立、验证和代码生成中得到重要应用。

参考文献
[1]TheDAO[EB/OL].(2016-06-17)[2016-10-10].https://en.wikipedia.org/wiki/Decentralized_autonimous_organization.
[2]Kenneth M,Symmetry and model checking[J].Formal Methods in System Design,1996,9:105-131.
[3]Formal methods[EB/OL].2002[2016-10-10].http://en.wikipedia.orgi/Formal_methods.

智能合约的形式化描述、分析和验证相关推荐

成都链安重磅出品 | 基于VS Code插件的智能合约自动形式化验证工具Beosin—VaaS『离线免费版』...
11月4日,成都链安重磅推出『离线免费版』智能合约自动形式化验证工具Beosin-VaaS,该版本基于流行的开发工具VS Code插件,供广大开发者免费使用.获得方式如下,欢迎体验使用: https: ...
智能合约安全审计公司选型分析和审计报告资源下载---国内篇
国内影响力平台 2020年9月6日,区块链行业三家知名安全公司slowmist.PeckShield 和成都链安联合宣布完成对去中心化交易协议oneswap的全面安全审计.查看审计报告. 慢雾slow ...
构造形式化证明，解决智能合约安全问题——你的合约亟待证明
安比(SECBIT)实验室与 Consensys 中国.轻信科技等团队联手,在智能合约安全的形式化证明领域展开深度合作. 智能合约安全问题始终是萦绕在数字货币各个项目方.开发者和投资者心头的一颗定时炸 ...
这些智能合约漏洞，可能会影响你的账户安全！
摘要:区块链联盟链智能合约形式化验证揭秘,解释了我们为什么要对区块链上的智能合约进行形式化验证,以及形式化验证的分类和业界针对每种分类所推出的形式化验证工具,最后作者描述了一下目前形式化验证的种种方法 ...
【论文笔记04】Model-driven approach for the design of multi-chainsmart contracts—用于设计多链智能合约的模型驱动方法
A. Barišić, E. Zhu and F. Mallet, "Model-driven approach for the design of Multi-Chain Smart Co ...
区块链技术精华：四十种智能合约支持平台（三）
摘要: 智能合约是以数字形式定义的承诺,控制数字资产并涵盖合约参与者约定的权利和义务.它由计算机系统自动执行.在基于区块链的智能合约中,数据管理.事务验证和状态处理都是在区块链上完成的,区块链提供完备 ...
智能合约重构社会契约（5）比特犬模型实现智能合约
1. 设计思想针对法律.司法执法应用场景,将智能合约的许多问题简化, 在智能合约的自然语言处理.形式化方法.软件测试方面,突出智能合约的核心功能,降低使用智能合约的门槛,使其可靠且高效. 2.模型驱 ...
从并发视角来看智能合约（上）【渡鸦论文系列】
论文作者: Ilya Sergey1and Aquinas Hobor2 1 University College London, United Kingdomi.sergey@ucl.ac.uk 2 ...
智能合约自动检测工具『链必验』，如何带你解锁Web3.0世界
在我们发布[链必验]新版本之后,目前已有大批开发者前来试用,今天,我们还需要详细介绍这款工具. [链必验]智能合约自动检测工具,可用来检测区块链智能合约漏洞.平台针对每个用户模拟了一条单独的测试链,用 ...
12在以太坊上定义智能合约缺陷
原文标题: Defining Smart Contract Defects on Ethereum 原文作者: Jiachi Chen, Xin Xia, David Lo, John Grundy, ...

智能合约的形式化描述、分析和验证

智能合约的形式化描述、分析和验证相关推荐

最新文章

热门文章