Real-world formal verification of smart contracts using the K Framework
Everett Hildenbrandt, Daejun Park, Yi Zhang, Grigore Roșu
Runtime Verification
Abstract
Smart contract failures have caused millions of dollars of lost funds, and rigorous formal analyses are required to ensure the correctness and security of contract implementations. This tutorial will present various formal analysis and verification tools and their industry case studies for smart contracts based on the K framework. K is a language framework where programming languages are given formal semantics, and various formal methods tools (from interpreters, to model checkers and deductive program verifiers, to compilers) are automatically generated from the formal semantics in a correct-by-construction manner. In this tutorial, we will present the formal semantics of the Ethereum Virtual Machine (EVM) and the Ethereum WebAssembly (eWASM) languages written in K, and the real-world use of the automatically derived formal tools to ensure correctness of high-profile smart contracts. At the end of the tutorial, the audience will have sufficient knowledge to get started to formalize their own (new) languages for smart contracts, and/or formally verify their smart contracts using the K framework.
Bio:
Grigore Rosu does research in design, semantics and implementation of programming and specification languages, automated software engineering and formal methods, especially push-button techniques for certification, monitoring, synthesis and modularization, and in automated reasoning about computer systems, applications of logics, theorem proving, algorithms, (co)algebra, and category theory. He teaches classes on software engineering, programming languages, formal methods, and runtime verification. Before joining UIUC in 2002, he was a research scientist at NASA Ames. He obtained his Ph.D. at the University of California at San Diego in 2000 and his M.S. at the University of Bucharest, Romania, in 1996. Grigore was offered the CAREER award by the NSF in 2005, the outstanding junior award by the CS Department at UIUC in 2005, and the Dean's award for excellence in research by the College of Engineering at UIUC in 2014. He won the ASE IEEE/ACM most influential paper award in 2016 and the RV test of time award for papers published in 2001 that shaped the runtime verification field, and distinguished/best paper awards at ASE 2008, ASE 2016, OOPSLA 2016, ETAPS 2002. He was ranked a UIUC excellent teacher in Spring 2013, Fall 2012, Spring 2008 and Fall 2004.
Rosu is known for work in runtime verification, the K framework, matching logic, and automated coinduction.
