A smart contract is a program executed on a blockchain, based on which many cryptocurrencies are implemented, and is being used for automating transactions. Due to the large amount of money that smart contracts deal with, there is a surging demand for a method that can statically and formally verify them. This article describes our type-based static verification tool HELMHOLTZ for Michelson, which is a statically typed stack-based language for writing smart contracts that are executed on the blockchain platform Tezos. HELMHOLTZ is designed on top of our extension of Michelson's type system with refinement types. HELMHOLTZ takes a Michelson program annotated with a user-defined specification written in the form of a refinement type as input; it then typechecks the program against the specification based on the refinement type system, discharging the generated verification conditions with the SMT solver Z3. We briefly introduce our refinement type system for the core calculus Mini-Michelson of Michelson, which incorporates the characteristic features such as compound datatypes (e.g., lists and pairs), higher-order functions, and invocation of another contract. \HELMHOLTZ{} successfully verifies several practical Michelson programs, including one that transfers money to an account and that checks a digital signature.
翻译:智能合同是一个在块链上执行的程序,许多加密都基于此,并被用于交易自动化。由于智能合同涉及大量资金,因此对一种可以静态和正式核实的方法的需求激增。本篇文章描述了我们基于型的静态核查工具Michelson的HELHOLTZ,这是一个静态打字的堆叠语言,用于写写在块链平台Tezos上执行的智能合同。HELMHOLTZ是在Michelson类型系统扩展的顶端设计的。HELMHOLTZ采用一个米歇尔森程序,用用户定义的规格附加说明,该规格以精细类型的形式写成,作为输入;然后将程序与基于精细的系统规格进行核对,与SMT解答Z3.一起执行生成的核查条件。我们简要介绍了我们对Michelson的微型-Michelson核心计算器的精细型系统,它包含复合数据类型(eg、清单和纸质签名)等特征,包括一个高级和另一个数字程序,包括一个高级HEMLASL协议的高级和另一个功能。