Abstract. Recently, blockchain technology, which adds records to a list using cryptographic links, has been widely applied in the financial field. 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 Coq proof assistant, 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. The execution efficiency of FEther far exceeded that of the interpreters which are developed in Coq in accordance with the standard tutorial. To our knowledge, FEther is the first definitional interpreter of the Solidity language in Coq.
Yang and Lei REF developed a definitional interpreter FEther, which supports hybrid symbolic executions of Ethereum smart-contract formal verifications in Coq.
FEther: An Extensible Definitional Interpreter for Smart-contract Verifications in Coq
IEEE Access, 2019
Computer Science