Goodbye Bugs? How Formal Verification Could Fortify Smart Contracts

As a way to eliminate bugs in high-risk code, a style of software programming known as formal verification is making its way into the blockchain world.

Put simply, formal verification uses math to specify and analyze a program for errors in logic. However, because of the time and cost involved, formal verification is best reserved for situations where human life or large sums of money are at stake.

Currently, formal verification is used to verify the correctness of high-risk code in transportation, the military and cryptography. Chip companies use it to fortify algorithms before embedding them in silicon. And banks use it to develop financial algorithms.

Applied to blockchain technology, formal verification could provide assurances that self-executing transactions known as smart contracts will work as intended, eliminating some of the bugs and financial losses that come as a result of coding errors.

This year alone, bugs in Ethereum’s Parity wallet accounted for $180 million in losses. Last year, a bug in a virtual organization known as The DAO enabled a hacker to siphon $50 million from the Ethereum smart contract.  

Platforms like Cardano and Tezos are already working on smart contract languages specifically designed to facilitate formal verification. Ethereum is also working on bringing formal verification to its smart contracts.

But what is formal verification? How does it work? And why is software so difficult to get right in the first place?

To Err Is Human

Software is inherently unforgiving. If you are constructing a building, you can leave out a nail or a screw, and the structure still stands. But when it comes to software, something as simple as a single typo can cause the entire program to stop working.

“Programming languages are incredibly powerful,” Gerard Holzmann, former lead scientist at NASA, explained in an interview with Bitcoin Magazine. “As a programmer, you have to deal with a lot of detail, and unless you get every detail right, there is some effect.”  

The traditional approach to getting software right is testing. After you write an algorithm, you input a variable and check to see if it gives back the correct output. But how do you test every single input? You can’t. There are too many to test, and there could be errors lurking in the cases that you do not test.

“There are so many possible executions that really, when you test or execute, you just scratch the surface of what is possible,” Holzmann said.

Put another way, testing only looks for the presence of bugs, not the absence of bugs, and one small mistake could have devastating results.  

“If you take any failure of a system, like Fukushima and Three Mile Island, and look at the sequence of events that led to that failure, it is always fascinating because there are so many things that nobody could have predicted that would happen in a particular accommodation,” said Holzmann. “Same as in software; so many things can happen.”

In contrast, instead of testing one situation at a time, formal verification is a way to test that a program works in every situation. What you care about is whether the logic holds true, and the best way to check that logic is with a computer.  

“A formalism for me has the purpose that you can reason about things, and the most useful way of reasoning about things is if you can program a machine to do the reasoning for you,” said Holzmann.

Making a Plan

Generally, the first step in formal verification is to create a mathematical model. The math needed is not complicated; it’s just basic logic written up in a so-called “formal language” that is machine checkable.  

Typically, the process of specifying a model begins with a stakeholder who understands what the system needs to do. In the case of a medical device, the stakeholder might be a doctor; in the case of a smart contract, it might be a lawyer or a banker, or both.

The job of a stakeholder is to convey the information in her head to a requirements engineer who collects that information and creates the model. The process begins informally with discussions and abstractions, but ends formally with a precise mathematical specification.

This is not easy. It is a time consuming, iterative process that can take months, depending on the situation, but it often brings a clarity to a situation that was not there before because it forces programmers to think deeply about the behavior of a software.

“You can think of it as laws and regulations,” said Andreas Zeller, professor of software engineering at Saarland University in Saarbruecken, Germany, who likens creating a formal specification to developing a plan for a building.

“You refine the regulations,” he told Bitcoin Magazine. “But if you do not have regulations in the first place, your building crashes, and that is when you realize, you had better make a plan.”   

Checking the Logic

Once a model is specified, the next step is to verify the model’s logic with proofs. This is a critical step in the process. “If you do not have a proof, you do not have a guarantee that the model, as it is, will work,” explained Zeller.

But because you have to make explicit every single logical step, proofs can be immensely long and complex. In the past, this made formal verification agonizingly difficult. Even the simplest statement could require dozens of theorems and lemmas.

Fortunately, these days, many formal systems use automated theorem provers, like Coq, Isabelle or Metamath, that can check or even partially construct a formal proof.

Once a model is proven to work, the next step is building your program. But you still must make sure the software you build conforms to the specification.  

This is where functional programming languages like ML, Haskell, OCaml or F# enter into the picture. Because these languages are closer to algebra in their expressiveness, they are a better match for formal verification than languages like C, Java, or JavaScript.

For this reason, Tezos is written in OCaml and Cardano is written in Haskell, so changes to the protocol are easier to formally verify. (A formal specification for Ouroboros Praos, the next generation of the consensus algorithm powering Cardano, is already in the works.) Similarly, Tezos’ smart contract language Michelson is based on OCaml; Cardano’s smart contract language Plutus is based on Haskell.

Pros and Cons

On the plus side, formal verification allows computer scientists greater assurances in developing software. On the negative side, because of the rigor involved, formal methods can be a time-consuming, costly undertaking for projects developing the code.

Because of this, formal methods are best used to guarantee smaller building blocks of code that get reused over and over. You would not use it for, say, an entire operating system, but only those parts of a system that require the highest safety or security assurances.  

Naturally, any type of security comes at a cost. The question is, how much security will blockchain and smart contract developers be willing to pay for?

If you want something that is error free, “you had better be prepared to spend tens to hundreds of thousands of dollars for people who will provide a full proof,” cautioned Zeller.  

On the other hand, for smart contracts securing tens of millions of dollars in funds, those costs may be well worth it. Looking at it another way, in a competitive environment, formal verification could make smart contracts more appealing to the consumer.

If, for instance, you had the choice of entrusting your funds to a smart contract that had been formally verified versus one that has not, which one would you choose?  

___________

Thanks to Tim Menzies, professor of computer science at North Carolina University, and Brighten Godfrey, co-founder and CTO at Veriflow, and Automated Software Engineering 2017.