Introduction

If you find a bug in a smart contract, it's really hard to mitigate that bug. In formal verification, we really look for bugs. We can identify subtle bugs, like reentrancy attacks, ownership violation, incorrect transactions, bugs due to updated code. We also want to assure the absence of bugs.

Device drivers

I come from the domain of Windows device drivers. These are drivers produced by third parties, and it integrates with operating system code. Bugs in the device drivers crash the operating system. How many of you know about verification of device drivers? These device drivers interoperate with the operating system. If you have a bug in your driver, it can crash the system. You've probably seen the blue screen of death. In the last few years, we have been seeing fewer blue screens of death, and the reason for this is formal verification.

Microsoft Research has taken a huge effort in integrating formal verification techniques. So you take correctness rules, that say that every time you acquire a lock, you release it, and so on. These are some of the correctness rules required in the drivers. The Microsoft team developed this really nice algorithm which is fully automatic and the user isn't aware of anything. It's a fully automatic method. It's a static driver verifier. You write your C program, you download it, you check this thing, and it basically gives you an error or it shows you the program obeys these rules.

"Things like even software verification, this has been the Holy Grail of computer science for many decades but now in some very key areas, for example, driver verification we're building tools that can do actual proof about the software and how it works in order to guarantee the reliability." - Bill Gates

What we're trying to do at our company is doing something inspired by that, but for blockchain. We're trying to build this automatic technology that can reason about your code and automatically find bugs.

Challenges in formal verification

My background is academic, but I spent 3-4 years at IBM and it shaped my whole thinking. One of the things they told us at IBM is that there are no such things as obstacles, only challenges. In formal verification, there are two challenges. One of them is technological. The other one is the specification. How do you specify the right behavior? What does it mean for the contract to be correct? How do we know which contract is correct and which one is not correct?

Microsoft device drivers all have informal rules but we need some kind of rules that say what is a correct smart contract. In this talk, I am going to focus on this one. I am only going to talk about the specification. I will tell you a little bit about technology. I will focus mainly on the problem of specifying correctness. How do you even say the contract is correct?

This talk

I will talk about two kinds of statements. The first is generic properties. It's a statement that should be true for all contracts. There are also specific properties, which are statements that are true for a specific use case of contracts. The question is, what are these properties for smart contracts?

Reentrancy attacks

We can prevent reentrancy attacks in all contracts. If we want immunity to reentrancy attacks, Certora can prevent all reentrancy attacks using proprietary technology. This is the most precise method and guarantee atomicity in presence of callbacks. We check that each contract obeys this property.

Contract vulnerability language

We have a language for defining the properties of the contract. We call it the contract vulnerability language. It's publicly available. It allows us to express the properties we care about like ERC20 or limit price changes over time for stablecoin. This is a language that defines the properties that we care about. We're hoping to define this as a joint effort with the community. One CVL covers many contracts. It can cover all of the properties of ERC20, for example. Another one can cover the properties of ERC721. We have the ability to write reusable specifications.

Another property of this is that it's verifiable.

We have three principles: generalization, math is law (goes back to VDM and Dines Bjorner) and the third one is that relating states from multiple executions.