CN-122020668-A - Intelligent contract auditing method and system based on model detection technology

CN122020668ACN 122020668 ACN122020668 ACN 122020668ACN-122020668-A

Abstract

The application discloses an intelligent contract auditing method and system based on a model detection technology, which belong to the technical field of blockchain, and the technical scheme is characterized by comprising a contract model construction module, a security attribute definition module, a model detection module, a result analysis module and a restoration suggestion module.

Inventors

CHEN ZHENTING
YE ZHENQIANG

Assignees

厦门慢雾科技有限公司

Dates

Publication Date: 20260512
Application Date: 20260209

Claims (9)

1. An intelligent contract auditing system based on a model detection technology, which is characterized by comprising: the contract model construction module is used for receiving intelligent contract codes, analyzing the codes to extract state variables, functions and event information of the contracts, and constructing a formal model of the contracts based on the extracted information, wherein the formal model is expressed by adopting a finite state machine or a conversion system, and abstracting an execution path of the contracts into a state conversion path in the model; The security attribute definition module is used for defining security attributes and execution specifications according to security requirements of the intelligent contract, and formally describing the security attributes and the execution specifications by adopting temporal logic or modal logic; The model detection module is internally provided with a model detector and a model detection algorithm, and the model detection module is used for checking whether a state or a path violating the safety attribute or the execution specification output by the safety attribute definition module exists in the formalized model or not through the model detection algorithm; The result analysis module is used for receiving the detection result of the model detection module, identifying a specific path, a specific state and a corresponding security vulnerability type which violate security attributes or execution specifications, counting the number and the influence degree of the vulnerabilities and generating an audit report containing vulnerability descriptions and influence ranges; And the repair suggestion module is used for generating a targeted repair suggestion according to the vulnerability type and the audit report identified by the result analysis module.
2. The intelligent contract auditing system based on the model detection technology as set forth in claim 1, wherein the contract model construction module comprises a code analysis unit and a model generation unit; The code analysis unit adopts a grammar analyzer to perform lexical analysis and grammar analysis on the intelligent contract code to generate an abstract grammar tree, and extracts the type and initial value of the state variable, the input parameter and execution logic of the function and the triggering condition of the event from the abstract grammar tree; The model generating unit defines each execution state of the contract as a state variable value collection and a binary group of a function execution stage according to the extracted information, defines operations such as function call, variable modification and the like as state conversion conditions, and constructs a finite state machine formalized model or describes a non-deterministic conversion relation among states through a conversion system.
3. The intelligent contract auditing system based on the model detection technology as set forth in claim 1, wherein the security attribute definition module includes an attribute classification unit and a formalized description unit; The attribute classification unit divides the security attribute into a basic security attribute and a business security attribute; the formalized description unit adopts CTL logic description or LTL logic description to ensure that the security attribute can be analyzed by a model detection algorithm.
4. The intelligent contract auditing system based on the model detection technology as set forth in claim 1, wherein the model detection module further comprises a state space optimizing unit, the state space optimizing unit compresses a state space of the formalized model by adopting a symbol execution technology or an abstract interpretation technology, redundant states and unreachable states are removed, and time complexity and space complexity of model detection are reduced.
5. The intelligent contract auditing system based on the model detection technology as set forth in claim 1, wherein the result analysis module comprises a vulnerability localization unit and a risk rating unit; The vulnerability positioning unit positions the corresponding key sentences in the contract codes through backward tracing of paths violating the security attribute, and associates the line numbers of the sentences in the codes; And the risk rating unit classifies the loopholes into three grades of high risk, medium risk and low risk according to the influence range and the utilization difficulty of the loopholes.
6. An intelligent contract auditing method based on a model detection technology is characterized by comprising the following steps: s1, constructing a contract model, analyzing an intelligent contract code, extracting state variables, functions and event information, and constructing a formalized model expressed by a finite state machine or a conversion system; s2, defining safety attributes, classifying and defining the safety attributes and the execution specifications according to intelligent contract safety requirements, and carrying out formal description by adopting temporal logic or modal logic; s3, model detection, namely traversing a state space of the formalized model by using a model detector, and checking whether a state or a path violating the safety attribute or the execution specification exists or not through a CTL or LTL model detection algorithm; s4, analyzing results, identifying the type of the vulnerability, positioning the vulnerability position, counting the vulnerability risk level and generating an audit report; And S5, generating a repair suggestion, and outputting a targeted code modification and logic optimization suggestion according to the vulnerability type and the risk level.
7. The intelligent contract auditing method based on the model detection technology according to claim 6, characterized in that the formalized model construction process in step S1 includes: S11, code analysis, namely generating a grammar analyzer of an intelligent contract language by using an ANTLR tool, performing lexical analysis on the contract code, splitting the code into lexical units such as keywords, identifiers, operators and the like, and generating an abstract grammar tree through the grammar analysis; S12, information extraction, traversing an abstract syntax tree, extracting the type, initial value and modification function of a state variable, parameter list, return value and execution branch logic of the function, and triggering condition of an event; and S13, generating a model, defining a value combination of each state variable and a currently executed function stage as a state, defining variable modification and branch jump caused by function call as state conversion, and constructing a finite state machine.
8. The intelligent contract auditing method based on model detection technology according to claim 6, characterized in that the specific implementation process of the model detection in step S3 includes: S31, importing a model, and converting the formalized model constructed in the step S1 into a format recognizable by a model detector; S32, importing the attribute, namely importing the formalized security attribute defined in the step S2 into a model detector; S33, state traversal, wherein a model detector adopts a depth-first search or breadth-first search strategy to traverse a state space of a model and record whether each state meets the safety attribute; and S34, generating counterexamples, wherein if the path violating the security attribute is detected, the model detector automatically generates counterexamples.
9. The intelligent contract auditing method based on model detection technology according to claim 6, characterized in that the repair suggestion generation process in step S5 includes: S51, matching the loopholes, and matching a preset repair scheme library according to the loopholes identified in the step S4; and S52, verifying supplementation, namely adding a verification step in the repair suggestion to ensure that the repair scheme can thoroughly eliminate the loopholes.

Description

Intelligent contract auditing method and system based on model detection technology Technical Field The application relates to the technical field of blockchain, in particular to an intelligent contract auditing method and system based on a model detection technology. Background An intelligent contract is a computer protocol that aims to propagate, verify, or execute contracts in an informative manner. Traditional intelligent contract auditing methods rely primarily on manual code inspection and testing, which has several drawbacks. First, manual inspection and testing is time consuming and prone to missing potential problems, particularly for complex smart contracts, the audit process can be very cumbersome and prone to error. Secondly, the accuracy of the manual audit is limited by experience and expertise of auditors, and different auditors can have different understandings and judgments, so that the consistency and reliability of audit results are affected. On the other hand, intelligent contract auditing methods based on static analysis detect potential security vulnerabilities and risks by static analysis of contract codes. However, static analysis methods may have problems with false positives and false negatives. False positives refer to marking codes in a contract that are actually secure as unsafe, while false negatives refer to the inability to discover potential problems in the contract. These problems stem mainly from the limited ability of static analysis methods to understand complex contract logic and dynamic behavior. Furthermore, static analysis methods typically only analyze static properties of contracts, and cannot cover all execution paths of the contract, so that some hidden security vulnerabilities and risks may not be discovered. Disclosure of Invention Aiming at the defects existing in the prior art, the invention aims to provide an intelligent contract auditing method and system based on a model detection technology, which have the advantages that potential security holes and risks in intelligent contracts are comprehensively, accurately and intelligently discovered and repaired by the model detection technology, and the security and reliability of the contracts are improved. In order to achieve the above purpose, the invention provides a technical scheme that an intelligent contract auditing system based on a model detection technology comprises: the contract model construction module is used for receiving intelligent contract codes, analyzing the codes to extract state variables, functions and event information of the contracts, and constructing a formal model of the contracts based on the extracted information, wherein the formal model is expressed by adopting a finite state machine or a conversion system, and abstracting an execution path of the contracts into a state conversion path in the model; The security attribute definition module is used for defining security attributes and execution specifications according to security requirements of the intelligent contract, and formally describing the security attributes and the execution specifications by adopting temporal logic or modal logic; The model detection module is internally provided with a model detector and a model detection algorithm, and the model detection module is used for checking whether a state or a path violating the safety attribute or the execution specification output by the safety attribute definition module exists in the formalized model or not through the model detection algorithm; The result analysis module is used for receiving the detection result of the model detection module, identifying a specific path, a specific state and a corresponding security vulnerability type which violate security attributes or execution specifications, counting the number and the influence degree of the vulnerabilities and generating an audit report containing vulnerability descriptions and influence ranges; And the repair suggestion module is used for generating a targeted repair suggestion according to the vulnerability type and the audit report identified by the result analysis module. The contract model construction module comprises a code analysis unit and a model generation unit; The code analysis unit adopts a grammar analyzer to perform lexical analysis and grammar analysis on the intelligent contract code to generate an abstract grammar tree, and extracts the type and initial value of the state variable, the input parameter and execution logic of the function and the triggering condition of the event from the abstract grammar tree; The model generating unit defines each execution state of the contract as a state variable value collection and a binary group of a function execution stage according to the extracted information, defines operations such as function call, variable modification and the like as state conversion conditions, and constructs a finite state machine formalized model or describes a non-determin