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

韩宁 等:以太坊中间语言的可执行语义 1719

节简单介绍证明辅助工具 Isabelle/HOL.第 3 节介绍 Yul 语言语法的形式化.第 4 节介绍 Yul 语言类型系统的形
式化.第 5 节介绍 Yul 语言小步语义的形式化以及对语义正确性的测试.第 6 节利用一个代币合约(token
contract)演示 Yul 语言合约的类型检查以及依据形式化语义的执行.第 7 节总结本工作并展望未来工作.

1 相关工作

1.1 智能合约语言形式化及智能合约验证

本文的研究领域为智能合约语言的形式化(机械化)语义,以下讨论该方面的现有工作.此外,由于智能合约
验证工作是语义形式化工作的自然延伸,且部分现有的语义形式化工作同时处理一些验证问题,故本节亦讨论
一些重要的智能合约验证工作.
在高级语言方面,Bhargavan 等人给出 Solidity 语言部分核心特性的形式化,并提出一个基于 F*验证以太坊
智能合约的框架 [10] .Zakrzewski 在 Coq 中给出 Solidity 一个子集的大步语义 [11] .Yang 等人在 Coq 中对 Solidity
语言的核心子集 Lolisa 进行形式化 [12] ,并开发了关于智能合约可靠性、安全性的验证系统 [13] .Jiao 等人在 K
framework 中提出了智能合约高级语言的一般形式语义框架 [14] 以及 Solidity 语言的较为完整的形式化 [15] .
Ahrendt 等人提出在 KeY 工具中对智能合约进行演绎验证的技术 [16] .在中间语言方面,Sergey 等人在 Coq 中定
义了一种基于通信自动机的智能合约中间语言 Scilla [17] .Bernardo 等人为 Tezos 平台提出了一种智能合约中间
语言 Albert,且在 Coq 中描述了 Albert 的编译器 [18] .Li 等人讨论了在中间语言层进行智能合约定理证明的优势,
并基于中间语言 Yul 的大步语义(首先在文献[19]中给出),在 Isabelle/HOL 中,对一数字货币合约进行了正确性
证明 [20] .在低级语言层面,Hirai 在 Lem 中对以太坊虚拟机(EVM)的指令集进行形式化建模,并利用该模型,在
Isabelle/HOL 中验证了以太坊智能合约的一些不变式和关于账户余额增减的正确性 [21] .Amani 等人基于该工作
定义了 EVM 字节码的一个可靠程序逻辑 [22] .Grishchenko 等人给出了 EVM 字节码的第一个完整的小步语义,
并给出了 Ethereum 智能合约的 3 种安全属性 [23] .Hildenbrandt 等人在 K framework 中创建了可执行的 EVM 字
节码语义 [24] .Kasampalis 等人提出了一种以虚拟寄存器为基础的智能合约底层语言 IELE,并在 K framework 中
对语义进行了形式化 [25] .
以上工作侧重支撑演绎推理的智能合约语言形式化.此外,Luu 等人对 EVM 的 CALL,RETURN 等指令给出
了纸笔定义,并构建了基于符号执行的漏洞检测工具 Oyente [26] .Permenev 等人基于软件模型检测相关技术,构
建了自动验证以太坊智能合约功能属性的验证器 VerX [27] .Li 等人利用 SAPIC 演算对 BNB 智能合约进行建模,
并在 Tamarin 自动证明器中,通过把模型转换成重写规则来验证该合约的安全性 [28] .Nehai 等人在模型检测工具
NuSMV 中构建以太坊智能合约的模型,验证智能合约是否符合时序逻辑规范 [29] .Kalra 等人构造了借助 LLVM
中间表示验证智能合约正确性、公平性的工具 ZEUS,并分析了大量智能合约代码 [30] .
由上述相关研究可知:在以太坊智能合约的形式化建模方面,现有工作多为以太坊字节码语言和高级语言
的形式化.但 EVM 字节码作为一种具有简单指令编码的机器语言,不具有可读性,对以字节码形式存在的智能
合约难于描述所需的证明目标和证明所需的支撑性断言.而高级语言特性多且复杂,变化更新快,很难形式化全
部特性来实现完整规范.已有的面向中间语言的工作 [17,18] 所涉及的中间语言往往并非以太坊智能合约开发所
用工具链支持的中间语言.相比之下,本工作形式化的中间语言 Yul 是以太坊项目自身的中间语言,可作为
Solidity 等高级语言的翻译目标,亦可编译为 EVM1.0,EVM1.5,eWASM 等低级语言.在文献[19]中亦包含 Yul 语
言的部分形式化,但其语义为大步语义,且不包括 gas 的建模.相较于该工作,本工作定义 Yul 语言的类型系统以
及包含 gas 模型的小步语义.小步语义反映智能合约执行的中间过程,能够很好地支撑智能合约安全属性
(security property)的验证.
1.2 其他程序语言的形式化
已有工作对各种通用编程语言进行了不同程度的形式化,以下讨论其中的主要工作.关于 C 语言,
Leinenbach 等人在 Isabelle/HOL 中形式化了 C 语言子集 C0 的小步语义并实现了其编译器规范的纸笔证明 [31] .