A system and method for formal verification of smart contracts based on state space

Abstract

The present invention relates to a system and method for formal verification of smart contracts based on state space. The system includes: a code compilation module for compiling smart contract source codes into source codes and virtual machine operation instruction byte code sequences; basic block division The module is used to divide the byte code sequence of the virtual machine operation instruction into a set of basic blocks; the control flow graph generation module is used to generate the control flow graph containing the condition identifier; the logic rule module is used to convert the condition identifier into a logic rule condition ; The source code formalization module is used to analyze the behavior elements from the source code and save it as a formal behavior file; the model generation module is used to generate a behavior model file according to the formal behavior file; generate execution according to the logic rule condition and control flow graph Model files; Execution and Validation Modules for obtaining state space reports and state space directed graphs. Compared with the prior art, the invention has the advantages of comprehensive detection, high efficiency, and ability to intuitively reflect abnormal states.

Description

technical field [0001] The invention relates to the technical field of blockchain, in particular to a state space-based smart contract formal verification system and method. Background technique [0002] Blockchain is a new application mode of computer technology such as distributed data storage, point-to-point transmission, consensus mechanism, and encryption algorithm. The technology of using a decentralized consensus mechanism to maintain a complete, distributed, and immutable ledger database enables participants in the blockchain to implement a unified ledger system without establishing a trust relationship. Smart contracts are based on immutable data on the blockchain and can automatically execute some pre-defined rules and terms. Digitally writing smart contracts into the blockchain to disseminate, verify or execute contracts in an informative way allows for trusted transactions that are traceable and irreversible without a third party. [0003] In the application of...

AI Technical Summary

Problems solved by technology

[0004] 1. Existing technologies still mainly rely on manual verification, with heavy workload, low degree of automation, and high time cost. The correctness of the model cannot be guaranteed, and the correctness of the model depends on the programmer's modeling experience and technical level

[0005] 2. Most of the current methods are limited to loopholes at the coding level. For problems such as logical loopholes such as concurrent behavior in the blockchain network, and resource consumption at the bottom of the operating environment, they lack a complete verification strategy and the ability to describe potential bugs

[0006] 3. The existing formal verification strategy establishes a complete formal model based on the source code of the smart contract, and checks all possible execution paths. However, the contract execution process itself will contain a large number of actual unreachable paths, and complete detection will generate unnecessary the cost of

[0007] 4. The methods are scattered, and the models established by common formal verification methods are not standardized. Even if a security vulnerability is detected in the contract code, it may take time to locate and troubleshoot, and the usability is poor

[0009] The smart contract formal verification system and method still have the following shortcomings: 1. It only targets the loopholes in the coding level of the contract source code, ignoring logical loopholes such as behavior concurrency in the blockchain network; 2. Only theorem proofs are used in the formal proof Verification results, the verification strategy is one-sided; 3. It is necessary to check all possible execution paths, and the detection cost is high

Images