基于类型检测的智能合约信息流完整性验证方法及系统

摘要

本发明公开了一种基于类型检测的智能合约信息流完整性验证方法及系统，属于区块链和信息安全领域。该方法可用于解决以太坊区块链环境下智能合约潜在的信息篡改问题，包括：为智能合约编程语言构建形式化语法、语义；构建智能合约的安全类型系统STC，用于检测智能合约信息流完整性；构建基于智能合约类型系统STC的类型验证器STV，自动为智能合约的状态变量寻找最优安全类型分配。本发明给出智能合约形式化语法和语义，同时结合了类型检测在安全信息流检查中的优点，可以对智能合约源代码的信息流完整性进行有效的分析与验证，减少智能合约在运行过程中出现可信信息被篡改的概率。

说明书

技术领域

本发明属于区块链及程序验证领域，特别涉及一种基于类型检测的智能合约信息流完整性验证方法及系统。

背景技术

智能合约是运行在区块链(例如，以太坊)上的计算机程序，不需要外部可信的权威机构。它们被证明适用于许多领域，包括拍卖、选举、商业和游戏。数据显示，智能合约最近已经变得无处不在，数量急剧增加。然而，如何保证智能合约的安全性是一个挑战。首先，它们通常是在上市时间的压力下开发的，可能充满安全漏洞，或者可能被网络罪犯利用，窃取加密货币和其他数字资产。其次，它们是可以与复杂环境(例如，用户和其他智能合约)交互的程序。在部署不安全的智能合约时，区块链的性质导致不可逆转的破坏。例如，2016年6月DAO合约利用递归漏洞使得1.5亿美元被盗，2017年7月多签名钱包利用函数可见性说明符使得3100万美元被盗，和几个月后在同一钱包由于错误使用delegatecall使得3亿美元被冻结。

为了应对这一挑战，许多技术已经扩展和应用到创建安全合约或检测恶意合约上。例如，使用有限状态机与严格语义跟踪智能合约的行为，以防止常见漏洞；使用形式化EVM(以太虚拟机)定义来定理证明智能合约中的安全属性，形式化方法可以为EVM字节码提供强大的形式化验证保证，但完全自动化形式化验证方法并非易事；使用模糊测试通过生成合约交易序列来检测合约中潜在的漏洞，但模糊测试方法需要一个模拟的执行环境。保持信息流的完整性可能会阻止可信域被不可信数据篡改。实现程序信息流完整性的一种方法是通过基于语言的安全方法，例如，为信息流使用类型系统。在安全类型语言中，通过指定所有程序变量和表达式的类型，可以在编译时强制执行安全策略。然而，为智能合约开发类型检查器并不简单。首先，Solidity的语法比简单的命令式语言更复杂，这使得它不可能使用现有的类型检查器。例如，为了与不遵守ABI的合约交互，或者为了获得更直接的控制，在Solidity中提供了唯一的函数操作callcode和delegatecall。其次，许多类型系统只在不干涉属性上执行可靠性证明，而没有自动类型推断的工具。手动执行类型推断很容易出错，而且可能无法处理大规模的智能合约。此外，基于对现有合约的分析，用户迫切需要工具来检测合约中哪些状态变量是可信的(可信的)，以便存储不能被篡改的信息。

发明内容

本发明的目的在于针对上述现有技术存在的问题，解决以太坊区块链环境下智能合约潜在的信息篡改问题，提供一种基于类型检测的智能合约信息流完整性验证方法。

实现本发明目的的技术解决方案为：一种基于类型检测的智能合约信息流完整性验证方法，所述方法包括以下步骤：

步骤1，为智能合约编程语言构建形式化语法、语义；

步骤2，构建智能合约的安全类型系统STC，用于检测智能合约信息流完整性；

步骤3，构建基于智能合约类型系统STC的类型验证器STV，自动为智能合约的状态变量寻找最优安全类型分配，即状态变量中被分配为可信的数量最多，使得智能合约满足信息流完整性。

进一步地，步骤1中所述构建形式化语法，具体包括：

(1)将智能合约编程语言抽象为短语，这些短语为表达式或语句；

智能合约的表达式包括8种类型：值v、全局变量g、状态变量id、表达式组

|NewExp|OperatorExp

|IndexAccess|MemberAccess

NewExp：：＝new id

OperatorExp：：＝op

IndexAccess：：＝exp[]|exp

MemberAccess：：＝exp.id|exp.IndexAccess

其中，new为实例化合约的标识符，op

智能合约的语句包括3种类型：简单语句SimpleStmt、语句块BlockStmt和语句序列；其中，SimpleStmt表示单个基本语句，包括函数调用FunctionCall、普通赋值语句exp

(Statements)stmt：：＝SimpleStmt；|BlockStmt

|stmt

SimpleStmt：：＝FunctionCall|exp

|exp op＝FunctionCall

LowLevelCall：：＝call|delegatecall|callcode

BlockStmt：：＝if(exp)then stmt

|while(exp)stmt

|letvar id op＝exp in stmt

|require(exp)in stmt

|{stmt}

其中，id

(2)在编写的智能合约中，函数类型分为普通函数normal function、构造函数constructor和回退函数fallbackfunction；一个智能合约有且只有一个未命名的fallback function，其不能有输入或输出参数，并且必须有external可见性；其中，普通函数normal function的语法定义如下：

式中，id

构造函数constructor与普通函数normal function的区别在于：id

回退函数fallback function的语法定义如下：

fun

(3)智能合约包括状态变量声明和函数声明，其语法的定义如下：

(Contracts)ctr：：＝contract id{ctrPart}

ctrPart：：＝letvar id op＝exp|fun|ctrPart ctrPart

步骤1中所述构建形式化语义具体包括：

(1)智能合约的表达式的操作语义形式为

(2)智能合约的语句的操作语义形式为

进一步地，步骤2所述构建智能合约的安全类型系统STC，具体包括：

1)构建STC安全类型

由≤偏序排序的短语安全类型分层如下：

(Expression types)τ::＝T|U

(Phrase types)ρ：：＝τ|τ var|τ stmt

式中，τ为Solidity表达式的安全类型，ρ为Solidity短语的安全类型，包括表达式安全类型、变量安全类型τ var和语句安全类型τ stmt，T、U分别为可信和不可信；变量安全类型τ var存储安全类型为τ或更低的信息，语句安全类型τ stmt指定语句中的每个赋值都是对安全类型为τ或更高的变量进行的；函数的安全类型为：

2)构建STC安全类型规则，包括：

(1)智能合约表达式的安全类型规则的形式为：

(2)智能合约语句的安全类型规则的形式为：

(3)函数的安全类型规则的形式为：

3)STC的可靠性证明

对STC的安全类型规则进行验证，证明其满足不干扰属性，以此得证能被STC证明是类型良好的合约是满足信息流完整性的。

进一步地，所述STC的可靠性证明，具体过程包括：

步骤2-1，给定定义1用于描述智能合约的良好类型属性，给定定义2用于描述不可分辨关系，具体定义如下：

定义1.假设S是一个由有限函数组成的智能合约，由FD和FT分别作为S的函数声明表和函数类型表；在S中声明的每个fun都具有函数类型，即

定义2.给定两个求值环境μ

步骤2-2，基于上述良好类型属性及不可分辨关系，建立引理1及引理2支持STC的可靠性证明；引理1及引理2的具体描述如下：

引理1.假定

引理2.假定

步骤2-3，基于引理1及引理2，给定定义3用于描述Solidity语句的不干涉性，给定定义4用于描述Solidity智能合约的不干涉性，具体定义如下：

定义3.一个智能合约语句stmt在智能合约中执行的语句S是满足不干涉属性的，当且仅当：假设有

定义4.一个智能合约在S中是不干涉的，当且仅当：在S中执行的所有智能合约语句都是满足不干涉属性的；

步骤2-4，基于引理1～2及定义1～4，给定引理3的描述如下：

引理3.假定

步骤2-5，基于引理1～3，给定定理1用于说明良好类型的智能合约是满足不干扰属性的，具体描述如下：

定理1.如果由有限函数组成的智能合约S是类型良好的，那么它是满足不干扰属性的。

进一步地，步骤3所述构建基于智能合约类型系统STC的类型验证器STV，自动为合约的状态变量寻找最优安全类型分配，具体过程包括：

步骤3-1，依据步骤2中对STC的可靠性证明及智能合约的状态变量个数，定义智能合约的安全类型分配的格结构，用于自动生成智能合约中的所有安全类型分配，具体定义如下：

给定智能合约S，其带有n个状态变量的集合V，给定两种安全类型T和U，安全类型分配t是V中所有状态变量的安全类型的组合；用

步骤3-2，基于智能合约的安全类型分配的格结构和STC，采用基于STC的类型验证器算法执行类型检测，直到找到最小数目U的安全类型分配，即最优安全类型分配；其中基于STC的类型验证器算法具体如下：

输入：智能合约S，包含n个状态变量。

输出：一个安全类型分配t使S是良好类型的：

假设

对

对所有属于

计算完毕后，如果S是类型良好的，则输出t，否则输出无解。

一种基于类型检测的智能合约信息流完整性验证系统，所述系统包括：

第一构建模块，用于为智能合约编程语言构建形式化语法、语义；

第二构建模块，用于构建智能合约的安全类型系统STC，用于检测智能合约信息流完整性；

第三构建模块，用于构建基于智能合约类型系统STC的类型验证器STV，自动为智能合约的状态变量寻找最优安全类型分配，即状态变量中被分配为可信的数量最多，使得智能合约满足信息流完整性。

一种计算机设备，包括存储器、处理器及存储在存储器上并可在处理器上运行的计算机程序，处理器执行计算机程序时实现以下步骤：

步骤1，为智能合约编程语言构建形式化语法、语义；

步骤2，构建智能合约的安全类型系统STC，用于检测智能合约信息流完整性；

步骤3，构建基于智能合约类型系统STC的类型验证器STV，自动为智能合约的状态变量寻找最优安全类型分配，即状态变量中被分配为可信的数量最多，使得智能合约满足信息流完整性。

一种计算机可读存储介质，其上存储有计算机程序，计算机程序被处理器执行时实现以下步骤：

步骤1，为智能合约编程语言构建形式化语法、语义；

步骤2，构建智能合约的安全类型系统STC，用于检测智能合约信息流完整性；

步骤3，构建基于智能合约类型系统STC的类型验证器STV，自动为智能合约的状态变量寻找最优安全类型分配，即状态变量中被分配为可信的数量最多，使得智能合约满足信息流完整性。

本发明与现有技术相比，其显著优点为：1)结合了类型检测在安全信息流检查中的优点，可以对智能合约源代码的信息流完整性进行有效的分析与验证，减少了智能合约在开发过程中出现可信信息被篡改的概率；2)提出了一个基于K-framework的智能合约安全类型验证框架，可以自动检测一个智能合约的信息流是否符合完整性策略，该策略由不干涉属性描述，即要求Trusted(T)变量永远不会被Untrusted(U)变量篡改；3)将原始合约作为输入，并且对合约中变量的安全类型进行手动注释，本发明通过提出的框架中的可靠类型检查器(STC)可以检测安全信息流是否满足完整性；4)将原始合约作为输入，并且不对合约中变量的安全类型进行手动注释，本发明的框架能够寻找变量的安全类型分配使得合约满足完整性策略；如果找不到这样的类型分配，则该合约被证明是不安全的；5)特别地，在诊断智能合约的潜在安全漏洞时，本发明的工具能够定位合约中哪些函数、语句违反完整性策略。

下面结合附图对本发明作进一步详细描述。

附图说明

图1为一个实施例中基于类型检测的智能合约信息流完整性验证方法流程图。

图2为一个实施例中Solidity形式化操作语义示例图。

图3为一个实施例中Solidity安全类型规则示例图。

图4为一个实施例中安全类型分配的格结构示意图。

图5为一个实施例中奇偶校验多签名钱包攻击示例图。

图6为一个实施例中基于STC的奇偶校验多签名钱包攻击类型推导示例图。

图7为一个实施例中奇偶校验多签名钱包攻击原始代码的安全类型分配格结构示意图。

图8为一个实施例中修正后的奇偶校验多签名钱包攻击原始代码的安全类型分配格结构示意图。

具体实施方式

为了使本申请的目的、技术方案及优点更加清楚明白，以下结合附图及实施例，对本申请进行进一步详细说明。应当理解，此处描述的具体实施例仅仅用以解释本申请，并不用于限定本申请。

需要说明的是，若本发明实施例中有涉及“第一”、“第二”等的描述，则该“第一”、“第二”等的描述仅用于描述目的，而不能理解为指示或暗示其相对重要性或者隐含指明所指示的技术特征的数量。由此，限定有“第一”、“第二”的特征可以明示或者隐含地包括至少一个该特征。另外，各个实施例之间的技术方案可以相互结合，但是必须是以本领域普通技术人员能够实现为基础，当技术方案的结合出现相互矛盾或无法实现时应当认为这种技术方案的结合不存在，也不在本发明要求的保护范围之内。

针对上述背景技术中的挑战，本发明提出了一个基于K-framework的智能合约安全类型验证框架，该框架在定义形式化分析工具方面具有固有的优势。本发明的框架可以自动检测一个智能合约的信息流是否符合完整性(由于以太坊的开放性，大多数智能合约的数据和交易都是对公众开放的，所以在本发明中没有考虑机密性)策略，该策略由不干涉属性描述，即要求Trusted(T)变量永远不会被Untrusted(U)变量篡改。将原始合约作为输入，本发明的框架可以在两方面提供帮助：1)通过对合约中变量的安全类型进行手动注释，本发明的框架能够通过提出的可靠类型检查器(STC)检测安全信息流是否满足完整性。2)如果没有手工标注，本发明的框架能够寻找变量的安全类型分配使得合约满足完整性策略。如果找不到这样的类型分配，则该合约被证明是不安全的。特别是，在诊断智能合约的潜在安全漏洞时，本发明的工具能够定位合约中哪些函数、语句违反完整性策略。

在一个实施例中，针对以太坊下Solidity智能合约，提供了一种基于类型检测的智能合约信息流完整性验证方法，结合图1，所述方法包括以下步骤：

步骤1，为智能合约编程语言Solidity构建形式化语法、语义；

步骤2，构建智能合约的安全类型系统STC，用于检测智能合约信息流完整性；

步骤3，构建基于智能合约类型系统STC的类型验证器STV，自动为智能合约的状态变量寻找最优安全类型分配，即状态变量中被分配为可信的数量最多，使得智能合约满足信息流完整性。这里，因为当使用STC对智能合约的信息流执行类型检测，用户可能并不总是要求智能合约中哪些状态变量应该存储可信信息，并且用户很难手动找到最优安全类型分配可以使智能合约是良好类型，本发明提出一个安全类型验证器STV。STV可以自动生成智能合约中的所有安全类型分配，并通过STC执行类型检测，直到找到最小数目U的安全类型分配，即最优安全类型分配。

进一步地，在其中一个实施例中，步骤1中所述构建形式化语法，具体包括：

(1)将Solidity语言抽象为短语，这些短语为表达式或语句；

Solidity的表达式包括8种类型：值v、全局变量g、状态变量id、表达式组

|NewExp|OperatorExp

|IndexAccess|MemberAccess

NewExp：：＝new id

OperatorExp：：＝op

IndexAccess：：＝exp[]|exp

MemberAccess：：＝exp.id|exp.IndexAccess

其中，new为实例化合约的标识符，op

智能合约的语句包括3种类型：简单语句SimpleStmt、语句块BlockStmt和语句序列；其中，SimpleStmt表示单个基本语句，包括函数调用FunctionCall、普通赋值语句exp

(Statements)stmt：：＝SimpleStmt；|BlockStmt

|stmt

SimpleStmt：：＝FunctionCall|exp

|exp op＝FunctionCall

LowLevelCall：：＝call|delegatecall|callcode

BlockStmt：：＝if(exp)then stmt

|while(exp)stmt

|letvar id op＝exp in stmt

|require(exp)in stmt

|{stmt}

其中，id

(2)在Solidity编写的智能合约中，函数类型分为普通函数normalfunction、构造函数constructor和回退函数fallback function；一个智能合约有且只有一个未命名的fallback function，其不能有输入或输出参数，并且必须有external可见性；其中，普通函数normal function的语法定义如下：

式中，id

构造函数constructor与普通函数normal function的区别在于：id

回退函数fallback function的语法定义如下：

fun

(3)智能合约包括状态变量声明和函数声明，其语法的定义如下：

(Contracts)ctr：：＝contract id{ctrPart}

ctrPart：：＝letvar id op＝exp|fun|ctrPart ctrPart

步骤1中所述构建形式化语义具体包括：

Solidity的操作语义如图2所示。

(1)Solidity的表达式的操作语义形式为

这里示例性地，解释了

(2)Solidity的语句的操作语义形式为

这里示例性地，解释了FunctionCall、exp op＝FunctionCall和require语句的语义。FunctionCall根据不同类型的函数调用有不同的语义规则。例如，规则(E-FC1)和(E-FC4)分别捕获内部函数调用和外部委托函数调用的语义。这两个规则表明，如果id

进一步地，在其中一个实施例中，步骤2所述构建智能合约的安全类型系统STC，具体包括：

1)构建STC安全类型

由≤偏序排序的短语安全类型分层如下：

(Expression types)τ：：＝T|U

(Phrase types)ρ：：＝τ|τ var|τ stmt

式中，τ为Solidity表达式的安全类型，ρ为Solidity短语的安全类型，包括表达式安全类型、变量安全类型τ var和语句安全类型τ stmt。

本方法用

变量安全类型τ var存储安全类型为τ或更低的信息。语句安全类型τ stmt指定语句中的每个赋值都是对安全类型为τ或更高的变量进行的。特别地，⊥var类型的变量不能存储具有安全类型的信息，而

函数的安全类型为：

2)构建STC安全类型规则。在本发明的类型系统中，有三种安全类型规则可以分别用于表达式、语句和函数。所有这些规则都由一个函数类型表FT隐式参数化，FT将所有函数名映射为函数安全类型。值得注意的是，本发明还为表达式和语句引入了子类型规则(S-Var-Exp)、(S-Sub-Exp)和(S-Sub-Stmt)，以避免标签升级。

STC安全类型规则如图3所示。

(1)Solidity表达式的安全类型规则的形式为：

大多数表达式的安全类型规则都很直观，示例性地，Solidity表达式的安全类型规则包括：

规则

规则(S-NExp)：描述了NewExp的安全类型规则，表示NewExp在Γ中具有最低的安全类型⊥，因为它等价于新的智能合约地址，应该是最可信的；

规则(S-op-u)和(S-op-b)：描述了OperatorExp的安全类型规则，其表明如果OperatorExp中的所有表达式在Γ中都是安全类型τ，那么这两个规则都类型化OperatorExp为τ；

规则(S-IA1)：描述了exp[]的安全类型规则，其类型化exp[]为Γ中exp的安全类型；

规则(S-IA2)描述了exp1[exp2]的安全类型规则，其类型化exp

规则(S-MA1)和(S-MA2)：描述了MemberAccess的安全类型规则，其都将MemberAccess类型化为MemberAccess中表达式类型的最小上界。

(2)Solidity语句的安全类型规则的形式为：

示例性地，Solidity语句的安全类型规则包括：

FunctionCall根据其语义有5种类型规则，规则(S-FC1)至规则(S-FC5)。规则(S-FC1)和(S-FC4)指定，如果id

类似地，exp op＝FunctionCall也有5种类型规则。因为exp op＝FunctionCall和FunctionCall的主要区别是前者更新exp的值。规则(S-op-FC2),(S-op-FC3)和(S-op-FC5)类型化exp op＝FunctionCall为

(3)函数的安全类型规则的形式为：

3)STC的可靠性证明

对STC的安全类型规则进行验证，证明其满足不干扰属性，以此得证能被STC证明是类型良好的合约是满足信息流完整性的。

进一步地，在其中一个实施例中，为了验证STC的可靠性，本发明假设Solidity短语是封闭的，这意味着没有自由标识符。本发明假设如果观察者的观察能力是τ

所述STC的可靠性证明，具体过程包括：

步骤2-1，给定定义1用于描述智能合约的良好类型属性，给定定义2用于描述不可分辨关系，具体定义如下：

定义1.假设S是一个由有限函数组成的智能合约，由FD和FT分别作为S的函数声明表和函数类型表；在S中声明的每个fun都具有函数类型，即

定义2.给定两个求值环境μ

步骤2-2，基于上述良好类型属性及不可分辨关系，建立引理1及引理2支持STC的可靠性证明；引理1及引理2的具体描述如下：

引理1.假定

这里示例性地，给出引理1针对规则(S-IA2)的证明。

证明：本发明有规则(S-IA2)。因为

引理2.假定

这里示例性地，给出引理2针对规则(S-op-FC4)的证明。

证明：因为

这里，本发明通过建立上面所示的两个引理来支持可靠性证明。直观地说，这些引理的证明是通过对

步骤2-3，基于引理1及引理2，给定定义3用于描述Solidity语句的不干涉性(因为证明安全类型系统的可靠性本质上是证明类型系统强制执行不干涉属性)，给定定义4用于描述Solidity智能合约的不干涉性，具体定义如下：

定义3.一个智能合约语句stmt在智能合约中执行的语句S是满足不干涉属性的，当且仅当：假设有

定义4.一个智能合约在S中是不干涉的，当且仅当：在S中执行的所有智能合约语句都是满足不干涉属性的；

步骤2-4，基于引理1～2及定义1～4，给定引理3的描述如下：

引理3.假定

这里，引理3中STC的可靠性被表述为语句的不干涉属性，它的证明是通过对exp和stmt进行归纳法同时对

这里示例性地，给出引理3针对规则(S-op-FC4)的证明。

证明：因为规则(S-op-FC4)和分别在μ

情况1：

情况2：

步骤2-5，基于引理1～3，给定定理1用于说明良好类型的智能合约是满足不干扰属性的，具体描述如下：

定理1.如果由有限函数组成的智能合约S是类型良好的，那么它是满足不干扰属性的。

证明：通过引理3，得证良好类型的智能合约是满足不干涉属性的，即满足信息流完整性。

进一步地，在其中一个实施例中，步骤3所述构建基于智能合约类型系统STC的类型验证器STV，自动为合约的状态变量寻找最优安全类型分配，具体过程包括：

步骤3-1，依据步骤2中对STC的可靠性证明及智能合约的状态变量个数，定义智能合约的安全类型分配的格结构，用于自动生成智能合约中的所有安全类型分配，具体定义如下：

给定智能合约S，其带有n个状态变量的集合V，给定两种安全类型T和U，安全类型分配t是V中所有状态变量的安全类型的组合；用

步骤3-2，基于智能合约的安全类型分配的格结构和STC，采用基于STC的类型验证器算法执行类型检测，直到找到最小数目U的安全类型分配，即最优安全类型分配；其中基于STC的类型验证器算法具体如下：

输入：智能合约S，包含n个状态变量。

输出：一个安全类型分配t使S是良好类型的：

假设

对

对所有属于

计算完毕后，如果S是类型良好的，则输出t，否则输出无解。

定理2.类型验证器算法会给出最优解。

证明：由于

在一个实施例中，提供了一种基于类型检测的智能合约信息流完整性验证系统，所述系统包括：

第一构建模块，用于为智能合约编程语言构建形式化语法、语义；

第二构建模块，用于构建智能合约的安全类型系统STC，用于检测智能合约信息流完整性；

第三构建模块，用于构建基于智能合约类型系统STC的类型验证器STV，自动为智能合约的状态变量寻找最优安全类型分配，即状态变量中被分配为可信的数量最多，使得智能合约满足信息流完整性。

关于基于类型检测的智能合约信息流完整性验证系统的具体限定可以参见上文中对于基于类型检测的智能合约信息流完整性验证方法的限定，在此不再赘述。上述基于类型检测的智能合约信息流完整性验证系统中的各个模块可全部或部分通过软件、硬件及其组合来实现。上述各模块可以硬件形式内嵌于或独立于计算机设备中的处理器中，也可以以软件形式存储于计算机设备中的存储器中，以便于处理器调用执行以上各个模块对应的操作。

在一个实施例中，提供了一种计算机设备，包括存储器、处理器及存储在存储器上并可在处理器上运行的计算机程序，处理器执行计算机程序时实现以下步骤：

步骤1，为智能合约编程语言构建形式化语法、语义；

步骤2，构建智能合约的安全类型系统STC，用于检测智能合约信息流完整性；

步骤3，构建基于智能合约类型系统STC的类型验证器STV，自动为智能合约的状态变量寻找最优安全类型分配，即状态变量中被分配为可信的数量最多，使得智能合约满足信息流完整性。

关于每一步的具体限定可以参见上文中对于基于类型检测的智能合约信息流完整性验证方法的限定，在此不再赘述。

在一个实施例中，提供了一种计算机可读存储介质，其上存储有计算机程序，计算机程序被处理器执行时实现以下步骤：

步骤1，为智能合约编程语言构建形式化语法、语义；

步骤2，构建智能合约的安全类型系统STC，用于检测智能合约信息流完整性；

步骤3，构建基于智能合约类型系统STC的类型验证器STV，自动为智能合约的状态变量寻找最优安全类型分配，即状态变量中被分配为可信的数量最多，使得智能合约满足信息流完整性。

关于每一步的具体限定可以参见上文中对于基于类型检测的智能合约信息流完整性验证方法的限定，在此不再赘述。

作为一种具体示例，在其中一个实施例中，对本发明进行进一步验证说明。本实施例以一个简化的奇偶校验多签名钱包智能合约为例，采用STC检测合约的信息流完整性，并采用STV自动寻找该合约的最优安全类型分配。

如图5所示，在奇偶校验多签名钱包中，智能合约Wallet利用了智能合约库WalletLibrary提供的共享服务。例如，在部署合约Wallet时，它的构造函数将初始化任务委托给WalletLibrary中提供的函数initWallet()，以设置钱包的所有者为_owner。值得注意的是，Wallet和WalletLibrary具有相同的状态变量owner，因此当委托WalletLibrary设置owner(第5行)时，实际被更新的变量是Wallet的owner(第11行)。基于WalletLibrary库的设计，initWallet()函数应该只被想要使用WalletLibrary的合约实例的构造函数调用一次。

在Solidity中，允许开发人员定义一个特殊的函数，称为“回退函数”。合约的回退函数没有名称，如果有对该合约的函数调用，但是该合约没有提供匹配的函数，回退函数将被执行。例如，Wallet合约有一个回退函数，如图5中行27～29所示。这个回退函数的作用是，当有一个对Wallet合约的函数调用，而Wallet没有提供该函数时，Wallet将该函数调用委托给WalletLibrary来执行该函数调用。

攻击者可以基于此机制利用漏洞。省略了技术细节，但在高层次上总结了攻击如下：攻击者通过调用initWallet(attk_addr)到Wallet合约来执行一个交易，其中attk_addr是攻击者的地址。值得注意的是，这个函数调用及其参数是在msg.data中编译和封装的。由于Wallet合约没有提供任何名为initWallet的函数，因此回退函数将被调用，initWallet(attk_addr)将被委托给WalletLibrary来执行(第28行)。然后，钱包的主人就变成了攻击者。

上述漏洞是一种典型的信息流完整性破坏。从完整性的角度来看，owner变量应该被注释为可信的。因为在创建(部署)钱包时，initWallet函数应该只执行一次，所以钱包的所有者应该始终是可信合约的创建者。然而，initWallet函数的public可见性意味着initWallet函数的参数应该被注释为不可信。因此，当不受信任的用户通过delegatecall从init Wallet合约中的回退函数调用delegatecall时，init Wallet函数中的赋值会导致不受信任的_owner变量篡改可信的owner变量。这直接导致了完整性的破坏。因为这种脆弱性的根源来自于init Wallet函数的可见性，这个错误很容易修正，若将init Wallet函数的可见性改为intemal，就可以防止initWallet的执行通过delegatecall改变钱包的所有者。通过检查智能合约信息流的完整性，可以很容易地发现和消除这些漏洞。

1、STC检测合约的信息流完整性

为了更清楚地说明STC类型检测可以很容易地检测到奇偶性多签名钱包攻击，具体实施细节如下。首先，使用安全类型对合约Wallet和WalletLibrary中的变量进行注释。由于用户不希望钱包的所有者被攻击者篡改，所以使用T分配给所有owner和m_owners变量。由于变量_walletLib是在构造函数中创建新WalletLibrary合约的地址，因此可以认为该变量在默认情况下被赋值后是不可变的，并且在Wallet合约中也使用T分配。除了所有的状态变量外，还应该使用安全类型分配全局变量。全局变量的安全类型应该根据特定的条件来分配。例如，如果在构造函数中使用全局变量，则应该使用T分配给它们，在其他情况下，应该使用U分配给它们。这是有意义的，因为合约创建者(例如攻击者)可能不会调用构造函数中没有的全局变量。因此,msg.data和Wallet.fallback使用U分配。

通过STC类型检查的分析，给出了函数Wallet.init Wallet和Wallet.fallback的类型推导，如图6所示。因为msg.data不可信，规则(S-FC4)类型化函数Wallet.init Wallet中的_owner为U(因为Γ(msg.data)应该小于等于Γ(_owner))。但是，函数Wallet.initWallet中的语句owner＝_owner不是良好类型的，因为它将不可信的_owner分配给可信的owner，这违反了规则(S-op-＝)。因此，Wallet.initWallet和Wallet.fallback的类型无法得到，这意味着合约Wallet不是良好类型的，即违反了信息流完整性。

2、STV自动寻找该合约的最优安全类型分配

为了展示STV类型验证器如何在奇偶性多签名钱包攻击中工作，提供了原始合约Wallet的格结构，如图7所示。在安全类型分配中，分配变量的顺序为:owner、_walletLib和m_owners。通过应用STC，可以获悉UUU、UUT、UTU和UTT这样的类型分配可以使合约Wallet类型良好，类型验证器算法找到的最优组合是UTT。然而，就用户需求而言，希望当owner被分配为T时，该合约仍然是类型良好的。通过STV，可以明显看出原来的合约不能满足用户的需求。

现有的针对奇偶性多签名钱包攻击的改进方法，如将initWallet函数的可见性更改为intemal，可以防止任意的外部委托对调用者合约的状态变量的篡改。同样，修改后的合约的格结构如图8所示。通过应用STV，所有8(2

以上显示和描述了本发明的基本原理、主要特征及优点。本行业的技术人员应该了解，本发明不受上述实施例的限制，上述实施例和说明书中描述的只是说明本发明的原理，在不脱离本发明精神和范围的前提下，本发明还会有各种变化和改进，这些变化和改进都落入要求保护的本发明范围内。本发明要求保护范围由所附的权利要求书及其等效物界定。