Instruction Verification of Ethereum Virtual Machine by Formal Method

Chun Sheng Ke, Yean Ru Chen

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish
Title of host publicationIndo - Taiwan 2nd International Conference on Computing, Analytics and Networks, Indo-Taiwan ICAN 2020 - Proceedings
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages69-74
Number of pages6
ISBN (Electronic)9781728149998
DOIs
Publication statusPublished - 2020 Feb
EventIndo - Taiwan 2nd International Conference on Computing, Analytics and Networks, Indo-Taiwan ICAN 2020 - Rajpura, Punjab, India
Duration: 2020 Feb 72020 Feb 15

Publication series

NameIndo - 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
CountryIndia
CityRajpura, Punjab
Period20-02-0720-02-15

All Science Journal Classification (ASJC) codes

  • Artificial Intelligence
  • Computer Networks and Communications
  • Computer Science Applications
  • Information Systems
  • Information Systems and Management

Fingerprint Dive into the research topics of 'Instruction Verification of Ethereum Virtual Machine by Formal Method'. Together they form a unique fingerprint.

Cite this