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

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


背景技术：

2.智能合约是运行在区块链(例如，以太坊)上的计算机程序，不需要外部可信的权威机构。它们被证明适用于许多领域，包括拍卖、选举、商业和游戏。数据显示，智能合约最近已经变得无处不在，数量急剧增加。然而，如何保证智能合约的安全性是一个挑战。首先，它们通常是在上市时间的压力下开发的，可能充满安全漏洞，或者可能被网络罪犯利用，窃取加密货币和其他数字资产。其次，它们是可以与复杂环境(例如，用户和其他智能合约)交互的程序。在部署不安全的智能合约时，区块链的性质导致不可逆转的破坏。例如，2016年6月dao合约利用递归漏洞使得1.5亿美元被盗，2017年7月多签名钱包利用函数可见性说明符使得3100万美元被盗，和几个月后在同一钱包由于错误使用delegatecall使得3亿美元被冻结。
3.为了应对这一挑战，许多技术已经扩展和应用到创建安全合约或检测恶意合约上。例如，使用有限状态机与严格语义跟踪智能合约的行为，以防止常见漏洞；使用形式化evm(以太虚拟机)定义来定理证明智能合约中的安全属性，形式化方法可以为evm字节码提供强大的形式化验证保证，但完全自动化形式化验证方法并非易事；使用模糊测试通过生成合约交易序列来检测合约中潜在的漏洞，但模糊测试方法需要一个模拟的执行环境。保持信息流的完整性可能会阻止可信域被不可信数据篡改。实现程序信息流完整性的一种方法是通过基于语言的安全方法，例如，为信息流使用类型系统。在安全类型语言中，通过指定所有程序变量和表达式的类型，可以在编译时强制执行安全策略。然而，为智能合约开发类型检查器并不简单。首先，solidity的语法比简单的命令式语言更复杂，这使得它不可能使用现有的类型检查器。例如，为了与不遵守abi的合约交互，或者为了获得更直接的控制，在solidity中提供了唯一的函数操作callcode和delegatecall。其次，许多类型系统只在不干涉属性上执行可靠性证明，而没有自动类型推断的工具。手动执行类型推断很容易出错，而且可能无法处理大规模的智能合约。此外，基于对现有合约的分析，用户迫切需要工具来检测合约中哪些状态变量是可信的(可信的)，以便存储不能被篡改的信息。


技术实现要素：

4.本发明的目的在于针对上述现有技术存在的问题，解决以太坊区块链环境下智能合约潜在的信息篡改问题，提供一种基于类型检测的智能合约信息流完整性验证方法。
5.实现本发明目的的技术解决方案为：一种基于类型检测的智能合约信息流完整性验证方法，所述方法包括以下步骤：
6.步骤1，为智能合约编程语言构建形式化语法、语义；
7.步骤2，构建智能合约的安全类型系统stc，用于检测智能合约信息流完整性；
8.步骤3，构建基于智能合约类型系统stc的类型验证器stv，自动为智能合约的状态变量寻找最优安全类型分配，即状态变量中被分配为可信的数量最多，使得智能合约满足信息流完整性。
9.进一步地，步骤1中所述构建形式化语法，具体包括：
10.(1)将智能合约编程语言抽象为短语，这些短语为表达式或语句；
11.智能合约的表达式包括8种类型：值v、全局变量g、状态变量id、表达式组智能合约实例表达式newexp、操作表达式operatorexp、智能合约数组或映射表达式indexaccess，和自定义类型的数据字段访问表达式memberaccess；智能合约表达式的语法定义如下：
[0012][0013]
|newexp|operatorexp
[0014]
|indexaccess|memberaccess
[0015][0016]
newexp：：＝new id
c
()
[0017]
operatorexp：：＝op
u exp|exp
1 op
b exp2[0018]
indexaccess：：＝exp[]|exp1[exp2]
[0019]
memberaccess：：＝exp.id|exp.indexaccess
[0020]
其中，new为实例化合约的标识符，op
u
为一元操作符，op
b
为二元操作符，id
c
为合约名称变量；
[0021]
智能合约的语句包括3种类型：简单语句simplestmt、语句块blockstmt和语句序列；其中，simplestmt表示单个基本语句，包括函数调用functioncall、普通赋值语句exp1op＝exp2和接收函数调用返回值的赋值语句exp op＝functioncall；blockstmt表示一个语句块，包括分支结构语句if(exp)then stmt
1 else stmt2、重复语句while(exp)stmt、变量定义语句letvar id op＝exp in stmt、需求语句require(exp)in stmt和一个花括号语句块{stmt}；函数调用functioncall包括三种类型：内部函数调用外部函数调用和底层函数调用底层函数调用包括三类：call底层函数调用delegatecall底层函数调用和callcode底层函数调用智能合约语句的语法定义如下：
[0022]
(statements)stmt：：＝simplestmt；|blockstmt
[0023]
|stmt
1 stmt2[0024]
simplestmt：：＝functioncall|exp1op＝exp2[0025]
|exp op＝functioncall
[0026][0027][0028]
[0029]
lowlevelcall：：＝call|delegatecall|callcode
[0030]
blockstmt：：＝if(exp)then stmt
1 else stmt2[0031]
|while(exp)stmt
[0032]
|letvar id op＝exp in stmt
[0033]
|require(exp)in stmt
[0034]
|{stmt}
[0035]
其中，id
f
为函数名称变量，op＝为赋值操作符；
[0036]
(2)在编写的智能合约中，函数类型分为普通函数normal function、构造函数constructor和回退函数fallbackfunction；一个智能合约有且只有一个未命名的fallback function，其不能有输入或输出参数，并且必须有external可见性；其中，普通函数normal function的语法定义如下：
[0037][0038]
式中，id
c
表示智能合约的名称，id
f
表示函数的名称，表示函数的输入参数，表示函数的输出参数，q表示函数的可见性；
[0039]
构造函数constructor与普通函数normal function的区别在于：id
f
被关键字constructor替换；
[0040]
回退函数fallback function的语法定义如下：
[0041]
fun
f
：：＝id
c
.function()external{stmt}
[0042]
(3)智能合约包括状态变量声明和函数声明，其语法的定义如下：
[0043]
(contracts)ctr：：＝contract id{ctrpart}
[0044]
ctrpart：：＝letvar id op＝exp|fun|ctrpart ctrpart
[0045]
步骤1中所述构建形式化语义具体包括：
[0046]
(1)智能合约的表达式的操作语义形式为声明表达式exp在求值环境μ中计算为值v；同时使用dom(μ)和ran(μ)分别表示μ的定义域和值域；并假设按合约名索引的表ca存储newexp的地址，以模拟随机合约地址；
[0047]
(2)智能合约的语句的操作语义形式为其中μ，μ
′
分别为执行语句stmt之前和之后的求值环境，s表示stmt所属的调用方智能合约；同时假设函数定义存储在按函数名索引的表fd中。
[0048]
进一步地，步骤2所述构建智能合约的安全类型系统stc，具体包括：
[0049]
1)构建stc安全类型
[0050]
由≤偏序排序的短语安全类型分层如下：
[0051]
(expression types)τ::＝t|u
[0052]
(phrase types)ρ：：＝τ|τ var|τ stmt
[0053]
式中，τ为solidity表达式的安全类型，ρ为solidity短语的安全类型，包括表达式安全类型、变量安全类型τ var和语句安全类型τ stmt，t、u分别为可信和不可信；变量安全类型τ var存储安全类型为τ或更低的信息，语句安全类型τ stmt指定语句中的每个赋值都是对安全类型为τ或更高的变量进行的；函数的安全类型为：其中
和τ
′
都属于都属于表示表达式安全类型集，1≤i≤n，表示输入参数的安全类型，τ
′
stmt表示函数体的安全类型，表示返回变量的安全类型，若函数中没有参数，可将参数的安全类型省略为_；
[0054]
2)构建stc安全类型规则，包括：
[0055]
(1)智能合约表达式的安全类型规则的形式为：其中ρ是表达式exp在短语安全类型环境γ的安全类型；
[0056]
(2)智能合约语句的安全类型规则的形式为：其中ρ是表达式exp在短语安全类型环境γ和stmt所属的调用方智能合约s下的安全类型；
[0057]
(3)函数的安全类型规则的形式为：表示函数的输入参数和返回变量的类型分别最多为和同时，函数体中的每个赋值都是对安全类型至少为τ
′
的变量进行的；
[0058]
3)stc的可靠性证明
[0059]
对stc的安全类型规则进行验证，证明其满足不干扰属性，以此得证能被stc证明是类型良好的合约是满足信息流完整性的。
[0060]
进一步地，所述stc的可靠性证明，具体过程包括：
[0061]
步骤2
‑
1，给定定义1用于描述智能合约的良好类型属性，给定定义2用于描述不可分辨关系，具体定义如下：
[0062]
定义1.假设s是一个由有限函数组成的智能合约，由fd和ft分别作为s的函数声明表和函数类型表；在s中声明的每个fun都具有函数类型，即是可派生的；
[0063]
定义2.给定两个求值环境μ1、μ2，类型环境γ，安全类型τ0，的定义如下：
[0064][0065]
步骤2
‑
2，基于上述良好类型属性及不可分辨关系，建立引理1及引理2支持stc的可靠性证明；引理1及引理2的具体描述如下：
[0066]
引理1.假定如果τ≤τ0，和那么v1＝v2；
[0067]
引理2.假定如果那么
[0068]
步骤2
‑
3，基于引理1及引理2，给定定义3用于描述solidity语句的不干涉性，给定定义4用于描述solidity智能合约的不干涉性，具体定义如下：
[0069]
定义3.一个智能合约语句stmt在智能合约中执行的语句s是满足不干涉属性的，当且仅当：假设有当且仅当：假设有dom(γ)＝dom(μ1)＝dom(μ2)和那么
[0070]
定义4.一个智能合约在s中是不干涉的，当且仅当：在s中执行的所有智能合约语句都是满足不干涉属性的；
[0071]
步骤2
‑
4，基于引理1～2及定义1～4，给定引理3的描述如下：
[0072]
引理3.假定如果和那么
[0073]
步骤2
‑
5，基于引理1～3，给定定理1用于说明良好类型的智能合约是满足不干扰属性的，具体描述如下：
[0074]
定理1.如果由有限函数组成的智能合约s是类型良好的，那么它是满足不干扰属性的。
[0075]
进一步地，步骤3所述构建基于智能合约类型系统stc的类型验证器stv，自动为合约的状态变量寻找最优安全类型分配，具体过程包括：
[0076]
步骤3
‑
1，依据步骤2中对stc的可靠性证明及智能合约的状态变量个数，定义智能合约的安全类型分配的格结构，用于自动生成智能合约中的所有安全类型分配，具体定义如下：
[0077]
给定智能合约s，其带有n个状态变量的集合v，给定两种安全类型t和u，安全类型分配t是v中所有状态变量的安全类型的组合；用表示非线性有序格结构，该结构由状态变量的2
n
安全类型分配的有限集和类型分配对上的流关系
→
组成；给定两种类型分配t1，t2，在中，t1→
t2表示当且仅当由t1分配的所有变量的安全类型相应地小于或等于由t2分配的安全类型；
[0078]
步骤3
‑
2，基于智能合约的安全类型分配的格结构和stc，采用基于stc的类型验证器算法执行类型检测，直到找到最小数目u的安全类型分配，即最优安全类型分配；其中基于stc的类型验证器算法具体如下：
[0079]
输入：智能合约s，包含n个状态变量。
[0080]
输出：一个安全类型分配t使s是良好类型的：
[0081]
假设是n个状态变量的格结构；
[0082]
对应用拓扑排序；
[0083]
对所有属于的安全类型分配t，使用stc检测s的信息流；
[0084]
计算完毕后，如果s是类型良好的，则输出t，否则输出无解。
[0085]
一种基于类型检测的智能合约信息流完整性验证系统，所述系统包括：
[0086]
第一构建模块，用于为智能合约编程语言构建形式化语法、语义；
[0087]
第二构建模块，用于构建智能合约的安全类型系统stc，用于检测智能合约信息流完整性；
[0088]
第三构建模块，用于构建基于智能合约类型系统stc的类型验证器stv，自动为智能合约的状态变量寻找最优安全类型分配，即状态变量中被分配为可信的数量最多，使得智能合约满足信息流完整性。
[0089]
一种计算机设备，包括存储器、处理器及存储在存储器上并可在处理器上运行的计算机程序，处理器执行计算机程序时实现以下步骤：
[0090]
步骤1，为智能合约编程语言构建形式化语法、语义；
[0091]
步骤2，构建智能合约的安全类型系统stc，用于检测智能合约信息流完整性；
[0092]
步骤3，构建基于智能合约类型系统stc的类型验证器stv，自动为智能合约的状态
变量寻找最优安全类型分配，即状态变量中被分配为可信的数量最多，使得智能合约满足信息流完整性。
[0093]
一种计算机可读存储介质，其上存储有计算机程序，计算机程序被处理器执行时实现以下步骤：
[0094]
步骤1，为智能合约编程语言构建形式化语法、语义；
[0095]
步骤2，构建智能合约的安全类型系统stc，用于检测智能合约信息流完整性；
[0096]
步骤3，构建基于智能合约类型系统stc的类型验证器stv，自动为智能合约的状态变量寻找最优安全类型分配，即状态变量中被分配为可信的数量最多，使得智能合约满足信息流完整性。
[0097]
本发明与现有技术相比，其显著优点为：1)结合了类型检测在安全信息流检查中的优点，可以对智能合约源代码的信息流完整性进行有效的分析与验证，减少了智能合约在开发过程中出现可信信息被篡改的概率；2)提出了一个基于k
‑
framework的智能合约安全类型验证框架，可以自动检测一个智能合约的信息流是否符合完整性策略，该策略由不干涉属性描述，即要求trusted(t)变量永远不会被untrusted(u)变量篡改；3)将原始合约作为输入，并且对合约中变量的安全类型进行手动注释，本发明通过提出的框架中的可靠类型检查器(stc)可以检测安全信息流是否满足完整性；4)将原始合约作为输入，并且不对合约中变量的安全类型进行手动注释，本发明的框架能够寻找变量的安全类型分配使得合约满足完整性策略；如果找不到这样的类型分配，则该合约被证明是不安全的；5)特别地，在诊断智能合约的潜在安全漏洞时，本发明的工具能够定位合约中哪些函数、语句违反完整性策略。
[0098]
下面结合附图对本发明作进一步详细描述。
附图说明
[0099]
图1为一个实施例中基于类型检测的智能合约信息流完整性验证方法流程图。
[0100]
图2为一个实施例中solidity形式化操作语义示例图。
[0101]
图3为一个实施例中solidity安全类型规则示例图。
[0102]
图4为一个实施例中安全类型分配的格结构示意图。
[0103]
图5为一个实施例中奇偶校验多签名钱包攻击示例图。
[0104]
图6为一个实施例中基于stc的奇偶校验多签名钱包攻击类型推导示例图。
[0105]
图7为一个实施例中奇偶校验多签名钱包攻击原始代码的安全类型分配格结构示意图。
[0106]
图8为一个实施例中修正后的奇偶校验多签名钱包攻击原始代码的安全类型分配格结构示意图。
具体实施方式
[0107]
为了使本申请的目的、技术方案及优点更加清楚明白，以下结合附图及实施例，对本申请进行进一步详细说明。应当理解，此处描述的具体实施例仅仅用以解释本申请，并不用于限定本申请。
[0108]
需要说明的是，若本发明实施例中有涉及“第一”、“第二”等的描述，则该“第一”、
[0123]
indexaccess：：＝exp[]|exp1[exp2]
[0124]
memberaccess：：＝exp.id|exp.indexaccess
[0125]
其中，new为实例化合约的标识符，op
u
为一元操作符，op
b
为二元操作符，id
c
为合约名称变量；
[0126]
智能合约的语句包括3种类型：简单语句simplestmt、语句块blockstmt和语句序列；其中，simplestmt表示单个基本语句，包括函数调用functioncall、普通赋值语句exp
1 op＝exp2和接收函数调用返回值的赋值语句exp op＝functioncall；blockstmt表示一个语句块，包括分支结构语句if(exp)then stmt
1 else stmt2、重复语句while(exp)stmt、变量定义语句letvar id op＝exp in stmt、需求语句require(exp)in stmt和一个花括号语句块{stmt}；函数调用functioncall包括三种类型：内部函数调用外部函数调用和底层函数调用底层函数调用包括三类：call底层函数调用delegatecall底层函数调用和callcode底层函数调用solidity语句的语法定义如下：
[0127]
(statements)stmt：：＝simplestmt；|blockstmt
[0128]
|stmt
1 stmt2[0129]
simplestmt：：＝functioncall|exp1op＝exp2[0130]
|exp op＝functioncall
[0131][0132][0133][0134]
lowlevelcall：：＝call|delegatecall|callcode
[0135]
blockstmt：：＝if(exp)then stmt
1 else stmt2[0136]
|while(exp)stmt
[0137]
|letvar id op＝exp in stmt
[0138]
|require(exp)in stmt
[0139]
|{stmt}
[0140]
其中，id
f
为函数名称变量，op＝为赋值操作符；
[0141]
(2)在solidity编写的智能合约中，函数类型分为普通函数normalfunction、构造函数constructor和回退函数fallback function；一个智能合约有且只有一个未命名的fallback function，其不能有输入或输出参数，并且必须有external可见性；其中，普通函数normal function的语法定义如下：
[0142][0143]
式中，id
c
表示智能合约的名称，id
f
表示函数的名称，表示函数的输入参数，表示函数的输出参数，q表示函数的可见性。在solidity中，有四种可见性：external、public、internal和private。stmt表示函数体，表示保存函数返回值的本地变量。和
是作用域内的变量。(本发明只考虑封闭函数(closed function)，即在stmt中被处理的变量要么是由letvar引入的，要么是从集合引入的。)
[0144]
构造函数constructor与普通函数normal function的区别在于：id
f
被关键字constructor替换；
[0145]
回退函数fallback function的语法定义如下：
[0146]
fun
f
：：＝id
c
.function()external{stmt}
[0147]
(3)智能合约包括状态变量声明和函数声明，其语法的定义如下：
[0148]
(contracts)ctr：：＝contract id{ctrpart}
[0149]
ctrpart：：＝letvar id op＝exp|fun|ctrpart ctrpart
[0150]
步骤1中所述构建形式化语义具体包括：
[0151]
solidity的操作语义如图2所示。
[0152]
(1)solidity的表达式的操作语义形式为声明表达式exp在求值环境μ中计算为值v；同时使用dom(μ)和ran(μ)分别表示μ的定义域和值域；并假设按合约名索引的表ca存储newexp的地址，以模拟随机合约地址；solidity表达式的操作语义不会造成副作用，并且大多数表达式的操作语义都很直观。
[0153]
这里示例性地，解释了newexp、operatorexp、indexaccess和memberaccess的语义。规则描述了的语义，表明如果每个表达式exp
i
(1≤i≤n)在μ中求值为v
i
，那么在μ中求值为规则(e
‑
nexp)描述了newexp的语义，该语义表示如果新智能合约实例的值v(合约地址)没有出现在求值环境的值域内，则newexp的值为v。规则(e
‑
op
‑
u)和(e
‑
op
‑
b)描述了operatorexp的语义，它们表示如果μ中的表达式求值为相应的值，则操作符op
u
和op
b
将对这些值执行操作。规则(e
‑
ia1)和(e
‑
ia2)捕获indexaccess的语义。这两个规则说明，如果μ中的表达式求值为相应的值，那么由这些表达式在μ中组成的数组/映射将求值为由这些值组成的数组/映射。规则(e
‑
ma1)和(e
‑
ma2)描述了memberaccess的语义，它们表示如果μ中的表达式求值为相应的值，则由这些表达式在μ中形成的数据字段访问求值为由这些值形成的数据字段访问。
[0154]
(2)solidity的语句的操作语义形式为其中μ，μ
′
分别为执行语句stmt之前和之后的求值环境，s表示stmt所属的调用方智能合约；同时假设函数定义存储在按函数名索引的表fd中。solidity语句的操作语义不会产生值，并且大多数solidity语句的操作语义都很直观。
[0155]
这里示例性地，解释了functioncall、exp op＝functioncall和require语句的语义。functioncall根据不同类型的函数调用有不同的语义规则。例如，规则(e
‑
fc1)和(e
‑
fc4)分别捕获内部函数调用和外部委托函数调用的语义。这两个规则表明，如果id
f
在函数体中有stmt，那么由stmt在被调用智能合约(碰巧是调用方智能合约)的上下文中获得的更新的μ也是函数调用的更新的求值环境。但是，规则(e
‑
fc2)、(e
‑
fc3)和(e
‑
fc5)没有更新的求值环境，因为在这些函数调用的调用方智能合约中stmt没有被执行。类似地，exp op＝functioncall也有5种语义规则，具体取决于5种函数调用类型。以规则(e
‑
op
‑
fc1)为例：它捕获了的语义。除了更新像规则(e
‑
fc1)这样的环境之外，x的值也更新为函数调用的返回值。require语句的语义由规则(e
‑
req
‑
t)和(e
‑
req
‑
f)给出。规则表明如
果exp为真，则require语句中的stmt更新μ；否则，μ保持不变。
[0156]
进一步地，在其中一个实施例中，步骤2所述构建智能合约的安全类型系统stc，具体包括：
[0157]
1)构建stc安全类型
[0158]
由≤偏序排序的短语安全类型分层如下：
[0159]
(expression types)τ：：＝t|u
[0160]
(phrase types)ρ：：＝τ|τ var|τ stmt
[0161]
式中，τ为solidity表达式的安全类型，ρ为solidity短语的安全类型，包括表达式安全类型、变量安全类型τ var和语句安全类型τ stmt。
[0162]
本方法用表示表达式安全类型集，其中最高的表达式类型标记为最低的表达式类型标记为
⊥
。如果给定两种表达式τ1，τ1≤τ2意味着τ1安全类型低于或等于τ2,意味着τ1高于τ2，τ1＝τ2意味着两种安全类型是相等的，是τ1和τ2的最小上界，是τ1和τ2的最大下界。特别地，本方法使用来指定一个表达式组的安全类型τ1...τ
i
...τ
n
，其中1≤i≤n。值得注意的是，假设意味着其中τ
i
在中。表示在方法只考虑完整性的安全类型，包括可信(t)和不可信(u)，其中
[0163]
变量安全类型τ var存储安全类型为τ或更低的信息。语句安全类型τ stmt指定语句中的每个赋值都是对安全类型为τ或更高的变量进行的。特别地，
⊥
var类型的变量不能存储具有安全类型的信息，而var类型的变量可以存储任何安全类型的信息。类似地，
⊥
stmt类型的语句指定该语句中的每个赋值可以对任何安全类型的变量进行赋值，而stmt类型的语句指定该语句中的每个赋值不能对具有安全类型的变量进行赋值。特别地，本方法使用来指定该语句中的赋值给安全类型为的表达式组的语句类型。
[0164]
函数的安全类型为：其中其中和τ
′
都属于都属于表示输入参数的安全类型，τ
′
stmt表示函数体的安全类型，表示返回变量的安全类型。如果函数中没有参数，可以将参数的安全类型省略为_。
[0165]
2)构建stc安全类型规则。在本发明的类型系统中，有三种安全类型规则可以分别用于表达式、语句和函数。所有这些规则都由一个函数类型表ft隐式参数化，ft将所有函数名映射为函数安全类型。值得注意的是，本发明还为表达式和语句引入了子类型规则(s
‑
var
‑
exp)、(s
‑
sub
‑
exp)和(s
‑
sub
‑
stmt)，以避免标签升级。
[0166]
stc安全类型规则如图3所示。
[0167]
(1)solidity表达式的安全类型规则的形式为：其中ρ是表达式exp在短语安全类型环境γ的安全类型。
[0168]
大多数表达式的安全类型规则都很直观，示例性地，solidity表达式的安全类型规则包括：
[0169]
规则描述了的安全类型规则，表示如果中的每个表达式exp
i
(1≤
i≤n)有对应的安全类型那么表达式组有安全类型组
[0170]
规则(s
‑
nexp)：描述了newexp的安全类型规则，表示newexp在γ中具有最低的安全类型
⊥
，因为它等价于新的智能合约地址，应该是最可信的；
[0171]
规则(s
‑
op
‑
u)和(s
‑
op
‑
b)：描述了operatorexp的安全类型规则，其表明如果operatorexp中的所有表达式在γ中都是安全类型τ，那么这两个规则都类型化operatorexp为τ；
[0172]
规则(s
‑
ia1)：描述了exp[]的安全类型规则，其类型化exp[]为γ中exp的安全类型；
[0173]
规则(s
‑
ia2)描述了exp1[exp2]的安全类型规则，其类型化exp1[exp2]为γ(exp1)和γ(exp2)的最小上界；
[0174]
规则(s
‑
ma1)和(s
‑
ma2)：描述了memberaccess的安全类型规则，其都将memberaccess类型化为memberaccess中表达式类型的最小上界。
[0175]
(2)solidity语句的安全类型规则的形式为：其中ρ是表达式exp在短语安全类型环境γ和stmt所属的调用方智能合约s下的安全类型；
[0176]
示例性地，solidity语句的安全类型规则包括：
[0177]
functioncall根据其语义有5种类型规则，规则(s
‑
fc1)至规则(s
‑
fc5)。规则(s
‑
fc1)和(s
‑
fc4)指定，如果id
f
具有安全类型则内部函数调用和外部委托调用具有安全类型τ
′
stmt。由于其他函数调用不改变调用方合约中的任何变量，规则(s
‑
fc2)、(s
‑
fc3)和(s
‑
fc5)将这样的函数调用类型化为t stmt。
[0178]
类似地，exp op＝functioncall也有5种类型规则。因为exp op＝functioncall和functioncall的主要区别是前者更新exp的值。规则(s
‑
op
‑
fc2),(s
‑
op
‑
fc3)和(s
‑
op
‑
fc5)类型化exp op＝functioncall为此外，id
f
的返回变量也被传递回调用方智能合约，因此应该小于等于在此基础上，规则(s
‑
op
‑
fc1)和(s
‑
op
‑
fc4)将它们的函数调用类型化为
[0179]
(3)函数的安全类型规则的形式为：直观地看，表示函数的输入参数和返回变量的类型分别最多为和同时，函数体中的每个赋值都是对安全类型至少为τ
′
的变量进行的。
[0180]
3)stc的可靠性证明
[0181]
对stc的安全类型规则进行验证，证明其满足不干扰属性，以此得证能被stc证明是类型良好的合约是满足信息流完整性的。
[0182]
进一步地，在其中一个实施例中，为了验证stc的可靠性，本发明假设solidity短语是封闭的，这意味着没有自由标识符。本发明假设如果观察者的观察能力是τ0，那么观察者可以在安全类型为≤τ0的环境中观察变量。如果两个评估环境对观察者来说是不可分辨的，那么在这两个评估环境之间有一种不可分辨的关系。
[0183]
所述stc的可靠性证明，具体过程包括：
[0184]
步骤2
‑
1，给定定义1用于描述智能合约的良好类型属性，给定定义2用于描述不可分辨关系，具体定义如下：
[0185]
定义1.假设s是一个由有限函数组成的智能合约，由fd和ft分别作为s的函数声明表和函数类型表；在s中声明的每个fun都具有函数类型，即是可派生的；
[0186]
定义2.给定两个求值环境μ1、μ2，类型环境γ，安全类型τ0，的定义如下：
[0187][0188]
步骤2
‑
2，基于上述良好类型属性及不可分辨关系，建立引理1及引理2支持stc的可靠性证明；引理1及引理2的具体描述如下：
[0189]
引理1.假定如果τ≤τ0，和那么v1＝v2；
[0190]
这里示例性地，给出引理1针对规则(s
‑
ia2)的证明。
[0191]
证明：本发明有规则(s
‑
ia2)。因为ia2)。因为和我们有v1＝v3和v2＝v4。因此，v1[v2]＝v3[v4]。
[0192]
引理2.假定如果那么
[0193]
这里示例性地，给出引理2针对规则(s
‑
op
‑
fc4)的证明。
[0194]
证明：因为那么通过规则(s
‑
op
‑
fc4)，可以得到因为只更改安全类型大于τ0的变量，所以证得
[0195]
这里，本发明通过建立上面所示的两个引理来支持可靠性证明。直观地说，这些引理的证明是通过对进行归纳法推导和对进行子归纳法推导得到的；
[0196]
步骤2
‑
3，基于引理1及引理2，给定定义3用于描述solidity语句的不干涉性(因为证明安全类型系统的可靠性本质上是证明类型系统强制执行不干涉属性)，给定定义4用于描述solidity智能合约的不干涉性，具体定义如下：
[0197]
定义3.一个智能合约语句stmt在智能合约中执行的语句s是满足不干涉属性的，当且仅当：假设有当且仅当：假设有和那么
[0198]
定义4.一个智能合约在s中是不干涉的，当且仅当：在s中执行的所有智能合约语句都是满足不干涉属性的；
[0199]
步骤2
‑
4，基于引理1～2及定义1～4，给定引理3的描述如下：
[0200]
引理3.假定如果和那么
[0201]
这里，引理3中stc的可靠性被表述为语句的不干涉属性，它的证明是通过对exp和
stmt进行归纳法同时对和进行子归纳法推导得到的。引理1和引理2可用于引理3的证明。
[0202]
这里示例性地，给出引理3针对规则(s
‑
op
‑
fc4)的证明。
[0203]
证明：因为规则(s
‑
op
‑
fc4)和分别在μ1和μ2中执行stmt得到的μ
′1和μ
′2，有两种情况：
[0204]
情况1：可以通过引理2证明；
[0205]
情况2：假定和因为引理1，所以这两种映射在≤τ0的变量在中是一致的。即有通过归纳法得证
[0206]
步骤2
‑
5，基于引理1～3，给定定理1用于说明良好类型的智能合约是满足不干扰属性的，具体描述如下：
[0207]
定理1.如果由有限函数组成的智能合约s是类型良好的，那么它是满足不干扰属性的。
[0208]
证明：通过引理3，得证良好类型的智能合约是满足不干涉属性的，即满足信息流完整性。
[0209]
进一步地，在其中一个实施例中，步骤3所述构建基于智能合约类型系统stc的类型验证器stv，自动为合约的状态变量寻找最优安全类型分配，具体过程包括：
[0210]
步骤3
‑
1，依据步骤2中对stc的可靠性证明及智能合约的状态变量个数，定义智能合约的安全类型分配的格结构，用于自动生成智能合约中的所有安全类型分配，具体定义如下：
[0211]
给定智能合约s，其带有n个状态变量的集合v，给定两种安全类型t和u，安全类型分配t是v中所有状态变量的安全类型的组合；用表示非线性有序格结构，该结构由状态变量的2
n
安全类型分配的有限集和类型分配对上的流关系
→
组成，如图4所示；给定两种类型分配t1，t2，在中，t1→
t2表示当且仅当由t1分配的所有变量的安全类型相应地小于或等于由t2分配的安全类型；
[0212]
步骤3
‑
2，基于智能合约的安全类型分配的格结构和stc，采用基于stc的类型验证器算法执行类型检测，直到找到最小数目u的安全类型分配，即最优安全类型分配；其中基于stc的类型验证器算法具体如下：
[0213]
输入：智能合约s，包含n个状态变量。
[0214]
输出：一个安全类型分配t使s是良好类型的：
[0215]
假设是n个状态变量的格结构；
[0216]
对应用拓扑排序；
[0217]
对所有属于的安全类型分配t，使用stc检测s的信息流；
[0218]
计算完毕后，如果s是类型良好的，则输出t，否则输出无解。
[0219]
定理2.类型验证器算法会给出最优解。
[0220]
证明：由于是一个偏序集，并且算法对应用了拓扑排序，可以获得所有安全类型分配的升序，按分配u的数量排序。算法遵循这个顺序来应用stc的完整性类型检测，一旦
发现类型分配t使智能合约s是类型良好的，就可以保证t具有分配u的最小数目。
[0221]
在一个实施例中，提供了一种基于类型检测的智能合约信息流完整性验证系统，所述系统包括：
[0222]
第一构建模块，用于为智能合约编程语言构建形式化语法、语义；
[0223]
第二构建模块，用于构建智能合约的安全类型系统stc，用于检测智能合约信息流完整性；
[0224]
第三构建模块，用于构建基于智能合约类型系统stc的类型验证器stv，自动为智能合约的状态变量寻找最优安全类型分配，即状态变量中被分配为可信的数量最多，使得智能合约满足信息流完整性。
[0225]
关于基于类型检测的智能合约信息流完整性验证系统的具体限定可以参见上文中对于基于类型检测的智能合约信息流完整性验证方法的限定，在此不再赘述。上述基于类型检测的智能合约信息流完整性验证系统中的各个模块可全部或部分通过软件、硬件及其组合来实现。上述各模块可以硬件形式内嵌于或独立于计算机设备中的处理器中，也可以以软件形式存储于计算机设备中的存储器中，以便于处理器调用执行以上各个模块对应的操作。
[0226]
在一个实施例中，提供了一种计算机设备，包括存储器、处理器及存储在存储器上并可在处理器上运行的计算机程序，处理器执行计算机程序时实现以下步骤：
[0227]
步骤1，为智能合约编程语言构建形式化语法、语义；
[0228]
步骤2，构建智能合约的安全类型系统stc，用于检测智能合约信息流完整性；
[0229]
步骤3，构建基于智能合约类型系统stc的类型验证器stv，自动为智能合约的状态变量寻找最优安全类型分配，即状态变量中被分配为可信的数量最多，使得智能合约满足信息流完整性。
[0230]
关于每一步的具体限定可以参见上文中对于基于类型检测的智能合约信息流完整性验证方法的限定，在此不再赘述。
[0231]
在一个实施例中，提供了一种计算机可读存储介质，其上存储有计算机程序，计算机程序被处理器执行时实现以下步骤：
[0232]
步骤1，为智能合约编程语言构建形式化语法、语义；
[0233]
步骤2，构建智能合约的安全类型系统stc，用于检测智能合约信息流完整性；
[0234]
步骤3，构建基于智能合约类型系统stc的类型验证器stv，自动为智能合约的状态变量寻找最优安全类型分配，即状态变量中被分配为可信的数量最多，使得智能合约满足信息流完整性。
[0235]
关于每一步的具体限定可以参见上文中对于基于类型检测的智能合约信息流完整性验证方法的限定，在此不再赘述。
[0236]
作为一种具体示例，在其中一个实施例中，对本发明进行进一步验证说明。本实施例以一个简化的奇偶校验多签名钱包智能合约为例，采用stc检测合约的信息流完整性，并采用stv自动寻找该合约的最优安全类型分配。
[0237]
如图5所示，在奇偶校验多签名钱包中，智能合约wallet利用了智能合约库walletlibrary提供的共享服务。例如，在部署合约wallet时，它的构造函数将初始化任务委托给walletlibrary中提供的函数initwallet()，以设置钱包的所有者为_owner。值得
注意的是，wallet和walletlibrary具有相同的状态变量owner，因此当委托walletlibrary设置owner(第5行)时，实际被更新的变量是wallet的owner(第11行)。基于walletlibrary库的设计，initwallet()函数应该只被想要使用walletlibrary的合约实例的构造函数调用一次。
[0238]
在solidity中，允许开发人员定义一个特殊的函数，称为“回退函数”。合约的回退函数没有名称，如果有对该合约的函数调用，但是该合约没有提供匹配的函数，回退函数将被执行。例如，wallet合约有一个回退函数，如图5中行27～29所示。这个回退函数的作用是，当有一个对wallet合约的函数调用，而wallet没有提供该函数时，wallet将该函数调用委托给walletlibrary来执行该函数调用。
[0239]
攻击者可以基于此机制利用漏洞。省略了技术细节，但在高层次上总结了攻击如下：攻击者通过调用initwallet(attk_addr)到wallet合约来执行一个交易，其中attk_addr是攻击者的地址。值得注意的是，这个函数调用及其参数是在msg.data中编译和封装的。由于wallet合约没有提供任何名为initwallet的函数，因此回退函数将被调用，initwallet(attk_addr)将被委托给walletlibrary来执行(第28行)。然后，钱包的主人就变成了攻击者。
[0240]
上述漏洞是一种典型的信息流完整性破坏。从完整性的角度来看，owner变量应该被注释为可信的。因为在创建(部署)钱包时，initwallet函数应该只执行一次，所以钱包的所有者应该始终是可信合约的创建者。然而，initwallet函数的public可见性意味着initwallet函数的参数应该被注释为不可信。因此，当不受信任的用户通过delegatecall从init wallet合约中的回退函数调用delegatecall时，init wallet函数中的赋值会导致不受信任的_owner变量篡改可信的owner变量。这直接导致了完整性的破坏。因为这种脆弱性的根源来自于init wallet函数的可见性，这个错误很容易修正，若将init wallet函数的可见性改为intemal，就可以防止initwallet的执行通过delegatecall改变钱包的所有者。通过检查智能合约信息流的完整性，可以很容易地发现和消除这些漏洞。
[0241]
1、stc检测合约的信息流完整性
[0242]
为了更清楚地说明stc类型检测可以很容易地检测到奇偶性多签名钱包攻击，具体实施细节如下。首先，使用安全类型对合约wallet和walletlibrary中的变量进行注释。由于用户不希望钱包的所有者被攻击者篡改，所以使用t分配给所有owner和m_owners变量。由于变量_walletlib是在构造函数中创建新walletlibrary合约的地址，因此可以认为该变量在默认情况下被赋值后是不可变的，并且在wallet合约中也使用t分配。除了所有的状态变量外，还应该使用安全类型分配全局变量。全局变量的安全类型应该根据特定的条件来分配。例如，如果在构造函数中使用全局变量，则应该使用t分配给它们，在其他情况下，应该使用u分配给它们。这是有意义的，因为合约创建者(例如攻击者)可能不会调用构造函数中没有的全局变量。因此,msg.data和wallet.fallback使用u分配。
[0243]
通过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不是良好类型的，即违反了信息流完整性。
[0244]
2、stv自动寻找该合约的最优安全类型分配
[0245]
为了展示stv类型验证器如何在奇偶性多签名钱包攻击中工作，提供了原始合约wallet的格结构，如图7所示。在安全类型分配中，分配变量的顺序为:owner、_walletlib和m_owners。通过应用stc，可以获悉uuu、uut、utu和utt这样的类型分配可以使合约wallet类型良好，类型验证器算法找到的最优组合是utt。然而，就用户需求而言，希望当owner被分配为t时，该合约仍然是类型良好的。通过stv，可以明显看出原来的合约不能满足用户的需求。
[0246]
现有的针对奇偶性多签名钱包攻击的改进方法，如将initwallet函数的可见性更改为intemal，可以防止任意的外部委托对调用者合约的状态变量的篡改。同样，修改后的合约的格结构如图8所示。通过应用stv，所有8(23)种安全类型分配都可以使合约类型良好，这意味着即使所有变量都用t分配，修改后的合约也是良好类型的，即修改后的合约满足了用户的需求，而且显然是安全的。由此可知本发明的有效性。
[0247]
以上显示和描述了本发明的基本原理、主要特征及优点。本行业的技术人员应该了解，本发明不受上述实施例的限制，上述实施例和说明书中描述的只是说明本发明的原理，在不脱离本发明精神和范围的前提下，本发明还会有各种变化和改进，这些变化和改进都落入要求保护的本发明范围内。本发明要求保护范围由所附的权利要求书及其等效物界定。

技术特征：
1.一种基于类型检测的智能合约信息流完整性验证方法，其特征在于，所述方法包括以下步骤：步骤1，为智能合约编程语言构建形式化语法、语义；步骤2，构建智能合约的安全类型系统stc，用于检测智能合约信息流完整性；步骤3，构建基于智能合约类型系统stc的类型验证器stv，自动为智能合约的状态变量寻找最优安全类型分配，即状态变量中被分配为可信的数量最多，使得智能合约满足信息流完整性。2.根据权利要求1所述的基于类型检测的智能合约信息流完整性验证方法，其特征在于，步骤1中所述构建形式化语法，具体包括：(1)将智能合约编程语言抽象为短语，这些短语为表达式或语句；智能合约的表达式包括8种类型：值v、全局变量g、状态变量id、表达式组智能合约实例表达式newexp、操作表达式operatorexp、智能合约数组或映射表达式indexaccess，和自定义类型的数据字段访问表达式memberaccess；智能合约表达式的语法定义如下：自定义类型的数据字段访问表达式memberaccess；智能合约表达式的语法定义如下：newexp：：＝new id
c
()operatorexp：：＝op
u exp|exp
1 op
b exp2indexaccess：：＝exp[]|exp1[exp2]memberaccess：：＝exp.id|exp.indexaccess其中，new为实例化合约的标识符，op
u
为一元操作符，op
b
为二元操作符，id
c
为合约名称变量；智能合约的语句包括3种类型：简单语句simplestmt、语句块blockstmt和语句序列；其中，simplestmt表示单个基本语句，包括函数调用functioncall、普通赋值语句exp
1 op＝exp2和接收函数调用返回值的赋值语句exp op＝functioncall；blockstmt表示一个语句块，包括分支结构语句if(exp)then stmt
1 else stmt2、重复语句while(exp)stmt、变量定义语句letvar id op＝exp in stmt、需求语句require(exp)in stmt和一个花括号语句块{stmt}；函数调用functioncall包括三种类型：内部函数调用外部函数调用和底层函数调用底层函数调用包括三类：call底层函数调用delegatecall底层函数调用和callcode底层函数调用智能合约语句的语法定义如下：(statements)stmt：：＝simplestmt；|blockstmt|stmt
1 stmt2simplestmt：：＝functioncall|exp1op＝exp2|exp op＝functioncall
lowlevelcall：：＝call|delegatecall|callcodeblockstmt：：＝if(exp)then stmt
1 else stmt2|while(exp)stmt|letvar id op＝exp in stmt|require(exp)in stmt|{stmt}其中，id
f
为函数名称变量，op＝为赋值操作符；(2)在编写的智能合约中，函数类型分为普通函数normal function、构造函数constructor和回退函数fallback function；一个智能合约有且只有一个未命名的fallback function，其不能有输入或输出参数，并且必须有external可见性；其中，普通函数normal function的语法定义如下：式中，id
c
表示智能合约的名称，id
f
表示函数的名称，表示函数的输入参数，表示函数的输出参数，q表示函数的可见性；构造函数constructor与普通函数normal function的区别在于：id
f
被关键字constructor替换；回退函数fallback function的语法定义如下：fun
f
：：＝id
c
.function()external{stmt}(3)智能合约包括状态变量声明和函数声明，其语法的定义如下：(contracts)ctr：：＝contract id{ctrpart}ctrpart：：＝letvar id op＝exp|fun|ctrpart ctrpart步骤1中所述构建形式化语义具体包括：(1)智能合约的表达式的操作语义形式为声明表达式exp在求值环境μ中计算为值v；同时使用dom(μ)和ran(μ)分别表示μ的定义域和值域；并假设按合约名索引的表ca存储newexp的地址，以模拟随机合约地址；(2)智能合约的语句的操作语义形式为其中μ，μ
′
分别为执行语句stmt之前和之后的求值环境，s表示stmt所属的调用方智能合约；同时假设函数定义存储在按函数名索引的表fd中。3.根据权利要求1或2所述的基于类型检测的智能合约信息流完整性验证方法，其特征在于，步骤2所述构建智能合约的安全类型系统stc，具体包括：1)构建stc安全类型由≤偏序排序的短语安全类型分层如下：(expression types)τ：：＝t|u(phrase types)ρ：：＝τ|τ var|τ stmt式中，τ为solidity表达式的安全类型，ρ为solidity短语的安全类型，包括表达式安全类型、变量安全类型τ var和语句安全类型τ stmt，t、u分别为可信和不可信；变量安全类型τ var存储安全类型为τ或更低的信息，语句安全类型τ stmt指定语句中的每个赋值都是对
安全类型为τ或更高的变量进行的；函数的安全类型为：其中和τ
′
都属于都属于表示表达式安全类型集，1≤i≤n，表示输入参数的安全类型，τ
′
stmt表示函数体的安全类型，表示返回变量的安全类型，若函数中没有参数，可将参数的安全类型省略为_；2)构建stc安全类型规则，包括：(1)智能合约表达式的安全类型规则的形式为：其中ρ是表达式exp在短语安全类型环境γ的安全类型；(2)智能合约语句的安全类型规则的形式为：其中ρ是表达式exp在短语安全类型环境γ和stmt所属的调用方智能合约s下的安全类型；(3)函数的安全类型规则的形式为：表示函数的输入参数和返回变量的类型分别最多为和同时，函数体中的每个赋值都是对安全类型至少为τ
′
的变量进行的；3)stc的可靠性证明对stc的安全类型规则进行验证，证明其满足不干扰属性，以此得证能被stc证明是类型良好的合约是满足信息流完整性的。4.根据权利要求3所述的基于类型检测的智能合约信息流完整性验证方法，其特征在于，所述stc的可靠性证明，具体过程包括：步骤2
‑
1，给定定义1用于描述智能合约的良好类型属性，给定定义2用于描述不可分辨关系，具体定义如下：定义1.假设s是一个由有限函数组成的智能合约，由fd和ft分别作为s的函数声明表和函数类型表；在s中声明的每个fun都具有函数类型，即是可派生的；定义2.给定两个求值环境μ1、μ2，类型环境γ，安全类型τ0，则不可分辨关系的定义如下：步骤2
‑
2，基于上述良好类型属性及不可分辨关系，建立引理1及引理2支持stc的可靠性证明；引理1及引理2的具体描述如下：引理1.假定如果τ≤τ0，，和那么v1＝v2；引理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是类型良好的，那么它是满足不干扰属性的。5.根据权利要求4所述的基于类型检测的智能合约信息流完整性验证方法，其特征在于，步骤3所述构建基于智能合约类型系统stc的类型验证器stv，自动为合约的状态变量寻找最优安全类型分配，具体过程包括：步骤3
‑
1，依据步骤2中对stc的可靠性证明及智能合约的状态变量个数，定义智能合约的安全类型分配的格结构，用于自动生成智能合约中的所有安全类型分配，具体定义如下：给定智能合约s，其带有n个状态变量的集合v，给定两种安全类型t和u，安全类型分配t是v中所有状态变量的安全类型的组合；用表示非线性有序格结构，该结构由状态变量的2
n
安全类型分配的有限集和类型分配对上的流关系
→
组成；给定两种类型分配t1，t2，在中，t1→
t2表示当且仅当由t1分配的所有变量的安全类型相应地小于或等于由t2分配的安全类型；步骤3
‑
2，基于智能合约的安全类型分配的格结构和stc，采用基于stc的类型验证器算法执行类型检测，直到找到最小数目u的安全类型分配，即最优安全类型分配；其中基于stc的类型验证器算法具体如下：输入：智能合约s，包含n个状态变量。输出：一个安全类型分配t使s是良好类型的：假设是n个状态变量的格结构；对应用拓扑排序；对所有属于的安全类型分配t，使用stc检测s的信息流；计算完毕后，如果s是类型良好的，则输出t，否则输出无解。6.基于权利要求1至5任意一项所述方法的基于类型检测的智能合约信息流完整性验证系统，其特征在于，所述系统包括：第一构建模块，用于为智能合约编程语言构建形式化语法、语义；第二构建模块，用于构建智能合约的安全类型系统stc，用于检测智能合约信息流完整性；第三构建模块，用于构建基于智能合约类型系统stc的类型验证器stv，自动为智能合约的状态变量寻找最优安全类型分配，即状态变量中被分配为可信的数量最多，使得智能合约满足信息流完整性。7.一种计算机设备，包括存储器、处理器及存储在存储器上并可在处理器上运行的计算机程序，其特征在于，所述处理器执行所述计算机程序时实现权利要求1至5中任一项所述方法的步骤。8.一种计算机可读存储介质，其上存储有计算机程序，其特征在于，所述计算机程序被处理器执行时实现权利要求1至5中任一项所述方法的步骤。
技术总结
本发明公开了一种基于类型检测的智能合约信息流完整性验证方法及系统，属于区块链和信息安全领域。该方法可用于解决以太坊区块链环境下智能合约潜在的信息篡改问题，包括：为智能合约编程语言构建形式化语法、语义；构建智能合约的安全类型系统STC，用于检测智能合约信息流完整性；构建基于智能合约类型系统STC的类型验证器STV，自动为智能合约的状态变量寻找最优安全类型分配。本发明给出智能合约形式化语法和语义，同时结合了类型检测在安全信息流检查中的优点，可以对智能合约源代码的信息流完整性进行有效的分析与验证，减少智能合约在运行过程中出现可信信息被篡改的概率。合约在运行过程中出现可信信息被篡改的概率。合约在运行过程中出现可信信息被篡改的概率。


技术研发人员：胡镡文 庄毅 林尚威 章甫源 阚双龙 曹子宁
受保护的技术使用者：南京航空航天大学
技术研发日：2021.03.19
技术公布日：2021/6/29