规范即法律：以太坊智能合约的安全创建与升级
软件工程
2022-05-17 v1 计算机科学中的逻辑
摘要
智能合约是“代码即法律”范式的基石：智能合约的代码无可争议地描述了其资产如何被管理——一旦创建，其代码通常是不可变的。有缺陷的智能合约是该范式实用性最显著的反证；它们有详尽记录，并导致价值巨额的资产被侵害。为解决此问题，以太坊社区提出了(i)审计/分析智能合约的工具与流程，以及(ii)实现使合约代码可变的机制的设计模式。单独地，(i)和(ii)仅部分解决了“代码即法律”范式带来的挑战。在本文中，我们结合(i)和(ii)中的元素创建一个系统性框架，该框架脱离“代码即法律”并催生新的“规范即法律”范式。它允许合约被创建和升级，但仅当它们满足相应的形式化规范。该框架围绕一个可信部署者：一个对符合性这一概念进行形式化验证并强制执行的链下服务而构建。我们已对该框架进行原型实现，并考察了其对实现两个广泛使用的以太坊标准(ERC20 代币标准和 ERC1155 多代币标准)的合约的适用性，结果令人鼓舞。
引用
@article{arxiv.2205.07529,
title = {Specification is Law: Safe Creation and Upgrade of Ethereum Smart Contracts},
author = {Pedro Antonino and Juliandson Ferreira and Augusto Sampaio and A. W. Roscoe},
journal= {arXiv preprint arXiv:2205.07529},
year = {2022}
}