Smart Contract Entry Series | Important Links in Smart Contract Engineering: Formal Verification Methods

Distributed Laboratory of Beihang University, Yunnan Institute of Innovation, Beijing University of Aeronautics and Astronautics

Formal Verification is an important part of smart contract engineering. It can become a technology for deterministic verification of contracts. Formal language can be used to convert concepts, judgments, and inferences in contracts into smart contract models, which can be eliminated. The ambiguity and incompatibility of natural language, and then use formal tools to model, analyze, and verify smart contracts, conduct consistency tests, and finally automatically generate verified contract codes to form a trusted full life cycle for smart contract production.

Formal verification

Formal Verification is based on the relevant theories of Formal Method. Formal methods originated from the study of compilation technology in the 1950s, and a "software crisis" occurred in the 1960s. At that time, there were mainly two solutions to the "software crisis": one was to adopt a reasonable and effective engineering method to Managing and organizing the software development process is also the origin of software engineering; the other is to establish a strict mathematical derivation theory to guide the software development process, which has promoted in-depth research on formal methods.

• Technical Perspectives | After two years of developing DApps and Layer 2 networks, I switched to the Substrate camp
• Technology Viewpoint | Want to develop dApp with Wasm? You have to read the introductory tutorial (1)
• Technical Perspectives | Contract Upgrade for Python Smart Contract Tutorial

Formal methods mainly include formal specifications and formal verification. Formal specification refers to the application of formal language with precise grammar and semantics to characterize 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 specifications to establish the behavior and The nature of the relationship, which in turn verifies the critical nature of the system's requirements. There is a close relationship between formal verification and formal statutes. Formal verification is to verify whether the existing program (system) P meets the requirements of its statute (φ, ψ) (that is, P (φ, ψ)). It It is also the core problem to be solved by formal methods.

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, and proves that the system has certain properties through some axioms or inference rules. Currently the main deduction verification tools are: STeP (Stanford Theorem Prover), TLV, machine theorem prover (ACL2, Coq, HOL, Isabelle, Larch, Nuprl, PVS, TPS), etc. based on Manna-Pnueli proof system. The basic idea of ​​the Model Checking method is to confirm whether the contract has certain properties through state space search. That is, given a contract (procedure) P and a statute ψ, generating a contract model M, and then proving that M╞ψ, that is, the statute formula ψ is established in the contract model M, so that it proves that the contract (procedure) P satisfies the statute ψ. Commonly used model verification tools include: SMV (Symbolic Model Verifier), SPIN (Simple Promela Interpreter), SDL (Specification and Description Language), UPPAAL, etc.

Model detection technology is one of the most successful automatic verification technologies in the past thirty years, and is currently widely used in the verification of finite state systems, including the analysis and verification of circuit designs and communication protocols. According to the specifications and characteristics of the model to be verified, it can be divided into composite checkers, temporal logic model checkers, and behavior consistency checkers. According to 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. Generally, models need to go through an iterative verification process to finally meet the verification conditions.

Figure 1 Principle of model detector

Formal verification is a method based on mathematics and logic. Before the smart contract is deployed, its code and documents are formally modeled, and then the security and functional correctness of the code are strictly proved by mathematical means. Can effectively detect whether there are security holes and logic holes in smart contracts. This method can effectively make up for the traditional defect of finding logic logic holes by manual experience. The advantage of formal verification technology is that traditional testing and other methods cannot exhaust all possible inputs, and we can overcome this problem from the perspective of mathematical proof and provide a more complete security audit.

2. Application status of formal verification in the field of blockchain

With the popularization of blockchain platform-level applications, the amount of smart contracts has increased exponentially, and the security of smart contracts has also become the focus of attention of investors and developers. Since this year, several ERC-20-based projects have been hacked due to vulnerabilities in smart contract code, resulting in huge losses for investors. In order to prevent similar incidents, exchanges, wallets, project parties, etc. have increased their investment in smart contract security. At the same time, the surrounding ecology surrounding smart contract security has become a hot spot for investment.

Formal verification technology has achieved quite successful applications in high system security requirements such as military industry and aerospace. Formal methods have been applied to smart contracts, resulting in normative constraints on the generation and execution of contracts, ensuring the credibility of contracts. It allows people to trust the production process and execution effectiveness of smart contracts. Through formal language, the concepts, judgments, and inferences in contracts are transformed into smart contract models, which can eliminate the ambiguity and incompatibility of natural language, and then use formal tools to model, analyze and verify smart contracts for consistency test. The formal verification of the contract guarantees the correct attributes of the contract, automated code generation improves the efficiency of contract generation, and the consistency test of the contract ensures 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 platforms, public chains, and languages. Applications are still in the early stages of technology, the degree of automation and practicability, and user tools have yet 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, 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 formal verification of the EVM virtual machine binary code, instead of the high-level language used for the smart contract itself, so it goes a step further in security and avoids the possibility of the compiler compiling process. The resulting loophole.

(2) Language

Language products are generally sub-languages ​​of functional languages ​​and provide developer libraries and tools related to formal verification of smart contracts. There are currently projects such as Imandra and Tezos.

Among them, Imandra has released a set of open source Ethereum virtual machines marked with the ImandraML language model, and focuses on formal verification of financial application scenarios such as exchanges to ensure the legal compliance of financial transactions. It is said that related technologies have been used Trading system for top investment banks on Wall Street.

(3) Public chain

The public chain products that directly include a formal verification engine currently only have The Matrix project, which is characterized by AI-assisted formal verification and dynamic constraint checking. Whether AI will help 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 that may exist in smart contracts are: 1) one party in the contract uses the contract loophole to modify the contract, so that the contract execution result is biased to one party; 2) smart contract attackers use the contract loophole to attack the contract , Causing loss of property in the contract. This will eventually lead to mistrust of smart contracts. In the verification of smart contracts, formal verification methods can check many attributes of smart contracts, such as fairness, reachability, boundedness, livelock, deadlock, unreachability, and stateless ambiguity of the contract. . Formal methods can focus on the credibility of smart contract generation and execution. The advantage of using model detection is that it is completely automated and fast to verify. Even if only a part of the contract is given, the search can provide useful information about the correctness of the known part. It is particularly important that when the nature is not satisfied, the termination of the search can give a counterexample. This information often reflects small errors in contract design, which is of great help in contract troubleshooting.

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

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

We define smart contracts Is 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 to distinguish the contract, CTime is the time limit of the contract, that is, the validity period of the contract, 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 = { }, Which represents the set of execution state machines of each contract party, Represents the execution state machine of the i-th contractor.

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

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

CInput is the contract input set, CInput = {CIEvent, CITime}, CIEvent is the contract input event, CITime is the contract input time. Smart contracts have two trigger execution mechanisms, which are time trigger and event trigger. The contract triggers the execution of the contract through the input of time or events, causing the state of the smart contract to change.

COutput is a collection of contract outputs, COutput = {COData}, and COData is the data output by the contract. The smart contract stipulates that partial execution can be completed. Therefore, the output of the contract may be a result output in the middle of contract execution, or it may be the completion of the entire execution of the contract. The output of the contract is uniformly represented by the data type. Each output means the migration of the contract state, and each contract output corresponds to a contract state.

CFunction is a collection of contract state transition functions, and has CFunction: MStatus MStatus.

CInit is the initial value of the contract, and .

CFinal is the set of contract termination status, CFinal = { , , , }, And .

CBackground is a description of other related information of the smart contract.

In the description of smart contracts, 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 starts with describing the specifications of the system model. After analysis by the compiler to determine that there are no syntax errors, the interaction between the system model processes is simulated until the behavior that appears 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 high-level protocol of the system, which will be compiled and executed by the compiler. During execution, it will detect whether the correctness statement has been violated. If there is a counter-example, it will return to the interactive simulation. Re-correct the execution status of the software to confirm the cause of the error until the correctness verification is completed. The verification framework is shown in Figure 2.

Figure 2 SPIN-based authentication framework

Based on this verification framework, we have designed and completed a formal verification system, which has achieved good verification results and 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!