Tezla：一种用于 Michelson 智能合约静态分析的中间表示
编程语言
2020-05-26 v1
摘要
本文介绍 Tezla，一种 Michelson 智能合约的中间表示，旨在简化静态智能合约分析器的设计。该中间表示使用存储，并保留了原始智能合约的语义、流程和资源使用情况。这使得诸如 Gas 消耗之类的属性可以被静态验证。我们提供了一个从 Michelson 智能合约到 Tezla 的自动反编译器。为了支持我们关于 Tezla 充分性的主张，我们开发了一个静态分析器，它利用 Michelson 智能合约的 Tezla 表示来证明简单但非平凡的性质。
引用
@article{arxiv.2005.11839,
title = {Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts},
author = {João Santos Reis and Paul Crocker and Simão Melo de Sousa},
journal= {arXiv preprint arXiv:2005.11839},
year = {2020}
}