以太坊中间语言的可执行语义
作者:
作者简介:

韩宁(1996-),女,硕士生,主要研究领域为智能合约,形式化验证.
王国辉(1984-),男,博士,实验师,CCF专业会员,主要研究领域为高可靠嵌入式系统与定理证明.
李希萌(1987-),男,博士,讲师,CCF专业会员,主要研究领域为形式化验证,区块链系统可靠性,信息流安全.
施智平(1974-),男,博士,教授,博士生导师,CCF高级会员,主要研究领域为形式化方法,人工智能.
张倩颖(1986-),女,博士,讲师,CCF专业会员,主要研究领域为嵌入式操作系统,系统安全,形式化验证.
关永(1966-),男,博士,教授,博士生导师,CCF专业会员,主要研究领域为形式化验证,高可靠嵌入式系统,机器人.

通讯作者:

李希萌,lixm@cnu.edu.cn

基金项目:

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


Executable Semantics of Ethereum Intermediate Language
Author:
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)

  • 摘要
  • | |
  • 访问统计
  • |
  • 参考文献 [41]
  • |
  • 相似文献 [20]
  • | | |
  • 文章评论
    摘要:

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

    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.

    参考文献
    [1] Yaga D, Mell P, Roby N, Scarfone K. Blockchain technology overview. U.S., National Institute of Standards and Technology, 2018:1-6.[doi:10.6028/NIST.IR.8202]
    [2] Wood G. Ethereum:A secure decentralized generalized transaction ledger. Ethereum Project Yellow Paper, 2014,151(2014):1-32.
    [3] Li XQ, Jiang P, Chen T, Luo XP, Wen QY. A survey on the security of blockchain systems. Future Generation Computer Systems, 2020,107:841-853.[doi:10.1016/j.future.2017.08.020]
    [4] CNVD blockchain vulnerability sub-library. 2020. https://bc.cnvd.org.cn/statistics
    [5] Wang J, Zhan NJ, Feng XY, Liu ZM. Overview of formal methods. Ruan Jian Xue Bao/Journal of Software, 2019,30(1):33-61(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5652.htm[doi:10.13328/j.cnki.jos.005652]
    [6] Tolmach P, Li Y, Lin SW, Liu Y, Li ZX. A survey of smart contract formal specification and verification. arXiv:2008.02712, 2020.
    [7] Yul-Solidity documentation (v0.6.1). https://solidity.readthedocs.io/en/v0.6.1/yul.html
    [8] Bartoletti M, Galletta L, Murgia M. A minimal core calculus for solidity contracts. In:Pérez-Solà C, Navarro-Arribas G, Biryukov A, García-Alfaro J, eds. Proc. of the Cryptocurrencies and Blockchain Technology on Data Privacy Management. Springer-Verlag, 2019. 233-243.[doi:10.1007/978-3-030-31500-9_15]
    [9] Nielson HR, Nielson F. Semantics with applications:An appetizer. In:Proc. of the Undergraduate Topics in Computer Science. Springer-Verlag, 2007. 19-41.[doi:10.1007/978-1-84628-692-6]
    [10] Bhargavan K, Delignat-Lavaud A, Fournet C, Gollamudi A, Gonthier G, Kobeissi N, Kulatova N, Rastogi A, Sibut-Pinote T, Swamy N, Zanella-Béguelin S. Formal verification of smart contracts:Short paper. In:Murray TC, Stefan D, eds. Proc. of the 2016 ACM Workshop on Programming Languages and Analysis for Security. 2016. 91-96.[doi:10.1145/2993600.2993611]
    [11] Zakrzewski J. Towards verification of Ethereum smart contracts:A formalization of core of solidity. In:Piskac R, Rümmer P, eds. Proc. of the Working Conf. on Verified Software:Theories, Tools and Experiments. Springer-Verlag, 2018. 229-247.[doi:10. 1007/978-3-030-03592-1_13]
    [12] Yang Z, Lei H. Lolisa:Formal syntax and semantics for a subset of the solidity programming language in mathematical tool coq. In:Proc. of the Mathematical Problems in Engineering. 2020.[doi:10.1155/2020/6191537]
    [13] Yang Z, Lei H, Qian WZ. A hybrid formal verification system in coq for ensuring the reliability and security of ethereum-based service smart contracts. IEEE Acess, 2020,8:21411-21436.[doi:10.1109/ACCESS.2020.2969437]
    [14] Jiao J, Lin SW, Sun J. A generalized formal semantic framework for smart contracts. In:Wehrheim H, Cabot J, eds. Proc. of the Fundamental Approaches to Software Engineering. Springer-Verlag, 2020. 75-96.[doi:10.1007/978-3-030-45234-6_4]
    [15] Jiao J, Kan S, Lin SW, Sanan D, Liu Y, Sun J. Semantic understanding of smart contracts:Executable operational semantics of solidity. In:Proc. of the 2020 IEEE Symp. on Security and Privacy. IEEE, 2020. 1695-1712.[doi:10.1109/SP40000.2020. 00066]
    [16] Ahrendt W, Pace GJ, Schneider G. Smart contracts:A killer application for deductive source code verification. In:Müller P, Schaefer I, eds. Proc. of the Principled Software Development. Springer-Verlag, 2018. 1-18.[doi:10.1007/978-3-319-98047-8_1]
    [17] Sergey I, Kumar A, Hobor A. Scilla:A smart contract intermediate-level language. arXiv:1801.00687, 2018.
    [18] Bernardo B, Cauderlier R, Pesin B, Tesson J. Albert, an intermediate smart-contract language for the tezos blockchain. arXiv:2001. 02630, 2020.
    [19] Eth-isabelle. 2018. https://github.com/pirapira/eth-isabelle
    [20] Li XM, Shi ZP, Zhang QY, Wang GH, Guan Y, Han N. Towards verifying Ethereum smart contracts at intermediate language level. In:Ameur YA, Qin SC, eds. Proc. of the Int'l Conf. on Formal Engineering Methods. Springer-Verlag, 2019. 121-137.[doi:10. 1007/978-3-030-32409-4_8]
    [21] Hirai Y. Defining the Ethereum virtual machine for interactive theorem provers. In:Brenner M, Rohloff K, Bonneau J, Miller A, Ryan PYA, Teague V, Bracciali A, Sala M, Pintore F, Jakobsson M, eds. Proc. of the Int'l Conf. on Financial Cryptography and Data Security. Springer-Verlag, 2017.520-535.[doi:10.1007/978-3-319-70278-0_33]
    [22] Amani S, Bégel M, Bortin M, Staples M. Towards verifying Ethereum smart contract bytecode in Isabelle/HOL. In:Andronick J, Felty AP, eds. Proc. of the 7th ACM SIGPLAN Int'l Conf. on Certified Programs and Proofs. ACM, 2018. 66-77.[doi:10.1145/3167084]
    [23] Grishchenko I, Maffei M, Schneidewind C. A semantic framework for the security analysis of Ethereum smart contracts. In:Bauer L, Küsters R, eds. Proc. of the 7th Int'l Conf. on Principles of Security and Trust. Springer-Verlag, 2018. 243-269.[doi:10.1007/978-3-319-89722-6_10]
    [24] Hildenbrandt E, Saxena M, Rodrigues N, Zhu XR, Daian P, Guth D, Moore B, Park D, Zhang Y, Ștefănescu A, Roşu G. KEVM:A complete formal semantics of the Ethereum virtual machine. In:Proc. of the 31st Computer Security Foundations Symp. IEEE Computer Society, 2018. 204-217.[doi:10.1109/CSF.2018.00022]
    [25] Kasampalis T, Guth D, Moore B, Șerbănuță TF, Zhang Y, Filaretti D, Serbanuta V, Johnson R, Roşu G. IELE:A rigorously designed language and tool ecosystem for the blockchain. In:Beek MH, McIver A, Oliveira JN, eds. Proc. of the Int'l Symp. on Formal Methods. Spinger-Verlag, 2019. 593-610.[doi:10.1007/978-3-030-30942-8_35]
    [26] Luu L, Chu DH, Olickel H, Saxena P, Hobor A. Making smart contracts smarter. In:Weippl ER, Katzenbeisser S, Kruegel C, Myers AC, Halevi S, eds. Proc. of the 2016 ACM SIGSAC Conf. on Computer and Communications Security. ACM, 2016. 254-269.[doi:10.1145/2976749.2978309]
    [27] Permenev A, Dimitrov D, Tsankov P, Drachsler-Cohen D, Vechev M. VerX:Safety verification of smart contracts. In:Proc. of the 2020 IEEE Symp. on Security and Privacy. 2020. 1661-1677.[doi:10.1109/SP40000.2020.00024]
    [28] Li XY, Su C, Xiong Y, Huang WC, Wang WS. Formal verification of BNB smart contract. In:Proc. of the Int'l Conf. on Big Data. IEEE, 2019. 74-78.[doi:10.1109/BIGCOM.2019.00021]
    [29] Nehai Z, Piriou PY, Daumas F. Model-Checking of smart contracts. In:Proc. of the 2018 IEEE Int'l Conf. on Internet of Things and IEEE Green Computing and Communications and IEEE Cyber, Physical and Social Computing and IEEE Smart Data. IEEE, 2018. 980-987.[doi:10.1109/Cybermatics_2018.2018.00185]
    [30] Kalra S, Goel S, Dhawan M, Sharma S. ZEUS:Analyzing safety of smart contracts. In:Proc. of the Network and Distributed System Security Symp.. The Internet Society, 2018.[doi:10.14722/NDSS.2018.23082]
    [31] Leinenbach D, Paul W, Petrova E. Towards the formal verification of a C0 compiler:Code generation and implementation correctness. In:Aichernig BK, Beckert B, eds. Proc. of the IEEE Int'l Conf. on Software Engineering and Formal Methods. IEEE Computer Society, 2005. 2-12.[doi:10.1109/SEFM.2005.51]
    [32] Blazy S, Leroy X. Mechanized semantics for the clight subset of the c language. Journal of Automated Reasoning, 2009,43(3):263-288.[doi:10.1007/s10817-009-9148-3]
    [33] Ellison C, Roşu G. An executable formal semantics of C with applications. In:Field J, Hicks M, eds. Proc. of the 39th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. ACM, 2012. 533-544.[doi:10.1145/2103656. 2103719]
    [34] Wasserrab D, Nipkow T, Snelting G, Tip F. An operational semantics and type safety proof for multiple inheritance in C++. In:Tarr PL, Cook WR, eds. Proc. of the 21th Annual ACM SIGPLAN Conf. on Object-Oriented Programming Systems, Languages, and Applications. ACM, 2006. 345-362.[doi:10.1145/1167473.1167503]
    [35] Norrish M. A formal semantics for C++. Technical Report, Australia:NICTA, 2008. 1-124.
    [36] Drossopoulou S, Eisenbach S. Towards an operational semantics and proof of type soundness for Java. In:Proc. of the Formal Syntax and Semantics of Java. 1998. 1523.
    [37] Bogdanaş D, Roşu G. K-Java:A complete semantics of Java. In:Rajamani SK, Walker D, eds. Proc. of the 42nd Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. ACM, 2015. 445-456.[doi:10.1145/2676726. 2676982]
    [38] Nipkow T, Wenzel M, Paulson LC. Isabelle/HOL:A Proof Assistant for Higher-Order Logic. Springer-Verlag, 2002. 1-223.[doi:10.1007/3-540-45949-9]
    [39] ERC-20 token standard. 2019. https://github.com/ethereum/EIPs/blob/master/EIPS/eip-20.md
    附中文参考文献:
    [5] 王戟,詹乃军,冯新宇,刘志明.形式化方法概貌.软件学报,2019,30(1):33-61. http://www.jos.org.cn/1000-9825/5652.htm[doi:10.13328/j.cnki.jos.005652]
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

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

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2020-08-30
  • 最后修改日期:2020-10-26
  • 在线发布日期: 2021-02-07
  • 出版日期: 2021-06-06
文章二维码
您是第19528971位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号