-
题名以太坊中间语言的可执行语义
被引量:5
- 1
-
-
作者
韩宁
李希萌
张倩颖
王国辉
施智平
关永
-
机构
首都师范大学信息工程学院
电子系统可靠性技术北京市重点实验室(首都师范大学)
北京成像理论与技术高精尖创新中心(首都师范大学)
-
出处
《软件学报》
EI
CSCD
北大核心
2021年第6期1717-1732,共16页
-
基金
国家自然科学基金(61572331,61602325,61802375,61876111,61877040,62002246)
北京市教育委员会科技计划(KM20190028005,KM202010028010)
中国科学院计算技术研究所计算机体系结构国家重点实验室开放课题(CARCH201920)。
-
文摘
智能合约是实现各类区块链应用的核心软件程序.近期,以太坊区块链平台(Ethereum)上的智能合约暴露出大量错误和安全隐患,在国际上引发了智能合约形式化验证的研究热潮.为提供高可信度的验证结果,智能合约程序语言的形式化必不可少.对以太坊中间语言Yul进行形式化,首次给出了其类型系统和小步操作语义的形式化定义.该语义为可执行语义(executable semantics),由120个Yul语言程序组成的测试集进行测试.该工作在Isabelle/HOL证明辅助工具中完成,为基于定理证明的智能合约正确性、安全性验证奠定了基础.
-
关键词
智能合约
yul语言
Isabelle/HOL
形式化语义
以太坊
-
Keywords
smart contract
yul language
Isabelle/HOL
formal semantics
Ethereum
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-