Runtime Verification Completes Initial Formal Verification of Ethereum Casper Protocol

In February of this year Runtime Verification, Inc, (RV) received the very first security grant from the Ethereum Foundation to formally model/specify and verify the Casper smart contract.

Formal Verification of Casper FFG Smart Contract (see report and code)

Following our formal verification methodology, we modified the high-level business logic specification of the contract and refined it to the EVM-level specification against which we formally verified the contract bytecode using our KEVM verifier. We found several bugs in the contract source code in the course of the verification, later fixed by the developer team. See the GitHub issue pages for more detail (e.g., issues #57, #74, #75). As a side benefit of this work-stream, we discovered several issues in the Vyper compiler that resulted in generating an incorrect bytecode from the contract (issues #767, #768. These issues were later fixed by the Vyper compiler team.

In late June of this year the Ethereum Foundation pivoted away from Casper FFG, instead focusing development efforts on a new approach then called Casper + Sharding. As part of this new effort, RV worked on two work-streams: (1) Formal modeling and verification of the beacon chain Casper protocol, and (2) Statistical Verification of RANDAO design alternatives. RV completed each of these work-streams in November of this year. A summary of each is included below as well as links to their individual repository from where you can access a technical report. Please note that as of November 2018, "Casper + Sharding" has been folded into Serenity 2.0, the Ethereum 2.0 upgrade path.

Formal Verification of Beacon Chain Casper Protocol (see report and code)

This project provides models and proofs of the Casper blockchain finality system in the Coq proof assistant. The major theorems proven are Accountable Safety and Plausible Liveness. Accountable safety intuitively states that conflicting blocks in different block tree forks cannot both be finalized if more than 2/3 of validators (by deposit) behave honestly. Plausible liveness states that regardless of what has happened before, it is always possible to continue to finalize blocks when more than 2/3 of validators follow the protocol.

Statistical Verification of RANDAO (see report and code)

This is a formal model of the RANDAO-based Random Number Generator (RNG) schemes as a probabilistic rewrite theory specified in the Maude system. Decentralized random number generation, using RANDAO coupled with a reward system, is a core process of Ethereum’s Serenity protocol. RV investigated the susceptibility of this process to look-ahead attacks enabling attackers to bias randomness to their advantage. RV developed a probabilistic, real-time and computational model of the RANDAO scheme in the context of Serenity, and then applied statistical model checking and quantitative verification algorithms using Maude's PVeStA tool to analyze different measures of potentially achievable bias. The analysis provides a formal evaluation of RANDAO’s resilience against look-ahead attacks assuming different attack strategies and protocol configurations.

Acknowledgements
We would like to warmly thank the Ethereum Foundation for funding this effort, and to Vitalik Buterin, Danny Ryan, and Justin Drake (all from the Ethereum Foundation) as well as to Yoichi Hirai and Jon Choi (both previously at the Ethereum Foundation) for their collaboration during this engagement.