(19)国家知识产权局 (12)发明 专利 (10)授权公告 号 (45)授权公告日 (21)申请 号 202111637894.1 (22)申请日 2021.12.2 9 (65)同一申请的已公布的文献号 申请公布号 CN 114218809 A (43)申请公布日 2022.03.22 (73)专利权人 中国科学技术大学 地址 230000 安徽省合肥市金寨路96号 (72)发明人 汪万森　黄文超　熊焰　熊峰　 方贤进　 (74)专利代理 机构 安徽思沃达知识产权代理有 限公司 342 20 专利代理师 唐明 (51)Int.Cl. G06F 30/20(2020.01) G06F 21/57(2013.01)G06Q 40/04(2012.01) G06F 16/27(2019.01) 审查员 邱祥吉 (54)发明名称 面向以太坊智能合约的协议自动形式化建 模方法与系统 (57)摘要 本发明公开了一种面向以太坊智能合约 的 协议自动形式化建模 方法与系统， 在不需要人工 参与的前提下， 不仅能够建模合约中各个交易的 行为， 还可以建模交易之间的关系(即交易之间 的顺序、 区块变量)， 因此， 可以应用于验证： 1)在 不同交易顺序下是否满足特定安全属性； 2)处于 不同区块的交易是否满足特定属性， 在能够用于 分析溢出、 重入等漏洞的基础上， 还可 以用于交 易顺序依赖、 区块变量依赖漏洞的自动分析。 权利要求书2页 说明书7页 附图2页 CN 114218809 B 2022.06.03 CN 114218809 B 1.一种面向以太坊智能合约的协议自动形式化建模方法， 其特 征在于， 包括： 步骤1、 获取以太坊智能合约源码以及安全属性； 步骤2、 解析 所述以太坊智能合约源码， 获得全局变量 集合与函数集 合； 步骤3、 针对每一函数， 生成外部账户行为子模型， 表示任意外部账户调用相应函数的 行为； 步骤4、 结合以太坊智能合约源码中的函数， 针对不同身份的攻击者， 生成相应的攻击 者行为子模型， 建模相应攻击者的能力； 步骤5、 针对每一函数中的语句， 按照预设转换方式， 根据语句类型、 使用变量以及所在 函数， 将语句转换为智能合约行为子模型； 步骤3～步骤5不区分执 行的先后顺序， 可以同步执 行， 也可以按照任意 顺序先后执 行； 步骤6、 根据所述安全属性的类型， 对三种行为子模型或者部分行为子模型进行修改， 得到以太坊智能合约形式化模型， 包括： 针对等价的安全属性， 将三种行为子模 型构成的集 合复制得到新的集合， 以两个集合对应表示两组交易， 将两个集合对应的初始区块变量设 置为不同， 表示两组交易对应的初始区块变量不同； 修改对应返回语句的行为子模型， 添加 动作表示两组 交易执行完成后存在一个账户的余 额不一致。 2.根据权利要求1所述的一种面向以太坊智能合约的协议自动形式化建模方法， 其特 征在于， 所述外部账户行为子模型表示发起调用的外部账户以及局部变量初始值是任意 的。 3.根据权利要求1所述的一种面向以太坊智能合约的协议自动形式化建模方法， 其特 征在于， 所述结合以太坊智能合约源码中的函数， 针对不同身份的攻击者， 生成相应的攻击 者行为子模型包括： 所述不同身份的攻击者包括： 外部账户攻击者、 合约账户攻击者与矿工攻击者； 其中， 对于智能合约中的公开函数， 建模外部账户攻击者， 它能够调用智能合约中的任意公开函 数； 当智能合约中的函数存在以太币转账行为， 建模合约账户攻击者， 它能够构造fallback 函数实现 间接调用以太坊智能合约中的任意 公开函数； 当智能合约中的函数使用了区块变 量时， 建模 矿工攻击者， 它能够 在打包区块时修改区块变量。 4.根据权利要求1所述的一种面向以太坊智能合约的协议自动形式化建模方法， 其特 征在于， 针对每一函数中的语句， 按照预设转换方式， 根据语句类型、 使用变量以及所在函 数， 将语句转换为智能合约行为子模型包括： 根据语句类型， 生成相应的子模型： 对于条件语句， 生成两条不同的子模型， 表示条件 满足和不满足时的执行分支； 对于循环语句， 展开后获得条件语句和/或其他语句， 对于其 他语句， 生成一条子模型， 对于条件语句， 则生成两条不同子模型； 对于每一条子模型， 根据使用变量及所在函数进行转换： 子模型的左值和右值分别表 示语句执行的前提和结果， 左值和右值中分别使用了LVar与Gvar， LVar表示语句所在函数 的局部变量 值， Gvar表示合约的全局变量 值； 综合所有子模型的转换 结果， 获得智能合约行为子模型。 5.根据权利要求1所述的一种面向以太坊智能合约的协议自动形式化建模方法， 其特 征在于， 所述根据所述安全属 性的类型， 对三种 行为子模型或者部分行为子模型进行修改 包括：权　利　要　求　书 1/2 页 2 CN 114218809 B 2对于不变式的安全属性， 修改外部账户行为子模型， 添加动作表示不变式在交易执行 之前成立； 和/或修改智能合约行为子模型中对应返回语句， 添加 动作表示不变式在交易执 行完成后不成立。 6.根据权利要求1所述的一种面向以太坊智能合约的协议自动形式化建模方法， 其特 征在于， 所述根据所述安全属 性的类型， 对三种 行为子模型或者部分行为子模型进行修改 包括： 针对等价属性， 将三种行为子模型构成的集合复制得到三个新的集合， 以四个集合对 应表示四组交易， 将集合对应的变量初始 值设置为两两相同， 以此表示相同的交易； 将代表 不同交易的集合以不同的先后顺序组合； 修改对应返回语句的行为子模型， 添加动作表示 两组交易执行完成后存在一个账户的余 额不一致。 7.一种面向以太坊智能合约的协议自动形式化建模系统， 其特征在于， 用于实现权利 要求1～6任一项所述的方法， 该系统包括： 数据信息获取 单元， 用于获取以太坊智能合约源码以及安全属性； 解析单元， 用于解析 所述以太坊智能合约源码， 获得全局变量 集合与函数集 合； 外部账户行为子模型生成单元， 用于针对每一函数， 生成外部账户行为子模型， 表示任 意外部账户调用相应函数的行为； 攻击者行为子模型生成单元， 结合以太坊智能合约源码中的函数， 针对不同身份的攻 击者， 生成相应的攻击者行为子模型， 建模相应攻击者的能力； 智能合约行为子模型生成单元， 针对每一函数中的语句， 按照预设转换方式， 根据语句 类型、 使用变量以及所在函数， 将语句转换为智能合约行为子模型； 修改单元， 用于根据所述安全属性的类型， 对三种行为子模型或者部分行为子模型进 行修改， 得到以太坊智能合约形式化模型。 8.一种处理设备， 其特征在于， 包括： 一个或多个处理器； 存储器， 用于存储一个或多个 程序； 其中， 当所述一个或多个程序被所述一个或多个处理器执行时， 使得所述一个或多个 处理器实现如权利要求1～6任一项所述的方法。 9.一种可读存储介质， 存储有计算机程序， 其特征在于， 当计算机程序被处理器执行时 实现如权利要求1～6任一项所述的方法。权　利　要　求　书 2/2 页 3 CN 114218809 B 3