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

北京航空航天大学分布式实验室 北航云南创新研究院 白晓敏，段张博

在智能合约的形式化验证过程中，总是需要专业的编程人员对不同模板的智能合约进行特征分析、模型建立和模型验证。然而，未来使用智能合约的必然不会全都是会编写模型的人员，因此，我们在智能合约和模型检测技术原理的基础上提出一套智能合约辅助用户工具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合约模型

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

—-

编译者/作者：北航云南数字经济

玩币族申明：玩币族作为开放的资讯翻译/分享平台，所提供的所有资讯仅代表作者个人观点，与玩币族平台立场无关，且不构成任何投资理财建议。文章版权归原作者所有。