Mooly Sagiv and Eric Smith on Formal Verification for Ethereum

We are pleased to have Mooly Sagiv and Eric Smith speak to us on formal verification of smart contracts and cryptographic code. Mooly Sagiv is a professor in the School of Computer Science at Tel-Aviv University and a visiting scholar at VMware Research Group. Sagiv is a recipient of the most prestigious European grant given by the European Research Council (Senior ERC). Eric Smith is a Senior Computer Scientist at Kestrel Institute where he co-leads Kestrel's Automated Program Transformations project, which is used in the ACL2 model of an Ethereum client that the Ethereum Foundation funded with $400k [1][2]. See below for talk abstracts and bios. This will be a great event; join us!

Professor Sagiv will speak on "Certora's exact and automatic formal verification of smart contracts"; his abstract follows. "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 aim 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."

Dr Smith will speak on "Formal Verification of Cryptographic Code"; his abstract follows. "I will discuss approaches for automated verification and analysis of programs, focusing on cryptographic operations such as those used in cryptocurrencies. Much of this work uses a tool I am developing called Axe, a high-performance rewriter and equivalence checker that is capable of verifying cryptographic algorithms such as block ciphers and hash functions. Axe is built on the ACL2 theorem prover and interoperates with it. Axe can "lift" bytecode or binary programs into a logical representation, using symbolic execution and a formal model of the underlying machine (e.g., the Java Virtual Machine or the x86 processor). It also includes an equivalence checker that can prove equivalence of a specification and an implementation (or of two implementations). Axe can also be used for program analysis, e.g., to prove various desired properties, or, in many cases, to find inputs that cause programs to exhibit particular behaviors."

"To put this work in context: Kestrel has a long history of deriving
correct-by-construction code from formal specifications. Currently,
we are developing a formal specification of Ethereum, with the goal of
using it to synthesize a full Ethereum reference implementation in the
ACL2 theorem prover. This will include an ACL2 model of the Ethereum
Virtual Machine. Having the formal specification of Ethereum opens
the possibility of verifying existing implementations, using tools
such as ACL2 and Axe. Having an ACL2 model of the Ethereum Virtual
Machine opens the possibility of using ACL2 and Axe to prove
properties of smart contracts."

[1] https://www.kestrel.edu/home/projects/ethereum/
[2] https://blog.ethereum.org/2018/08/17/ethereum-foundation-grants-update-wave-3/