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

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
Journal of Software,2021,32(6):1717−1732 [doi: 10.13328/j.cnki.jos.006246] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

∗
以太坊中间语言的可执行语义

1,2
1,3
1,2
1,2
1,2
韩 宁 , 李希萌 , 张倩颖 , 王国辉 , 施智平 , 关 永 1,3
1
(首都师范大学 信息工程学院,北京 100048)
2 (电子系统可靠性技术北京市重点实验室(首都师范大学),北京 100048)
3 (北京成像理论与技术高精尖创新中心(首都师范大学),北京 100048)
通讯作者: 李希萌, E-mail: lixm@cnu.edu.cn

摘 要: 智能合约是实现各类区块链应用的核心软件程序.近期,以太坊区块链平台(Ethereum)上的智能合约暴露
出大量错误和安全隐患,在国际上引发了智能合约形式化验证的研究热潮.为提供高可信度的验证结果,智能合约程
序语言的形式化必不可少.对以太坊中间语言 Yul 进行形式化,首次给出了其类型系统和小步操作语义的形式化定
义.该语义为可执行语义(executable semantics),由 120 个 Yul 语言程序组成的测试集进行测试.该工作在 Isabelle/
HOL 证明辅助工具中完成,为基于定理证明的智能合约正确性、安全性验证奠定了基础.
关键词: 智能合约;Yul 语言;Isabelle/HOL;形式化语义;以太坊
中图法分类号: TP311

中文引用格式: 韩宁,李希萌,张倩颖,王国辉,施智平,关永.以太坊中间语言的可执行语义.软件学报,2021,32(6):1717−1732.
http://www.jos.org. cn/1000-9825/6246.htm
英文引用格式: Han N, Li XM, Zhang QY, Wang GH, Shi ZP, Guan Y. Executable semantics of Ethereum intermediate language.
Ruan Jian Xue Bao/Journal of Software, 2021,32(6):1717−1732 (in Chinese). http://www.jos.org.cn/1000-9825/6246.htm
Executable Semantics of Ethereum Intermediate Language

1,2
1,2
1,2
1,2
1,3
HAN Ning , LI Xi-Meng , ZHANG Qian-Ying , WANG Guo-Hui , SHI Zhi-Ping , GUAN Yong 1,3
1 (College of Information Engineering, Capital Normal University, Beijing 100048, China)
2 (Beijing Key Laboratory of Electronic System Reliability and Prognostics (Capital Normal University), Beijing 100048, China)
3 (Beijing Advanced Innovation Center for Imaging Theory and Technology (Capital Normal University), Beijing 100048, China)
Abstract: Smart contracts are key software components of blockchain applications. Recently, a great number of bugs and security
vulnerabilities have been exposed in smart contracts on the Ethereum blockchain. This resulted in extensive research efforts in the formal
verification of smart contracts at the international level. To obtain highly trustworthy verification results, the formalization of
programming languages for smart contracts is necessary. This work formalizes Yul—the Ethereum intermediate language. The core of this
formalization consists of the first formal definitions of the type system and the small-step operational semantics for Yul. The semantics is
executable, and it is validated using a test suite of 120 Yul programs. The proposed formalization is performed in the Isabelle/HOL proof
assistant. It lays a solid foundation for the formal verification of the correctness and security of Ethereum smart contracts through theorem
proving.
Key words: smart contract; Yul language; Isabelle/HOL; formal semantics; Ethereum

∗ 基金项目: 国家自然科学基金(61572331, 61602325, 61802375, 61876111, 61877040, 62002246); 北京市教育委员会科技计划
(KM20190028005, KM202010028010); 中国科学院计算技术研究所计算机体系结构国家重点实验室开放课题(CARCH201920)
Foundation item: National Natural Science Foundation of China (61572331, 61602325, 61802375, 61876111, 61877040, 62002246);
General Project of Beijing Municipal Education Commission (KM20190028005, KM202010028010); Open Project of State Key
Laboratory of Computer Architecture, Institute of Computing Technology, Chinese Academy of Sciences (CARCH201920)
本文由“形式化方法与应用”专题特约编辑邓玉欣教授推荐.
收稿时间: 2020-08-30; 修改时间: 2020-10-26; 采用时间: 2020-12-19; jos 在线出版时间: 2021-02-07