Abstract:

This paper reports on the development and verification of a novel formal symbolic process virtual machine (FSPVM) for verifying the reliability and security of Ethereum smart contracts, denoted as FSPVM-E, in Coq proof assistant. It adopts execution-verification isomorphism (EVI), an extension of Curry-Howard isomorphism (CHI), as its fundamental theoretical framework. The current version of FSPVM-E is constructed on a general, extensible, and reusable formal memory (GERM) framework, an extensible and universal formal intermediate programming language Lolisa, which is a large subset of the Solidity programming language using generalized algebraic datatypes, and the corresponding formally verified interpreter of Lolisa, denoted as FEther. It supports the ERC20 standard and can automatically, simultaneously, and symbolically execute the smart contract programs of Ethereum and verify their reliability and security properties using Hoare logic in Coq. In addition, this work contributes to solving the problems of automation, inconsistency, and reusability in higher-order logic theorem proving.