Main Goal
FRESCO (Formal Verification of Tezos Smart Contracts) is a project generously funded by Tezos Foundation that includes two Ph.D. theses. The main goal of this project is to explore tools for the static analysis of smart contracts in programming languages such as Michelson, as well as focus on formal verification techniques and support for machine-checked smart contracts using proof assistants like Why3 and Coq.
From this goal derive two lines of work (two Ph.D. theses) that focus on:
- formal verification of smart contracts;
- static analysis of smart contracts.
Static Analysis of Tezos Smart Contracts
Focused on static analysis of smart contracts, this line of work aims at developing methods and tools to automatically analyse, infer and verify certain properties of smart contracts.
This line of work will carry on a study of common problems and characteristics of smart contracts in order to develop the tools and techniques to infer and detect such properties.
As a target of these tool, any smart contract written in Michelson (or other future low-level like languages) should be supported.
Current Work
SCIL++
SCIL is an intermediate language for static analysis tools targeted at imperative high-level languages with a store. In order to have greater flexibility at representing different control flows, the platform (Softcheck) and SCIL were extend in order to support low-level constructs such as jumps. This extensions introduces some complexity to the control flow graph generation process, but allows an easier and flexible way to describe certain flows.
Semantics of SCIL++
In order to have good foundations, a semantics for SCIL++ has been defined. This denotational continuation-style semantics will serve as a base for defining a semantics of the full integration of Michelson into the Softcheck platform. This semantics were also written so that one may easily obtain interpreters for the interfaced languages adopted in SCIL++, through the development of a modular interpreter that defines the core of SCIL++ and can be instantiated given an implementation of the interpretation of the interfaced language specific components.
releaselab/fresco/scilpp-semantics
MichelSCIL
MichelSCIL is the representation of Michelson using Softcheck intermediate language. This translation relies on a developped mechanism to translate stack usage to store usage (variables). The current version contemplates all instructions not related to inter-contract interaction (ongoing work).
Formal Verification of Tezos Smart Contracts
Current Work
Executable Operational Semantics for Michelson using Why3
This implementation represents the first effort towards creating a platform for the formal verification of Smart Contracts for the blockchain Tezos.
This platform aims not only to validate the execution mechanism of the smart contracts, but also for the smart contract themselves.
In this work we describe a big step style interpreter for the Michelson language, which is not only executable, but we also aim it to be a formal semantic of our logic, which means, it should be a mathematical function giving any Michelson program its semantic value.
Saying this, it is necessary to show that eval is a total function, which is
the equivalent of proving its termination.
Thanks to the code extraction mechanism of the Why3, it is possible to obtain an OCaml implementation of this interpreter.
releaselab/fresco/michelson-why3
People
Simão Melo de Sousa
João Reis
