Username   Password       Forgot your password?  Forgot your username? 


Formal Process Virtual Machine for Smart Contracts Verification

Volume 14, Number 8, August 2018, pp. 1726-1734
DOI: 10.23940/ijpe.18.08.p9.17261734

Zheng Yang and Hang Lei

School of Information and Software Engineering, University of Electronic Science and Technology of China, Chengdu, 610054, China

(Submitted on May 20, 2018; Revised on June 19, 2018; Accepted on July 16, 2018)


This paper reports on the development and verification of a novel formal symbolic process virtual machine (FSPVM) for verifying the reliability and security of Ethereum smart contracts, denoted as FSPVM-E, in Coq proof assistant. It adopts execution-verification isomorphism (EVI), an extension of Curry-Howard isomorphism (CHI), as its fundamental theoretical framework. The current version of FSPVM-E is constructed on a general, extensible, and reusable formal memory (GERM) framework, an extensible and universal formal intermediate programming language Lolisa, which is a large subset of the Solidity programming language using generalized algebraic datatypes, and the corresponding formally verified interpreter of Lolisa, denoted as FEther. It supports the ERC20 standard and can automatically, simultaneously, and symbolically execute the smart contract programs of Ethereum and verify their reliability and security properties using Hoare logic in Coq. In addition, this work contributes to solving the problems of automation, inconsistency, and reusability in higher-order logic theorem proving.


References: 20

              1. N. Satoshi, “Bitcoin: A Peer-to-Peer Electronic Cash System,” 2008
              2. A. W. Appel, “Verified Functional Algorithms,” 2016
              3. C. Cadar, D. Dunbar, and D. Engler, “KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs,” in Proceedings of the 8th USENIX conference on Operating systems design and implementation, pp. 209-224, San Diego, December 2008
              4. W. A. Howard, “The Formulae-as-Types Notion of Construction,” To HB Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Vol. 44, pp. 479-490, 1980
              5. Z. Yang and H. Lei, “A General Formal Memory Framework in Coq for Verifying the Properties of Programs based on Higher-Order Logic Theorem Proving with Increased,” (, 2018)
              6. The Coq Development Team. The Coq Proof Assistant (, 1999-2018)
              7. X. Leroy, “Formal Verification of a Realistic Compiler,” Communications of the ACM, Vol. 52, No. 7, pp. 107-115, 2009
              8. A. W. Appel, “Verified Software Toolchain,” Springer Berlin Heidelberg, 2011
              9. R. Gu, J. Koenig, T. Ramananandro, Z. Shao, X. N. Wu, S. C.Weng, S. C. Weng, H. Z. Zhang, and Y. Guo, “Deep Specifications and Certified Abstraction Layers,” In Proceedings of ACM Sigplan-Sigact Symposium on Principles of Programming Languages, pp. 595-608, Mumbai, India, 2015
              10. E. Hildenbrandt, M. Saxena, X. Zhu, N. Rodrigues, P. Daian, D. Guth, and G. Rosu, “KEVM: A Complete Semantics of the Ethereum Virtual Machine,” 2017
              11. Y. Hirai, “Defining the Ethereum Virtual Machine for Interactive Theorem Provers,” in Proceedings of International Conference on Financial Cryptography and Data Security, pp. 520-535, Sliema, Malta, 2017
              12. X. Zhang, W. Hong, Y. Li, and M. Sun, “Reasoning About Connectors in Coq,” in Proceedings of International Workshop on Formal Aspects of Component Software, pp. 172-190, Besancon, France, October 2016
              13. P. Wadler, “Propositions as Types,” Communications of the ACM, Vol. 58, No. 12, pp. 75-84, 2015
              14. Z. Yang, H. Lei, “Lolisa: Formal Syntax and Semantics for a Subset of the Solidity Programming Language,” (, 2018)
              15. Ethereum, Ethereum solidity documentation (, 2018)
              16. T. Duff, “On Duff’s Device,” (http://www. lysator. liu. se/c/duffs-device. html. Msg. to the comp. lang. c Usenet group, 53, 1988)
              17. X. H. Wei, C. Chen, and G. Chen, “Guarded Recursive Datatype Constructors,” ACM SIGPLAN Notices, Vol. 38, No. 1, pp. 224-235, 2003
              18. A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, “Symbolic Model Checking without BDDs,” in Proceedings of International Conference on Tools and Algorithms for Construction and Analysis of Systems, pp. 193-207, Amsterdam, The Netherlands, 1999
              19. G. Bird, Cloud Data Services, “Block Chain Technology, Smart Contracts and Ethereum,” (, accessed April 2017)
              20. X. Yang, Z. Yang, H. Y. Sun, Y. Fang, J. Y. Liu, and J. Song, “Formal Verification for Ethereum Smart Contract using Coq,” World Academy of Science, Engineering and Technology, International Science Index, Information and Communication Engineering, Vol. 12, No. 6, pp. 126, 2018


                          Please note : You will need Adobe Acrobat viewer to view the full articles.Get Free Adobe Reader

                          This site uses encryption for transmitting your passwords.