Since its inception, the formal verification (Formal Verification) method has been associated with words such as "niche, unpopular". Some people say that formal verification methods are a "military-grade" anti-hacking method, which adds a touch of mystery to this technology.

What exactly is a formal verification method?

Wikipedia explains formal verification like this:

In the design process of computer hardware (especially integrated circuits) and software systems, the meaning of formal verification is to use mathematical methods to prove its correctness or incorrectness according to one or some formal specifications or properties.

The sense of mystery probably comes from the two rigorous and abstract keywords in the definition - "formal specification" and "mathematical method proof". In fact, uncovering this layer of mystery, you will find many interesting aspects of formal verification.

The question I want to discuss in the following article is: At this stage, which of the following stories can really satisfy your imagination of formal verification? Can formal verification really catch on as a technology in the blockchain space? If so, how can it be done?

(PS: The concept of "formal specification" mentioned above will also be discussed below.)

To answer the above questions, we can first consider another simpler question:

>At this stage, what do people use formal methods for?

There are only two answers to this question:

>1. Avoid mistakes

>first level title

| avoid mistakes

Avoiding mistakes is actually avoiding losses.

Let's first explore, which areas have zero tolerance for programming errors? In which areas, the loss caused by programming errors is immeasurable?

In fact, formal methods have been popularized since hardware design. A famous example is: Intel's Pentium CPU floating-point unit made an error (FDIV Bug), and tens of thousands of CPUs had to be recycled and replaced, causing huge losses to Intel (475M $)[1].

Since then, Intel has adopted formal methods extensively in its chip design.

Computer hardware giants such as IBM, AMD, NVIDIA and CADENCE[2] are also users of formal methods...

To say that you can learn a lot of wisdom through a ditch, in fact, there are trial and error people in all walks of life, and it is the same in the industrial world. For example: In 1996, the first launch of the European Space Agency's Ariane 5 (Ariane 5) rocket, due to the wrong command sent by the inertial navigation system (floating point number converted to an integer causing overflow), the rocket was only 37 seconds after launch. Then it deviated from the predetermined track and finally crashed. The European Space Agency's huge research and development funding (8B $)[3] went up in flames.

Shortly thereafter, EADS began using formal methods to develop the mission scheduling model for the Ariane rocket.

The National Aeronautics and Space Administration NASA and the British Ministry of Defense successively issued design standards in the 1990s [4], among which the use of formal methods was listed. my country's Yutu lunar rover control system and my country's first self-developed space vehicle embedded real-time operating system SpaceOS[5] also verify their correctness through formal methods.

The development of history tells us that money is the first driving force to promote social development! No one can afford to sigh the huge losses caused by program errors.

If the above two stories sound too heavy, let's take a look at the following picture:

The figure above shows the global distribution of metro projects developed using formal methods [6].

It can be seen that starting from the Paris subway signaling system, formal methods have been widely used in the development of subway systems in major countries in North America, Europe, Asia, and some countries in South America. This is perhaps the reason why we almost never hear of major losses and disasters due to subway system failures.

Again, money is the primary productive force.

Now that the contribution of formal methods in ensuring daily travel has been widely recognized, in the field of digital assets developed on the basis of blockchain technology, formal verification technology can be used to ensure the security of smart contracts, thereby protecting property The idea of ​​security becomes reasonable and even urgent.

What should I do? Here is a brief introduction.

First of all, it is necessary to introduce the concept of "formal specification".

Formal specification (formal specification) refers to the strict and comprehensive implementation of the expected behavior of the system (such as transferring a number of S tokens from account A to account B) and properties (such as transfer will not cause the overflow of account B) through mathematical language. Definition. Formal specifications often define the correctness and security of a system.

Given a formal specification of a system, we can iteratively design and implement the system starting from the specification. In each step of the iteration, we can mathematically strictly ensure that the system produced by the iteration is consistent with the specification or system before the iteration through a series of methods including refinement, synthesis, and formal proof.

In addition to designing and implementing a system from a formal specification, we can also use a series of methods including symbolic execution, model checking and formal proving to verify the existing design and Implementations are consistent with this specification.

Sounds grand, right?

For example, for a smart contract program, we can start from all possible inputs (such as the combination of function parameters) and initial state (such as the combination of initial values ​​of state variables), according to the semantics of each statement, sentence by sentence Deduce all possible end states of the program (such as the value of the state variable and the generated event log after the execution of the contract), and check whether the combination of all inputs, initial state, and end state of the contract is consistent with the formal specification. This is a bit similar to how Conan solved the case, step by step. However, all the definitions here are described in strict mathematical language, and the derivation and inspection are also strict mathematical derivation and proof. Depending on the complexity of the system to be verified and its formal specification, derivations and proofs can be constructed manually or automatically generated by machines.

first level title

| Against attack

Adversarial attack is actually another sense of avoiding losses.

The story begins with an electronic attack by the US military. In the summer of 2015, a hacker was ordered to launch an electronic attack on the U.S. military’s Little Bird unmanned helicopter and took control of the drone. However, when the U.S. Department of Defense redeveloped the UAV's core control program, hackers used all the attack methods in the world today, but failed to break through the newly deployed system [7].

What kind of technology gives Little Bird its super defense ability, so that it blocks all attacks? The answer is: formal verification methods.

Formal verification methods ensure that program behavior is consistent with expectations through rigorous mathematical proofs, but the correctness of formal verification programs is very labor-intensive. Therefore, unlike general techniques such as program testing, formal verification methods are often only applied to security Critical domains, such as program correctness verification for drones, spacecraft, operating systems, etc.

What I have to mention here is Dirty Cow (CVE-2016-5195)[8], a very serious Linux operating system kernel vulnerability discovered in 2016. Attackers can use this vulnerability to obtain the highest privilege of the system, so that the entire system can be exploited. in the state of use.

first level title

| Security-critical blockchain field

The same is true in the blockchain field. On the one hand, small mistakes can lead to big losses; on the other hand, huge economic benefits can also attract a large number of attackers.

In the first major Ethereum hacking case, The DAO, the attackers stole Ethereum worth US$55 million at the time, which led to a hard fork of Ethereum[11]; after that, attacks related to Ethereum smart contracts have been Continuing—for example, in November 2017, the Ethereum Parity wallet was hacked, causing users to lose digital assets worth approximately $150 million [11].

According to statistics from Ambi Labs, in the first half of 2018 alone, about $1.1 billion in digital assets have been stolen, and vulnerabilities related to blockchain systems (such as smart contract vulnerabilities in Ethereum) and the ecosystem surrounding digital assets Security issues (such as the theft of multiple centralized exchanges) are emerging in an endless stream.

At present, the relevant loopholes in the blockchain system and the security issues of the digital asset ecosystem are ultimately related to the design and implementation of related programs. Before formal methods, such problems were mostly discovered through program testing.

In the early days when formal verification entered the blockchain field, Yoichi Hirai of the Ethereum community did a complete formal modeling of Ethereum's smart contract virtual machine EVM. In addition, a team from UIUC University also formally modeled and verified EVM [12]. EVM is the underlying core of Ethereum smart contracts. It is related to the security of Ethereum and involves major issues such as digital asset protection, which has attracted widespread attention from the community.

In addition, the MakerDAO project released the first formally verified decentralized application (DApp) [13]. MakerDAO is an Ethereum-based smart contract platform that provides stablecoins, collateral loans, and decentralized community governance functions. In order to ensure the security of the smart contracts deployed, the MakerDAO team verified the contract code of the core engine contract of the mortgage loan (CDP) through K-Framewok, thus showing that its smart contract program can completely resist hacker attacks.

Ambi Labs has also done a lot of work on the formal verification of Ethereum smart contracts, proposed a formal verification framework for smart contracts, and proved some common Token contracts within this framework, such as ERC20, ERC721, etc. (including General functions such as transfer, Token total amount, etc.). These mathematically proven smart contracts can be used directly without worrying about security issues. These contract source codes and proof processes have been contributed to the community in the form of open source [14].

first level title

https://github.com/sec-bit/tokenlibs-with-proofs

| Conclusion

Most people think that the formal verification method is unfathomable. The reason is that the formal verification method is not a general technology, but a specific technology that needs to be combined with the field to exert its value. In the field of blockchain, whether the formal method is a nice to have or a must have is also inseparable from the characteristics of the project.

As the exploration of blockchain technology and project applications continues to deepen, the project party's demand for avoiding mistakes, resisting hacker attacks and avoiding property losses has become stronger and stronger.

first level title

Written at the end | How much do you know about the entanglement between Verification and Testing?

Finally, let’s talk about the relationship between Formal Verification and Testing.

"Program testing can prove the existence of errors, but it cannot prove the absence of errors." Edsger Dijkstra (the winner of the Turing Award in 1972 and the proposer of the core idea of ​​the formal method) commented in this way.

In practice, especially in scenarios where the code is sufficiently complex, the verification effect of formal verification (Verification) and program testing method (Testing) is as different as clouds and mud.

For example: In 2009, scientists in Australia used formal methods to conduct a complete functional verification of the seL4 microkernel of the industrial-grade operating system [15]. The verification methods were carried out in two ways: formal verification and program testing. The result of the verification is: more than 460 bugs were found by the formal method, but only 16 bugs were found by the program test.

What's more interesting is that in the field of formal verification known for its high verification cost, the verification cost of fully verifying the seL4 microkernel is only 6 million U.S. dollars, while the cost of passing the CC EAL6 certification by testing is as high as 87 million U.S. dollars [15 ].

It can be seen that formal verification can provide a stronger security guarantee for the seL4 microkernel more economically.

references

references

【1】History of Formal Verification at Intel

https://dac.com/blog/post/history-formal-verification-intel

[2] Wang Jian: Let’s talk about Formal Verification

http://chainb.com/?P=Cont&id=1957

【3】Modeling and Validation of a Software Architecture for the Ariane-5 Launcher

https://link.springer.com/chapter/10.1007/11768869_6

【4】Tenth NASA Formal Methods Symposium 

https://shemesh.larc.nasa.gov/NFM2018/

[5] The domestic SpaceOS operating system used by Yutu is expected to be derived into a civilian version in the future

http://blog.sina.com.cn/s/blog_ae55841d0101hemg.html

【6】Cimatti, A., Corvino, R., Lazzaro, A., Narasamdya, I., Rizzo, T., Roveri, M., Sanseviero, A. and Tchaltsev, A., 2012, July. Formal verification and validation of ERTMS industrial railway train spacing system. In International Conference on Computer Aided Verification (pp. 378-393). Springer, Berlin, Heidelberg.

【7】COMPUTER SCIENTISTS CLOSE IN ON PERFECT, HACK-PROOF CODE https://www.wired.com/2016/09/computer-scientists-close-perfect-hack-proof-code/

[8] Use Dirty Cow to realize docker escape

https://www.anquanke.com/post/id/84866

【9】CertiKOS: Yale develops world’s first hacker-resistant operating system

https://www.ibtimes.co.uk/certikos-yale-develops-worlds-first-hacker-resistant-operating-system-1591712

【10】Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang and Zhaohui Li. A Practical Verification Framework for Preemptive OS Kernels. Proc. 28th International Conference on Computer Aided Verification (CAV’16)

【11】Analysis of attack methods against THE DAO from a technical point of view

https://www.8btc.com/article/93713

【12】kframework/evm-semantics

https://github.com/kframework/evm-semantics

【13】Venture capital giant A16Z invests in stable currency project MakerDAO

https://www.jinse.com/bitcoin/246582.html

[14] Constructing formal proofs to solve smart contract security issues - your contract needs to be proved urgently

https://mp.weixin.qq.com/s/xUNKT8v9ikEYFnuMWzvXdg

【15】Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009. seL4: formal verification of an OS kernel. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles (SOSP '09).