CN112131587A - 一种智能合约伪随机数安全检验方法、系统、介质和装置 - Google Patents

Abstract

本发明公开了一种智能合约伪随机数安全检验方法、系统、介质和装置，包括：在图神经网络预测模块中，利用图神经网络技术对所要审计的智能合约进行筛选，筛选出包含伪随机数的智能合约；将筛选出的包含伪随机数的智能合约递交到形式化验证模块中，建立计算图模型进行代码剥离，然后利用形式化验证工具对伪随机数的安全性进行逻辑检验；将逻辑检验完成后的智能合约递交到最终审计模块中，将形式化验证的结果呈递给审计人员，由其确保检验结果完整且准确后得到最终检验结果。本发明实现半自动化智能合约中伪随机数的安全性检测，确保伪随机数安全性检测安全性的同时，提高智能合约伪随机数安全检测效率，减轻人工审查的压力。

Description

一种智能合约伪随机数安全检验方法、系统、介质和装置

技术领域

本发明属于智能合约安全性检验领域，具体涉及一种智能合约伪随机数安全检验方法、系统、介质和装置。

背景技术

自2008年区块链技术诞生以来，区块链技术的发展已走过十多年，区块链技术的研究与应用也逐渐被很多学者和科研人员重视，并呈现出爆发式增长的态势。智能合约以区块链为支持平台也逐渐发展起来。

智能合约是一段由事件驱动的、具有状态的、能够保管账本上资产的可执行程序。区块链技术实现了去中心化，而以区块链作为运行底层，智能合约将会自动执行；智能合约降低了人与人之间的信任成本，加快了合约检验和执行的进程，自动化执行也提高智能合约在区块链上执行的效率。智能合约一旦部署到区块链上，智能合约的内容便不会被更改，排除了人为更改智能合约的可能性，保证执行合规合法，实现安全数据处理和公平的网络环境。

智能合约中广泛使用伪随机数，例如Decent.bet透明博彩平台需要使用伪随机数来随机化每次竞猜；Mycrypto Champ游戏合约需要使用伪随机数产生掷骰子的结果。伪随机数是用确定性的算法计算出来数值，当计算条件被满足时，伪随机数可以复现，并不真正的随机，但具有类似于随机数的统计特征，如均匀性、独立性等。伪随机数的安全性对于这些智能合约的安全性至关重要，一旦伪随机数的生成算法被利用破解，智能合约平台、发布者和参与者可能会面临巨大损失。因此，检验智能合约中伪随机数的安全性很有必要。

目前，在智能合约领域，针对随机数的研究大多是寻找一种安全的伪随机数生成算法，而缺乏对智能合约中伪随机数的安全性检验；智能合约中可使用的伪随机数生成方法千变万化，无法确保每个智能合约编写者编写智能合约时都会使用安全性足够高的伪随机数生成算法；在工业界，对智能合约安全性检验的方法主要是人工审查，智能合约审计人员根据合约中使用的算法依据自己的经验给出伪随机数的安全性评测结果，然而，对大量智能合约的安全性进行人工审计的效率过于低下，同时人工审查存在无法确保对智能合约中随机数进行全面检验的问题。

在以上问题没有解决的情况下，赌博和博彩等智能合约会始终成为黑客的潜在攻击目标，一旦涉及利益足够大，这些智能合约将岌岌可危。为了解决这些问题，急需一种可以自动化或者半自动化检验智能合约中伪随机数的安全性的方法，来提高智能合约中伪随机数安全性检验的效率，增强智能合约中伪随机数的的安全性，同时通过智能合约专业人员提供修改建议，来引起智能合约编写者对伪随机数使用的高度注意。

发明内容

本发明基于上述背景和现有技术所存在的问题，拟设计本发明提供了一种智能合约中伪随机数安全检验方法、系统、介质和装置。本发明利用图神经网络技术对智能合约进行分拣，利用形式化验证技术对智能合约中的伪随机数的安全性进行检验，实现半自动化地检测智能合约中伪随机数的安全性，确保伪随机数安全性检测安全性的同时，提高智能合约伪随机数安全检测效率，减轻人工审查的压力。

为了实现本发明的这些目的和其它优点，提供了一种智能合约中伪随机数安全检验方法：

对所要审计的智能合约进行筛选，所述筛选利用图神经网络技术识别出包含伪随机数的智能合约；

基于识别出的包含伪随机数的智能合约建立计算图模型进行代码剥离，然后进行形式化验证，所述形式化验证利用形式化验证工具对伪随机数的安全性进行逻辑检验，得到形式化验证结果；

对逻辑检验完成后的智能合约形式化验证结果进行审计处理，所述审计处理是对形式化验证结果进行完整性与准确性确认并得到最终检验结果。

进一步地，所述神经网络技术具体包括：

搜索不同类型的智能合约数据集，同时为不同的数据集指定标签，根据数据集分别分类为含有伪随机数的智能合约和不含伪随机数的智能合约；

对包含伪随机数的智能合约进行有效信息规约，将智能合约的函数抽象为图神经网络中的节点，智能合约的函数调用关系抽象为节点之间的边，形成图结构，形成图神经网络；

将找到的数据集向量化形成有效数据集，训练图神经网络；

将待检测的智能合约作为图神经网络的输入，由图神经网络对输入的智能合约进行分类。

进一步地，所述形式化验证技术具体包括：

确定伪随机数检验方法；

经过神经网络技术处理得到含有伪随机数的智能合约，将智能合约转换为图模型，在所述图模型中找伪随机数的种子和生成算法；

使用形式化验证工具根据所述检验方法分别设置检验过程所需的定理，并得到最终需要检验的结论，使用形式化验证工具进行定理到结论的形式化验证。

进一步地，所述确定伪随机数检验方法包括伪随机数生成器的设置方法，具体实现包括：

设置伪随机数生成器生成相同序列的概率性；

设置伪随机数生成器生成的序列的统计学平均性；

设置伪随机数的不可预测性能；

设置随机数生成器的工作状态不可回溯预测性能。

进一步地，所述审计的具体实现步骤包括：

响应于接收到所述形式化验证结果，对所述形式化验证结果进行检验，检验形式化验证结果的正确性以及伪随机数生成的种子和生成算法是否正确；

若检验结果为存在缺陷则进行相应的修改，并对所述形式化验证的结果进行补充，提供合理化建议的方法，修改包括伪随机数算法的种子以及限制未来区块变量的使用以及伪随机数算法的选择建议。

另一方面，本发明提出了一种实现上述方法步骤的智能合约伪随机数安全检验系统，具体组成包括：

图神经网络预测模块：用于对所要审计的智能合约进行筛选，识别出包含伪随机数的智能合约；在图神经网络预测模块中，利用图神经网络技术对所要审计的智能合约进行筛选，通过所述筛选识别出包含伪随机数的智能合约；

形式化验证模块：用于建立计算图模型对伪随机数的安全性进行逻辑检验；在形式化验证模块中，将识别出的包含伪随机数的智能合约递交到形式化验证模块中，建立计算图模型进行代码剥离，然后利用形式化验证工具对伪随机数的安全性进行逻辑检验，得到形式化验证结果，并且形式化验证结果发送至最终审计模块中；

最终审计模块：用于对逻辑检验完成后的智能合约形式化验证结果审计处理，所述审计处理是对形式化验证的结果进行完整性与准确性确认并得到最终检验结果。

第三方面，本发明提出了一种计算机可读存储介质，所述计算机可读存储介质存储有计算机程序，所述计算机程序被处理器执行时可实现以上任意一项的方法和步骤。

第四方面，本发明提出了一种智能合约伪随机数安全检验装置，包括存储器、处理器以及存储在所述存储器中并可在所述处理器上运行的计算机程序，所述处理器执行所述计算机程序时可实现以上任意一项的方法和步骤。

本发明的其它优点、目标和特征将部分通过下面的说明体现，部分还将通过对本发明的研究和实践而为本领域的技术人员所理解。本发明至少包括以下有益效果：

1.本发明使用形式化验证工具对智能合约中伪随机数的安全性进行检验，因为形式化验证可以建立状态机对模型进行状态逻辑检验，使得系统在逻辑上完整、安全，能够使智能合约中的伪随机数在逻辑上获得检验，从而减少在伪随机数使用过程当中可能产生的错误以及黑客嗅探等行为。

2.本发明使用图神经网络等深度学习的方式进行智能合约的筛选，智能合约中可以使用的种子很丰富，例如未来区块变量和用户提交的数据等；智能合约编写者可以使用的伪随机数生成策略也非常丰富为准确预测造成了障碍，例如使用各种哈希加密函数、取余运算和使用第三方函数。但是图神经网络通过对函数调用关系进行记录和处理，使得预测准确率相对于其他手段提高很多，可以精确识别使用了伪随机数的智能合约。

3.本发明使用计算图模型对智能合约进行图结构表示，不仅清晰地表达出智能合约的内部结构，还方便了对智能合约中变量及其操作的追溯，计算图模型与形式化证明工具一起，完成了对伪随机数相关条件的查询及检验的环节，保证了伪随机数生成的安全性。

4.本发明在使用形式化验证技术检验包含伪随机数的智能合约的安全性的基础上，还带有对智能合约中伪随机数生成的建议，不仅可以帮助找出合约中的伪随机数漏洞，还会给出指导性建议，帮助智能合约编写者解决发现的问题。

附图说明

图1为本发明系统工作流程示意图；

图2为本发明图神经网络预测模块的实现流程示意图；

图3为本发明形式化验证模块的实现流程示意图；

图4为本发明计算图模型的简易示意图；

图5为本发明计算图模型的最终结果。

具体实施方式

为了清晰地阐述本发明，使本发明实施例的目的、技术方案和优点更加清楚，下面结合了本发明实施例中的附图，对本发明实施例中的技术方案进行清楚、完整地描述，以令本领域技术人员参照说明书文字能够据以实施。下面将附图结合具体实施方式对本发明的技术加以详细说明。

本发明的实施涉及的相关技术如下：

(1)神经元模型。神经元模型的灵感来源于人脑神经细胞的信号传递现象。神经元模型正是对生物神经网络的原始机制这一结构进行了抽象，神经元模型也称“阈值逻辑单元“，其中树突对应于模型的输入部分，每个神经元收到其他神经元传递过来的输入信号，这些信号通过带权重的连接传递给细胞体。而细胞体分为两部分，前一部分计算总输入值，即输入信号的加权和，后一部分先计算总输入值与该神经元兴奋阈值的差值，然后通过激活函数的处理，产生输出从轴突传送给其它神经元，以此来完成神经信号的传递。

(2)神经网络技术。神经网络模型由神经元模型组成。多个神经元模型结合在一起形成层，通过层与层之间信息的传递和处理模拟人的大脑做出反应。神经网络技术具有大规模并行处理，分布式存储，弹性拓扑，高度冗余和非线性运算等特点，因而具有很髙的运算速度，很强的联想能力、适应性、容错能力和自组织能力。

(3)图神经网络技术。图结构由实体组成的节点与表示实体之间关系的连接着对应节点的边组成。比如在社交网络图中，如果将每个用户表示为一个节点，那么节点之间的连接关系就表示他们在社交网络存在某种关系，类似于关注、点赞、转发等关系。如果用户A发了一条动态，用户B点赞了A的动态，那我们可以在社交网络中在A的节点和B的节点之间划线连接，表示他们之间存在某种关系。图神经网络技术就是对结构化的图进行图构建和数据向量化，进而利用神经网络技术训练和预测的技术。

(4)形式化验证技术。形式化验证主要由模型检测和定理证明两种方法组成。模型检测基于模型理论，以穷尽搜索系统状态空间的方式判断模型是否满足性质。为了确保搜索的终止性，模型的状态空间通常会被限制为有穷。在模型检测中，可以使用各种形式化规范语言作为建模语言，并可以用使用时序逻辑作为性质描述语言。模型检测是一种自动化的检验方法，能够在模型不满足性质时，找到反例，便于定位和修改模型。定理证明建立在证明论的基础上，将系统的模型和期望性质表示成公理系统中的定理，通过证明该定理在该公理系统中是有效的来证明模型满足性质。形式化验证技术可以覆盖完整的设计状态空间，提供最小实例以及提供“基于状态”或“基于输出”的分析和调试方法。

(5)计算图模型。计算图模型是一种特殊的图结构，可以用来描述变量及其操作，计算图模型中有两种基本的要素：一种节点代表的变量，另一种节点代表的对变量的操作。计算图模型可以方便地表示函数内变量的操作流程和信息指向，通过将函数的表示结构化，可以方便地进行求导、积分和微分等操作。

具体实施例1：

本发明利用图神经网络技术对智能合约进行分拣，利用形式化验证技术对智能合约中的伪随机数的安全性进行检验，实现半自动化地检测智能合约中伪随机数的安全性，确保伪随机数安全性检测安全性的同时，提高智能合约伪随机数安全检测效率，减轻人工审查的压力。

本发明方法的具体实现步骤包括：

Step1：对所要审计的智能合约进行筛选，所述筛选利用图神经网络技术识别出包含伪随机数的智能合约。其中所述图神经网络技术的实现具体包括：

S11：搜索不同类型的智能合约数据集，同时为不同的数据集指定标签，根据数据集分别分类为含有伪随机数的智能合约和不含伪随机数的智能合约；

S12：对包含伪随机数的智能合约进行有效信息规约，将智能合约的函数抽象为图神经网络中的节点，智能合约的函数调用关系抽象为节点之间的边，形成图结构，形成图神经网络；

S13：将找到的数据集根据S11步骤和S12步骤处理并向量化形成有效数据集，训练图神经网络；

S14：将待检测的智能合约经过S12步骤处理作为图神经网络的输入，由图神经网络对输入的智能合约进行分类。

Step2：基于识别出的包含伪随机数的智能合约建立计算图模型进行代码剥离，然后进行形式化验证，所述形式化验证利用形式化验证工具对伪随机数的安全性进行逻辑检验。所述形式化验证具体实现方法如下：

S21：确定伪随机数检验方法，包括：

S21-K1：设置伪随机数生成器生成相同序列的概率性：设置伪随机数生成器生成相同序列的低概率；

S21-K2：设置伪随机数生成器生成的序列的统计学平均性：设置伪随机数生成器生成的序列符合统计学平均性，即能通过卡方检验和K-S检验，可以通过独立性检验；

S21-K3：设置伪随机数的不可预测性能：设置伪随机数不能从一段序列获得伪随机数发生器的工作状态或者下一个随机数；

S21-K4：设置随机数生成器的工作状态不可回溯预测性能：设置从随机数发生器的状态不能获得伪随机数发生器以前的工作状态；

S22：经过Step1得到含有伪随机数的智能合约，将智能合约转换为图模型，在图模型中找伪随机数的种子和生成算法；

S23：使用形式化验证工具根据检验标准分别设置检验过程所需的定理，并得到最终需要检验的结论，使用形式化验证工具进行定理到结论的形式化验证。

Step3：将逻辑检验完成后的智能合约形式化验证的结果呈递审计，所述审计进行确认检验结果完整且准确后得到最终检验结果。所述审计具体实现步骤包括：

S31：对Step2的结果递交到审计人员处，查看伪随机数生成的种子和生成算法，检查结果的正确性，人为修改形式化验证结果出现的错误。

S32：对于S31的结果进行补充，提供合理化建议的方法，包括但不限于修改伪随机数算法的种子，限制未来区块变量(例如未来某个区块的挖掘难度，未来某个区块的高度，未来某个区块的哈希值等)的使用以及伪随机数算法的选择建议。比如将随机数算法种子的确定性选择修改为密码学中的一次一密原则，禁止使用与合约结果有直接关系的未来区块变量等。

具体实施例2：

本发明提出一种智能合约中伪随机数安全检验方法和系统。其流程如图1所示。具体步骤如下：

(1)图神经网络预测模块

通过向量化数据集结构化构成的图，训练图神经网络，利用训练完成的图神经网络模型对待预测智能合约进行筛选，舍弃不含伪随机数的合约，将含有伪随机数的智能合约提交到下一模块。

其中，利用图神经网络预测模块的流程如图2所示，具体步骤如下：

1.1数据清洗阶段

获得数据集之后，首先对数据集按照标签分类。含有伪随机数的智能合约标签为1，不含有伪随机数的智能合约标签为0。

1.2特征融合阶段

1.2.1图归一化。指定图神经网络节点和边的归一化方法。

1)函数归一化方法：函数抽象为图结构的一般节点。

2)变量归一化方法：变量作为插入节点通过边与函数节点进行连接。

3)关系归一化方法：将函数与变量之间的调用统称为关系，关系作为图结构中的边连接不同的节点。

1.2.2将上一步骤特征融合的结果向量化，形成训练器的输入。图结构向量化方法如下：

1)函数向量化：

函数ID

函数名称

函数类型

外层调用函数

出边时序

入边时序

调用方式

2)变量向量化：

3)关系向量化：

头节点ID

尾节点ID

边时序

操作方式

标签

1.2.3按照归一化规则和向量化方法将智能合约进行特征融合，使图结构向量化，得到图神经网络模型的输入，具体实现还包括：

1.3模型训练阶段：选择GCN模型对1.2.3步骤所得的输入进行训练，然后进行测试集的预测，再多次调参之后获取最优参数值。

(2)形式化验证模块：利用形式化验证工具，通过建立计算图模型对智能合约中伪随机数的安全性进行逻辑检验，根据检验标准得到形式化验证结果。利用形式化证明工具coq进行形式化验证的流程如图3所示，具体步骤如下：

2.1数据处理阶段：根据步骤(2)得到的训练器预测出含有伪随机数的智能合约，利用计算图模型对智能合约变量的传递建立模型，由此形成一个或多个图模型，根据遍历图模型的节点和边，找到伪随机数的种子和生成算法，将结构传递到下一阶段。

此处举例说明计算图模型，如图4所示，最终结果为图5。需要指出的是，以下所述实施例旨在便于对本发明的理解，而对其不起任何限定作用。

示例：计算表达式E＝(A+B)*(B+1)。

A，B和数字1作为基础变量，都是叶节点，在计算“A+B”的过程中，假如最后值为C，则C为A和B的父节点，节点内容为“+”，同理，在计算“B+1”的过程中，假如最后的值为D，则D为B和1的父节点，节点内容为“+”。最终，E为根节点，内容为“*”。最终的计算图模型为图5。

2.2工具检验阶段：

2.2.1根据伪随机数的安全性标准分别设置检验所需的定理方法。

在设置基础公理的前提下，分别设置五个待证明定理方法(即伪随机数应符合的安全标准)：

1)同一序列概率检验：random(seed，algo)<万亿分之一

2)统计学卡方检验：chi_p(seed，algo)<0.95

3)统计学K-S检验：kstest(seed，algo)＝＝0

4)统计学自相关检验：rou(seed，algo)<1.96

5)统计学列联表检验：chi2cdf(seed，algo)<0.95

2.2.2根据2.1所得的种子和生成算法与已经设定好的待证明定理利用形式化验证工具进行检验。并汇总所有标准的检验结果。

(3)最终审计模块

系统将形式化验证的结果呈递给审计人员，由其检验结果的完整性，并为形式化验证的结果提供建议。最终审计模块实现的具体步骤如下：

3.1将上一模块的结果递交到审计人员，得到伪随机数生成的种子和生成算法的安全性检验结果，检查结果的正确性，如形式化验证结果出现错误，则人为进行改正。

3.2对于步骤3.1的结果进行补充，提供合理化建议方法，包括但不限于修改伪随机数算法的种子，限制未来区块变量的使用以及伪随机数算法的选择建议。

实施例3：

本实施例提出了一种计算机可读存储介质，所述计算机可读存储介质存储有计算机程序，所述计算机程序被处理器执行时可实现以下的方法和步骤，对智能合约伪随机数进行安全检验的方法：

对所要审计的智能合约进行筛选，所述筛选利用图神经网络技术识别出包含伪随机数的智能合约；

基于识别出的包含伪随机数的智能合约建立计算图模型进行代码剥离，然后进行形式化验证，所述形式化验证利用形式化验证工具对伪随机数的安全性进行逻辑检验；

将逻辑检验完成后的智能合约形式化验证的结果呈递审计，所述审计进行确认检验结果完整且准确后得到最终检验结果。

在一个实施例中，处理器执行计算机程序时，实现所述神经网络技术具体包括：

搜索不同类型的智能合约数据集，同时为不同的数据集指定标签，根据数据集分别分类为含有伪随机数的智能合约和不含伪随机数的智能合约；

对包含伪随机数的智能合约进行有效信息规约，将智能合约的函数抽象为图神经网络中的节点，智能合约的函数调用关系抽象为节点之间的边，形成图结构，形成图神经网络；

将找到的数据集向量化形成有效数据集，训练图神经网络；

将待检测的智能合约作为图神经网络的输入，由图神经网络对输入的智能合约进行分类。

在一个实施例中，处理器执行计算机程序时，实现所述形式化验证技术具体包括：

确定伪随机数检验方法；

经过神经网络技术处理得到含有伪随机数的智能合约，将智能合约转换为图模型，在所述图模型中找伪随机数的种子和生成算法；

使用形式化验证工具根据所述检验方法分别设置检验过程所需的定理，并得到最终需要检验的结论，使用形式化验证工具进行定理到结论的形式化验证。

在一个实施例中，处理器执行计算机程序时，实现所述确定伪随机数检验方法包括伪随机数生成器的设置方法，具体实现包括：

设置伪随机数生成器生成相同序列的概率性；

设置伪随机数生成器生成的序列的统计学平均性；

设置伪随机数的不可预测性能；

设置随机数生成器的工作状态不可回溯预测性能。

在一个实施例中，处理器执行计算机程序时，实现所述审计的具体实现步骤包括：

响应于接收到所述形式化验证结果，对所述形式化验证结果进行检验，检验形式化验证结果的正确性以及伪随机数生成的种子和生成算法是否正确；

若检验结果为存在缺陷则进行相应的修改，并对所述形式化验证的结果进行补充，提供合理化建议的方法，修改包括伪随机数算法的种子以及限制未来区块变量的使用以及伪随机数算法的选择建议。

实施例4：

本实施例提出了一种智能合约伪随机数安全检验装置，该智能合约伪随机数安全检验装置可以是服务器也可以是移动终端。该计算机设备包括通过系统总线连接的处理器、存储器、网络接口和数据库。其中，该计算机设备的处理器用于提供计算和控制能力。该计算机设备的存储器包括非易失性存储介质、内存储器。该非易失性存储介质存储有操作系统、计算机程序和数据库。该内存储器为非易失性存储介质中的操作系统和计算机程序的运行提供环境。该数据库用于计算机设备的所有数据。该计算机设备的网络接口用于与外部的终端通过网络连接通信。该计算机程序被处理器执行时以实现智能合约伪随机数安全检验方法。

上述对实施例的描述是为便于本技术领域的普通技术人员能理解和应用本发明。熟悉本领域技术的人员显然可以容易地对上述实施例做出各种修改，并把在此说明的一般原理应用到其他实施例中而不必经过创造性的劳动。因此，本发明不限于上述实施例，本领域技术人员根据本发明的揭示，对于本发明做出的改进和修改都应该在本发明的保护范围之内。

Claims (8)

1.一种智能合约伪随机数安全检验方法，其特征在于，具体实现步骤包括：

对所要审计的智能合约进行筛选，所述筛选利用图神经网络技术识别出包含伪随机数的智能合约；

基于识别出的包含伪随机数的智能合约建立计算图模型进行代码剥离，然后进行形式化验证，所述形式化验证利用形式化验证工具对伪随机数的安全性进行逻辑检验，得到形式化验证结果；

对逻辑检验完成后的智能合约形式化验证结果进行审计处理，所述审计处理是对形式化验证结果进行完整性与准确性确认并得到最终检验结果。

2.根据权利要求1所述智能合约伪随机数安全检验方法，其特征在于，所述神经网络技术具体包括：

搜索不同类型的智能合约数据集，同时为不同的数据集指定标签，根据数据集分别分类为含有伪随机数的智能合约和不含伪随机数的智能合约；

对包含伪随机数的智能合约进行有效信息规约，将智能合约的函数抽象为图神经网络中的节点，智能合约的函数调用关系抽象为节点之间的边，形成图结构，形成图神经网络；

将找到的数据集向量化形成有效数据集，训练图神经网络；

将待检测的智能合约作为图神经网络的输入，由图神经网络对输入的智能合约进行分类。

3.根据权利要求1所述智能合约伪随机数安全检验方法，其特征在于，所述形式化验证技术具体包括：

确定伪随机数检验方法；

经过神经网络技术处理得到含有伪随机数的智能合约，将智能合约转换为图模型，在所述图模型中找伪随机数的种子和生成算法；

使用形式化验证工具根据所述检验方法分别设置检验过程所需的定理，并得到最终需要检验的结论，使用形式化验证工具进行定理到结论的形式化验证。

4.根据权利要求3所述智能合约伪随机数安全检验方法，其特征在于，其中，所述确定伪随机数检验方法包括伪随机数生成器的设置方法，具体实现包括：

设置伪随机数生成器生成相同序列的概率性；

设置伪随机数生成器生成的序列的统计学平均性；

设置伪随机数的不可预测性能；

设置随机数生成器的工作状态不可回溯预测性能。

5.根据权利要求1所述智能合约伪随机数安全检验方法，其特征在于，所述审计的具体实现步骤包括：

响应于接收到所述形式化验证结果，对所述形式化验证结果进行检验，检验形式化验证结果的正确性以及伪随机数生成的种子和生成算法是否正确；

若检验结果为存在缺陷则进行相应的修改，并对所述形式化验证的结果进行补充，提供合理化建议的方法，修改包括伪随机数算法的种子以及限制未来区块变量的使用以及伪随机数算法的选择建议。

6.一种智能合约伪随机数安全检验系统，其特征在于，具体组成包括：

图神经网络预测模块：用于对所要审计的智能合约进行筛选，识别出包含伪随机数的智能合约；在图神经网络预测模块中，利用图神经网络技术对所要审计的智能合约进行筛选，通过所述筛选识别出包含伪随机数的智能合约；

形式化验证模块：用于建立计算图模型对伪随机数的安全性进行逻辑检验；在形式化验证模块中，将识别出的包含伪随机数的智能合约递交到形式化验证模块中，建立计算图模型进行代码剥离，然后利用形式化验证工具对伪随机数的安全性进行逻辑检验，得到形式化验证结果，并且形式化验证结果发送至最终审计模块中；

最终审计模块：用于对逻辑检验完成后的智能合约形式化验证结果审计处理，所述审计处理是对形式化验证的结果进行完整性与准确性确认并得到最终检验结果。

7.一种计算机可读存储介质，所述计算机可读存储介质存储有计算机程序，其特征在于，所述计算机程序被处理器执行时实现如权利要求1至5任意一项所述的方法步骤。

8.一种智能合约伪随机数安全检验装置，包括存储器、处理器以及存储在所述存储器中并可在所述处理器上运行的计算机程序，其特征在于，所述处理器执行所述计算机程序时实现如权利要求1至5任意一项所述的方法步骤。

Images