Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts

TL;DR

This paper presents Tezla, an intermediate representation for Michelson smart contracts that facilitates static analysis, enabling verification of properties like gas consumption through an automated decompiler and static analyser.

Contribution

Introducing Tezla, a novel intermediate representation for Michelson contracts that preserves semantics and resource usage, supporting static analysis and verification.

Findings

Tezla accurately models Michelson semantics and resource usage.

The static analyser successfully verifies properties like gas consumption.

Automated decompiler converts Michelson to Tezla efficiently.

Abstract

This paper introduces Tezla, 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, ow and resource usage of the original smart contract. This enables properties like gas consumption to be statically verified. We provide an automated decompiler of Michelson smart contracts to Tezla. In order to support our claim about the adequacy of Tezla, we develop a static analyser that takes advantage of the Tezla representation of Michelson smart contracts to prove simple but non-trivial properties.