How DeepSEA Works

CertiK | Jan 22, 2020

Article's Poster

Check out our DeepSEA research page for the latest updates!

DeepSEA is a flexible and compatible language that can create fundamentally secure programs with a high level of abstraction and reasoning using Coq. Check out our explainer article for a brief overview and introduction to the language.

***

DeepSEA aims to provide a way to formally verify difficult correctness properties about smart contracts using the Coq proof assistant.

Much existing work on smart contract verification is built around automatic theorem provers such as Z3. These are convenient in that you can simply state a theorem, and the program will try to prove it for you. However, they are most useful for relatively simple proofs about e.g. arithmetic expressions and data structures like arrays. In cases where the theorem requires creativity, or requires custom definitions to even state, automatic tools tend to get stuck. Coq an example of an interactive proof assistant, which means that it doesn’t prove the theorems for you: the user has to write both the theorem statement and the proof, and Coq checks whether the proof is correct or not. This involves more work, but means that it can handle arbitrarily advanced mathematics.

In order to reason about a contract in Coq we first need to define a model of what it is doing which can be loaded into the Coq proof assistant. There are many possible approaches to this, but the way we are doing it is to write the contracts in a fairly small programming language, theDeepSEA language.The DeepSEA compiler both compiles the contract into EVM bytecode, and also outputs the representation that can be loaded into Coq. We can reason about a convenient high-level representation of the contract, and because we also verify that the DeepSEA compiler is correct, we can be sure that the generated Coq contract representation actually matches what the compiled EVM bytecode is doing.

deepsea_dive_1

Example: using Coq to verify a token contract

The DeepSEA language syntax is inspired by functional languages like ML and Coq itself. The simple token contract below shows the general appearance, we will use it as a running example.

sample token contract

The gif below shows the process of compiling the token contract into EVM. The compilation pipeline first parses and type checks the contract and generates a corresponding set of Coq files. In order to generate EVM assembly, we link these files with a verified compiler backend, and use Coq’s extraction facility to compile it into OCaml. Finally, there is a pretty-printer pass (unverified, written in OCaml) which translates the assembly into the actual bytes. We demonstrate the contract by deploying it into a Ganache instance and calling the methods.

token compiling

For convenience there is also a DeepSEA compiler which is compiled as a single OCaml executable, so users can run it without having Coq installed on their computer. This replaces some of the compiler passes that were written in Coq with (unverified) OCaml code, so it is less trustworthy, and it does not generate the Coq representation of the contract. The gif below shows it running, it generates identical bytecode as the Coq version above. We can also print out an intermediate language representation, or the EVM assembly mnemonics.

token proofless

Now we can load the representation of the contract into Coq and start writing proofs about it. The contract is represented as a function written in Coq’s built-in programming language “Gallina”, shown below. Since this is the version that the user will reason about in the proofs, we want it to correspond in an obvious way to the input program, and it mostly does except apart from being written in Gallina syntax instead of DeepSEA syntax and using monadic combinators for the imperative operations.

If we look at the details, in some ways the Coq representation is actually more high-level and easier to reason about than the input program. While compiled Ethereum hash tables do not keep track of which keys are stored in them, in the Coq version we represent the balances table with a Int256Tree data type which does remember its keys. The executable code still cannot make use of the keys, but theorems about the code can talk about them. Similarly, while the executable program uses bounded 256-bit integers, the representation uses unbounded mathematical integers so that theorems about ordinary arithmetic applies. (We discuss how to deal with overflow below.)

transfer spec

The gif below shows part of the process of using the Coq proof assistant to prove that the transfer method in the contract preserves the sum of all tokens stored in all balances---in other words, there is no bug in it which could create or destroy tokens. (For examples of what could go wrong, note that the code checks for integer overflow, and checks that the sending and receiving account are different. If we forgot one of those if statements, the theorem would not be provable.) Proving a theorem in Coq is an interactive activity: the computer continuously displays what remains to the proven, and the programmer types in a series of commands which breaks down the theorem into simpler statements. It’s like a computer game.

functional correctness

In addition to the final contract representation, the DeepSEA system also generates a set of side conditions which must be proven true for the representation to be valid---mostly that there are no integer overflows. In Solidity, programmers usually use a “safemath” library which adds assert statements that revert the contract call if there is an overflow. DeepSEA provides an assert statement so we can do the same thing, in which case the side condition becomes trivially provable. But in this case there is no need, because (with a bit of work) we can prove that the math in the transfer method cannot overflow.

The proof (an excerpt shown in the gif below) is not completely trivial, since it also needs an invariant about the values stored in the balances. Because we completed this proof we know that the safemath assert statements were actually not needed. This is a small example of how program verification can improve efficiency, by giving us the confidence to use more “dangerous” programming techniques.

vc

DeepSEA is still a work in progress. Both the compiler and the compiler correctness proofs are unfinished. Over the next few weeks and months we will release more items, such as a compiler to download, a draft language manual, more example proofs, and eventually the full implementation. In this way we hope that the larger blockchain community can see what we are working on. We hope you enjoy this sneak peek as we work towards the alpha release!

To learn more and get the latest updates about DeepSEA, check out our DeepSEA research page.