Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types
Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types
复制标题
Helmholtz：基于细化类型的 Tezos 智能合约验证器
DOI：
10.1007/s00354-022-00167-1
复制
发表时间：
2022
影响因子：
2.6
通讯作者：
Igarashi Atsushi
中科院分区：
文献类型：
--
作者：
Nishida Yuki;Saito Hiromasa;Chen Ran;Kawata Akira;Furuse Jun;Suenaga Kohei;Igarashi Atsushi
Asmartcontracts是一个在区块链上执行的程序，许多加密货币都是在区块链上实现的，并被用于自动化交易。由于智能合约涉及大量资金，因此对一种可以静态和正式验证它们的方法的需求激增。本文介绍了我们为Michelson开发的基于类型的静态验证工具Helmholtz，它是一种静态类型的基于堆栈的语言，用于编写在区块链平台Tezos上执行的智能合约。Helmholtz是在我们对Michelson的类型系统进行细化类型扩展的基础上设计的。Helmholtz以一个以细化类型的形式编写的用户定义规范作为输入，并对Michelson程序进行注释;然后，它基于精化类型系统对照规范对程序进行类型化，用SMT求解器Z3排出所生成的验证条件。我们简要地介绍了我们的精化类型系统的核心演算迈克尔逊的迷你迈克尔逊，它结合了特征，如复合数据集（例如，Helmholtz成功地验证了几个实用的Michelson程序，包括一个向账户转账和检查数字签名的程序。
Asmart contractis 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 toolHelmholtzfor Michelson, which is a statically typed stack-based language for writing smart contracts that are executed on the blockchain platform Tezos.Helmholtzis designed on top of our extension of Michelson’s type system with refinement types.Helmholtztakes 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.Helmholtzsuccessfully verifies several practical Michelson programs, including one that transfers money to an account and that checks a digital signature.