IEEE - Institute of Electrical and Electronics Engineers, Inc. - FEther: An Extensible Definitional Interpreter for Smart-contract Verifications in Coq.
|Author(s):||Zheng Yang ; Hang Lei|
|Publisher:||IEEE - Institute of Electrical and Electronics Engineers, Inc.|
Recently, blockchain technology has been widely applied in the financial field. Therefore, the security of blockchain smart contracts is among the most popular contemporary research topics. To... View More
Recently, blockchain technology 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 proof en-gine, denoted as FEther, for Ethereum smart contract verification. Based on Lolisa, which is a large subset of Solidity mechanized in Coq, FEther guarantees the consistency between smart contracts and its formal model. Combining symbolic execution with higher-order logic theorem-proving, FEther contains a set of automatic strategies that execute and verify the smart contracts in Coq with a high level of automation. Besides, in FEther, the verified code segments also can be reused to assist in the verification of other properties. 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.View Less