A Formal Validation System Interpreter Model For EOS Smart Contract

With the development of blockchain technology,the security of blockchain has become a hot topic in computer science.Formal Symbolic Process Virtual Machine(FSPVM)is one of the most powerful verification toolchains which guarantees the security of the smart contract,but currently only the formalized validation engine FSPVM-E that supports validating the Ethereum smart contract written in Solidity is available,and its interpreter FEther-E cannot support validating the EOS smart contract written in C++.The research on extend the structure of the interpreter model to support formal verification of EOS intelligent contract is a problem worth studying.In current thesis,the original FEther supporting Ethereum is renamed as FEther-E,and the research target of this thesis is to extend the original FEther-E model of to support EOS smart contract formal verification,named FEther-C++.A conditional divider is embedded into the intermediate language parser of FEther to support the formalization of the scope error exit.A variable semantic layer is embedded into the FEther-E to construct a new structure which can analyze the formalization of variable syntax features.By classifying the error detection operations and formulating the corresponding structure,a variety of error detection code from FEther-E are integrated.The error detection module is also constructed into FEther-C++ in order to define the error detection operations.In addition,the structure of interpreter environment variables has been reconstructed;The local variable scope table stack and global variable table are expanded through adding a new memory state register structure which supports the formalization of features of scope changes.Furthermore,two formal schemes of C++ syntax features have been presented in current study.First,FEther-C++ formalizes the syntax features of C++ variables by defining variable declarations,variable reading,variable writting,variable destruction behavior.Second,the logic control flow for these operations also have been formalized in FEther-C++.Based on the feature formalization scheme of the first point,FEther-C++ formalizes the feature of variables scope by constructing the formal definition of local variables and global variables,developing the logic flow about verification classification and functionality of accessing those two types of variable speficiations.The experimental part of this paper presents two pieces of smart contract code written in C++.These two code sections contain C++ syntax features including variable declaration,variable assignment,scope exception exit,and function parameter invoking.The experimental results demostrate that FEther-C++ can support the verification of EOS smart contract written by C++ based on FSPVM.Besides,similarly to FEther-E,because some language features of C++ also appear in other mainstream languages,such as JAVA and Python,the FEther-C++ also can be extended to support formal verification of programs written by other programming languages.