迈向更安全的智能合约：语言与验证方法综述
密码学与安全
2018-11-02 v4
摘要
公开分布式账本在不到十年的时间里市值超过 2050 亿美元，得到了广泛采用。除了新颖的共识机制外，其成功也归功于智能合约。这些程序允许互不信任的各方达成自主执行的协议。然而，智能合约中的实现问题给此类合约的用户造成了严重损失。人们已付出大量努力，通过引入新的编程语言和先进的验证方法来提升其安全性。我们以两部分提供这些努力的综述。首先，我们介绍几种侧重于安全特性的智能合约语言。为此，我们给出关于范式、类型、指令集、语义和计量的概览。其次，我们考察针对智能合约和分布式账本的验证工具与方法。相应地，我们介绍其验证方法、自动化水平、覆盖范围和所支持的语言。最后，我们提出未来研究方向，包括形式语义、已验证编译器和自动化验证。
引用
@article{arxiv.1809.09805,
title = {Towards Safer Smart Contracts: A Survey of Languages and Verification Methods},
author = {Dominik Harz and William Knottenbelt},
journal= {arXiv preprint arXiv:1809.09805},
year = {2018}
}