FEther: An Extensible Definitional Interpreter for Smart-contract Verifications in Coq

TL;DR

FEther is an extensible definitional interpreter built in Coq that supports Solidity semantics and automates smart contract verification, enhancing theorem-proving capabilities for blockchain security.

Contribution

It introduces FEther, a novel extensible definitional interpreter in Coq, supporting Solidity semantics and automating smart contract verification.

Findings

FEther supports almost all Solidity semantics.

FEther executes and verifies smart contracts with high automation.

FEther's execution efficiency surpasses previous Coq interpreters.

Abstract

Blockchain technology adds records to a list using cryptographic links. Therefore, the security of blockchain smart contracts is among the most popular contemporary research topics. To improve the theorem-proving technology in this field, we are developing an extensible hybrid verification tool chain, denoted as FSPVM-E, for Ethereum smart contract verification. This hybrid system extends the proof assistants in Coq, a formal proof-management system. Combining symbolic execution with higher-order theorem-proving, it solves consistency, automation, and reusability problems by standard theorem-proving approaches. This article completes the FSPVM-E by developing its proof engine. FSPVM-E is an extensible definitional interpreter based on our previous work FEther, which is totally developed in the Coq proof assistant. It supports almost all semantics of the Solidity programing language, and simultaneously executes multiple types of symbols. FEther also contains a set of automatic strategies that execute and verify the smart contracts in Coq with a high level of automation. The functional correctness of FEther was verified in Coq. In standard tutorials, the execution efficiency of FEther far exceeded that of the interpreters developed in Coq.