| Blockchain is one of the emerging technologies developed to address a wide range of disparate problems.Due to the application potential of blockchain technology in critical industry fields such as digital finance and electronic deposit and certificate,blockchain technology is of great importance to the field of national information technology innovation and has been included in the current national development strategic plan.Currently,the most critical component of blockchain technology is the smart contract.The blockchain systems manage and evaluate critical resources and businesses by corresponding smart contracts automatically.However,due to the emerging nature of blockchain technology and the savage development of related technology communities,there is a lack of unified constraints and specifications during the process of developing and applying smart contracts,so there are serious security and reliability risks in untrusted smart contracts.Therefore,there is an urgent need for verification technology to safeguard the security and reliability of smart contracts effectively.To solve the above problems,based on the higher-order logic theorem proving technology,this dissertation analyzes the problems existing in conventional theorem proving technologies and the challenges of the required design,implementation,and verification of blockchain smart contracts.Moreover,this dissertation presented a universal,efficient and scalable modular formal verification framework for smart contract security and reliability verification.The main contributions and innovations of this dissertation can be summarized as follows:(1)To achieve the entire verification of blockchain smart contracts,taking inductive calculus of construction,Curry-Howard isomorphism,and matching logic as the theoretical foundation,the feasibility of combining higher-order theorem proving and symbolic execution as an application extension of Curry-Howard isomorphism is systematically illustrated in this dissertation.Furthermore,a scalable blockchain smart contract verification framework FSPVM that is deeply embedded with the logic environment of inductive calculus of construction is purposed in this dissertation.(2)To construct an efficient executable formal memory model,this dissertation analyzes the computing efficiency problem of conventional formal memory models and the scalability problem of record datatype-based formal memory model formalization,and proposed corresponding optimization solutions.Besides,a new polymorphism and modular recursion-based abstract specifications of formal memory model with multi-level table structure and corresponding memory operations are constructed.(3)A formal specification language at the source code level,denoted as Lolisa,is proposed in this dissertation to construct FSPVM.The formal syntax in Lolisa is defined using generalized algebraic datatypes and Lolisa is a large subset of the programming languages of mainstream blockchain platforms,such as Ethereum and EOS.Most mainstream smart contracts formalization is supported by the current version of Lolisa.Besides,the syntax sugar level is introduced to encapsulate the complex specification of formal syntax,to improve the readability of the formal model.(4)To achieve the symbolic execution engine of FSPVM,the low efficiency of evaluation and verification in the process of modeling executable operation semantic modeling by traditional standard methods is analyzed in detail,and the optimization schemes are presented for this issue.Taking advantage of the above work,a definitional interpreter,whose kernel is based on the executable semantics of Lolisa,is developed in Coq proof assistant with the matching automatic verification strategy library.(5)To avoid the semantic gap and ensure the self-correctness,the essential components of FSPVM are wholly developed and certified in Coq proof assistant.Meanwhile,a "one-stop" verification platform is constructed by integrating the above components,and taking a real smart contract as an example to expounds the formal verification process and innovation characteristics of the proposed platform.At present,there are still several challenges in the field of blockchain smart contracts formal verification.The dissertation aims to construct a new theoretical foundation and technical methodology for the development and verification of secure and reliable blockchain smart contracts. |
PDF Full Text Request