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/978-3-030-72013-1_14
复制
发表时间：
2021-02-26
期刊：
影响因子：
--
通讯作者：
Igarashi A
中科院分区：
文献类型：
--
作者：
Nishida Y;Saito H;Chen R;Kawata A;Furuse J;Suenaga K;Igarashi A
智能合约是在区块链上执行的程序，许多加密货币都是在此基础上实现的，并被用于自动化交易。由于智能合约涉及大量资金，因此对一种可以静态和正式验证它们的方法的需求激增。这篇工具论文描述了我们为Michelson开发的基于类型的静态验证工具Helmholtz，这是一种静态类型的基于堆栈的语言，用于编写在区块链平台Tezos上执行的智能合约。Helmholtz是在我们对Michelson类型系统的精化类型扩展之上设计的。Helmholtz以用户定义的规范（以精化类型的形式编写）为输入，对迈克尔逊程序进行注释;然后根据精化类型系统对程序进行类型化，使用SMT求解器Z3释放生成的验证条件。我们简要地介绍了我们的精化类型系统的核心演算迈克尔逊的迷你迈克尔逊，它结合了特征，如复合数据集（例如，列表和对）、高阶函数以及调用另一个合约。Helmholtz成功验证了几个实用的Michelson程序，包括一个将资金转移到帐户和检查数字签名的程序。
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 tool paper 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.
登录
查看更多内容
影响因子：
--
作者：
Rosu, Grigore;Serbanuta, Traian Florin
通讯作者：
Serbanuta, Traian Florin
影响因子：
--
作者：
Xi, HW;Harper, R
通讯作者：
Harper, R
影响因子：
1.8
作者：
Grossman, Shelly;Abraham, Ittai;Zohar, Yoni
通讯作者：
Zohar, Yoni
影响因子：
1.1
作者：
Xi, Hongwei
通讯作者：
Xi, Hongwei