一种可更新的智能合约的动态验证方法

摘要

本发明公开了一种可更新的智能合约的动态验证方法。该可更新的智能合约的动态验证方法包括以下步骤，步骤S1：编译器接收一份智能合约源代码作为输入；步骤S2：编译器接收一份验证条件作为输入；步骤S3：编译器输出经修改后的安全智能合约。本发明的可更新的智能合约的动态验证方法具有准确率高、可大规模验证扩展等优点。

说明书

技术领域

本发明涉及区块链技术领域，具体涉及一种可更新的智能合约的动态验证方法。

背景技术

现有的智能合约动态验证作者设计了一种源代码到源代码的Solidity编译器——Solythesis，用来对智能合约进行运行时的高效动态验证，确保合约的安全性。编译器接受Solidity合约源码和不变式，输出修改后的合约，该合约将拒绝所有违反不变式的交易。编译器通过不变式指定的条件生成Solidity语句并插入代码，在执行时合约将检查是否满足不变式。

上述方法在智能合约中插入代码，并将修改后的智能合约部署上链后，将不能再修改，该方法是在链下解析不变式并将不变式对应的Solidity代码插入智能合约中，不能在智能合约运行时刻动态解析验证条件，传统的形式化验证方法存在适用范围小、求解速度慢的问题，且存在较多假阳性的情况，因此需要新的方法来对智能合约进行高准确率的、可扩展的大规模验证。

发明内容

本发明提供了一种可更新的智能合约的动态验证方法，旨在解决上述问题。

根据本申请实施例提供的一种可更新的智能合约的动态验证方法，包括以下步骤：

步骤S1：编译器接收一份智能合约源代码作为输入；

步骤S2：编译器接收一份验证条件作为输入；

步骤S3：编译器输出经修改后的安全智能合约。

优选地，所述编译器的运行步骤包括：

步骤S10：转换并储存验证条件；

步骤S11：植入验证解释器；

步骤S12：添加验证函数调用；

步骤S13：输出结果。

优选地，所述步骤S10包括：在输入的智能合约源代码中添加一个string类型的storage变量且名称为verification，将输入的验证条件语言转换为字节码格式，并存储在verification变量中；

在智能合约源代码中添加一个setVerification函数，该函数的输入参数是一个string类型的变量，函数内部将这个参数赋值给verification变量，用于从外部更新verification变量的值，并限制该函数只能由智能合约的创建者调用。

优选地，所述步骤S11包括：在智能合约源代码中添加一个check函数用于验证，所述check函数的输入参数为一个string类型的变量且名称为information，表示函数调用时的函数名、传入的参数、调用位置经编码后的结果，函数内部为验证条件语言的解释器，将会依次执行存储在verification变量的字节码中的指令。

优选地，所述步骤S12包括：对智能合约源代码进行分析，找出其所有的函数，并在函数的第一行和最后一行插入一个check函数的调用语句，将函数名、函数的多个参数、当前位置的三种信息进行编码，转换为一个string类型的值并传入check函数中。

优选地，所述步骤S13包括：将处理后的智能合约代码输出，输出的智能合约代码为安全的经过验证的智能合约。

本申请实施例提供的技术方案可以包括以下有益效果：本申请设计了一种可更新的智能合约的动态验证方法，本申请允许智能合约开发者在部署后修改智能合约的验证条件，确保使用该智能合约进行交易的安全性，解决了传统静态方法的假阳性问题，准确率更高，解决了传统形式化验证方法的适用代码规模小、验证速度慢的问题，可用于大规模的验证。

允许用户编写验证条件，以便对智能合约进行验证。验证条件可被更新，以便将来在Solidity编译器中发现新的bug后，合约开发者可以及时更新该验证条件，拒绝不安全的交易。解决了现有技术中，对于以太坊智能合约，现有方法无法应对Solidity编译器内部尚未被发现的bug，这些bug会导致编译出的字节码的程序语义与源代码的语义不同，一旦编译部署后，合约内部将隐藏着某些改变语义的bug。

用于验证的代码将和智能合约的原始源代码一起部署上链，形成经验证的安全智能合约，该安全智能合约将拒绝所有不满足验证的判定条件的交易，从而保护智能合约正常运行。本申请部署上链的智能合约能够向后兼容，相比没有使用本方法处理过的合约，不影响用户的正常使用。

附图说明

为了更清楚地说明本发明实施例技术方案，下面将对实施例描述中所需要使用的附图作简单地介绍，显而易见地，下面描述中的附图是本发明的一些实施例，对于本领域普通技术人员来讲，在不付出创造性劳动的前提下，还可以根据这些附图获得其他的附图。

图1是本发明可更新的智能合约的动态验证方法的流程示意图；

图2是本发明可更新的智能合约的动态验证方法的另一流程示意图；

图3是本发明可更新的智能合约的动态验证方法的另一流程示意图。

具体实施方式

下面将结合本发明实施例中的附图，对本发明实施例中的技术方案进行清楚、完整地描述，显然，所描述的实施例是本发明一部分实施例，而不是全部的实施例。基于本发明中的实施例，本领域普通技术人员在没有做出创造性劳动前提下所获得的所有其他实施例，都属于本发明保护的范围。

还应当理解，在此本发明说明书中所使用的术语仅仅是出于描述特定实施例的目的而并不意在限制本发明。如在本发明说明书和所附权利要求书中所使用的那样，除非上下文清楚地指明其它情况，否则单数形式的“一”、“一个”及“该”意在包括复数形式。

还应当进一步理解，在本发明说明书和所附权利要求书中使用的术语“和/或”是指相关联列出的项中的一个或多个的任何组合以及所有可能组合，并且包括这些组合。

请参阅图1和图2，本发明公开了一种可更新的智能合约的动态验证方法10，所述可更新的智能合约的动态验证方法10包括以下步骤：

步骤S1：编译器接收一份智能合约源代码作为输入；

步骤S2：编译器接收一份验证条件作为输入；

步骤S3：编译器输出经修改后的安全智能合约。

验证条件用一个领域特定语言编写，其语言的语法如下：

(合约名"."函数名("pre"|"post"){断言语句*})*

其中，"pre"表示在该函数的首部进行验证，"post"表示在该函数的尾部进行验证。断言语句的语法为："assert"逻辑表达式"；"，该逻辑表达式的语法为：变量名逻辑运算符(值|变量名|算术表达式)，其中变量名是智能合约的storage变量或函数内部的变量的名称，逻辑运算符是"<"、"<＝"、"＝＝"、">＝"、">"、"！＝"的其中一个，值是任意数值或字符串，算术表达式的语法为：变量名算术运算符(值|变量名|算术表达式)，其中算术运算符是"+"、"-"、"*"、"/"的其中一个。

例如，对于以下智能合约，可以编写一个合法的验证条件：

智能合约：

验证条件：

在编译器的运行过程中，验证条件语言将会被转换为字节码，该字节码将被智能合约的内部函数用来做验证。该字节码基于栈的形式，有以下15种指令，其含义分别如下：

例如，一个验证条件会被转换为如下的字节码：

验证条件：

字节码：

请参阅图3，所述编译器的运行步骤包括：

步骤S10：转换并储存验证条件；

步骤S11：植入验证解释器；

步骤S12：添加验证函数调用；

步骤S13：输出结果。

其中，所述步骤S10包括：在输入的智能合约源代码中添加一个string类型的storage变量且名称为verification，将输入的验证条件语言转换为字节码格式，并存储在verification变量中；

在智能合约源代码中添加一个setVerification函数，该函数的输入参数是一个string类型的变量，函数内部将这个参数赋值给verification变量，用于从外部更新verification变量的值，并限制该函数只能由智能合约的创建者调用。

例如，对于以下智能合约代码：

该代码被转换为以下格式：

其中，所述步骤S11包括：在智能合约源代码中添加一个check函数用于验证，所述check函数的输入参数为一个string类型的变量且名称为information，表示函数调用时的函数名、传入的参数、调用位置经编码后的结果，函数内部为验证条件语言的解释器，将会依次执行存储在verification变量的字节码中的指令。

其中，所述步骤S12包括：对智能合约源代码进行分析，找出其所有的函数，并在函数的第一行和最后一行插入一个check函数的调用语句，将函数名、函数的多个参数、当前位置的三种信息进行编码，转换为一个string类型的值并传入check函数中。

其中，所述步骤S13包括：将处理后的智能合约代码输出，输出的智能合约代码为安全的经过验证的智能合约。

本申请实施例提供的技术方案可以包括以下有益效果：本申请设计了一种可更新的智能合约的动态验证方法，本申请允许智能合约开发者在部署后修改智能合约的验证条件，确保使用该智能合约进行交易的安全性，解决了传统静态方法的假阳性问题，准确率更高，解决了传统形式化验证方法的适用代码规模小、验证速度慢的问题，可用于大规模的验证。

允许用户编写验证条件，以便对智能合约进行验证。验证条件可被更新，以便将来在Solidity编译器中发现新的bug后，合约开发者可以及时更新该验证条件，拒绝不安全的交易。解决了现有技术中，对于以太坊智能合约，现有方法无法应对Solidity编译器内部尚未被发现的bug，这些bug会导致编译出的字节码的程序语义与源代码的语义不同，一旦编译部署后，合约内部将隐藏着某些改变语义的bug。

用于验证的代码将和智能合约的原始源代码一起部署上链，形成经验证的安全智能合约，该安全智能合约将拒绝所有不满足验证的判定条件的交易，从而保护智能合约正常运行。本申请部署上链的智能合约能够向后兼容，相比没有使用本方法处理过的合约，不影响用户的正常使用。

以上所述，仅为本发明的具体实施方式，但本发明的保护范围并不局限于此，任何熟悉本技术领域的技术人员在本发明揭露的技术范围内，可轻易想到各种等效的修改或替换，这些修改或替换都应涵盖在本发明的保护范围之内。因此，本发明的保护范围应以权利要求的保护范围为准。