微信服务号

微信订阅号

2025-4-9- 9
Home > Archive>Volume 32, Issue 6, 2021 >1717-1732. DOI:10.13328/j.cnki.jos.006246
PDF HTML XML Export Cite reminder
Executable Semantics of Ethereum Intermediate Language
Author:
Affiliation:

Fund Project:

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)

  • Article
    • | |
  • Metrics
    • |
  • Reference
    • |
  • Related
    • | | |
  • Comments
    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.

    Reference
    Related
    Cited by
Get Citation

韩宁,李希萌,张倩颖,王国辉,施智平,关永.以太坊中间语言的可执行语义.软件学报,2021,32(6):1717-1732

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:August 30,2020
  • Revised:October 26,2020
  • Online: February 07,2021
  • Published: June 06,2021
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2034054Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063