主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公English
2022年专刊出版计划 微信服务介绍 最新一期:2021年第2期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
韩宁,李希萌,张倩颖,王国辉,施智平,关永.以太坊中间语言的可执行语义.软件学报,2021,32(6):21-0
以太坊中间语言的可执行语义
Executable Semantics of the Ethereum Intermediate Language
投稿时间:2020-08-30  修订日期:2020-10-26
DOI:10.13328/j.cnki.jos.006246
中文关键词:  智能合约  Yul语言  Isabelle/HOL  形式化语义  以太坊
英文关键词:Smart Contract  Yul Language  Isabelle/HOL  Formal Semantics  Ethereum
基金项目:国家自然科学基金(61572331,61602325,61802375,61876111,61877040,62002246);北京市教育委员会科技计划一般项目(KM20190028005,KM202010028010);中国科学院计算技术研究所计算机体系结构国家重点实验室开放课题(CARCH201920)
作者单位E-mail
韩宁 首都师范大学 信息工程学院, 北京 100048
“成像理论与技术” 北京高精尖创新中心, 北京 100048 
 
李希萌 首都师范大学 信息工程学院, 北京 100048
“电子系统可靠性技术” 北京市重点实验室, 北京 100048 
lixm@cnu.edu.cn 
张倩颖 首都师范大学 信息工程学院, 北京 100048
“电子系统可靠性技术” 北京市重点实验室, 北京 100048 
 
王国辉 首都师范大学 信息工程学院, 北京 100048
“电子系统可靠性技术” 北京市重点实验室, 北京 100048 
 
施智平 首都师范大学 信息工程学院, 北京 100048
“电子系统可靠性技术” 北京市重点实验室, 北京 100048 
 
关永 首都师范大学 信息工程学院, 北京 100048
“成像理论与技术” 北京高精尖创新中心, 北京 100048 
 
摘要点击次数: 57
全文下载次数: 42
中文摘要:
      智能合约是实现各类区块链应用的核心软件程序.近期,以太坊区块链平台(Ethereum)上的智能合约暴露出大量错误和安全隐患,在国际上引发了智能合约形式化验证的研究热潮.为提供高可信度的验证结果,智能合约程序语言的形式化必不可少.本工作对以太坊中间语言Yul进行形式化,首次给出了其类型系统和小步操作语义的形式化定义.该语义为可执行语义(executable semantics),由120个Yul语言程序组成的测试集进行测试.本工作在Isabelle/HOL证明辅助工具中完成,为基于定理证明的智能合约正确性、安全性验证奠定了基础.
英文摘要:
      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. In this work, we formalize 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. Our 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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利