Page 144 - 《软件学报》2021年第6期

1718 Journal of Software 软件学报 Vol.32, No.6, June 2021

[1]
区块链(blockchain)是去中心化、分布式的数字账本 ,它能够可靠记录多方事务的处理过程和结果,维护多
方共识,并提供交易记录可验证、难篡改、交易历史可追溯等优良特性.以太坊(Ethereum)是目前使用最广泛的
[2]
公有区块链平台之一 .以太坊上的智能合约(smart contract)是一种约定多方任务逻辑的计算机程序,能够自动
执行并产生经过共识的链上结果.近年来,智能合约已被应用在数字金融、供应链管理、在线游戏等不同领域.
然而,许多链上合约暴露出编程漏洞,且针对智能合约的安全攻击屡见不鲜.例如:2016 年 6 月,The DAO 合约因
[3]
重入漏洞造成超过 6 000 万美元的损失 ;2017 年 11 月,Parity 电子钱包因多重签名漏洞造成约 1.5 亿美元的资
金被冻结于智能合约中;2018 年 4 月,美链(BEC)合约因整数溢出漏洞,使得市值数亿的项目惨淡收场.据 CNVD-
[4]
BC 区块链漏洞子库统计 ,在 2019 年 6 月~2020 年 6 月之间,发现区块链漏洞中,关于智能合约漏洞的数量占据
首位.智能合约的正确性和安全性问题,已成为制约区块链落地应用的主要因素之一.
[5]
形式化验证是为系统正确性、安全性提供高度保障的有效工具 .近年来,国际上许多为智能合约提供正确
[6]
性、安全性保障的研究工作不同程度地采用形式化验证的思想和方法 .其中,定理证明方法通过将验证任务转
化为数学证明,并使用计算机程序检查证明的基本步骤,为验证结果提供极高的可信度.若要可靠验证智能合约
的正确性和安全性,仍须明确给出编写智能合约所用程序语言的语义,较为有效的手段是在软件工具(如证明辅
助工具)中对语义进行形式化.
[7]
在以太坊的技术体系中,Yul 语言是一种结构化的中间语言 .可由 Solidity [7,8] 等高级语言所编写的智能合
约经编译得到其 Yul 语言表示,或在 Solidity 的内联汇编中使用 Yul 语言,或直接使用 Yul 语言进行合约的编写.
此外,Yul 语言能够被编译到多种低级语言(如不同版本的 EVM 字节码、EWASM 等),使合约能在以太坊平台上
执行.Yul 语言具备高级语言中的函数、代码块、控制流结构等抽象,以该语言表示的智能合约相较于字节码合
约更容易理解,因而易于参照代码进行形式规约.作为中间语言,Yul 语言的特性相较于 Solidity 等高级语言更为
简单,因而更易于形式化.
本文在证明辅助工具 Isabelle/HOL 中,采用小步语义对以太坊中间语言 Yul 进行形式化建模.小步语义属于
[9]
操作语义中的一种,能够反映程序执行的中间状态 ,因而能够为许多安全性质(security property)的验证提供支
撑.本文的形式化语义是可执行语义,因而既能在证明辅助工具中模拟智能合约的执行,又能支撑对智能合约正
确性、安全性的定理证明.本文工作的主要贡献有:
(1) Yul 语言类型系统的形式化;
(2) Yul 语言小步语义的定义和形式化;
(3) Yul 语言小步语义的测试.
其中,类型系统的形式化,实现了对 Yul 语言官方文档中自然语言描述的数据类型、变量作用域等规范的严
格表达;小步语义的定义和形式化,实现了对 Yul 语言程序执行过程和结果(包括单步执行所消耗的 gas 量)的严
格描述;在 Isabelle/HOL 中对语义的测试,保证该语义如实反映 Yul 语言规范以及实际观察的合约执行行为.
Yul 语言具有一定的复杂程度.除去在证明辅助工具中使用高阶逻辑对目标理论进行表述外,本研究的另
一难点是通过自然语言文档研读、Yul 程序编译执行实验、形式化代码检视、测试等手段保障 Yul 语言各种
特性形式化的准确性,所涉及的语言特性包括数据类型、变量作用域、控制流结构(if,switch,for 等)、可嵌套的
函数定义(Yul 是分程序语言)、内部函数调用与外部合约调用、大部分内置函数、异常、燃料(gas)等.本工作
为基于定理证明的智能合约正确性和安全性验证奠定了坚实基础.
本工作针对 2020 年初发布的 Yul 0.6.1 版本,在 Isabelle/HOL 中的形式化覆盖了 Yul 0.6.1 中除 break,
continue 和 leave 语句外的所有语言特性,以及所有(78 个)内置函数中的 62 个(形式化代码请参见 https://github.
com/lixm/yul-smallstep).其中:break 和 continue 用于细粒度循环控制;而 leave 是近期引入 Yul 语言的新特性,用
于退出当前函数.在智能合约中,这 3 个语句的使用并不多见,且在需要的场合,常常可由其他语法元素实现相同
的功能,故目前形式化中对它们的省略并不会严重影响智能合约的表达.尽管如此,后文仍会对如何在形式化语
义中支持这 3 个语句进行讨论.
本文第 1 节介绍国内外关于智能合约形式化验证、程序语言形式化的相关工作,并与本工作进行比较.第 2