Bucharest FP
A functional programming group for those living and working in Bucharest
We gather monthly, watch someone talk about something they're passionate about and then continue the discussion in a pub
#030: Verification of Blockchain Languages and Virtual Machines
This meetup took place at Bucharest TechHub, Thursday, 05 July 2018 at 19:00. Find out when our next meetup is.
Verification of Blockchain Languages and Virtual Machines
Grigore Roșu
Grigore Roșu is a professor in the Department of Computer Science at the University of Illinois at Urbana-Champaign (UIUC), where he leads the Formal Systems Laboratory (FSL), and the founder and president of Runtime Verification, Inc (RV).
His research interests encompass both theoretical foundations and system development in the areas of formal methods, software engineering and programming languages.
Before joining UIUC in 2002, he was a research scientist at NASA. He obtained his Ph.D. at the University of California at San Diego in 2000. He was offered the CAREER award by the NSF, the Dean's award for excellence in research by the College of Engineering at UIUC in 2014, and the outstanding junior award by the Computer Science Department at UIUC in 2005. He won the ASE IEEE/ACM most influential paper award in 2016 (for an ASE 2001 paper that helped shape the runtime verification field), the ACM SIGSOFT distinguished paper awards at ASE 2008, ASE 2016, and OOPSLA 2016, and the best software science paper award at ETAPS 2002.
Abstract
Many of the recent cryptocurrency bugs and exploits are due to flaws or weaknesses of the underlying blockchain programming languages or virtual machines.
The usual post-mortem approach to formal language semantics and verification, where the language is firstly implemented and used in production for many years before a need for formal semantics and verification tools naturally arises, simply does not work anymore.
New blockchain languages or virtual machines are proposed at an alarming rate, followed by new versions of them every few weeks, together with programs (or smart contracts) in these languages that are responsible for financial transactions of potentially significant value.
Formal analysis and verification tools are therefore needed immediately for such languages and virtual machines.
We present recent academic and commercial results in developing blockchain languages and virtual machines that come directly equipped with formal analysis and verification tools.
The main idea is to generate all these automatically, correct-by- construction from a formal specification.
We demonstrate the feasibility of the proposed approach by applying it to two blockchains, Ethereum and Cardano.
We also discuss the mathematical foundations underlying our formal analysis and verification tools, specifically matching logic and the K framework.