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协议的高级和另一个功能。

0
下载
关闭预览

相关内容

【陈天奇】TVM:端到端自动深度学习编译器,244页ppt
专知会员服务
86+阅读 · 2020年5月11日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
151+阅读 · 2019年10月12日
【新书】Python编程基础,669页pdf
专知会员服务
194+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
最新BERT相关论文清单,BERT-related Papers
专知会员服务
52+阅读 · 2019年9月29日
CCF C类 | DSAA 2019 诚邀稿件
Call4Papers
6+阅读 · 2019年5月13日
CCF A类 | 顶级会议RTSS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年4月17日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
已删除
将门创投
7+阅读 · 2018年12月12日
【NIPS2018】接收论文列表
专知
5+阅读 · 2018年9月10日
【推荐】基于TVM工具链的深度学习编译器 NNVM compiler发布
机器学习研究会
5+阅读 · 2017年10月7日
【推荐】SVM实例教程
机器学习研究会
17+阅读 · 2017年8月26日
【推荐】TensorFlow手把手CNN实践指南
机器学习研究会
5+阅读 · 2017年8月17日
Arxiv
0+阅读 · 2021年10月29日
Arxiv
4+阅读 · 2018年5月10日
VIP会员
相关VIP内容
【陈天奇】TVM:端到端自动深度学习编译器,244页ppt
专知会员服务
86+阅读 · 2020年5月11日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
151+阅读 · 2019年10月12日
【新书】Python编程基础,669页pdf
专知会员服务
194+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
最新BERT相关论文清单,BERT-related Papers
专知会员服务
52+阅读 · 2019年9月29日
相关资讯
CCF C类 | DSAA 2019 诚邀稿件
Call4Papers
6+阅读 · 2019年5月13日
CCF A类 | 顶级会议RTSS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年4月17日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
已删除
将门创投
7+阅读 · 2018年12月12日
【NIPS2018】接收论文列表
专知
5+阅读 · 2018年9月10日
【推荐】基于TVM工具链的深度学习编译器 NNVM compiler发布
机器学习研究会
5+阅读 · 2017年10月7日
【推荐】SVM实例教程
机器学习研究会
17+阅读 · 2017年8月26日
【推荐】TensorFlow手把手CNN实践指南
机器学习研究会
5+阅读 · 2017年8月17日
Top
微信扫码咨询专知VIP会员