Advertisement

Proof-Carrying Smart Contracts

  • Thomas Dickerson
  • Paul GazzilloEmail author
  • Maurice Herlihy
  • Vikram Saraph
  • Eric Koskinen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10958)

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 \(\varphi \) 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 \(\varphi \) 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 \(\varphi \). 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.

References

  1. 1.
    Atzei, N., Bartoletti, M., Cimoli, T.: A survey of attacks on ethereum smart contracts (SoK). In: Maffei, M., Ryan, M. (eds.) POST 2017. LNCS, vol. 10204, pp. 164–186. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54455-6_8CrossRefGoogle Scholar
  2. 2.
    Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006).  https://doi.org/10.1007/11804192_17CrossRefGoogle Scholar
  3. 3.
    Barnett, M., Leino, K.R.M., Schulte, W.: The spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005).  https://doi.org/10.1007/978-3-540-30569-9_3CrossRefGoogle Scholar
  4. 4.
    Bobot, F., Filliâtre, J.C., Marché, C., Melquiond, G., Paskevich, A.: The Why3 platform. http://why3.lri.fr/manual.pdf. Accessed 14 Jan 2018
  5. 5.
    Daian, P., Breidenbach, L.: Parity proposals’ potential problems. http://hackingdistributed.com/2017/12/13/ether-resurrection/. Accessed 14 Jan 2018
  6. 6.
    DAO: the DAO smart contract. Accessed 8 Feb 2017Google Scholar
  7. 7.
    Ethereum. https://github.com/ethereum/. Accessed 14 Jan 2018
  8. 8.
    Filliâtre, J.-C., Paskevich, A.: Why3—where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-37036-6_8CrossRefGoogle Scholar
  9. 9.
    Grossman, S., et al.: Online detection of effectively callback free objects with applications to smart contracts. In: ACM SIGPLAN Symposium on Principles of Programming Languages (POPL) (2018)Google Scholar
  10. 10.
    Hicks, M., Nettles, S.: Dynamic software updating. ACM Trans. Program. Lang. Syst. 27(6), 1049–1096 (2005).  https://doi.org/10.1145/1108970.1108971CrossRefGoogle Scholar
  11. 11.
    Hildenbrandt, E., et al.: KEVM: a complete semantics of the ethereum virtual machine. Technical report (2017)Google Scholar
  12. 12.
    Hirai, Y.: Defining the ethereum virtual machine for interactive theorem provers. In: Brenner, M., et al. (eds.) FC 2017. LNCS, vol. 10323, pp. 520–535. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-70278-0_33CrossRefGoogle Scholar
  13. 13.
    Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-17511-4_20CrossRefzbMATHGoogle Scholar
  14. 14.
    Leroy, X., et al.: The CompCert verified compiler. Documentation and user’s manual, INRIA Paris-Rocquencourt (2012)Google Scholar
  15. 15.
    Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. CCS 2016, pp. 254–269. ACM, New York (2016).  https://doi.org/10.1145/2976749.2978309
  16. 16.
    Necula, G.C.: Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL 1997, pp. 106–119. ACM, New York (1997).  https://doi.org/10.1145/263699.263712
  17. 17.
    Sergey, I., Hobor, A.: A concurrent perspective on smart contracts. CoRR abs/1702.05511 (2017). http://arxiv.org/abs/1702.05511
  18. 18.
    Sirer, E.G.: Parity’s Wallet Bug is not Alone (2017). https://blogs.apache.org/foundation/entry/apache-struts-statement-on-equifax. Accessed 05 Nov 2017
  19. 19.
    Various: formal verification for solidity contracts. https://forum.ethereum.org/discussion/3779/formal-verification-for-solidity-contracts. Accessed 14 Jul 2018
  20. 20.
    Vladimirov, M., Khovratovich, D.: ERC20 API: an attack vector on approve/transferfrom methods. https://docs.google.com/document/d/1YLPtQxZu1UAvO9cZ1O2RPXBbT0mooh4DYKjA_jp-RLM/edit#heading=h.m9fhqynw2xvt. Accessed: 14 Jan 2018
  21. 21.
    The Ethereum Wiki: ERC20 token standard. https://theethereum.wiki/w/index.php/ERC20_Token_Standard. Accessed 14 Jan 2018

Copyright information

© International Financial Cryptography Association 2019

Authors and Affiliations

  • Thomas Dickerson
    • 1
  • Paul Gazzillo
    • 2
    Email author
  • Maurice Herlihy
    • 1
  • Vikram Saraph
    • 1
  • Eric Koskinen
    • 2
  1. 1.Brown UniversityProvidenceUSA
  2. 2.Stevens Institute of TechnologyHobokenUSA

Personalised recommendations