Title: Towards formally-verified Solidity specifications

Quand: le mardi 05 juin 2018 à 14h00
Où: Salle G09, Télécom SudParis, Evry.

Abstract: In the last few years, permission-less distributed execution platforms have gained enormous popularity, as they have become a computing environment of choice for decentralized asset management. Concretely, the Ethereum project implements a distributed ledger featuring a Turing-complete execution engine with read/write capability to the underlying blockchain-based storage. Thus, users can immutably store and interact with other « smart contracts », which has allowed the development of rich trustless applications. However, lack of central control does come at a prize: once a contract is deployed to the blockchain, its code is in principle immutable, thus bugs take a very different dimension as the same autonomy that makes the permissionless setting interesting works against the effective mitigation of vulnerabilities.
We aim to improve this situation with the introduction of Consolidity, a formal semantics and compiler for a subset of the Solidity programming language; Consolidity’s formal semantics provide a principled basis for the formal reasoning about high-level properties of given contracts, and allow us to define a specification language formally capturing the intent of ERCs. Contrary to other works in the smart contracts verification arena, Consolidity targets the widely-used Solidity language in an attempt to both reach a larger number of users and to gain a deeper understanding of real-world Ethereum platform use.
In the talk, we will review the basics of the Ethereum execution platform: the EVM, and of the Solidity programming language. We will discuss a few example smart contracts that make interesting targets for the verification of high-level properties. Then, we will present our semantics for Solidity, and use it to formally model some key properties under realistic assumptions on consensus and transaction fairness. In particular we will address the core of the ERC 20 and ERC 721 standards, and strategy proofness for a smart contract implementing an energy market.

Short Bio: Emilio is a postdoctoral researcher at the CRI, MINES ParisTech. He works on formal semantics of Digital Signal Processing and interactive theorem proving. He likes to code in a variety of functional programming languages, including Coq, OCaml, and Haskell; and enjoys contributing to research open source projects. Previously, he was a postdoctoral appointee in the privacy group of the University of Pennsylvania working on privacy, security, software verification, and semantics. He holds a PhD from the Technical University of Madrid on the categorical and relational semantics of constraint logic programming.