Research On Blockchain Application Modeling And Verification Technology Based On Security Model

With the wide use of blockchain and smart contract technology,more and more sensitive data such as digital assets and private information are stored on blockchain.Therefore,the security flaws in blockchain-enabled applications can lead to serious consequences.An effective approach for improving security is to verify these applications based on security patterns.Existing methods on pattern-based system verification start with identification of security requirements and selection of appropriate security patterns.Then these patterns and functional modules are composed into the system design model,which is verified through model checking.However,these methods focus on the composition of system modules as a whole module,and the details about how these modules are composed are omitted.This paper proposes an approach that employs the algebraic specification language SOFIA to specify security patterns and their compositions,thereby modeling the blockchain-enabled application.The specifications are then translated into the Alloy formalism and their correctness and security are verified using the Alloy model checker.This thesis mainly includes the following four aspects:1.We analyze the main structures of security pattern and give the definition of pattern.Based on this,we use the algebraic specification language SOFIA to specify data structures,operation behaviors and security requirements of security pattern.We also build the security pattern database using Neo4 j to manage and retrieve patterns.2.We give a pattern-based method to formally model blockchain-enabled applications.This method starts with decomposing the application into a collection of basic modules and composition modules,and identifies the security pattern used by each basic module.Then the specifications of basic modules are formed by instantiating the security patterns and the composition modules are specified by the dual structure of abstract and implementation specifications,where the abstract specification defines the module’s functions,and the implementation specification describes the implementation details of module compositions.3.We propose a bottom-up verification method for blockchain-enabled applications.After translating the SOFIA specifications into the Alloy specifications,the method uses the model checker Alloy Analyzer to verify the functions and security requirements of basic modules,as well as the correctness of module compositions and requirements in composition modules.A prototype tool A2 A that translates SOFIA into Alloy is also presented.4.We report two case studies on blockchain-enabled crowdfunding and online medical system with the proposed method and compare our method with the existing method.The experimental results demonstrate that the proposed method can effectively detect faults in the specifications and improve the security of blockchain-enabled applications.