一种用于智能合约代码设计生成的EB2S系统及使用方法

一种用于智能合约代码设计生成的eb2s系统及使用方法
技术领域
1.本发明属于区块链智能合约与软件安全技术领域，尤其涉及一种用于智能合约代码设计生成的eb2s系统及使用方法。


背景技术：

2.智能合约本质上可以看作在区块链上部署的一段可信交易执行程序，蕴含着契约关系和利益交易，承载了巨大的价值和交易量，比一般的软件具有更复杂的逻辑性和更高的安全性要求。
3.形式化方法是一种基于严格数学模型的软硬件设计方法，也是在安全关键软件系统中被广泛采用且高效的验证方法，同时也是国际软件验证的最高级别标准，形式化方法对整个系统使用非二义性的形式语言进行描述，并可以通过相应的验证工具对模型的各种属性进行验证
4.通过对智能合约以及形式化方法应用在智能合约领域现状的分析，现有技术主要存在以下不足：
5.1)智能合约存在大量的潜在安全风险，并且大部分隐患来源于合约开发者的设计逻辑出现的漏洞。常见的静态分析方法、软件测试或人工审计很难发现这种类型漏洞。
6.2)形式化方法和智能合约代码之间存在语义鸿沟和技术壁垒。应用形式化方法需要深厚的数学功底，而开发智能合约代码需要熟练使用合约的编程语言。在面向大规模智能合约的应用场景时，很难让所有的开发者同时掌握形式化方法和智能合约开发方法。
7.3)形式化模型和智能合约存在语义不一致的情况，现有技术中可行的规约语言或模型工具无法保证建立的模型行为和智能合约的需求文档保持一致。
8.4)形式化验证智能合约的自动化程度低。通常建立智能合约的形式化模型需要很高的人力成本和时间成本，在面向大规模智能合约应用场景时，人工建模和手动验证导致效率低下，且很难保证建模的正确性和一致性。


技术实现要素：

9.本发明的目的是提供一种用于智能合约代码设计生成的eb2s系统及使用犯法，将其投入到智能合约代码的自动设计生成，以解决智能合约现有安全问题以及形式化方法与智能合约结合的不足。
10.本发明一方面提供了一种用于智能合约代码设计生成的eb2s系统，包括：
11.eb2s插件以及rodin平台，所述eb2s插件为所述rodin的插件，所述eb2s插件调用所述rodin平台提供的api输入一个event-b模型，获取所述event-b模型中的元素，所述元素包括集合、常量、公理、变量、事件；然后所述eb2s工具应用转换规则得到对应的solidity合约文件。
12.优选的，所述rodin为基于eclipse开发的平台，由多个插件组成，多个插件包括编辑器，证明义务生成器，证明器，模型检测工具和定理证明器。
13.优选的，所述rodin平台的组件包括：
14.(1)org.rodinp.core组件，实现所述rodin平台的数据库功能，用于存储证明义务和证明策略，所述org.rodinp.core组件包含一个静态检查器、证明义务生成器和证明器，eb2s插件通过所述org.rodinp.core组件捕捉待转换的机器和文本中的信息，所述信息包括集合，常量，公理，变量，不变量和事件；
15.(2)org.eventb.core.ast组件，用于将数学语言编码为抽象语法树的节点，并提供visitor方式遍历语法树并解析数学表达式、打印数学表达式、构建新的数学表达式、检查数学表达式的类型和检查表达式的之间的相等性；
16.(3)org.eventb.core组件，所述org.eventb.core组件为org.eventb.core.ast组件提供部分输入，eb2s使用所述org.eventb.core组件解析数学表达式，然后转换到solidity代码，并且eb2s不会对该组件产生影响。由此在图中使用单向箭头表示两者的关系。eb2s扩展了该visitor模式，用于遍历抽象语法树，每个语法类型的访问操作都不一样；
17.(4)序列证明器org.eventb.core.prover，实现一个用于证明序列的库；
18.(5)event-b用户界面组件org.eventb.ui，包含一个图形用户界面，允许用户编写event-b模型并和证明引擎交互。例如，用户可以选择转换第几个机器；该组件和eb2s插件有一个双向的交互：从组件到eb2s插件可以捕捉到用户的输入请求；从eb2s插件到组件可以展示生成的solidity代码。
19.优选的，所述eb2s系统生成三个文件，分别是主合约，工具合约和日志文件；主合约和被转换的机器保持语义一致的对应，工具合约包含一些辅助主合约的函数和数据类型；日志文件记录了整个转换过程的步骤和状态以及可能出现的异常情况。
20.优选的，所述eb2s系统包括多个转换方法对应的规则和算法，所述规则和算法按照从整体到局部的顺序包括：
21.(1)规则m：将一个完整的event-b机器及其参考的文本转换到solidity合约，所述规则m规定在转换之前必须验证通过所有的证明义务；
22.(2)抽象集数据结构及查重规则：基于solidity语法规则构造一个语义一致的数据结构，选择数组作为和抽象集对应的数据结构，限制数组中不能有相同的元素，即数组中存储的元素值不能一样；
23.(3)集合转换规则set：通过set规则将集合转换为数组；
24.(4)常量转换规则cons规则及变量转换规则var规则：分别用于将event-b中的常量和变量转换到solidity语言中对应的常量和变量；
25.(5)公理转换规则axiom、定理转换规则theorem以及不变量转换规则inv：公理转换规则axiom用于将公理转换为断言；所述定理转换规则theorem用于将定理转换为断言；所述不变量转换规则inv用于将不变量转换为断言；solidity支持两种断言：assert和require，所述公理、定理和不变量都转换为assert断言；
26.(6)初始化事件转换规则init：初始化事件在所有事件中最先执行，并只执行一次，用于初始化机器中的变量，将所述初始化事件直接转换为solidity合约中的构造函数，所述构造函数是使用construct关键字声明的特殊函数，用于初始化合约中的变量；
27.(7)普通事件转换规则：普通事件可以转换为两个solidity函数，其中一个为守卫函数，用于测试对应事件的守卫条件是否满足，另一个为执行函数，用于执行对应事件的动
作；
28.(8)针对普通事件中有无参数的规则when规则和any规则；
29.(9)赋值操作转换规则assign：考虑赋值后的表达式e’可能会发生变化，而被赋值的变量应当等于赋值前的表达式e’，定义一个常量ec，用于记录赋值前的表达式e’的值；
30.(10)多赋值操作规则：根据event-b的语义，对于单个事件，所有的动作(actions)是同时进行的；当事件中的多个赋值操作时，将每个赋值操作分别转换，为了验证其赋值操作的安全属性，采用合取操作来合并结果；
31.(11)赋值操作的变量集合规则：定义了三个辅助运算子mod，pred和typeof；其中mod运算子用于计算由事件中动作赋值的变量集；所述pred运算子用于计算event-b语言中的变量或表达式到对应的solidity中定义的变量或表达式，基于pred运算子，确定pow规则和relationhas规则，pow规则用于转换event-b中的属于运算表达式；relationhas规则用于转换event-b中的关系到solidity语言中的mapping数据结构；该运算子允许用户定义嵌套的关系；所述typeof运算子将event-b变量和常量的类型转换到对应的solidity类型；
32.(12)event-b模型执行模拟算法：将合约m看作一个对象，其中的所有方法都可以通过this.method()来调用；event-b中所有事件的执行顺序是随机的，通过随机数的方式，来模拟其事件的执行；通过if
…
break控制语句保证了事件执行的原子性；其中，solidity合约本身没有提供生成随机数的工具类或方法，需要自定义随机数的方法来生成伪随机数；所述伪随机数使用线性同余发生器lcg算法生成，包括：计算参数的紧密打包编码；通过keccak256算法对结果进行hash计算；转换成uint256类型；在获得随机数后，根据其取值范围进行取模操作，最终获得伪随机数。
33.优选的，所述初始化事件转换规则init还包括：将eb2s运算子递归地应用在初始化事件，实现对整个initialisation事件转换。
34.优选的，所述普通事件转换规则还包括：
35.在event-b中，事件的所有守卫条件是同时评估的，但每次只能执行一个事件。根据event-b语义：如果事件的守卫条件不满足，事件不会执行，因此不会改变系统状态；为了满足其语义，构造两种场景：
36.第一种情况是守卫条件不满足，即不能执行run_evt方法，其后置条件是合约中变量不能发生改变；为了判断合约中变量是否被修改，定义一个can_assign函数，以及两个全局数组变量g和g
′
，由于合约的全局状态变量数目是确定的，因此可以定义一个数组g保存着合约中所有的全局变量；g
′
表示经过了某个run_evt方法后的g，如果该run_evt方法没有对变量修改，则g＝g
′
，反之，g≠g
′
。can_assign方法定义输入为指定变量组成的数组，表示该数组中的元素可以进行赋值操作，允许其发生变化，而不在该数组中的元素则不能被修改；
37.第二种情况是事件的守卫条件满足，可以执行run_evt方法，其后置条件为合约状态的变化必须满足该事件的动作；
38.在所述形式化模型event-b中，机器会不断的运行下去直到所有事件的守卫条件都不被满足；机器可以一直运行只要有至少一个事件的守卫条件满足；任何一个事件在守卫条件满足的时候便可以执行，并且所有的事件的执行满足原子性，即该事件的执行是不可中断的，要么全部执行成功要么全部执行失败。
39.本发明第二方面提供了一种用于智能合约代码设计生成的eb2s系统的使用方法，包括：
40.步骤1，用户安装rodin平台，并同时安装该eb2s插件；
41.步骤2，打开eb2s插件后，会弹出一个交互界面，用户通过中间的下拉菜单选择需要转换的项目名称，然后可以选择“全部转换”或“部分转换”模式，前者会直接转换整个项目下的所有机器，后者提供了下拉菜单，指定需要转换的机器；
42.步骤3，输入指定的项目文件，在项目所在路径上生成一个solidity文件夹，里面保存着生成的日志文件和solidity合约文件；“全部转换”模式会直接根据最后一次精化得到的机器来转换；在遇到精化过程中可能会有一些分支机器的情况，或在用户希望生成建模过程中某一次精化的机器对应的合约代码时，该模式便无法实现，转而采用“部分转换”的模式，选择特定的机器进行转换。
43.本发明的第三方面提供一种电子设备，包括处理器和通信电路，所述处理器连接所述通信电路，所述处理器用于执行指令以实现如第二方面所述的使用方法。
44.本发明的第四方面提供一种计算机可读存储介质，所述计算机可读存储介质存储有多条指令，所述多条指令可被处理器读取并执行如第二方面所述的使用方法。
45.本发明提供的用于智能合约代码设计生成的eb2s系统、使用方法以及电子设备，具有如下有益效果：
46.(1)智能合约没有潜在安全风险。
47.(2)适用于面向大规模智能合约的应用场景设计，对开发者同时掌握形式化方法和智能合约开发方法的要求降低。
48.(3)能够确保建立的模型行为和智能合约的需求文档保持一致。
49.(4)形式化验证智能合约的自动化程度高，在面向大规模智能合约应用场景时，在保证高效率的前提下可以保证建模的正确性和一致性。
附图说明
50.图1为根据本发明优选实施例的eb2s总体架构图。
51.图2为根据本发明优选实施例的eb2s内部结构示意图。
52.图3为根据本发明优选实施例的eb2s工具界面示意图。
53.图4为根据本发明优选实施例的电子设备构成图。
具体实施方式
54.下面结合附图和实施例，对本发明的具体实施方式作进一步详细描述。以下实施例用于说明本发明，但不用来限制本发明的范围。
55.本实施例提供一种用于智能合约代码设计生成的eb2s系统，基于rodin插件开发，应用java语言开发，在rodin3.5版本上进行测试和应用。图1所示为eb2s系统的总体架构，所述用于智能合约代码设计生成的eb2s系统包括：
56.eb2s插件以及rodin平台，所述eb2s插件为所述rodin的插件，所述eb2s插件调用所述rodin平台提供的api输入一个event-b模型，获取所述event-b模型中的元素，所述元素包括集合、常量、公理、变量、事件；然后所述eb2s工具应用转换规则得到对应的solidity
合约文件。
57.作为优选的实施方式，所述rodin为基于eclipse开发的平台，由多个插件组成，图1的虚线矩形表示多个插件，包括编辑器，证明义务生成器，证明器，模型检测工具和定理证明器。
58.如图2所示为所述eb2s插件的内部结构和涉及到的rodin主要组件之间关系。
59.作为优选的实施方式，如图2所示为所述rodin平台的主要组件，以org.*形式展示；其中：
60.(1)org.rodinp.core组件，实现所述rodin平台的数据库功能，用于存储证明义务和证明策略，所述org.rodinp.core组件包含一个静态检查器、证明义务生成器和证明器(prover)，eb2s插件通过所述org.rodinp.core组件捕捉待转换的机器(machine)和文本(context)中的信息，所述信息包括集合，常量，公理，变量，不变量和事件，图2中单箭头表示eb2s从组件中获取上述信息，而不会对该组件产生影响。
61.(2)在event-b中，模型是通过数学语言来表示的，org.eventb.core.ast组件将数学语言编码为抽象语法树的节点，并提供visitor方式遍历语法树并解析数学表达式、打印数学表达式、构建新的数学表达式、检查数学表达式的类型和检查表达式的之间的相等性。
62.(3)org.eventb.core组件，所述org.eventb.core组件为org.eventb.core.ast组件提供部分输入，eb2s使用所述org.eventb.core组件解析数学表达式，然后转换到solidity代码，并且eb2s不会对该组件产生影响。由此在图中使用单向箭头表示两者的关系。eb2s扩展了该visitor模式，用于遍历抽象语法树，每个语法类型的访问操作都不一样。
63.(4)序列证明器org.eventb.core.prover，实现一个用于证明序列的库。
64.(5)event-b用户界面组件org.eventb.ui，包含一个图形用户界面，允许用户编写event-b模型并和证明引擎交互。例如，用户可以选择转换第几个机器(如图3所示)。该组件和eb2s插件有一个双向的交互：从组件到eb2s插件可以捕捉到用户的输入请求；从eb2s插件到组件可以展示生成的solidity代码。
65.作为优选的实施方式，eb2s系统主要生成三个文件，分别是主合约，工具合约和日志文件。主合约和被转换的机器保持语义一致的对应，工具合约包含一些辅助主合约的函数和数据类型，例如不包含重复元素的数组结构和可以生成随机数的rand函数等，供主合约调用。日志文件记录了整个转换过程的步骤和状态(成功或失败)，以及可能出现的异常情况。
66.作为优选的实施方式，所述eb2s系统包括多个转换方法对应的规则和算法，所述规则和算法按照从整体到局部的顺序包括：
67.(1)规则m：表1定义了规则m，将一个完整的event-b机器及其参考的文本转换到solidity合约，所述规则m规定在转换之前必须验证通过所有的证明义务，因为一方面，转换一个不能通过证明义务的机器是没有意义的；另一方面，转换通过证明义务的机器，不需要考虑转换模型中的见证者(witness)和变体(variant)到solidity合约中。其中，见证者用于规约在抽象模型中的变量，但该变量在精化后的模型中不再使用，变体用于证明event-b某个事件的收敛性，即一定会终止；这两个元素用于辅助证明模型的精化属性和事件收敛性，这对于solidity合约是不需要考虑的，因此，不用将其转换到solidity合约。
68.表1转换规则m
[0069][0070]
(2)抽象集数据结构及查重规则：由于solidity语言没有关于抽象集的概念和相关的数据结构，因此需要基于solidity语法规则构造一个语义一致的数据结构，这里选择数组作为和抽象集对应的数据结构，限制数组中不能有相同的元素，即数组中存储的元素值不能一样。本实施例对于数组a，设计如表2所示的算法用于判断其是否含有重复元素。
[0071]
表2集合对应的数组校验算法
[0072][0073]
(3)集合转换规则set，如表3所示，通过set规则将集合转换为数组，其中typeof运算子用于计算集合s的类型。
[0074]
表3转换规则set
[0075][0076]
(4)常量转换规则cons规则及变量转换规则var规则：分别用于将event-b中的常量和变量转换到solidity语言中对应的常量和变量，如表4所示。
[0077]
表4转换规则cons和var
[0078][0079]
(5)公理转换规则axiom、定理转换规则theorem以及不变量转换规则inv：公理(axioms)通常用来规约常量的性质，将其转换为断言；定理(theorems)必须由公理推导得到，因此也转换为断言；不变量(invariant)用来规约机器中变量的性质，因此将它们转换为断言。solidity支持两种断言：assert和require。assert()相对于require()，在报错的时候，会扣除gas费用，但require()在报错后会返还gas费用。因此，require()声明失败被认为是正常和健壮的情况，当assert()声明失败时，则意味程序存在需要修复的bug，通常用来验证变量越界、不变量、验证发生改变后的状态，预防不应该发生的条件等。require()通常用来验证用户的输入、外部合约响应等。因此，公理、定理和不变量都转换为assert断言。表5定义了axiom、theorem和inv三个转换规则，其中，pred运算子用于计算event-b变量或语句转换得到的solidity的变量或语句。
[0080]
表5转换规则axiom、theorem与inv
[0081][0082]
(6)初始化事件转换规则init：初始化事件(initialisation)在所有事件中最先执行，并只执行一次，用于初始化机器中的变量，所以直接转换为solidity合约中的构造函数。构造函数是使用construct关键字声明的特殊函数，用于初始化合约中的变量。在表6中定义了init规则，将eb2s运算子递归地应用在初始化事件，可实现对整个initialisation事件转换。
[0083]
表6转换规则init
[0084][0085]
(7)普通事件转换规则：普通事件可以转换为两个solidity函数，其中一个为守卫函数，用于测试对应事件的守卫条件是否满足，另一个为执行函数，用于执行对应事件的动作。在event-b中，事件的所有守卫条件是同时评估的，但每次只能执行一个事件。根据event-b语义：如果事件的守卫条件不满足，事件不会执行，因此不会改变系统状态。为了满足其语义，我们构造了两种场景。
[0086]
第一种情况是守卫条件不满足，即不能执行run_evt方法，我们规定其后置条件是合约中变量不能发生改变。为了判断合约中变量是否被修改，定义一个can_assign函数，以
及两个全局数组变量g和g
′
，由于合约的全局状态变量数目是确定的，因此可以定义一个数组g保存着合约中所有的全局变量。g
′
表示经过了某个run_evt方法后的g，如果该run_evt方法没有对变量修改，则g＝g
′
，反之，g≠g
′
。can_assign方法(用于判断合约中变量是否被修改)定义如表7所示，输入为指定变量组成的数组，表示该数组中的元素可以进行赋值操作，允许其发生变化，而不在该数组中的元素则不能被修改。例如，can_assign(null)表示传入了空数组，即没有变量可以被修改；can_assign(s)表示传入了数组s，即任何s中保存的合约变量可以被修改，非s中的其他合约变量不能被修改。
[0087]
表7 can_assign函数
[0088][0089]
第一种情况的断言如表8所示。
[0090]
表8不满足守卫条件的断言
[0091][0092]
第二种情况是事件的守卫条件满足，可以执行run_evt方法，我们规定其后置条件为合约状态的变化必须满足该事件的动作。其断言如表9所示。assert(a
′
)表示对函数中所有赋值语句进行断言，如赋值语句var＝expr，其断言为assert(var＝＝expr)。
[0093]
表9满足守卫条件的断言
[0094][0095]
(8)针对普通事件中有无参数的规则when规则和any规则，如表10所示。when规则由于不考虑参数，比any更加简单。
[0096]
表10转换规则any与when
[0097][0098]
(9)赋值操作转换规则assign：在solidity语言中变量都是值类型，它们的比较操作使用＝＝符号。考虑赋值后的表达式e’可能会发生变化，因为表达式中的变量可能会发生变化，而被赋值的变量应当等于赋值前的表达式e’，为了转换这条安全属性，定义一个常量ec，用于记录赋值前的表达式e’的值，如表11所示。
[0099]
表11转换规则assign
[0100][0101]
(10)多赋值操作规则：根据event-b的语义，对于单个事件，所有的动作(actions)是同时进行的。当事件中的多个赋值操作时，将每个赋值操作分别转换，为了验证其赋值操作的安全属性，采用合取操作来合并结果。例如，给出某个event-b事件的赋值操作，如表12所示。
[0102]
表12多赋值操作
[0103][0104]
其转换结果如表13所示。
[0105]
表13多赋值操作的转换结果
[0106][0107]
(11)赋值操作的变量集合规则：为了便于介绍eb2s工具的转换方法，定义了三个辅助运算子mod，pred和typeof。
[0108]
(11-1)mod运算子用于计算由事件中动作赋值的变量集。在modasg规则中，ν是一个变量，e是表达式，该规则将被赋值的变量添加到集合中。在event-b中，:|符号表示非确定赋值，可以和确定性赋值(:＝)等价替换。如v：＝v+w可以表示成v:|v
′
＝v+w。如表14所示，基于mod运算子，定义了几个类似的规则来计算涉及到赋值操作的变量集合，如modsel，modany和modsim。需要强调的是，在modany规则中，由于引入了局部变量x，所以全局变量中的x(如果有的话)不应该被计算在数组s中，因此需要从s中去掉。
[0109]
表14 mod衍生规则
[0110][0111]
(11-2)pred运算子用于计算event-b语言中的变量或表达式到对应的solidity中定义的变量或表达式。例如，event-b谓词、布尔值、关系和一些算术表达式通过pred运算子，可以直接转换到对应的solidity语法结构。
[0112]
基于pred运算子，给出了pow规则和relationhas规则。pow规则用于转换event-b中的属于运算表达式(∈)。我们在solidity中定义了两个内置函数has和powset，has函数设计如表15所示。has函数的输入为一个元素x和一个数组a，返回一个布尔值，用于判断数组a中是否有该元素，由于元素x可能是引用类型，因此我们比较它们的哈希值。
[0113]
表15 has函数
[0114][0115]
参考event-b中计算幂集的方法，考虑一个集合x＝{a,b,c}，其幂集合为{}、{a}、{b}、{a,b}、{c}、{a,c}、{b,c}、{a,b,c}。可以总结出：
[0116]
每增长一个元素组成的新的幂集＝增长前的幂集+该元素与增长前幂集的组合。
[0117]
基于该思路，定义powset函数，如表16所示，输入为一个数组a，输出一个数组b，数组b中元素是数组a元素可能构成的每个数组。
[0118]
表16幂集函数
[0119][0120][0121]
有了has和powset作为辅助函数，定义pow规则如表17所示，其中x和y表示集合。
[0122]
表17 pow转换规则
[0123][0124]
如表18所示，relationhas规则用于转换event-b中的关系(relation)到solidity语言中的mapping数据结构。r是一个关系，并且rd和rr是关系r的定义域和值域。
[0125]
表18转换规则relationhas
[0126][0127]
该运算子允许用户定义嵌套的关系。例如，该运算子允许用户定义嵌套的关系。例如，这
里f是一个关系，fd，fr和fs是集合。经过pred运算子，可以得到：
[0128]
new mapping(fd
′
＝＞new mapping(fr
′
，fs
′
)).has(f)
[0129]
(11-3)typeof运算子可以将event-b变量和常量的类型转换到对应的solidity类型。例如整数类型转换到solidity的整数类型int/uint，关系(relation)和函数(function)转换到solidity的映射结构，集合类型转换到solidity的数组类型。
[0130]
在event-模型中，机器会不断的运行下去直到所有事件的守卫条件都不被满足。也就是说，机器可以一直运行只要有至少一个事件的守卫条件满足。任何一个事件在守卫条件满足的时候便可以执行，并且所有的事件的执行满足原子性，即该事件的执行是不可中断的，要么全部执行成功要么全部执行失败。
[0131]
(12)event-b模型执行模拟算法：将event-b模型转换到solidity合约时，需要在solidity合约中实现event-b模型的执行机制。如表19所示，为event-b模型执行模拟算法，实现了符合event-b语义的事件执行机制，将合约m看作一个对象，其中的所有方法都可以通过this.method()来调用。event-b中所有事件的执行顺序是随机的，因此通过随机数的方式，来模拟其事件的执行。通过if
…
break控制语句保证了事件执行的原子性。
[0132]
表19 event-b模型模拟算法
[0133][0134]
其中，solidity合约本身没有提供生成随机数的工具类或方法，因此需要自己定义个随机数的方法rand()来生成伪随机数，这是使用一个确定性算法计算出来的似乎是随机的数序，因此并不是真正意义上的随机。使用“线性同余发生器”(lcg)算法，如表20所示。第一步通过abi.encodepacked(
…
)returns(bytes)计算参数的紧密打包编码，然后通过keccak256算法对结果进行hash计算，最后转换成uint256类型。在获得随机数后，根据其取值范围进行取模操作，最终获得伪随机数。
[0135]
表20 solidity中随机数生成算法
[0136][0137]
本实施例还提供了一种用于智能合约代码设计生成的eb2s系统的使用方法，包括：
[0138]
步骤1，用户安装rodin平台，并同时安装该eb2s插件；
[0139]
步骤2，打开eb2s插件后，会弹出一个交互界面，如图3所示，用户通过中间的下拉菜单选择需要转换的项目名称，然后可以选择“全部转换”或“部分转换”模式，前者会直接转换整个项目下的所有机器，后者提供了下拉菜单，指定需要转换的机器；
[0140]
步骤3，输入指定的项目文件，在项目所在路径上生成一个solidity文件夹，里面保存着生成的日志文件和solidity合约文件；“全部转换”模式会直接根据最后一次精化得到的机器来转换；在遇到精化过程中可能会有一些分支机器的情况，或在用户希望生成建模过程中某一次精化的机器对应的合约代码时，该模式便无法实现，转而采用“部分转换”的模式，选择特定的机器进行转换，更加方便。
[0141]
如图4所示，本实施例还提供了一种电子设备，包括处理器301和与处理器301连接的通信电路302，处理器301内存储有多条指令，指令可被处理器加载并执行，以使处理器301能够执行如上所述的方法。
[0142]
本实施例还提供了一种计算机可读存储介质，存储有多条指令，指令用于实现如上所述的方法。
[0143]
本实施例提供的用于智能合约代码设计生成的eb2s系统及使用方法，具有如下有益效果：
[0144]
(1)智能合约没有潜在安全风险。
[0145]
(2)适用于面向大规模智能合约的应用场景设计，对开发者同时掌握形式化方法和智能合约开发方法的要求降低。
[0146]
(3)能够确保建立的模型行为和智能合约的需求文档保持一致。
[0147]
(4)形式化验证智能合约的自动化程度高，在面向大规模智能合约应用场景时，在保证高效率的前提下可以保证建模的正确性和一致性。
[0148]
尽管已描述了本发明的优选实施例，但本领域内的技术人员一旦得知了基本创造性概念，则可对这些实施例作出另外的变更和修改。所以，所附权利要求意欲解释为包括优选实施例以及落入本发明范围的所有变更和修改。显然，本领域的技术人员可以对本发明进行各种改动和变型而不脱离本发明的精神和范围。这样，倘若本发明的这些修改和变型属于本发明权利要求及其等同技术的范围之内，则本发明也意图包含这些改动和变型在内。

技术特征：
1.一种用于智能合约代码设计生成的eb2s系统，其特征在于，包括：eb2s插件以及rodin平台，所述eb2s插件为所述rodin的插件，所述eb2s插件调用所述rodin平台提供的api输入一个event-b模型，获取所述event-b模型中的元素，所述元素包括集合、常量、公理、变量、事件；然后所述eb2s工具应用转换规则得到对应的solidity合约文件。2.根据权利要求1所述的一种用于智能合约代码设计生成的eb2s系统，其特征在于，所述rodin为基于eclipse开发的平台，由多个插件组成，多个插件包括编辑器，证明义务生成器，证明器，模型检测工具和定理证明器。3.根据权利要求1所述的一种用于智能合约代码设计生成的eb2s系统，其特征在于，所述rodin平台的组件包括：(1)org.rodinp.core组件，实现所述rodin平台的数据库功能，用于存储证明义务和证明策略，所述org.rodinp.core组件包含一个静态检查器、证明义务生成器和证明器，eb2s插件通过所述org.rodinp.core组件捕捉待转换的机器和文本中的信息，所述信息包括集合，常量，公理，变量，不变量和事件；(2)org.eventb.core.ast组件，用于将数学语言编码为抽象语法树的节点，并提供visitor方式遍历语法树并解析数学表达式、打印数学表达式、构建新的数学表达式、检查数学表达式的类型和检查表达式的之间的相等性；(3)org.eventb.core组件，所述org.eventb.core组件为org.eventb.core.ast组件提供部分输入，eb2s使用所述org.eventb.core组件解析数学表达式，然后转换到solidity代码，并且eb2s不会对该组件产生影响。由此在图中使用单向箭头表示两者的关系。eb2s扩展了该visitor模式，用于遍历抽象语法树，每个语法类型的访问操作都不一样；(4)序列证明器org.eventb.core.prover，实现一个用于证明序列的库；(5)event-b用户界面组件org.eventb.ui，包含一个图形用户界面，允许用户编写event-b模型并和证明引擎交互。例如，用户可以选择转换第几个机器；该组件和eb2s插件有一个双向的交互：从组件到eb2s插件可以捕捉到用户的输入请求；从eb2s插件到组件可以展示生成的solidity代码。4.根据权利要求1所述的一种用于智能合约代码设计生成的eb2s系统，其特征在于，所述eb2s系统生成三个文件，分别是主合约，工具合约和日志文件；主合约和被转换的机器保持语义一致的对应，工具合约包含一些辅助主合约的函数和数据类型；日志文件记录了整个转换过程的步骤和状态以及可能出现的异常情况。5.根据权利要求1所述的一种用于智能合约代码设计生成的eb2s系统，其特征在于，所述eb2s系统包括多个转换方法对应的规则和算法，所述规则和算法按照从整体到局部的顺序包括：(1)规则m：将一个完整的event-b机器及其参考的文本转换到solidity合约，所述规则m规定在转换之前必须验证通过所有的证明义务；(2)抽象集数据结构及查重规则：基于solidity语法规则构造一个语义一致的数据结构，选择数组作为和抽象集对应的数据结构，限制数组中不能有相同的元素，即数组中存储的元素值不能一样；(3)集合转换规则set：通过set规则将集合转换为数组；
(4)常量转换规则cons规则及变量转换规则var规则：分别用于将event-b中的常量和变量转换到solidity语言中对应的常量和变量；(5)公理转换规则axiom、定理转换规则theorem以及不变量转换规则inv：公理转换规则axiom用于将公理转换为断言；所述定理转换规则theorem用于将定理转换为断言；所述不变量转换规则inv用于将不变量转换为断言；solidity支持两种断言：assert和require，所述公理、定理和不变量都转换为assert断言；(6)初始化事件转换规则init：初始化事件在所有事件中最先执行，并只执行一次，用于初始化机器中的变量，将所述初始化事件直接转换为solidity合约中的构造函数，所述构造函数是使用construct关键字声明的特殊函数，用于初始化合约中的变量；(7)普通事件转换规则：普通事件可以转换为两个solidity函数，其中一个为守卫函数，用于测试对应事件的守卫条件是否满足，另一个为执行函数，用于执行对应事件的动作；(8)针对普通事件中有无参数的规则when规则和any规则；(9)赋值操作转换规则assign：考虑赋值后的表达式e’可能会发生变化，而被赋值的变量应当等于赋值前的表达式e’，定义一个常量ec，用于记录赋值前的表达式e’的值；(10)多赋值操作规则：根据event-b的语义，对于单个事件，所有的动作(actions)是同时进行的；当事件中的多个赋值操作时，将每个赋值操作分别转换，为了验证其赋值操作的安全属性，采用合取操作来合并结果；(11)赋值操作的变量集合规则：定义了三个辅助运算子mod，pred和typeof；其中mod运算子用于计算由事件中动作赋值的变量集；所述pred运算子用于计算event-b语言中的变量或表达式到对应的solidity中定义的变量或表达式，基于pred运算子，确定pow规则和relationhas规则，pow规则用于转换event-b中的属于运算表达式；relationhas规则用于转换event-b中的关系到solidity语言中的mapping数据结构；该运算子允许用户定义嵌套的关系；所述typeof运算子将event-b变量和常量的类型转换到对应的solidity类型；(12)event-b模型执行模拟算法：将合约m看作一个对象，其中的所有方法都可以通过this.method()来调用；event-b中所有事件的执行顺序是随机的，通过随机数的方式，来模拟其事件的执行；通过if
…
break控制语句保证了事件执行的原子性；其中，solidity合约本身没有提供生成随机数的工具类或方法，需要自定义随机数的方法来生成伪随机数；所述伪随机数使用线性同余发生器lcg算法生成，包括：计算参数的紧密打包编码；通过keccak256算法对结果进行hash计算；转换成uint256类型；在获得随机数后，根据其取值范围进行取模操作，最终获得伪随机数。6.根据权利要求5所述的一种用于智能合约代码设计生成的eb2s系统，其特征在于，所述初始化事件转换规则init还包括：将eb2s运算子递归地应用在初始化事件，实现对整个initialisation事件转换。7.根据权利要求5所述的一种用于智能合约代码设计生成的eb2s系统，其特征在于，所述普通事件转换规则还包括：在event-b中，事件的所有守卫条件是同时评估的，但每次只能执行一个事件。根据event-b语义：如果事件的守卫条件不满足，事件不会执行，因此不会改变系统状态；为了满足其语义，构造两种场景：
第一种情况是守卫条件不满足，即不能执行run_evt方法，其后置条件是合约中变量不能发生改变；为了判断合约中变量是否被修改，定义一个can_assign函数，以及两个全局数组变量g和g'，由于合约的全局状态变量数目是确定的，因此可以定义一个数组g保存着合约中所有的全局变量；g'表示经过了某个run_evt方法后的g，如果该run_evt方法没有对变量修改，则g＝g'，反之，g≠g'。can_assign方法定义输入为指定变量组成的数组，表示该数组中的元素可以进行赋值操作，允许其发生变化，而不在该数组中的元素则不能被修改；第二种情况是事件的守卫条件满足，可以执行run_evt方法，其后置条件为合约状态的变化必须满足该事件的动作；在所述形式化模型event-b中，机器会不断的运行下去直到所有事件的守卫条件都不被满足；机器可以一直运行只要有至少一个事件的守卫条件满足；任何一个事件在守卫条件满足的时候便可以执行，并且所有的事件的执行满足原子性，即该事件的执行是不可中断的，要么全部执行成功要么全部执行失败。8.一种根据权利要求1-7任一所述用于智能合约代码设计生成的eb2s系统的使用方法，其特征在于，包括：步骤1，用户安装rodin平台，并同时安装该eb2s插件；步骤2，打开eb2s插件后，会弹出一个交互界面，用户通过中间的下拉菜单选择需要转换的项目名称，然后可以选择“全部转换”或“部分转换”模式，前者会直接转换整个项目下的所有机器，后者提供了下拉菜单，指定需要转换的机器；步骤3，输入指定的项目文件，在项目所在路径上生成一个solidity文件夹，里面保存着生成的日志文件和solidity合约文件；“全部转换”模式会直接根据最后一次精化得到的机器来转换；在遇到精化过程中可能会有一些分支机器的情况，或在用户希望生成建模过程中某一次精化的机器对应的合约代码时，该模式便无法实现，转而采用“部分转换”的模式，选择特定的机器进行转换。9.一种电子设备，其特征在于，包括处理器和通信电路，所述处理器连接所述通信电路，所述处理器用于执行指令以实现如权利要求8所述的使用方法。10.一种计算机可读存储介质，其特征在于，所述计算机可读存储介质存储有多条指令，所述多条指令可被处理器读取并执行如权利要求8所述的使用方法。

技术总结
本发明公开了一种用于智能合约代码设计生成的EB2S系统，包括：EB2S插件以及Rodin平台，EB2S插件为Rodin的插件，EB2S插件调用Rodin平台提供的API输入一个Event-B模型，获取Event-B模型中的元素，元素包括集合、常量、公理、变量、事件；然后EB2S工具应用转换规则得到对应的Solidity合约文件。还公开了EB2S系统的使用方法，包括：安装Rodin平台，并同时安装该EB2S插件；打开EB2S插件后，会弹出一个交互界面，用户通过中间的下拉菜单选择需要转换的项目名称，然后可以选择“全部转换”或“部分转换”模式；输入指定的项目文件，在项目所在路径上生成一个Solidity文件夹，里面保存着生成的日志文件和Solidity合约文件，通过选择的“全部转换”或“部分转换”模式进行转换。模式进行转换。模式进行转换。


技术研发人员：胡凯 朱健 李洁
受保护的技术使用者：北京航空航天大学
技术研发日：2021.11.29
技术公布日：2022/3/8