Securify：智能合约的实用安全分析
密码学与安全
2018-08-27 v2
摘要
无许可区块链允许执行任意程序（称为智能合约），使互不信任的实体能够不依赖可信第三方进行交互。尽管潜力巨大，反复出现的安全问题已动摇了由智能合约处理数十亿美元资产的信任。为解决该问题，我们提出Securify，一种用于以太坊智能合约的安全分析器，可扩展、全自动化，并能针对给定属性将合约行为证明为安全/不安全。Securify的分析包含两步。首先，它对合约的依赖图进行符号分析，从代码中提取精确语义信息。然后，它检查合规与违例模式，这些模式捕获了用于证明属性是否成立充分条件。为支持可扩展，所有模式均以指定领域特定语言描述。Securify已公开发布，已分析用户提交的>18K份合约，并被专家定期用于安全审计。我们对真实世界以太坊智能合约上的Securify进行了广泛评估，证明其可有效证明智能合约正确性并发现严重违例。
引用
@article{arxiv.1806.01143,
title = {Securify: Practical Security Analysis of Smart Contracts},
author = {Petar Tsankov and Andrei Dan and Dana Drachsler Cohen and Arthur Gervais and Florian Buenzli and Martin Vechev},
journal= {arXiv preprint arXiv:1806.01143},
year = {2018}
}