软件学报

作者：韩宁，李希萌，张倩颖，王国辉，施智平，关永

单位：韩宁，首都师范大学 信息工程学院, 北京 100048;北京成像理论与技术高精尖创新中心(首都师范大学), 北京 10004811,李希萌，首都师范大学 信息工程学院, 北京 100048;电子系统可靠性技术北京市重点实验室(首都师范大学), 北京 10004802,张倩颖，首都师范大学 信息工程学院, 北京 100048;电子系统可靠性技术北京市重点实验室(首都师范大学), 北京 10004803,王国辉，首都师范大学 信息工程学院, 北京 100048;电子系统可靠性技术北京市重点实验室(首都师范大学), 北京 10004804,施智平，首都师范大学 信息工程学院, 北京 100048;电子系统可靠性技术北京市重点实验室(首都师范大学), 北京 10004805,关永，首都师范大学 信息工程学院, 北京 100048;北京成像理论与技术高精尖创新中心(首都师范大学), 北京 10004806

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

基金：国家自然科学基金（61572331，61602325，61802375，61876111，61877040，62002246）；北京市教育委员会科技计划（KM20190028005，KM202010028010）；中国科学院计算技术研究所计算机体系结构国家重点实验室开放课题（CARCH201920）

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

来源：2021年第6期

《软件学报》期刊编辑部

查看软件学报杂志2021年第6期