Skip to main content
Top

2025 | OriginalPaper | Chapter

Trusted Deployer: A Tool for Safe Creation and Upgrade of Ethereum Smart Contracts

Authors : Juliandson Ferreira, Pedro Antonino, Augusto Sampaio, A. W. Roscoe, Filipe Arruda

Published in: Formal Methods: Foundations and Applications

Publisher: Springer Nature Switzerland

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

The lack of systematic and, particularly, mechanised support to ensure a safe creation and upgrade of smart contracts has led to the deployment of instances with flaws that have been thoroughly exploited, putting digital assets at risk. Formal verification can potentially help to eliminate these high impact flaws, particularly by allowing one to check whether smart contracts obey some desired properties. We have already proposed the concept of a trusted deployer to address these issues. In this work we present the detailed design of a public, open-source, and off-chain tool that supports the creation and upgrade of smart contracts, ensuring that they meet corresponding formal specifications. We detail the tool’s overall architecture, its usage, and its applicability to real-world smart contracts.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Literature
3.
go back to reference Arruda, F., Antonino, P., Sampaio, A., Roscoe, A.W.: Solver-aided inference of abstraction invariant for the safe evolution of smart contracts. Technical report (2022) Arruda, F., Antonino, P., Sampaio, A., Roscoe, A.W.: Solver-aided inference of abstraction invariant for the safe evolution of smart contracts. Technical report (2022)
6.
go back to reference Thomas, D., Gazzillo, P., Herlihy, M., Saraph, V., Koskinen, E.: Proof-carrying smart contracts. In: Financial Cryptography Workshops (2018) Thomas, D., Gazzillo, P., Herlihy, M., Saraph, V., Koskinen, E.: Proof-carrying smart contracts. In: Financial Cryptography Workshops (2018)
10.
go back to reference Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. (TOSEM) 11(2), 256–290 (2002)CrossRef Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. (TOSEM) 11(2), 256–290 (2002)CrossRef
12.
go back to reference Meyer, B.: Applying ‘design by contract’. Computer 25(10), 40–51 (1992)CrossRef Meyer, B.: Applying ‘design by contract’. Computer 25(10), 40–51 (1992)CrossRef
13.
go back to reference Misson, H.A.: Applying formal verification techniques to embedded software in UAV design (2019) Misson, H.A.: Applying formal verification techniques to embedded software in UAV design (2019)
16.
go back to reference Permenev, A., Dimitrov, D., Tsankov, P., Drachsler-Cohen, D., Vechev, M.: Verx: safety verification of smart contracts. In: 2020 IEEE Symposium on Security and Privacy (SP), pp. 1661–1677 (2020) Permenev, A., Dimitrov, D., Tsankov, P., Drachsler-Cohen, D., Vechev, M.: Verx: safety verification of smart contracts. In: 2020 IEEE Symposium on Security and Privacy (SP), pp. 1661–1677 (2020)
17.
go back to reference Rodler, M., Li, W., Karame, G.O., Davi, L.: EVMPatch: timely and automated patching of ethereum smart contracts. In: 30th USENIX Security Symposium (USENIX Security 21), pp. 1289–1306. USENIX Association (2021) Rodler, M., Li, W., Karame, G.O., Davi, L.: EVMPatch: timely and automated patching of ethereum smart contracts. In: 30th USENIX Security Symposium (USENIX Security 21), pp. 1289–1306. USENIX Association (2021)
19.
go back to reference Stephens, J., Ferles, K., Mariano, B., Lahiri, S., Dillig, I.: Smartpulse: automated checking of temporal properties in smart contracts. In: 2021 IEEE Symposium on Security and Privacy (SP), pp. 555–571 (2021) Stephens, J., Ferles, K., Mariano, B., Lahiri, S., Dillig, I.: Smartpulse: automated checking of temporal properties in smart contracts. In: 2021 IEEE Symposium on Security and Privacy (SP), pp. 555–571 (2021)
21.
go back to reference Wang, Y., et al.: Formal verification of workflow policies for smart contracts in azure blockchain. In: VSTTE, pp. 87–106 (2020) Wang, Y., et al.: Formal verification of workflow policies for smart contracts in azure blockchain. In: VSTTE, pp. 87–106 (2020)
Metadata
Title
Trusted Deployer: A Tool for Safe Creation and Upgrade of Ethereum Smart Contracts
Authors
Juliandson Ferreira
Pedro Antonino
Augusto Sampaio
A. W. Roscoe
Filipe Arruda
Copyright Year
2025
DOI
https://doi.org/10.1007/978-3-031-78116-2_12

Premium Partner