The TAU Programming Languages and Systems Seminar - Certora: Automatic Exact Formal Verification of Smart Contracts

ABSTRACT:

The dream of trustless transactions on blockchains has only been partially achieved. One of the worst gaps is the need to trust code, especially smart contracts. True transparency cannot be achieved even by disclosing full source code, because subtle bugs and vulnerabilities in plain sight slip through careful inspection and testing. Breathtaking financial losses from exploited bugs in smart contracts, such as the DAO and Parity hacks, demonstrate this point. Bugs in smart contracts may be the most important limiting factor to mainstream adoption of blockchain technology.

Certora aims to create a safe haven in a world of buggy, insecure, and malicious contracts by applying recent advances in formal verification research that enable automatic, exact analysis. Our goal is to prove that smart contracts satisfy critical logical properties, routinely and automatically, with no false error reports and no missed errors. Furthermore, we will enable continuous checking after contracts are deployed to provide up-to-the minute security, tracking new vulnerabilities and upgrades to contracts.