Formal Verification 101 for Blockchain Systems and Smart Contracts

Blockchain technology coupled with smart contracts offers a tantalizing promise: enabling distributed, trusted, and verifiable computational platforms for applications with rigorous security requirements like finance, secure messaging, and more. Unfortunately, one does not have to look very hard to see that the path to this promise is fraught with danger, e.g., see articles on Mt. Gox, the DAO, this attack on Ethereum classic, and a smart contract bug. While blockchain systems may be sound in theory, in practice, blockchain systems and smart contracts are still highly prone to developer error.

The question proponents of blockchain systems must ask themselves is: how can we salvage (a) the promise of blockchain technology for building a new class of distributed systems as well as (b) its reputation in the eyes of a wary public? Clearly, this is a multi-faceted issue that cannot be fully deconstructed in a single article. However, in this series we will argue that formal verification (more on that below) will play an increasing role answering both of these challenges (a)-(b).

This article is the first in a four part series from Runtime Verification on formal verification as applied to blockchain systems and smart contracts. In this first article, we hope to provide a generalized and gentle introduction to formal verification (without specific reference to the blockchain or smart contracts) and why we need it. In future articles we will hone in more on technical details. With that intro aside, let’s dive in!

Whether you are building a business, a product, or a software system, you will have to answer the following question: does our system satisfy our essential requirements? This question involves two pieces:

1. a system to be verified, and
2. a list of requirements.

We call the process of answering this question verification. Complete verification means checking the system meets all of its requirements, i.e., that it does both everything it is supposed to do and nothing it is not supposed to do, by examining all possible cases. This leads to an important question: how can we verify our systems?

If you ask most software developers this question, they will respond with some variation of testing. What is testing? Testing is a process where we take a system and ask ourselves what if? If we start from some initial conditions (e.g., our web server has 1 gigabyte of RAM), will we achieve our desired result? The answer, of course, depends on what kind of system we are investigating. Unfortunately, expanding testing capabilities by adding more test cases can only ensure complete verification for the simplest of systems, which have a fixed bound on complexity.

As a simple example, consider a web application, e.g., a banking website, that must serve a number of users. How many sets of initial conditions are theoretically possible? Clearly, serving 5 users simultaneously is different from serving 6 users simultaneously. Applying this argument ad infinitum, note we already have an unlimited number of scenarios to consider stemming from a single input variable, that is, the number of simultaneous users.

And this is exactly where verification, formal verification specifically, can help.

Instead of using explicit states (as we used above), formal verification typically uses symbolic input variables (e.g., what if our website has n simultaneous users?) coupled with a precise mathematical model of the system in question. In essence, we turn the verification question into a precise mathematical proposition and then prove the correctness of that proposition using mathematical proofs.

This is the primary advantage of formal verification: when a proposition is formally proven, you’ve succeeded in verifying an infinite number of test cases with a finite number of testing steps. We’ll survey how we do this (for software systems) by starting with this diagram:

In the figure, boxes represent different artifacts that are produced during the verification process, while connecting lines represent transformations from one kind of artifact into another. Solid connecting lines represent transformations that preserve all essential information while dashed lines are lossy transformations, where essential information may be lost. All lines are annotated by the entity needed to perform the desired transformation. In conventional software development, a developer (and typically also compiler) together turn system requirements into executable code. A (possibly different) developer will then take those same system requirements and write tests that hook into the executable code, ensuring that certain code paths return desired results. These tests are helpful in showing that our code is correct, but we already know testing is not enough. While tests can demonstrate the presence of bugs, they typically can never prove the absence of bugs. The beauty of formal verification is that we can provably demonstrate a correspondence between our requirements and our system specification, i.e., we can prove that our source code has no bugs.

A key tool that we use in this process is a semantics. You can think of a semantics as a compiler that maps code into its mathematical meaning. Another key tool that we use is a theorem prover, which is just a computer program that assists us in proving mathematical propositions and avoiding careless errors. Since our formalized requirements and formalized system specification are both mathematical statements, we can use a theorem prover to talk about how they are related. Thus, to answer the question:

How can we know that our system implementation satisfies our system requirements?

We shift our thinking into the formal, mathematical domain and instead ask:

Can our theorem prover show that our formalized system specification satisfies our formalized requirements?

In the next three posts, you will learn how formal verification shifts the question of system correctness from informal human reasoning to formal mathematical reasoning. And a result, you’ll be able to understand and enjoy the benefits of adopting formal verification in your practice:

• Precision. Systematic, formal, and mathematical reasoning gives us a precise language for thinking about system design;
• Automation. Many important formal verification tasks are autommable by a computer; this means we can consider very difficult problems that would be intractable for a human to solve.
• Confidence. When working with complex legacy systems, especially in untrusted environments, (e.g. IoT/embedded systems, etc...), formal verification can provide high assurance that you are not doing the wrong thing.
• Speed. When designing new systems, we believe semantics-based formal verification can accelerate the process of system design and writing good code by mitigating costly design errors.

Well, that’s all that we have for now! We hope you have enjoyed this brief overview of formal verification and that you will join us for the next three articles in our series where will zoom in on the three legs of the semantics-based formal verification process as illustrated in the diagram above and how they can be applied to blockchain systems: (i) formalizing requirements, (ii) theorem proving tools for formal verification, and (iiI) formalizing system semantics.