Formal Process Virtual Machine for Smart Contracts Verification

TL;DR

This paper introduces FSPVM-E, a formal symbolic virtual machine for Ethereum smart contract verification, built entirely within Coq, leveraging execution-verification isomorphism and supporting automated security and reliability analysis.

Contribution

It presents a novel formal framework combining EVI, GERM, and Lolisa to enhance automation, consistency, and reusability in smart contract verification within Coq.

Findings

Supports ERC20 standard verification

Automates symbolic execution and security proof

Enhances automation and reusability in formal verification

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, completely 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 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.