contract vulnerability

IEEE Access

Blockchain technology adds records to a list using cryptographic links.\nTherefore, the security of blockchain smart contracts is among the most popular\ncontemporary research topics. To improve the theorem-proving technology in this\nfield, we are developing an extensible hybrid verification tool chain, denoted\nas FSPVM-E, for Ethereum smart contract verification. This hybrid system\nextends the proof assistants in Coq, a formal proof-management system.\nCombining symbolic execution with higher-order theorem-proving, it solves\nconsistency, automation, and reusability problems by standard theorem-proving\napproaches. This article completes the FSPVM-E by developing its proof engine.\nFSPVM-E is an extensible definitional interpreter based on our previous work\nFEther, which is totally developed in the Coq proof assistant. It supports\nalmost all semantics of the Solidity programing language, and simultaneously\nexecutes multiple types of symbols. FEther also contains a set of automatic\nstrategies that execute and verify the smart contracts in Coq with a high level\nof automation. The functional correctness of FEther was verified in Coq. In\nstandard tutorials, the execution efficiency of FEther far exceeded that of the\ninterpreters developed in Coq.\n

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