Proof-Carrying Smart Contracts
We propose a way to reconcile the apparent contradiction between the immutability of idealized smart contracts and the real-world need to update contracts to fix bugs and oversights. Our proposal is to raise the contract’s level of abstraction to guarante
- PDF / 393,614 Bytes
- 14 Pages / 439.37 x 666.142 pts Page_size
- 63 Downloads / 223 Views
1 Brown University, Providence, USA Stevens Institute of Technology, Hoboken, USA [email protected]
Abstract. We propose a way to reconcile the apparent contradiction between the immutability of idealized smart contracts and the real-world need to update contracts to fix bugs and oversights. Our proposal is to raise the contract’s level of abstraction to guarantee a specification ϕ instead of a particular implementation of that specification. A combination of proof-carrying code and proof-aware consensus allows contract implementations to be updated as needed, but so as to guarantee that ϕ cannot be violated by any future upgrade. We propose proof-carrying smart contracts (PCSCs), aiming to put formal correctness proofs of smart contracts on the chain. Proofs of correctness for a contract can be checked by validators, who can enforce the restriction that no update can violate ϕ. We discuss some architectural and formal challenges, and include an example of how our approach could address the well-known vulnerabilities in the ERC20 token standard.
1
Introduction
Motivation. The promise of smart contracts seems impossible to fulfill. In theory, a smart contract is a transparent agreement, freely agreed upon by informed parties. Irrevocable and immutable, it enforces itself without need for help from humans and their civic institutions. In reality, an unhappy history of exploits, theft, and fraud has established that people are bad at writing correct contracts, and no better at detecting flaws in the contracts they agree to [5,6,17,18]. The Solidity language and EVM bytecode permit contracts to call code at a dynamic address. While intended to support legitimate functions such as sending a payment to a user or contract, it allows the contract to implement the pointer to implementation (or PIMPL) idiom. This idiom has one benefit: it provides a path through which a buggy contract implementation might be patched. Even though the code is immutable, the state managed by the code, including the implementation pointer, is not. The danger, of course, is that a dishonest party could use such dynamic control flow to make substantial changes to the contract’s terms after it has been agreed upon. We believe this dilemma can be avoided, or at least mitigated, by including formal correctness proofs in the blockchain itself. Suppose we identify a property ϕ critical to the contract’s integrity. If a flawed implementation C that formally c International Financial Cryptography Association 2019 A. Zohar et al. (Eds.): FC 2018 Workshops, LNCS 10958, pp. 325–338, 2019. https://doi.org/10.1007/978-3-662-58820-8_22
326
T. Dickerson et al.
satisfies ϕ can only be replaced by an improved implementation C such that C ϕ, then all parties to the contract can be confident that ϕ will continue to hold even as bugs (not covered by ϕ) are detected and patched. The idea of mixing code and proofs goes back to Necula’s proof-carrying code (PCC) [16]. The blockchain context, however, brings new challenges: What format is needed for contracts’ specifi
Data Loading...
