Optimization of Executable Formal Interpreters developed in Higher-order Theorem Proving Systems

TL;DR

This paper improves the execution efficiency of a formal interpreter used in higher-order theorem proving systems for verifying smart contracts, addressing previous performance limitations to enhance verification effectiveness.

Contribution

It identifies root causes of low efficiency in formal interpreters and proposes targeted optimization schemes, significantly enhancing FEther's performance.

Findings

Execution efficiency of FEther improved significantly

Identified three root causes of low efficiency

Optimizations enable more effective smart contract verification

Abstract

In recent publications, we presented a novel formal symbolic process virtual machine (FSPVM) framework that combined higher-order theorem proving and symbolic execution for verifying the reliability and security of smart contracts developed in the Ethereum blockchain system without suffering the standard issues surrounding reusability, consistency, and automation. A specific FSPVM, denoted as FSPVM-E, was developed in Coq based on a general, extensible, and reusable formal memory (GERM) framework, an extensible and universal formal intermediate programming language, denoted as Lolisa, which is a large subset of the Solidity programming language that uses generalized algebraic datatypes, and a corresponding formally verified interpreter for Lolisa, denoted as FEther, which serves as a crucial component of FSPVM-E. However, our past work has demonstrated that the execution efficiency of the standard development of FEther is extremely low. As a result, FSPVM-E fails to achieve its expected verification effect. The present work addresses this issue by first identifying three root causes of the low execution efficiency of formal interpreters. We then build abstract models of these causes, and present respective optimization schemes for rectifying the identified conditions. Finally, we apply these optimization schemes to FEther, and demonstrate that its execution efficiency has been improved significantly.