Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Software and Systems Modeling

25.01.2024 | Special Section Paper

A refinement-based approach to safe smart contract deployment and evolution

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

Erschienen in: Software and Systems Modeling

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

In our previous work, we proposed a verification framework that shifts from the “code is law” to a new “specification is law” paradigm related to the safe evolution of smart contracts. The framework proposed there relaxed the well-established requirement that, once a smart contract is deployed in a blockchain, its code is expected to be immutable. More flexibly, contracts are allowed to be created and upgraded provided they meet a corresponding formal specification that was fixed. In the current paper, we extend this framework to allow specifications to evolve, provided a refinement notion is preserved. We propose a notion of specification refinement tailored for smart contracts and a methodology for checking it. In addition to weakening preconditions and strengthening postconditions and invariants, we allow for the change of data representation and interface extension. Thus, we are able to reason about a significantly wider class of smart contract evolution histories, when contrasted with the original framework. The new framework is centred around a trusted deployer: an off-chain service that formally verifies and enforces the notions of implementation conformance and specification refinement. We have investigated its applicability to the safe deployment and upgrade of contracts implementing widely used Ethereum standards (the ERC20 Token Standard, the ERC3156 Flash Loans, the ERC1155 Multi Token Standard and The ERC721 standard for Non-Fungible Tokens); we handle evolutions possibly involving changes in data representation and interface extensions.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Fußnoten
1
In fact, the function send also delegates control to msg.sender but it does in such a restricted way that it cannot perform any relevant computation. So, for the purpose of this paper and to simplify our exposition, we ignore this delegation.
 
2
Typically, specifications might involved user-defined types such as structs and enumerations. For the sake of conciseness and generality, our specification definition omits the explicit declaration of such types and assume that the types used in a specification, even when user-defined, are well known.
 
3
Recall that the interface I is a mapping from function names to their signatures defined by a pair of sequences: one for the input parameters and the other for the output parameters, with their types. So we use the notation \(n \mapsto (in, outs)\) to represent a maplet of the interface I.
 
4
The function verify-upgrade can be optimised as follows. Unlike \(\textit{verify-creation}\), this function can assume that the constructor’s obligations have been met. The constructor is only executed at contract-creation time. The upgrade process need only to check for conformance for the implementation of the (non-constructor) public functions.
 
5
We are assuming that the constructor function has no parameters for the sake of simplicity. Our framework could easily be adapted to include such parameters, but also, given that this function is only called once, its expected arguments could be hardcoded into the constructor code turning it into a function without parameters.
 
Literatur
1.
AMD SEV-SNP: Strengthening VM isolation with integrity protection and more (2020)
2.
Adhikari, C.: Secure framework for healthcare data management using ethereum-based blockchain technology. In: 2017 Undergraduate Research and Scholarship Conference (2017)
3.
Ahrendt, W., Bubel, R.: Functional verification of smart contracts via strong data integrity. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Applications, pp. 9–24. Springer, Cham (2020)CrossRef
4.
Ahrendt, W., Bubel, R., Ellul, J., Pace, G.J., Pardo, R., Rebiscoul, V., Schneider, G.: Verification of smart contract business logic. In: Hojjat, H., Massink, M. (eds.) Fundamentals of Software Engineering, pp. 228–243. Springer, Cham (2019)CrossRef
5.
Aitzhan, N.Z., Svetinovic, D.: Security and privacy in decentralized energy trading through multi-signatures, blockchain and anonymous messaging streams. IEEE Trans. Dependable Secure Comput. 15, 840–852 (2016)CrossRef
6.
Antonino, P., Derek, A., Wołoszyn, W.A.: Flexible remote attestation of pre-SNP SEV VMs using SGX enclaves. IEEE Access 11, 90839–90856 (2023)CrossRef
7.
Antonino, P., Ferreira, J., Sampaio, A., Roscoe, A.W.: Specification is law: safe creation and upgrade of ethereum smart contracts. In: Schlingloff, B.H., Chai, M. (eds.) 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, pp. 227–243. Springer (2022)
8.
Antonino, P., Roscoe, A.W.: Formalising and verifying smart contracts with solidifier: a bounded model checker for solidity (2020)
9.
Antonino, P., Roscoe, A.W.: Solidifier: bounded model checking solidity using lazy contract deployment and precise memory modelling. In: Proceedings of the 36th Annual ACM Symposium on Applied Computing, SAC’21, pp. 1788–1797 (2021)
10.
Atzei, N., Bartoletti, M., Cimoli, T.: A survey of attacks on ethereum smart contracts (sok). In: POST 2017, pp. 164–186. Springer (2017)
11.
Azzopardi, S., Ellul, J., Pace, G.J.: Monitoring smart contracts: contractlarva and open challenges beyond. In: Runtime Verification—18th International Conference, RV 2018, Limassol, Cyprus, November 10–13, 2018, Proceedings, volume 11237 of Lecture Notes in Computer Science, pp. 113–137. Springer (2018)
12.
Barnett, M., Chang, B.Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: FMCO 2005, pp. 364–387. Springer (2005)
13.
14.
Bernardo, B., Cauderlier, R., Hu, Z., Pesin, B., Tesson, J.: Mi-cho-coq, a framework for certifying tezos smart contracts. In: Formal Methods. FM 2019 International Workshops: Porto, Portugal, October 7–11, 2019, Revised Selected Papers, Part I 3, pp. 368–379. Springer (2020)
15.
Biryukov, A., Khovratovich, D., Tikhomirov, S.: Findel: secure derivative contracts for ethereum. In: Financial Cryptography and Data Security—FC 2017 International Workshops, pp. 453–467. FC (2017)
16.
Brünnler, K., Flumini, D., Studer, T.: A logic of blockchain updates. In: Logical Foundations of Computer Science: International Symposium, LFCS 2018, Deerfield Beach, FL, USA, January 8–11, 2018, Proceedings, pp. 107–119. Springer (2017)
17.
18.
Dickerson, T., Gazzillo, P., Herlihy, M., Saraph, V., Koskinen, E.: Proof-carrying smart contracts. In: Financial Cryptography Workshops (2018)
19.
Dihego, J., Sampaio, A., Oliveira, M.: A refinement checking based strategy for component-based systems evolution. J. Syst. Softw. 167, 110598 (2020)CrossRef
20.
Durieux, T., Ferreira, J.F., Abreu, R., Cruz, P.: Empirical review of automated analysis tools on 47,587 ethereum smart contracts. In: Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering, ICSE’20, pp. 530–541. Association for Computing Machinery, New York (2020)
21.
Edwards, S., Lavagno, L., Lee, E.A., Sangiovanni-Vincentelli, A.: Design of embedded systems: formal models, validation, and synthesis. Proc. IEEE 85(3), 366–390 (1997)CrossRef
22.
23.
24.
25.
Galimullin, R., Ågotnes, T.: Coalition logic for specification and verification of smart contract upgrades. In: PRIMA 2022: Principles and Practice of Multi-Agent Systems: 24th International Conference, Valencia, Spain, November 16–18, 2022, Proceedings, pp. 563–572. Springer (2022)
26.
27.
Grishchenko, I., Maffei, M., Schneidewind, C.: Ethertrust: sound static analysis of ethereum bytecode. Technische Universität Wien, Tech. Rep (2018)
28.
Groce, A., Feist, J., Grieco, G., Colburn, M.: What are the actual flaws in important smart contracts (and how can we find them)? In: Bonneau, J., Heninger, N. (eds.) Financial Cryptography and Data Security, pp. 634–653. Springer, Cham (2020)
29.
Hahn, A., Singh, R., Liu, C.C., Chen, S.: Smart contract-based campus demonstration of decentralized transactive energy auctions. In: 2017 IEEE Power & Energy Society Innovative Smart Grid Technologies Conference, pp. 1–5. IEEE (2017)
30.
Hajdu, Á., Jovanović, D.: SMT-friendly formalization of the solidity memory model. In: ESOP 2020, pp. 224–250. Springer (2020)
31.
Hajdu, Á., Jovanović, D.: solc-verify: a modular verifier for solidity smart contracts. In: VSTTE, pp. 161–179. Springer (2020)
32.
Heineman, G.T., Councill, W.T.: Component-based software engineering. In: Putting the pieces together, Addison-Westley, vol. 5, p. 1 (2001)
33.
Herlihy, M., Moir, M.: Blockchains and the logic of accountability: keynote address. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, pp. 27–30 (2016)
34.
Hildenbrandt, E., Saxena, M., Rodrigues, N., Zhu, X., Daian, P., Guth, D., Moore, B., Park, D., Zhang, Y., Stefanescu, A., et al.: Kevm: a complete formal semantics of the ethereum virtual machine. In: CSF 2018, pp. 204–217. IEEE (2018)
35.
Hu, B., Zhang, Z., Liu, J., Liu, Y., Yin, J., Lu, R., Lin, X.: A comprehensive survey on smart contract construction and execution: paradigms, tools, and systems. Patterns 2(2), 100179 (2021)CrossRef
36.
Kemmerer, R.A.: Testing formal specifications to detect design errors. IEEE Trans. Softw. Eng. 11(1), 32–43 (1985)CrossRef
37.
Leavens, G.T., Baker, A.L., Ruby, C.: JML: A Notation for Detailed Design, pp. 175–188. Springer, Boston (1999)
38.
Lee, J., Nikitin, K., Setty, S.: Replicated state machines without replicated execution. In: IEEE (2020)
39.
Leino, K.R.M.: This is boogie 2. manuscript KRML 178(131), 9 (2008)
40.
Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, pp. 348–370. Springer, Berlin (2010)CrossRef
41.
Liskov, B.H., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16(6), 1811–1841 (1994)CrossRef
42.
Liu, C., Liu, H., Cao, Z., Chen, Z., Chen, B., Roscoe, B.: Reguard: finding reentrancy bugs in smart contracts. In: ICSE 2018, pp. 65–68. ACM (2018)
43.
Liu, S.: Verifying consistency and validity of formal specifications by testing. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM’99—Formal Methods, pp. 896–914. Springer, Berlin (1999)
44.
45.
Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: CCS 2016, pp. 254–269. ACM (2016)
46.
Maene, P., Götzfried, J., de Clercq, R., Müller, T., Freiling, F., Verbauwhede, I.: Hardware-based trusted computing architectures for isolation and attestation. IEEE Trans. Comput. 67(3), 361–374 (2018)MathSciNetCrossRef
47.
McCorry, P., Shahandashti, S.F., Hao, F.: A smart contract for boardroom voting with maximum voter privacy. In: Kiayias, A. (eds.) Financial Cryptography and Data Security. FC 2017. Lecture Notes in Computer Science, volume 10322, pp. 357–375 (2017)
48.
Meyer, B.: Applying “design by contract’’. Computer 25(10), 40–51 (1992)CrossRef
49.
Meyer, B.: Object-Oriented Software Construction, 1st edn. Prentice-Hall Inc, Hoboken (1988)
50.
Morgan, C.: Programming from Specifications, 2nd edn. Prentice Hall International (UK) Ltd., Hoboken (1994)
51.
Mossberg, M., Manzano, F., Hennenfent, E., Groce, A., Grieco, G., Feist, J., Brunson, T., Dinaburg, A.: Manticore: a user-friendly symbolic execution framework for binaries and smart contracts. In: 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 1186–1189. IEEE (2019)
52.
53.
Nguyen, T.D., Pham, L.H., Sun, J.: Sguard: towards fixing vulnerable smart contracts automatically. In: 2021 IEEE Symposium on Security and Privacy (SP), pp. 1215–1229 (2021)
54.
Nielsen, C.B., Larsen, P.G., Fitzgerald, J., Woodcock, J., Peleska, J.: Systems of systems engineering: basic concepts, model-based techniques, and research directions. ACM Comput. Surv. 48(2), 1–41 (2015)CrossRef
55.
Notheisen, B., Gödde, M., Weinhardt, C.: Trading stocks on blocks—engineering decentralized markets. In: Hevner, A. (eds.) Designing the Digital Transformation. DESRIST 2017. Lecture Notes in Computer Science (2017)
56.
57.
Papazoglou, M.P., Traverso, P., Dustdar, S., Leymann, F.: Service-oriented computing: state of the art and research challenges. Computer 40(11), 38–45 (2007)CrossRef
58.
Permenev, A., Dimitrov, D., Tsankov, P., Drachsler-Cohen, D., Vechev, M.: Verx: safety verification of smart contracts. In: S &P 2020, pp. 18–20 (2020)
59.
60.
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)
61.
Shorish, J.: Blockchain state machine representation (2018)
62.
63.
64.
Tasiran, S., Keutzer, K.: Coverage metrics for functional validation of hardware designs. IEEE Des. Test Comput. 18(4), 36–45 (2001)CrossRef
65.
66.
Tikhomirov, S., Voskresenskaya, E., Ivanitskiy, I., Takhaviev, R., Marchenko, E., Alexandrov, Y.: Smartcheck: static analysis of ethereum smart contracts. In: WETSEB 2018, pp. 9–16. IEEE (2018)
67.
Tolmach, P., Li, Y., Lin, S.-W., Liu, Y., Li, Z.: A survey of smart contract formal specification and verification. ACM Comput. Surv. 54(7), 1–38 (2021)CrossRef
68.
Torres, C.F., Jonker, H., State, R.: Elysium: automagically healing vulnerable smart contracts using context-aware patching. In: CoRR, abs/2108.10071 (2021)
69.
Tsankov, P., Dan, A., Drachsler-Cohen, D., Gervais, A., Buenzli, F., Vechev, M.: Securify: practical security analysis of smart contracts. In: CCS 2018, pp. 67–82. ACM (2018)
70.
71.
72.
Wang, D., Wu, S., Lin, Z., Wu, L., Yuan, X., Zhou, Y., Wang, H., Ren, K.: Towards a first step to understand flash loan and its applications in defi ecosystem. In: Proceedings of the Ninth International Workshop on Security in Blockchain and Cloud Computing, pp. 23–28 (2021)
73.
Wang, Y., Lahiri, S.K., Chen, S., Pan, R., Dillig, I., Born, C., Naseer, I., Ferles, K.: Formal verification of workflow policies for smart contracts in azure blockchain. In: VSTTE, pp. 87–106 (2020)
74.
Wood, G.: Ethereum: a secure decentralised generalised transaction ledger (2014)
75.
Wüst, K., Matetic, S., Egli, S., Kostiainen, K., Capkun, S.: Ace: asynchronous and concurrent execution of complex smart contracts. In: Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security, CCS’20, pp 587–600 (2020)
76.
Xu, J., Vadgama, N.: From banks to DeFi: the evolution of the lending market. In: Vadgama, N., Xu, J., Tasca, P. (eds.) Enabling the Internet of Value. Future of Business and Finance. Springer, Cham (2022)
77.
Yermack, D.: Corporate governance and blockchains. In: Review of Finance, pp. 7–31 (2017)
78.
Yu, X.L., Al-Bataineh, O., Lo, D., Roychoudhury, A.: Smart contract repair. ACM Trans. Softw. Eng. Methodol. 29(4), 1–32 (2020)CrossRef
79.
Metadaten
Titel
A refinement-based approach to safe smart contract deployment and evolution
verfasst von
Pedro Antonino
Juliandson Ferreira
Augusto Sampaio
A. W. Roscoe
Filipe Arruda
Publikationsdatum
25.01.2024
Verlag
Springer Berlin Heidelberg
Erschienen in
Software and Systems Modeling
Print ISSN: 1619-1366
Elektronische ISSN: 1619-1374
DOI
https://doi.org/10.1007/s10270-023-01143-z

Premium Partner

    Bildnachweise