The Invariant That Wasn't

The ability to think about a problem in reverse is helpful in identifying logical errors and gaps in thinking. The movie Tenet explores a world where humans and objects can travel both forward and backwards in time. Looking at time and events through this perspective forces the viewer to apply multiple lenses to following the story. Learning how to write formal proofs for smart contracts is similar in that it forces the writer to think about the system they've built from a different lens. Being able to build a system, and then write invariants forces the author to develop a deeper understanding of the code they have written.

Last year, I took time to research different types of security tools and ways of detecting bugs. Formal verification seemed like the hardest to grok. I was intrigued and wanted to learn more.

I spent a week at Certora's office, and was taught by Shoham who helped me understand the language and paradigm behind the Certora Prover. It was quite a fun challenge. Instead of testing a certain scenario like you do with unit tests, with formal verification, you make claims about things that are always true about the system. Then stack more and more invariants and rules together until you get a model that describes the entire system.

There are two main types of symbolic tools for securing smart contracts on Ethereum. The first is symbolic execution, where a program is plugged into an SMT solver and the solver tells you whether any assert statements that should never revert can. The second is formal verification, which checks that the user provided model accurately describes the program being verified. Formal verification is closest to differential testing where you write two identical programs and then pass random inputs in to see that they both return the same value. Except instead of passing random inputs, the inputs are derived from the z3 solver, and the equivalent program is written in Certora Verification Language (CVL), which feels, and is, so much different than Solidity.

This prover stuff, it'll melt your brain

This type of software development felt like it was melting my brain because of how unique this paradigm is. All of the assumptions you usually make go right out the window. After a 6 hour day writing specifications, I was completely shot.

The main benefit of writing these formal specifications that is it forces you to explicitly state all of your assumptions about the system. All of the relationships between variables and states become documented in the specification, and the prover checks to ensure your assumptions are always correct. There are cans of worms around over-approximation, which is where I was really hung up initially. Basically the prover will tell provide a state that violates an invariant, but is not possible to reach given the contract implementation. You then learn to constrain the search space and tell the prover to only give you valid states. Over the course of the week, I learned to look at things differently to use the tool. I even caught a minor bug in a rate limited library implementation I had previously written.

Using this Prover, you realize, the tool is only as good as the user. You could write a tautology, which is an invariant that is always true, or a vacuously true statement which is always true because the premise is false. Or you could write and verify 99% of the invariants and relationships of system state, and miss the last invariant that lets an attacker through. The only way to write invariants and not miss is to take your time with things and methodically comb the system, writing out all of your assumptions. Once all the assumptions and relationships are documented, you then need to write invariants that prove these relationships always hold.

I wouldn't be surprised if hackers use symbolic tools, or even the Certora Prover itself to document their assumptions about a system, write out invariants they think should always hold true, and then try to break them. I guess it's either you write invariants, or the blackhats write them for you.

A professor once told me that formal verification has been the technology of the future for the last 50 years, but it seems like this technology has finally found product market fit with smart contract and blockchain systems. Here small pieces of software hold vast sums of money, and the price of making mistakes is incredibly high.

A special thanks to Tal from Certora who got me the last plane ticket out of Israel when the war broke out and all of my flights were cancelled.