The Certora Prover formally verifies high-level functional correctness properties of low-level smart contract code using automated techniques. Most real-world programs that the Certora Prover verifies are large and complex. Verification conditions generated by straightforward translation to SMT are frequently too complex for solvers, leading to slow verification times and timeouts.

To scale this product to realistic code, we developed a unique pointer analysis algorithm for low-level code. Our algorithm assumes certain invariants about low-level code generated by the compiler but verifies that the invariants are met. This algorithm has uncovered security errors in the Solidity compiler and sped up formal verification by orders of magnitude in several cases by enabling sound program simplifications. A key challenge in developing pointer analysis for low-level code in the domain of smart contracts is that the EVM manages memory using strategies like bump allocation that, while practical for usage in the blockchain, make analysis harder.

In this talk, I will first describe some lessons learned over the past five years at Certora and then suggest new static analysis problems for our community to target as new low-level languages like EVM bytecode and WebAssembly become more popular.

My research focuses on easing the task of developing reliable and efficient software systems. I am particularly interested in static program analysis which combines two disciplines: automated theorem proving and abstract interpretation. In the next decade, I am hoping to develop useful techniques in order to change the ways modern software is built. I am particularly interested in proof automation, given a program and a requirement, automatically prove or disprove that all executions of the program satisfy the requirements. This problem is in general undecidable and untractable. I am interested in developing practical solutions to proof-automation by: (i) exploring modularity of the system and (ii) relying on semi-automatic and interactive process, where the user manually and interactively guides the proof automation, and (iii) simplifying the verification task by using domain-specific abstractions expressed in a decidable logic. I am applying these techniques to verify safety of liveness of distributed systems.