Vincent Botbol – Introduction to the Tezos blockchain and static analysis of smart-contracts

In this talk, we will give a broad introduction of the Tezos blockchain by introducing its architecture and design choices regarding safety and security in an adversarial distributed system. We will then present Tezos smart-contract language: Michelson, a statically typed stacked-based (domain-specific) language. Lastly, we will talk an ongoing work aiming to develop a static analyzer tool using abstract interpretation to automatically infers (numerical) invariants allowing us to formally prove numerical safety properties along with more blockchain-specific functional properties, e.g., validating user authentication patterns, analyzing the evolution of contract’s storage, determining an upper-bound gas usage of a smart-contract, etc. This work is integrated as an addition to a modular abstract interpretation based platform, MOPSA, already capable of analyzing of C and Python programs.