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

    2020

    Santos Reis, João and Crocker, Paul and Melo de Sousa, Simão.

    arXiv: 2005.11839
    [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.
    @article{reisTezlaIntermediateRepresentation2020,
      title = {Tezla, an {{Intermediate Representation}} for {{Static Analysis}} of {{Michelson Smart Contracts}}},
      author = {{Santos Reis}, Jo{\~a}o and Crocker, Paul and {Melo de Sousa}, Sim{\~a}o},
      year = {2020},
      month = may,
      archiveprefix = {arXiv},
      eprint = {2005.11839},
      eprinttype = {arxiv},
      keywords = {Computer Science - Programming Languages},
      primaryclass = {cs.PL}
    }
    

  2. WhylSon: Proving your Michelson Smart Contracts in Why3.

    2020

    Arrojado da Horta, Luís Pedro and Santos Reis, João and Pereira, Mário and Melo de Sousa, Simão.

    arXiv: 2005.14650
    [abstract]
    This paper introduces WhylSon, 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. One major advantage of this approach is that it allows an out-of-the-box integration with the Why3 framework, namely its VCGen and the backend support for several automated theorem provers. We also discuss the use of WhylSon to automatically prove the correctness of diverse annotated smart contracts.
    @article{hortaWhylson2020,
      title = {WhylSon: Proving your Michelson Smart Contracts in Why3},
      author = {{Arrojado da Horta}, Luís Pedro and {Santos Reis}, João and Pereira, Mário and {Melo de Sousa}, Simão},
      year = {2020},
      month = may,
      archiveprefix = {arXiv},
      eprint = {2005.14650},
      eprinttype = {arxiv},
      keywords = {Computer Science - Programming Languages},
      primaryclass = {cs.PL}
    }
    


Funded by:

Tezos Foundation