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
Michelson parser and ADT
A Michelson parser parser implemented in OCaml and Menhir. With this parser we can obtain an OCaml-defined abstract syntax tree of a Michelson smart contract.
Tezla
Tezla is an intermediate representation of Michelson smart contracts that eases the design of static smart contract analysers. This intermediate representation uses a store and preserves the semantics, flow and resource usage of the original smart contract. This enables properties like gas consumption to be statically verified.
Publications:
Tezcheck
Tezcheck is an integration of Tezla and SoftCheck. It allow us to define and run data-flow analysis over Michelson smart contracts with minimal effort by taking advantage of Tezla store-based represenatation and the modular and extensible framework of SoftCheck.
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
WhylSon
WhylSon is a deductive verification tool for smart contracts written in Michelson, which is the low-level language of the Tezos blockchain.
WhylSon accepts a formally specified Michelson contract and automatically translates it to an equivalent program written in WhyML, the programming and specification language of the Why3 framework.
Smart contract instructions are mapped into a corresponding WhyML shallow-embedding of the their axiomatic semantics, which we also developed in the context of this work.
Publications:
Funded by:
