Smart Contract Entry Series | An important part of smart contract engineering: formal verification method

Beijing University of Aeronautics and Astronautics Distributed Laboratory Beijing Institute of Aeronautics and Astronautics Yunnan Innovation Institute Zhou Chuhan Hu Kai

Formal Verification is an important part of smart contract engineering. It can be a technique for deterministic verification of contracts. By formalizing language, the concept, judgment and reasoning in contracts can be transformed into smart contract models, which can eliminate The ambiguity and non-universality of natural language, and then use formal tools to model, analyze and verify smart contracts, conduct conformance testing, and finally generate verified contract codes to form a credible full lifecycle of smart contract production.

Formal verification

Formal Verification is based on the theory of Formal Method. The formal method originated from the research of compiler technology in the 1950s. In the 1960s, the "software crisis" occurred. At that time, there were two solutions to the "software crisis": one was to use reasonable and effective engineering methods. Management and organization of the software development process, which is also the origin of software engineering; the other is to establish a rigorous mathematical derivation theory to guide the software development process, which advances the in-depth study of formal methods.

• The BTC has been halved for six months, but the miners have "surrendered"?
• ShapShift, an established exchange, announced the implementation of “zero fee”, which refers to hosted exchanges such as Coinbase.
• Algorand 2.0 released, providing standardized asset creation, atomic transfer and smart contracts in Layer 1.

Formal methods mainly include formal stipulations and formal verification. Formal stipulation refers to the application of formal language with precise grammar and semantics to describe the nature and behavior of the system. It is the basis for designing system constraints and verifying whether the system is correct. Formal verification is based on formal stipulations, establishing system behavior and The association of its nature, in turn, verifies the critical nature of the system's needs. There is a close relationship between formal verification and formal specification. Formal verification is to verify that the existing program (system) P meets the requirements of its specification (φ, ψ) (ie P(φ, ψ)). It is also the core problem to be solved by the formal method.

At present, the common formal verification methods can be divided into two categories: deductive verification and model detection. Deductive verification is mainly based on the basic idea of ​​Theorem Proving. It uses logical formulas to describe the system and its properties. It proves that the system has certain properties through some axioms or inference rules. At present, the main deductive verification tools are: STeP (Stanford Theorem Prover) based on Manna-Pnueli proof system, TLV, machine theorem proving device (ACL2, Coq, HOL, Isabelle, Larch, Nuprl, PVS, TPS). The basic idea of ​​the Model Checking method is to confirm whether the contract has certain properties through a state space search. That is, given a contract (procedure) P and a statute ψ, the corresponding model M is generated, and then the proof M ╞ψ, that is, the statute formula 成立 is established in the contract model M, thus proving that the contract (procedure) P satisfies the statute ψ. Commonly used model verification tools are: SMV (Symbolic Model Verifier), SPIN (Simple Promela Interpreter), SDL (Specification and Description Language), UPPAAL, and the like.

Model detection technology is one of the most successful automatic verification techniques in the past 30 years. It is widely used in the verification of finite state systems, including circuit design and communication protocol analysis and verification. According to the specification characteristics of the model to be verified, it can be divided into a composite tester, a temporal logic model detector and a behavior consistency checker. According to the different technologies used, it can be divided into: state-oriented model detection and symbol model detection. The basic principle of the model detector is the same, and its working principle is shown in Figure 1. Often, the model requires an iteratively validated process to finally meet the validation criteria.

Figure 1 Model detector principle

Formal verification is a mathematical and logical based approach that formalizes the code and documentation of a smart contract before it is deployed, and then mathematically rigorously proves the security and functional correctness of the code. It can effectively detect whether there are security vulnerabilities and logical vulnerabilities in smart contracts. This method can effectively make up for the defects of the traditional logic of finding code logic by manual experience. The advantage of formal verification technology is that it is impossible to exhaust all possible inputs by means of traditional testing, and we can overcome this problem with a mathematical proof and provide a more complete security audit.

2. The application status of formal verification in the field of blockchain

With the generalization of blockchain platform-level applications, the amount of smart contracts involved has grown exponentially, and the security issues of smart contracts have become the focus of attention of investors and developers. This year, several ERC-20-based projects have been hacked because of vulnerabilities in smart contract codes, resulting in huge losses for investors. In order to prevent similar incidents, exchanges, wallets, project parties, etc. all increase investment in smart contract security, and the surrounding ecology around smart contract security has become a hot spot of investment.

Formal verification technology has been successfully applied in the field of high-system security requirements such as military and aerospace. The formal method is applied to smart contracts, which makes the contract generation and execution have normative constraints, which ensures the credibility of the contract. Sex, so that people can trust the production process and execution effectiveness of smart contracts. Through formal language, the concept, judgment and reasoning in the contract can be transformed into a smart contract model, which can eliminate the ambiguity and non-universality of natural language, and then use formal tools to model, analyze and verify intelligent contracts. test. The formal verification of the contract guarantees the correct attributes of the contract, the automated code generation improves the efficiency of the contract generation, and the conformance test of the contract guarantees the consistency of the contract code and the contract text.

At present, the products related to formal verification in the blockchain industry can be divided into three categories: VaaS platform, public chain, and language. The application is still in the early stage of technology, the degree of automation and practicality, and the user tools still need to be greatly progress.

(1) Vaas platform

It is a platform that provides formal verification services directly to developers. Currently Vaas projects include CertiKzecurify.ch, Runtime Verification and other projects. Currently, CertiK is still in its infancy, and the beta version of Securify.ch is online, and Runtime Verification is already in commercial operation.

Unlike several other projects, Runtime Verification is based on EVM virtual machine binary code for formal verification, not for the high-level language used by the smart contract itself, so it is further safer, avoiding the possibility of compiler compilation. The resulting vulnerability.

(2) Language

Language products are generally sub-language of functional languages, providing developer libraries and tools related to formal authentication of smart contracts. Currently there are projects such as Imandra and Tezos.

Among them, Imandra released a model of open source Ethereine virtual machine marked with ImandraML language, and focused on the formal verification of financial applications such as exchanges to ensure the legal compliance of financial transactions, allegedly related technology has been used The trading system of the top investment bank on Wall Street.

(3) Public chain

The public-chain products that directly include the formal verification engine are currently only available in The Matrix project, characterized by AI-assisted formal verification and dynamic constraint checking. Whether AI is helping to automate formal verification is still technically unknown.

3. Formal verification of smart contracts

The security verification problem of smart contracts is imminent. The main security risks of smart contracts are: 1) one of the contracts uses contract vulnerabilities to modify the contract, so that the contract execution results are biased toward one party; 2) the smart contract attacker uses the contract vulnerability to attack the contract. , resulting in the loss of property in the contract. This will eventually lead to people's distrust of smart contracts. In the verification of smart contracts, the formal verification method can check many attributes of smart contracts, such as fairness, reachability, boundedness, livelock, deadlock, unreachability, and stateless ambiguity. . The formal approach focuses on solving the credibility of smart contract generation and execution. The advantage of using model detection is that it is fully automated and fast to verify, even if only a partial description of the contract is given, the search can also provide useful information about the correctness of the known part. It is especially important that when the nature is not met, the search termination can give a counterexample, which often reflects subtle errors in the contract design and thus greatly assists in contract troubleshooting.

Here we use the model detection tool SPIN to verify the smart contract. SPIN is a model detector used to detect and verify distributed software systems. SPIN (Simple Promela Interpreter) is a PROMELA parser, a model detector developed by Bell Laboratories and used to formalize distributed software systems. It is a formal model widely used in large-scale complex software systems. Detector, SPIN is more free and open in terms of technology and use compared to commercial model detectors.

Describe a smart contract, including the following aspects: contractor information (identity, permissions, etc.), contract state machine (contract background, contract state set, state transition function, contract input, contract output, contract initial state, and contract Termination state), the execution state machine of each contract party.

We define smart contracts , for a two-tuple, where:

Con is the basic information description of the contract, Con={CId, CTimeStamp, CTime, CSign}, CId is the contract identifier, which is the unique identifier of the contract. CTime is the time limit of the contract, that is, the validity period of the contract, and CTimeStamp is the time stamp of the contract. That is, the date of signing the contract, CSign is the signature of the contracting party.

Machine={ }, indicating the set of execution state machines of each contract party, Indicates the execution state machine of the i-th contract party.

Contract state machine =<MStatus,CInput,COutput,CFunction,CInit,CFinal,CBackground>, is a multi-group, where:

MStatus is a collection of all states of the i-th contract state machine in the smart contract and a description of the set, MStatus={ , , , }, where i represents the ith process (0 i n), A collection of processes representing the i-th process of the contract. A contract is made up of one or more processes.

CInput is the input set of the contract, CInput={CIEvent, CITime}, CIEvent is the event input by the contract, and CITime is the time of the contract input. Smart contracts have two trigger execution mechanisms, time triggering and event triggering. The contract triggers the execution of the contract through the input of time or event, so that the state of the smart contract changes.

COutput is a collection of contract output, COutput={ COData}, COData is the data output by the contract. The smart contract specification can be partially executed. Therefore, the output of the contract may be a result output in the middle of the contract execution, or it may be that the contract is fully executed. The output of the contract is uniformly represented by a data type. Each output implies a contract state transition, and each contract output corresponds to a contract state.

CFunction is a collection of contract state transition functions with CFunction:MStatus MStatus.

CInit is the contract initial state value, and .

CFinal is a collection of contract termination states, CFinal={ , , , }, and .

CBackground is a description of other relevant information about smart contracts.

In the description process of the smart contract, the state transition process of the contract represents the execution process of the contract, and the contract model uses PROMELA for contract modeling.

The verification process of SPIN begins with describing the specifications of the system model. After the analysis of the compiler determines that there is no syntax error, the interaction between the system model processes is simulated until the behaviors appearing in the system model and the expected behavior of the system design are confirmed. Consistent. Secondly, SPIN will generate an optimized on-the-fly verification program from the system's high-level specification. After the compiler compiles and executes, the execution will detect whether there is a violation of the correctness description. If there is a counterexample, return to the interactive simulation. The execution status is re-corrected to confirm the cause of the error until the correctness verification is completed. Its verification framework is shown in Figure 2.

Figure 2 Based on the SPIN verification framework

According to this verification framework, we have designed a formal verification system and achieved good verification results, which is worthy of promotion and application. A verification case will be given later.

We will continue to update Blocking; if you have any questions or suggestions, please contact us!