智能合约的形式化验证工具

胡凯教授

在智能合约的形式化验证过程中，总是需要专业的编程人员对不同模板的智能合约进行特征分析、模型建立和模型验证。然而，未来使用智能合约的必然不会全都是会编写模型的人员，因此，我们在智能合约和模型检测技术原理的基础上提出一套智能合约辅助用户工具SCAVT。通过抽象出智能合约的基本性质和组件描述，比如多个合约方对合约中时间节点、合约关键条款、合约触发条件等重要合约内容的认定，以及合约方对合约附加条件的说明和合约的签署等，建立合约自动生成机制，包括开发智能合约通用模板、定制需求模板、自由组合模板等形式，用户只需要在模板相应位置填写参数，降低人工工作量。在未来的智能合约场景能加速其大规模应用部署。

1、智能合约通用验证框架

智能合约的全生命周期活动包括：合约的建立、协商与提交，合约的执行，还有合约的审计。为了支持合约的可观察性与可验证性，合约本身与合约执行的所有状态都应该作为证据存储在一个安全度高的数据库中。基于智能合约的特性并结合对智能合约形式化验证方法的研究，可以概括和总结出对智能合约通用的合约验证框架，如图1所示。智能合约的验证过程分为三个阶段：合约签订、合约建模，以及合约验证三部分。

图1智能合约通用验证框架

其中，合约签订是整个合约验证过程的基础和前提条件，合约签订过程包括多个合约方对合约中时间节点、合约关键条款、合约触发条件等重要合约内容的认定，以及合约方对合约附加条件的说明和合约的签署。

其次，合约建模是整个合约验证过程中最核心和最重要的过程，包括合约文本预处理和生成合约模型。为了便于合约模型的编写，设计和实现一个可自动生成合约模型的 工具 是非常有必要的，方便用户在签订合约之后，可以通过工具自动生成可执行的合约模型代码。为此，工具对用户签订的智能合约需要先进行预处理，并且规定合约的转换规则，通过对合约文本中关键字的提取，对应合约的转换规则，实现智能合约模型的自动生成。用户可以在不需要手动建模的前提下，在模型检测工具中运行智能合约模型，实现合约模型的快速验证。

最后，合约验证是合约验证框架中最后的一步。合约模型在选定的模型检测工具中运行，在合约模型的基础上，还需要对合约的属性进行约束。使用LTL、CTL或者其他公式对合约的属性进行约定，在合约运行验证的过程中，模型检测工具会通过判定合约的功能属性和非功能属性是否满足约定来确定智能合约模型是否是正确的。但是，往往模型检测工具的使用者都需要专业领域的知识，因此，为便于用户对合约模型的验证结果做出判断，我们还需要对合约验证结果进行处理后，才能将合约模型的验证结果直观的呈现给用户。

2、智能合约用户辅助工具

该辅助工具的开发以SPIN模型验证工具为基础，SPIN工具以进程为单位进行检测，智能合约以合约方为基础进行交互，二者具有很契合的对应关系。并且为了方便工具的扩展，智能合约模板到模型描述语言的转换之间，加入了模板描述到中间语言和中间语言到智能合约模型描述语言之间的转换。基于SCAVT辅助工具的需求，设计智能合约用户辅助工具的流程图如图2所示

图2 智能合约用户辅助工具流程图

基于合约验证辅助工具的功能需求和流程图，辅助工具划分为如下功能模块：编写合约模板模块、组合合约模板模块、合约模板转换合约模型模块，以及合约模型验证反馈模块

1）基础合约模块：此模块是合约辅助工具的基础模块，用于实现基础合约模板的编写和预处理，对基础合约模板按照一定的规则进行分类管理，并且设计友好的用户编辑合约界面。

2）复杂合约模块：此模块是基于基础模块设计的，这一模块的功能是为了增加用户使用合约模板的自由度。用户可以选择基础合约自由组合成复杂合约，在转换的时候，基础合约的组合必须满足一定的规则，例如，组合的合约必须是有意义的，且基础合约之间存在一定的逻辑关系。在组合完成之后，实现对复杂合约的模板管理，并设计友好的用户界面。

3）合约转换模型模块：此模块基于上一个模块的输出，实现智能合约模板向基于PROMELA的智能合约模型的转换。此模块是工具中最重要，也是最核心的一个模块。对基础合约模板和复杂合约模板进行预处理，通过关键字的提取和识别，将智能合约转换成中间文件。然后，再将按照约定规则生成的中间文件转换成SPIN可以处理的PROMELA智能合约模型，生成可执行文件。生成的模型检测可执行文件可以在SPIN中进行检测和验证，并对验证过程生成可解析文档。

4）模型验证反馈模块：此模块是合约验证辅助工具的最后一个模块。通过对合约模型验证结果文档的预处理和解析，生成简单的、自然语言描述的信息反馈给用户，以便于用户直观的理解合约验证结果。

以用户定制复杂合约为例，用户可以选择和填写的合约模板。用户可以自由组合工具内嵌的基础模板，组合并生成复杂合约模板，如图3所示，用户可以选择需要组合的合约模板，然后通过填写组合合约模板的参数信息，生成新的智能合约。经工具判定合约有效后，工具会对新的智能合约生成合约的PROMELA模型。

图3 合约模板组合界面

基于智能合约的PROMELA模型，通过使用assert语句、end标签和progress标签，实现智能合约基础性质的检测；通过消息通道，验证智能合约进程之间的信息交互是否正确，实现智能合约基础功能的检测；通过使用LTL描述智能合约的其他特定属性，验证给定场景的智能合约模型是否满足特定的属性要求。通过迭代验证，得到正确的和高可靠性的智能合约。如图4所示为合约对应生成的PROMELA合约模型。生成的PROMELA编写的智能合约模型，可以在模型检测器SPIN中进行模型的性质检测。

图4 工具自动生成PROMELA合约模型

用户都可以通过此工具完成智能合约的模板定制、合约签订到生成合约验证模型的完整过程。极大的节省了用户的编程开销，同时携带形式化验证的方法有效提高了用户编写合约的可靠性，改工具已初步实用化。

北京航空航天大学分布式实验室

北京航空航天大学分布式技术实验室具有悠久历史传承，是国内最早的分布式技术和形式化方法研究和应用的专业实验室，上世纪八十年代起就开始承担航空电子等各类军民两用分布式系统研制，先后承担国家基金、863重大、核高基等国家重点工程项目，获多项国家科技成果奖。在分布式处理、高性能计算、嵌入式、FPGA设计等方面国内领先。主编了国内分布式计算权威教材《分布式计算系统导论》，是国内区块链和智能合约技术早期研究单位，智能合约工程（SCE）和验证即服务（VaaS）等概念和理论方法的提出者。实验室与法国INRIA成立了形式化方法联合研究实验室，推动区块链和智能合约形式化验证方法和工具的应用。多年来潜心研究自有知识产权区块链底层技术，已拥有全系列区块链产品和工具，先后完成中国移动、国家网络应急中心、国家电网、金融领域等国内重要区块链应用落地项目，获得国家发明专利和软件著作权30余项。形成了科学研究与人才培养相结合，理论研究与应用系统研发协调发展的学科发展格局。

来源：北京航空航天大学分布式实验室--胡 凯

本文由布洛克专栏作者发布，不代表布洛克观点，版权归作者所有

——TheEnd——

关注“布洛克科技”