论文标题
Tezla，用于静态分析Michelson智能合约的中间表示
Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts
论文作者
论文摘要
本文介绍了Tezla，Tezla是Michelson Smart合同的中间表示，可简化静态智能合同分析仪的设计。该中间表示使用商店并保留原始智能合约的语义，OW和资源使用情况。这使得诸如气体消耗之类的属性得到静态验证。我们向Tezla提供了米歇尔森智能合约的自动反合。为了支持我们对Tezla充分性的主张，我们开发了一个静态分析仪，该仪表利用Tezla代表米歇尔森智能合约来证明简单但非平凡的属性。
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.
