TY - GEN
T1 - Proof-carrying smart contracts
AU - Dickerson, Thomas
AU - Gazzillo, Paul
AU - Herlihy, Maurice
AU - Saraph, Vikram
AU - Koskinen, Eric
N1 - Publisher Copyright:
© International Financial Cryptography Association 2019.
PY - 2019
Y1 - 2019
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85063491998&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85063491998&partnerID=8YFLogxK
U2 - 10.1007/978-3-662-58820-8_22
DO - 10.1007/978-3-662-58820-8_22
M3 - Conference contribution
AN - SCOPUS:85063491998
SN - 9783662588192
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 325
EP - 338
BT - Financial Cryptography and Data Security - FC 2018 International Workshops, BITCOIN, VOTING, and WTSC, Revised Selected Papers
A2 - Eyal, Ittay
A2 - Zohar, Aviv
A2 - Sala, Massimiliano
A2 - Bracciali, Andrea
A2 - Pintore, Federico
A2 - Teague, Vanessa
A2 - Clark, Jeremy
T2 - 22nd International Conference on Financial Cryptography and Data Security, FC 2018
Y2 - 26 February 2018 through 2 March 2018
ER -