Formal Verification: Tezos’s Feature Nobody Talks About

Formal Verification: Tezos’s Feature Nobody Talks About

TL;DR: Formal verification is like proving a theorem but with code. The tester either gets the proof of the code’s correct operation with any input params or discovers the existing bugs. Cores of Windows and macOS, space rocket control systems, or the software for nuclear power plants all undergo formal verification as an extra space may cost billions in those cases.

Let’s say, some developers have made a smart contract and had it audited, then launched an app and even raised a billion. And then a hacker came along and stole it all: not a sensation in the world of DeFi, unfortunately. A formal verification could have helped the devs to keep their contract safe but nobody really cares about verifying contracts formally. If it could save billions, why?

How Devs Test Smart Contracts

Say, Bob wrote a smart contract for a BB token consisting of three functions: “determine the sender’s address”, “add a new user to the database”, and “transfer tokens from the sender to the recipient.” He decides to test the contract by assigning himself 50 BB and then trying to send Alice 100 BB. The contract takes 100 BB from Bob and sends them to Alice, so Bob’s balance now reads -50. That’s because he forgot to set up the function “check whether the sender has sufficient funds.”

What Bob did is called manual testing: he actually tested the result of something he had done. It’s slow and, if there are many arguments, unreliable. Therefore, Bob decides to try automatic testing. He fixes the bug and writes a test: sending 100 BB to Alice’s address would return an error related to the insufficiency of funds. The contract passes the test and Bob is happy. But will the bug show itself if you send -50 or 0.000000001 BB? Bob is no longer happy. He has to run the same script with more and more new parameters.

Why Testing Proves Nothing

The more complex the contract’s logic, the more tests have to be done with different argument ranges. In the perfect world, the entire code has to be tested, from assigning arguments to executing functions. But even if you cover 100% of the code, there’s no guarantee that a seemingly normal transaction of 322.3782 BB does not cause a critical bug because Bob accidentally put two spaces instead of one. Manual and automatic testing answer the question: “With those input parameters, does the code do what the developer intended?” Formal verification, on the other hand, answers a different one: “Does the code do what the developer intended all the time?”

It’s easier to understand this idea through the fundamental theorem of arithmetic: any integer greater than 1 can be represented uniquely as a product of prime numbers. For example:

6 = 2 × 3

84 = 2× 2 × 3 × 7

4620 = 2 × 2 × 3 × 7 × 5 × 11

The theorem can be tested infinitely in the search for a number that could be represented in two ways instead of one. As a result, the testing will not prove the theorem is correct for all integer numbers. Mathematicians argued about prime numbers since the days of ancient Greece but only in 1801 did Karl Gauss manage to formulate the theorem and publish its mathematic proof. In terms of software testing, he formally verified it.

What Is Formal Verification

To formally verify a code is to prove it corresponds to its description and works as intended: correctly with correct parameters, and returns errors with incorrect ones. Such verification finds all possible bugs in the code and allows the developers to make the contract 99.9% safe (as bugs can also hide in the compiler and the environment).

For formal verification, Bob must write a specification, i.e. describe the contract’s whole operation in a system of equations. Roughly speaking, he has to represent the code as a theorem, then input it into a formal verification machine, and then set the range of input parameters and the expected result. In the case of normal testing, the developer only sets the input parameters the code will use. Formal verification machines don’t execute the code, however: they see it as a mathematic problem like a+b=x and look for input parameters a and b to get x.

Thus, if Bob specifies the result “the user’s balance becomes negative”, the machine will either produce a set of input parameters that cause the bug and result in a negative balance or say that no such parameters exist. Formal verification is a very complex process that requires the developer to represent the code as a system of formal rules. In fact, it means writing the whole contract in a different language while retaining its logic. Therefore, even in the case of a simple smart contract, formal verification costs much more than an audit of any kind.

What Tezos Has to Do With It

The VM language Tezos Michelson and the machine itself are formally verified: they don’t have known bugs and vulnerabilities. On top of that, developers have created the library Mi-Cho-Coq for Michelson, thanks to which the formal verification machine Coq understands instructions in Michelson. It simplifies transferring the contract into a formal specification and making up a theorem for verification.

Speaking at Hong Kong Blockchain Week 2020, Arthur Breitman called formal verification one of the three pillars of Tezos and explained why it is important:

“Two of Tezos pillars are self-governing aspect and proof of stake aspect. The third pillar that the people always mention is the formal verification. Formal verification is a technique, where you use technical proof to guarantee that some piece of code is doing what it supposed to do. You find it was used in things like rocketry or nuclear power plants. For example, Ariane-5 rocket blew up because one counter had an overflow in it. A single bug can blow up a rocket, rockets are very expensive, and if you think about it like “I have some code and if anything goes wrong it will be very expensive”, then it’s worth spending some time thinking about “How can I make sure that I don’t have bugs?”. Formal verification is one of the highest standards to verify that you don’t have bugs”

As a result, Tezos became more reliable and convenient for highly secure apps and contracts.

Subscribe and never miss updates from the world of Tezos:

  1. Telegram channel
  2. Facebook
  3. Twitter in Russian and Ukrainian
  4. Twitter in English
  5. YouTube channel
  6. Instagram
  7. LinkedIn
  8. hub at ForkLog

next

Tezos Monthly: Technology, Economy, and Community in November ‘21

Read similar posts

Meet the Brand New plenty.network! More Liquidity, and More Rewards

Meet the Brand New plenty.network! More Liquidity, and More Rewards

Flash Loans: Earning Off Someone Else’s Capital

Flash Loans: Earning Off Someone Else’s Capital

Tezos DApps Updated: Naan, Temple Wallet, Youves, Smartlink, and QuipuSwap

Tezos DApps Updated: Naan, Temple Wallet, Youves, Smartlink, and QuipuSwap

Read our blog and never miss news about TezosRead Blog

Community