nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

Defining the Ethereum Virtual Machine for Interactive Theorem Provers

verfasst von : Yoichi Hirai

Erschienen in: Financial Cryptography and Data Security

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

Smart contracts in Ethereum are executed by the Ethereum Virtual Machine (EVM). We defined EVM in Lem, a language that can be compiled for a few interactive theorem provers. We tested our definition against a standard test suite for Ethereum implementations. Using our definition, we proved some safety properties of Ethereum smart contracts in an interactive theorem prover Isabelle/HOL. To our knowledge, ours is the first formal EVM definition for smart contract verification that implements all instructions. Our definition can serve as a basis for further analysis and generation of Ethereum smart contracts.

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 Trust in Smart Contracts is a Process, As Well

Nächstes Kapitel SmartCast: An Incentive Compatible Consensus Protocol Using Smart Contracts

Several entities develop Ethereum clients in Python,

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-70278-0_33/459246_1_En_33_IEq4_HTML.gif

, Rust, Java, Scala and Go, and each contains its own EVM implementation.

The Coq users’ mailing list has 1,404 subscribers while the K-Framework’s has 127 at the time of writing.

https://github.com/pirapira/eth-isabelle/tree/wtsc01.

If nondeterminism existed in the EVM execution, at least, we would need to choose a representation of nondeterminism that works both in interactive theorem provers and in OCaml.

We can guarantee termination by the gas, but the proof is non-trivial (currently 980 lines of Isabelle code).

This property can be established only by checking all lines in the Yellow Paper that changes the balance.

One of the authors explained that the work had been done in a hackathon and the codebase had not been touched since.

The Coq proof assistant. https://coq.inria.fr/. Accessed 19 Dec 2016

Ethereum VM tests. https://github.com/ethereum/tests/tree/develop/VMTests. Accessed 02 Jan 2017

Solidity 0.4.8-develop documentation. https://solidity.readthedocs.io/. Accessed 19 Dec 2016

WebAssembly. http://webassembly.org/. Accessed 16 Dec 2016

Atzei, N., Bartoletti, M., Cimoli, T.: A survey of attacks on Ethereum smart contracts. Cryptology ePrint Archive (2016). http://eprint.iacr.org/2016/1007

Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. SIGPLAN Not. 46(1), 55–66 (2011)CrossRefMATH

Becker, H., et al.: Combining mechanized proofs and model-based testing in the formal analysis of a hypervisor. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 69–84. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-48989-6_5 CrossRef

Bhargavan, K., Delignat-Lavaud, A., Fournet, C., Gollamudi, A., Gonthier, G., Kobeissi, N., Kulatova, N., Rastogi, A., Sibut-Pinote, T., Swamy, N., Zanella-Béguelin, S.: Formal verification of smart contracts: short paper. In: PLAS 2016, pp. 91–96. ACM (2016)

Boyer, R.S., Yu, Y.: Automated proofs of object code for a widely used microprocessor. J. ACM 43(1), 166–192 (1996)MathSciNetCrossRefMATH

10.

Fox, A.: Formal specification and verification of ARM6. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 25–40. Springer, Heidelberg (2003). https://doi.org/10.1007/10930755_2 CrossRef

11.

Kennedy, A., Benton, N., Jensen, J.B., Dagand, P.E.: Coq: the world’s best macro assembler? In: PPDP 2013, pp. 13–24. ACM (2013)

12.

Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM Trans. Program. Lang. Syst. 28(4), 619–695 (2006)CrossRef

13.

Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: POPL 2014, pp. 179–191. ACM, New York (2014)

14.

Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)CrossRef

15.

Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: CCS 2016, pp. 254–269. ACM (2016)

16.

Mulligan, D.P., Owens, S., Gray, K.E., Ridge, T., Sewell, P.: Lem: reusable engineering of real-world semantics. SIGPLAN Not. 49(9), 175–188 (2014)CrossRefMATH

17.

Myreen, M.O., Gordon, M.J.C., Slind, K.: Decompilation into logic-improved. FMCAD 2012, 78–81 (2012)

18.

Myreen, M.O., Fox, A.C.J., Gordon, M.J.C.: Hoare logic for ARM machine code. In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol. 4767, pp. 272–286. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-75698-9_18 CrossRef

19.

Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9 MATH

20.

Owens, S., Myreen, M.O., Kumar, R., Tan, Y.K.: Functional big-step semantics. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 589–615. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49498-1_23 CrossRef

21.

Ramananandro, T., Dos Reis, G., Leroy, X.: Formal verification of object layout for C++ multiple inheritance. SIGPLAN Not. 46(1), 67–80 (2011)CrossRefMATH

22.

Roşu, G., Şerbănuţă, T.F.: An overview of the K semantic framework. J. Log. Algebr. Program. 79(6), 397–434 (2010)MathSciNetCrossRefMATH

23.

Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28–32. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71067-7_6 CrossRef

24.

Tan, G., Appel, A.W.: A compositional logic for control flow. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 80–94. Springer, Heidelberg (2005). https://doi.org/10.1007/11609773_6 CrossRef

25.

Wiedijk, F.: Pollack-inconsistency. Electron. Notes Theor. Comput. Sci. 285, 85–100 (2012)CrossRefMATH

26.

Wood, G.: Ethereum: a secure decentralised generalised transaction ledger-EIP-150 revision. http://paper.gavwood.com/. Accessed 19 Dec 2016

Titel: Defining the Ethereum Virtual Machine for Interactive Theorem Provers
verfasst von: Yoichi Hirai
Verlag: Springer International Publishing
Buch: Financial Cryptography and Data Security
Print ISBN: 978-3-319-70277-3

Electronic ISBN: 978-3-319-70278-0

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-70278-0_33

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner