智能合约安全框架的形式化规约
软件工程
2020-01-14 v1
摘要
随着智能合约规模和复杂度的增长，确保其正确性和安全性变得越来越困难。由于缺乏隔离机制，代码中的单个错误或漏洞就可能导致整个系统崩溃，因此智能合约的升级尤其危险。用于在代码部署到区块链之前保障智能合约安全性的传统方式，包括领域特定语言、审计和静态分析，在部署后无法提供任何保护。每次升级后都需要重新验证全部代码，这是一个困难且耗时的过程，容易出错。为解决这些问题，我们开发了名为 Cap9 的智能合约安全协议与框架。它为开发者提供了以安全且稳健的方式进行升级的能力，并通过使用低层基于能力的安全模型改善了隔离性与透明度。我们使用 Isabelle/HOL 对 Cap9 框架进行了形式化规约并证明其一致性。本文介绍了我们用于创建该规约的基于精化(refinement)的方法，并讨论了在此过程中遇到的一些困难。
引用
@article{arxiv.2001.04314,
title = {Formal specification of a security framework for smart contracts},
author = {Mikhail Mandrykin and Jake O'Shannessy and Jacob Payne and Ilya Shchepetkov},
journal= {arXiv preprint arXiv:2001.04314},
year = {2020}
}
备注
12 pages, FMBC'19