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

摘要：

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

关键词：智能合约、Yul语言、Isabelle/HOL、形式化语义、以太坊

所属期刊栏目：32

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金;国家自然科学基金;国家自然科学基金;国家自然科学基金;国家自然科学基金;国家自然科学基金;北京市教委科技项目;北京市教委科技项目;中国科学院计算技术研究所计算机体系结构国家重点实验室开放基金

在线出版日期：2021-07-06（万方平台首次上网日期，不代表论文的发表时间）

页数：共16页

页码：1717-1732