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
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Runtime Verification - 17 Years Later Kapitel lesen Erstes Kapitel lesen

2018 | OriginalPaper | Buchkapitel

Monitoring Smart Contracts: ContractLarva and Open Challenges Beyond

verfasst von : Shaun Azzopardi, Joshua Ellul, Gordon J. Pace

Erschienen in: Runtime Verification

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Smart contracts present new challenges for runtime verification techniques, due to features such as immutability of the code and the notion of gas that must be paid for the execution of code. In this paper we present the runtime verification tool ContractLarva and outline its use in instrumenting monitors in smart contracts written in Solidity, for the Ethereum blockchain-based distributed computing platform. We discuss the challenges faced in doing so, and how some of these can be addressed, using the ERC-20 token standard to illustrate the techniques. We conclude by proposing a list of open challenges in smart contract and blockchain monitoring.

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 "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

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
Vorheriges Kapitel Runtime Verification: From Propositional to First-Order Temporal Logic
Nächstes Kapitel Online and Offline Stream Runtime Verification of Synchronous Systems
Fußnoten
1
In this context, one typically finds the use of the term immutability for immutability of transactions or data written in the past, whilst still allowing for appending new entries (in a controlled manner) to the ledger.
 
2
In practice, what stops these parties from doing so is the threat to be sued for breach of contract, which happens outside the realm of the contract itself.
 
3
NP-complete problems are a classical case of this — although there is no known deterministic polynomial algorithm which can find a solution to instances of any one of these problems, a known solution to an NP-complete problem instance can be verified in polynomial time on a deterministic machine.
 
5
The choice of the term event, frequently used in runtime verification, is unfortunately overloaded with the notion of events in Solidity. In the rest of the paper, we use the term to refer to runtime points-of-interest.
 
6
The only case which is not covered by this approach is if the contract performs external delegate calls (which may result in the callee changing the state of the caller). However, this can be syntactically checked at instrumentation time.
 
7
Although in traditional systems, overheads in space, time and communication are still paid for financially (more memory, more CPU power or more bandwidth), the cost is indirect and the perception is that is a matter of efficiency, and not cost management..
 
8
ERC stands for Ethereum Request for Comment, with 20 being the number that was assigned to the request.
 
9
As reported by Etherscan (see www.​etherscan.​io/​tokens) in July 2018. The number of active, and trustworthy token implementations is, however, much lower than this figure.
 
Literatur
1.
Ahrendt, W., Chimento, J.M., Pace, G.J., Schneider, G.: Verifying data- and control-oriented properties combining static and runtime verification: theory and tools. Form. Methods Syst. Des. 51(1), 200–265 (2017)CrossRef
2.
Ahrendt, W., Pace, G.J., Schneider, G.: Smart contracts –a killer application for deductive source code verification. In: Festschrift on the Occasion of Arnd Poetzsch-Heffter’s 60th Birthday (ARND 2018) (2018)
3.
Amani, S., Bégel, M., Bortin, M., Staples, M.: Towards verifying Ethereum smart contract bytecode in Isabelle/Hol. In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, pp. 66–77, New York, NY, USA. ACM (2018)
4.
5.
6.
Bhargavan, K., et al.: Formal verification of smart contracts. In: The 11th Workshop on Programming Languages and Analysis for Security (PLAS 2016) (2016)
7.
8.
Bodden, E., Lam, P., Hendren, L.: Clara: a framework for partially evaluating finite-state runtime monitors ahead of time. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 183–197. Springer, Heidelberg (2010). https://​doi.​org/​10.​1007/​978-3-642-16612-9_​15CrossRefMATH
9.
Colombo, C., Ellul, J., Pace, G.J.: Contracts over smart contracts: recovering from violations dynamically. In: ISoLA. LNCS (2018)
10.
Colombo, C., Pace, G.J.: Monitor-oriented compensation programming through compensating automata. In: ECEASST, vol. 58 (2013)
11.
Colombo, C., Pace, G.J.: Comprehensive monitor-oriented compensation programming. In: FESCA, vol. 147, pp. 47–61. EPTCS (2014)
12.
13.
Colombo, C., Pace, G.J., Schneider, G.: Safe runtime verification of real-time properties. In: 7th International Conference Formal Modeling and Analysis of Timed Systems, FORMATS 2009, pp. 103–117 (2009)
14.
de Boer, F.S., de Gouw, S., Johnsen, E.B., Kohn, A., Wong, P.Y.H.: Run-time assertion checking of data- and protocol-oriented properties of Java programs: an industrial case study. In: Chiba, S., Tanter, É., Bodden, E., Maoz, S., Kienzle, J. (eds.) Transactions on Aspect-Oriented Software Development XI. LNCS, vol. 8400, pp. 1–26. Springer, Heidelberg (2014). https://​doi.​org/​10.​1007/​978-3-642-55099-7_​1CrossRef
15.
Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification. In: Broy, M., Peled, D.A., Kalus, G. (eds.) Engineering Dependable Software Systems, vol. 34. NATO Science for Peace and Security Series, D: Information and Communication Security, pp. 141–175. IOS Press (2013)
16.
Fröwis, M., Böhme, R.: In code we trust? In: Garcia-Alfaro, J., Navarro-Arribas, G., Hartenstein, H., Herrera-Joancomartí, J. (eds.) Data Privacy Management. Cryptocurrencies and Blockchain Technology, pp. 357–372. Springer, Cham (2017)
17.
Fuchs, N.E.: Specifications are (preferably) executable. Softw. Eng. J. 7(5), 323–334 (1992)CrossRef
18.
Grech, N., Kong, M., Jurisevic, A., Lexi, B., Scholz, B., Smaragdakis, Y.: Madmax: surviving out-of-gas conditions in Ethereum smart contracts. In: PACMPL, (OOPSLA) (2018)
19.
Grishchenko, I., Maffei, M., Schneidewind, C.: Foundations and tools for the static analysis of ethereum smart contracts. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification, pp. 51–78. Springer, Cham (2018)CrossRef
20.
Hayes, I., Jones, C.B.: Specifications are not (necessarily) executable. Softw. Eng. J. 4(6), 330–338 (1989)CrossRef
21.
Hirai, Y.: Defining the ethereum virtual machine for interactive theorem provers. In: Brenner, M., Rohloff, K., Bonneau, J., Miller, A., Ryan, P.Y., Teague, V., Bracciali, A., Sala, M., Pintore, F., Jakobsson, M. (eds.) Financial Cryptography and Data Security, pp. 520–535. Springer, Cham (2017)CrossRef
22.
Kalra, S., Goel, S., Dhawan, M., Sharma, S.: ZEUS: analyzing safety of smart contracts. In: 25th Annual Network and Distributed System Security Symposium, NDSS 2018, San Diego, California, USA, 18–21 February 2018
23.
Lessig, L.: Code 2.0. CreateSpace, 2nd edn. Paramount (2009)
24.
Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebr. Program. 78(5), 293–303 (2009)CrossRef
25.
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, New York, NY, USA. ACM (2016)
26.
27.
Nikolic, I., Kolluri, A., Sergey, I., Saxena, P., Hobor, A.: Finding the greedy, prodigal, and suicidal contracts at scale. CoRR, abs/1802.06038 (2018)
28.
Park, D., Zhang, Y., Saxena, M., Daian, P., Roşu, G.: A formal verification tool for Ethereum VM Bytecode. In: Proceedings of the 26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2018). ACM, November 2018
29.
30.
Szabo, N.: Smart contracts: building blocks for digital markets. Extropy, vol. 16 (1996)
31.
32.
Wood, G.: Ethereum: a secure decentralised generalised transaction ledger. Ethereum Proj. Yellow Pap. 151, 1–32 (2014)
Metadaten
Titel
Monitoring Smart Contracts: ContractLarva and Open Challenges Beyond
verfasst von
Shaun Azzopardi
Joshua Ellul
Gordon J. Pace
Copyright-Jahr
2018
Buch
Runtime Verification

Print ISBN: 978-3-030-03768-0

Electronic ISBN: 978-3-030-03769-7

Copyright-Jahr: 2018

DOI
https://doi.org/10.1007/978-3-030-03769-7_8

Premium Partner

    Bildnachweise