Instruction Verification of Ethereum Virtual Machine by Formal Method

Chun Sheng Ke, Yean Ru Chen

研究成果: Conference contribution

摘要

In recent years, many smart contracts on the ethereum platform are increasingly closer to our life. The existence of smart contract enables us to complete complicated transactions without depending on the third party. It should be not only fast, but also secure guaranteed. When the smart contract is requested to execute, the action is performed by ethereum virtual machine (EVM). If EVM occurs errors in the process of implementation, the contract execution result will also have mistaken. Therefore, ensuring the correctness of the EVM is very important. In this work, we propose a framework to formally verify EVM instruction implementations by model checking to check whether the instruction operation behaviors working on EVM is the same as the expected definitions in the ethereum yellow paper. In addition, we also define a set of interfaces specifically for EVM instruction verification to achieve the reusability of our proposed verification environment. The experimental results indicate that the formal verification method used in this work is more trustworthy than the conventional testing method. It can exactly capture the errors in the design which may be undetected by testing/simulation methods. The defined instructions are divided into 11 categories, and our work has completed to verify 7 categories, including 92 instructions of total 134, in 50 hours.

原文English
主出版物標題Indo - Taiwan 2nd International Conference on Computing, Analytics and Networks, Indo-Taiwan ICAN 2020 - Proceedings
發行者Institute of Electrical and Electronics Engineers Inc.
頁面69-74
頁數6
ISBN(電子)9781728149998
DOIs
出版狀態Published - 2020 二月
事件Indo - Taiwan 2nd International Conference on Computing, Analytics and Networks, Indo-Taiwan ICAN 2020 - Rajpura, Punjab, India
持續時間: 2020 二月 72020 二月 15

出版系列

名字Indo - Taiwan 2nd International Conference on Computing, Analytics and Networks, Indo-Taiwan ICAN 2020 - Proceedings

Conference

ConferenceIndo - Taiwan 2nd International Conference on Computing, Analytics and Networks, Indo-Taiwan ICAN 2020
國家/地區India
城市Rajpura, Punjab
期間20-02-0720-02-15

All Science Journal Classification (ASJC) codes

  • 人工智慧
  • 電腦網路與通信
  • 電腦科學應用
  • 資訊系統
  • 資訊系統與管理

指紋

深入研究「Instruction Verification of Ethereum Virtual Machine by Formal Method」主題。共同形成了獨特的指紋。

引用此