Safe evolution of smart contracts

• Augusto Sampaio UFPE
• Pedro Antonino The Blockhouse Technology Limited
• Juliandson Ferreira UFPE
• Filipe Arruda UFPE
• A. W. Roscoe The Blockhouse Technology Limited / University of Oxford / University College Oxford Blockchain Research Centre

DOI: https://doi.org/10.5753/cblockchain.2023.231559

Resumo

We present a framework that supports the safe deployment and upgrade of smart contracts based on the design-by-contract paradigm. The starting point is an interface specification with invariants and pre- and postconditions for each function. The first deployed smart contract must conform to this specification. Specification evolution might involve both changing the data representation as well as extending the interface with new functions, provided the evolved specification is a refinement of the original one. Implementation evolution must conform to the corresponding specification. We report on the applicability of the framework in the verification of smart contracts that implement some Ethereum standards.

Referências

Antonino, P., Ferreira, J., Sampaio, A., and Roscoe, A. W. (2022). Specification is law: Safe creation and upgrade of ethereum smart contracts. In Schlingloff, B. and Chai, M., editors, Software Engineering and Formal Methods 20th International Conference, SEFM 2022, Berlin, Germany, September 26-30, 2022, Proceedings, volume 13550 of Lecture Notes in Computer Science, pages 227–243. Springer.

Antonino, P., Ferreira, J., Sampaio, A., Roscoe, A. W., and Arruda, F. (2023). A refinement-based approach to safe smart contract deployment and evolution. SoSyM— International Journal on Software and Systems Modeling. Submitted.

Dickerson, T. D., Gazzillo, P., Herlihy, M., Saraph, V., and Koskinen, E. (2018). Proofcarrying smart contracts. In Financial Cryptography Workshops.

Hajdu, Á. and Jovanović, D. (2020). solc-verify: A modular verifier for solidity smart contracts. In VSTTE, pages 161–179. Springer.

Liskov, B. H. and Wing, J. M. (1994). A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst., 16(6):1811–1841.

Lu, A. (2018). Solidity DelegateProxy Contracts. [link].

Meyer, B. (1992). Applying ’design by contract’. Computer, 25(10):40–51.

Morgan, C. (1994). Programming from Specifications (2nd Ed.). Prentice Hall International (UK) Ltd., GBR.

Mudge, N. (2020). EIP-2535: Diamonds, Multi-Facet Proxy. [link].

OpenZeppelin (2018). Proxy Patterns. [link] accessed on 30 May 2023.

Patrick, A., Coelho, I. M., and Lopes, B. (2021). Automatic program verification in dynamic logic with applications to smart contracts. In Anais do II Workshop Brasileiro de Lógica, pages 1–8. SBC.

Rodler, M., Li, W., Karame, G. O., and Davi, L. (2021). Evmpatch: Timely and automated patching of ethereum smart contracts. In 30th USENIX Security Symposium (USENIX Security 21), pages 1289–1306. USENIX Association.

Siegel, D. (2016). Understanding the dao attack. [link] accessed on 22 July 2021.

Tolmach, P., Li, Y., Lin, S.-W., Liu, Y., and Li, Z. (2021). A survey of smart contract formal specification and verification. ACM Computing Surveys (CSUR), 54(7).

Vollmer, J. (2016). The biggest hacker whodunnit of the summer. [link]. accessed on 22 July 2021.