Abstract: Chain block chain alliance intelligence contracts formal verification reveal, explains why we contract for block chain intelligence to formal verification, and the classification of formal verification and industry for each classification introduced by formal verification tools, finally the author describes the current problems and facing a variety of approaches to formal verification technology development outlook for this field.

This article is shared from huawei Cloud community “These smart contract vulnerabilities, may affect your account security!” , author: Maidong dad.

What is formal validation?

In the design process of computer hardware (especially integrated circuits) and software systems, formal verification refers to the use of mathematical methods to prove the correctness or incorrectness of one or more formal specifications or attributes. Traditionally used in the field of hardware design. The main reason is that hardware takes a long time to design, costs a lot, and is hard to change once it’s in production. For example, if a CPU design has a chip, then something wrong is a big deal. Formal validation falls into three broad categories: AbstractInterpretation, FormalModel Checking (also known as feature Checking), and theorem proving.

Why do blockchain smart Contracts need formal validation?

Programs that can be programmed and run automatically in a blockchain system are called smart contracts. Smart contracts were first used on the Ethereum blockchain platform, such as Solidity, a smart contract programming language, to enable traditional application developers to write smart contracts. In the early days, there were only a few hundred people around the world who would write smart contracts for Solidity. With the rise of Ethereum and blockchain, the number of people who would write smart contracts for Solidity was increasing, but compared to the overall IT market, there were still too few people who would write smart contracts for Solidity. Lots of IT professionals who want to develop smart contracts have to learn Solidity. In order to enable more IT professionals to participate in smart contract writing and business rules implementation, the Smart Contract Platform extends the support of Solidity to more mainstream and even higher level languages, making IT possible for more IT professionals to write smart contracts. A large number of developers familiar with Java, Go, Php and other technical programming can participate in the development of smart contracts.

However, because blockchain transactions are immutable, errors in the smart contract code can have devastating consequences, undermining trust in the underlying blockchain technology. For example, the infamous TheDAO breach resulted in the loss of nearly $60 million worth of Ether, and the parity wallet breach resulted in $169 million worth of ether being locked forever. The only remedy to resolve these events is to hard fork the blockchain and restore one of the forks to the state it was in before the event occurred. However, this remedy in itself is devastating, as it destroys core blockchain values such as immutability and decentralized trust. However, smart contract is written for the purpose of industrial application, once applied in practice, we must consider the security of smart contract, smart contract to achieve machine credibility, it must first eliminate the destruction of smart contract caused by human factors. Intelligent contract formalized validation provides a can prove safety inspection mechanism, through the formal language of the contract concept, judgment, reasoning into intelligent model contract, can eliminate the ambiguity of natural language, no generality, and the use of formal tools for intelligent modeling, analysis and verification contract, consistency test, finally validated contract code automatically generated, Form a trusted full life cycle of smart contract production. The security risks that have appeared in the market can be investigated and audited. After auditing, the natural security of smart contract code is enhanced. Meanwhile, the formal verification of smart contract is also the most reliable measure to ensure the security of smart contract at present. The application of blockchain and smart contract in the industry requires formal verification of smart contract to eliminate security risks.

Classification of formal validation methods for smart contracts

The industry generally has a few general methods for formal validation of smart contracts, which can be divided into the following general methods, each method is supported by a number of tools and frameworks.

1. Theorem proof

Theorem proving is a formal method of using deductive reasoning to provide proof in symbolic logic. In this approach, each step of the proof introduces an axiom or a premise and provides a statement, which is deduced using predicate logic to arrive at the desired result. A theorem prover is often used to assist in proving that the system meets key expectations, because it requires a manual proof to be turned into a series of symbolic calculations that can be run on a computer and can be checked for correctness.

The advantage of this approach is that it uses mathematical methods to derive from axioms or premises, ensuring the rigor of verification. The disadvantage is that before mathematical verification, different types of source code need to be converted into relevant framework verification code, and currently there is no good way to ensure the consistency of the conversion between source code and verification code, the realization of high cost, low level of automation, correctness is also difficult to guarantee. In the field of blockchain smart contract, high privacy, security, functionality, semantic consistency and other strong needs are generally guaranteed through this method.

The industry has implemented many tools and frameworks to support this capability in theorem proving. There are some basic tools as follows:

Solidity* and EVM*, the framework verifies the correctness of the Solidity smart contract runtime using the functional language F*, a functional programming language used to formalize validation of program correctness.

Corral is an analysis tool for the Boogie language. By default, Corral performs bounded searches until the depth and fixed number of recursions reach a certain limit, and Boogie is an intermediate validation language designed to build the middle layer of validation programs in other languages.

Coq is an interactive theorem proving assistant that provides a formal language for writing mathematical definitions, executable algorithms, and theorems

Isabelle/HOL is a universal interactive theorem prover based on higher order logic.

Raziel is a programming framework for validating the security of multi-party computing for smart contracts, providing safeguards for the privacy of smart contracts.

2. Symbol execution

Symbolicexecution is a program analysis technique used in computer science to derive the output of each path abstraction by using abstract symbols instead of exact values as program input variables. This technology has certain applications in hardware and low-level program testing, and can effectively find the vulnerabilities in the program. The advantages of this approach are that symbolic values are input, specific test cases can be obtained with the help of appropriate tools, and high code coverage. This approach is testing in nature and cannot prove 100% that smart contracts are fine, because it is difficult to cover 100% of all scenarios based on testing. In general, this approach is recommended for functional validation when doing contract security.

Some of the more well-known architectures in the industry for symbolic execution are:

  • SASC, a tool used to identify potential logical risks, is a static analysis tool and can generate a topology of the calling relationship.

  • MAIAN, a tool used to query for vulnerabilities, is designed to track properties in smart contracts using symbol analysis and concrete validators.

  • Securify, a tool used for security vulnerability analysis, is a tool specifically for Ethereum smart contracts.

  • Mythril, a tool used for code security analysis, is a symbolic execution tool for ethereum’s smart contracts.

  • Verx is a validator that automatically verifies the functionality of Ethereum smart contracts, and ethereum-related issues can be increased by using a combination of the above three tools.

  • Oyente, a tool used to detect potential security vulnerabilities in contract code, is a testing tool based on symbolic execution techniques.

3. Model detection

Modelchecking, proposed by Clarke and Emerson, Quelle and Sifakis, is an important automatic verification and analysis technique. It mainly verifies the modal/propositional properties of finite state concurrent systems by explicit state search or implicit fixed point calculation. The basic idea is that it is much easier to test whether a structure satisfies a formula than to prove that the formula satisfies all the structures, so a new form of verification of formula satisfiability on a finite state model is created for concurrent systems. This method is also used to verify the correctness of smart contracts.

It has the advantages of using existing model inspection tools on the market and supports automated validation with less human involvement. However, it cannot guarantee the completeness and correctness of the model detection tools used. The complexity of the contract is too high, which will lead to the explosion of the state space, and then lead to the failure to complete the verification ability. In general, you need to ensure that the contract is secure, and functionality uses this approach.

There are also a number of such tools and architectures in the industry:

  • NuSMV, a tool used for industrial design validation, is highly reliable and is designed as an open architecture for model checking. It is a re-implementation and extension of the SMV tool, which was the first BDD based model inspector.

  • BIP, a framework that includes a complete set of tools to support modeling, model transformation, simulation, validation, and code generation, as well as hierarchical structures, is designed to be a generic, system-level, formal modeling framework.

  • Prism, a tool designed only for systems exhibiting random or probabilistic behavior, is designed as a probabilistic model checker to formally model and analyze probabilistic behavior.

  • SMC, a tool designed as a model detector to examine the safety and viability of concurrent programs under different fairness assumptions.

4. Formal modeling

The relationship between different components can be defined through accurate mathematical statements and model components to eliminate the ambiguity in the system. This kind of design system technology is formal modeling. The simulation results of the system based on this method can be reproduced, and there will be no accidental events. The advantage of this method is that the system is designed with precise mathematical statements or model components to ensure that the simulation results can be reproduced. However, this method mostly uses the existing modeling framework in the market, and the completeness and correctness of the framework cannot be guaranteed. Privacy, security, and functionality based on smart contracts can be tested using this approach. Hydra, a framework based on formal modeling, encourages developers and users to honestly disclose bugs and bugs in smart contracts. Its design is based on bug bounty patterns and NNVP programming.

5. Finite state machines

Finite state machine (FINite-state machine) is a tool used to model the behavior of an object. Its function is to describe the sequence of states that an object experiences during its life cycle and how it responds to various events from the outside world. The execution of a smart contract can also be viewed as a transition from one state to the next.

The advantage of this approach is that it is simple in mind, abstracts smart contracts into the form of a state machine, is easy to operate, and has a graphical interface. However, the quality of the state definition has a strong correlation with the verification of smart contract, and the complexity of the contract will also lead to the explosion of the state space. For the security of smart contracts, semantic conformance validation is typically used this way.

Common tools in the industry are described as follows:

  • Contract Larva, a tool that verifies the security of the smart Contract runtime, currently only supports Ethereum Solidity.

  • VeriSol, a tool that supports formal checks for consistency of smart contract semantics by checking state machine workflows using access control policies.

  • FSolidM, a tool that automatically generates Ethereum smart contract code with a graphical interface that supports designing and verifying smart contracts as finite state machines.

  • SPIN, a tool that tests whether a finite-state system satisfies PLTL formulas and other properties, including whether there is a loop or reachability, is an explicit model-checking tool.

Color Petri nets

Petri nets were invented by Carl Adam Petri in the 1960s and fit the description of asynchronous, concurrent system models. The so-called colored Petri net is to add elements such as color set and model declaration on the basis of the original Petri net, which can express more complex type information. The advantage of this method is that it is based on the existing Petri net model, carries out formal verification, has good semantic description and graphical interface. However, when the smart contract logic is more complex, it may lead to a series of problems such as the difficulty of generating the reachable graph and the explosion of the state space. For the security of smart contracts, functional validation can be chosen this way.

Problems and prospects of current technology application

Although there have been some achievements and progress in the formal verification of smart contracts, the field is still in its infancy and there is still a long way to go before it is fully developed. The following problems may still exist in the commercial process:

  • Ease of use issues, formal verification usually requires people with professional knowledge to participate in debugging, usually the people who write smart contracts do not have the technology to verify the correctness of the contract, it will cost a lot of money to find professionals to spend a lot of time to complete the testing. Automated formal validation of smart contracts also has some limitations. In general, the more automated the method and framework, the more limited the nature of the validation of smart contracts. It is an urgent problem to expand the universality of automated formal validation methods and support their use by non-professionals in order to prevent the widespread use of formal smart contract methods.

  • With the time and memory of the computer performing the validation, formal validation explores as many execution states as possible to discover the possibility of errors and security issues. In this case, the upper limit of computer runtime memory and execution time become the basic limits of complex programs and protocols. In commercial scenarios, users cannot implement detection results, and long waiting and analysis are required, which also affects relevant experience.

  • Correctness issues. When we use formal validation tools, we convert the code, security objectives, and operating environment through the tools between different models, converting high-level languages to languages supported by the formal validation tools. The execution results of the tool determine the accuracy of the formalization. However, we do not have a good tool to check the accuracy of language transformations or model transformations, and lack of strict proof of semantic consistency between source code and target language. For any formal system, we need to check correctness by looking at human formal code, so this limits the general applicability of formal validation.

  • The problem of trust, the current method of formal validation of smart contract is increasing, how to judge the accuracy of this method, the need for validation, the efficiency of validation contract, all depends on the experience of the developer, this method is not different from the test without formal validation. And when the cost of solving a problem outweighs the problem, we question whether it makes sense to solve it.

We believe that with the legalization of smart contract application and the development of blockchain technology, the formal verification method will play an increasingly important role in the whole life cycle of smart contract and be more widely used. Based on the above problems and existing methods, Huawei blockchain service has also built its own formal verification tool, which gives the correctness and necessity of its proof content, and improves its verification efficiency. It also provides a path for the industry to explore and think about the use of automated formal verification.

1. Luu, L.; Chu, D.H.; Olickel, H.; Saxena, P.; Hobor, A. Makingsmart contracts smarter. In Proceedings of the ACM SIGSAC Conf. Comput. Commun.Securit, New York, NY, USA, 24, 28 October 2016; Pp. 254-269.

2. Atzei, N.; Bartoletti, M.; Cimoli, T. A Survey of Attacks onEthereum Smart Contracts (SoK). In Proceedings of the Int. Conf. Princ. Secur.Trust, Uppsala, Sweden, 22 — 29 April 2017; Pp. 164 — 186. 3. The DAO Attacked: a Code Issue Leads to $60 Million Ether Theft. com/dao-attacked-code-issue-leads-60-million-ether-theft/(accessed on 17 June 2017).

3. Liu, J.; IEEE Access 2019, 7, 77894 — 77904. [CrossRef] Liu, Z.T. A Survey on Security fication of BlockchainSmart Contracts. IEEE Access 2019, 7, 77894 — 77904.

4. Wang Puwei, Yang Hangjie, Meng Ji, et al. Design and Implementation of smart Contracts [J]. Journal of software, 2019,30 (9) : 2608-2619.

5. Hu Kai, Bai Xiaomin, et al. A method for formal validation of smart Contracts [J]. Information security research, 2016,2 (12) : 1080-1089.

Click follow to learn about the fresh technologies of Huawei Cloud