References

references:

  • id: luumaking type: no-type author:

    • family: Luu given: Loi
    • family: Chu given: Duc-Hiep
    • family: Olickel given: Hrishi
    • family: Saxena given: Prateek
    • family: Hobor given: Aquinas issued:
    • year: '2016' title: Making smart contracts smarter publisher: Cryptology ePrint Archive, Report 2016/633 note: http://eprint.iacr.org/2016/633

  • id: hiraidefining type: no-type author:

    • family: Hirai given: Yoichi issued:
    • year: '2017' title: Defining the ethereum virtual machine for interactive theorem provers publisher: WSTC17, International Conference on Financial Cryptography and Data Security

  • id: guth2013formal type: article-journal author:

  • id: mulligan2014lem type: paper-conference author:

    • family: Mulligan given: Dominic P
    • family: Owens given: Scott
    • family: Gray given: Kathryn E
    • family: Ridge given: Tom
    • family: Sewell given: Peter issued:
    • year: '2014' title: 'Lem: Reusable engineering of real-world semantics' title-short: Lem container-title: ACM sigplan notices collection-number: '9' publisher: ACM page: '175-188' volume: '49'

  • id: chen2003towards type: article-journal author:

    • family: Chen given: Feng
    • family: Roşu given: Grigore issued:
    • year: '2003' title: 'Towards monitoring-oriented programming: A paradigm combining specification and implementation' title-short: Towards monitoring-oriented programming container-title: Electronic Notes in Theoretical Computer Science publisher: Elsevier page: '108-127' volume: '89' issue: '2'

  • id: kapproach type: no-type author:

  • id: szabo1994smart type: article-journal author:

  • id: peters2016understanding type: chapter author:

    • family: Peters given: Gareth W
    • family: Panayi given: Efstathios issued:
    • year: '2016' title: 'Understanding modern banking ledgers through blockchain technologies: Future of transaction processing and smart contracts on the internet of money' title-short: Understanding modern banking ledgers through blockchain technologies container-title: Banking beyond banks and money publisher: Springer page: '239-278'

  • id: atzei2016survey type: article-journal author:

    • family: Atzei given: Nicola
    • family: Bartoletti given: Massimo
    • family: Cimoli given: Tiziana issued:
    • year: '2016' title: A survey of attacks on Ethereum smart contracts. container-title: IACR Cryptology ePrint Archive page: '1007' volume: '2016'

  • id: narayanan2016bitcoin type: book author:

    • family: Narayanan given: Arvind
    • family: Bonneau given: Joseph
    • family: Felten given: Edward
    • family: Miller given: Andrew
    • family: Goldfeder given: Steven issued:
    • year: '2016' title: 'Bitcoin and cryptocurrency technologies: A comprehensive introduction' title-short: Bitcoin and cryptocurrency technologies publisher: Princeton University Press

  • id: sasson2014zerocash type: paper-conference author:

    • family: Sasson given: Eli Ben
    • family: Chiesa given: Alessandro
    • family: Garman given: Christina
    • family: Green given: Matthew
    • family: Miers given: Ian
    • family: Tromer given: Eran
    • family: Virza given: Madars issued:
    • year: '2014' title: 'Zerocash: Decentralized anonymous payments from bitcoin' title-short: Zerocash container-title: Security and privacy (sp), 2014 ieee symposium on publisher: IEEE page: '459-474'

  • id: ethereum type: no-type author:

  • id: barras1997coq type: thesis author:

    • family: Barras given: Bruno
    • family: Boutin given: Samuel
    • family: Cornes given: Cristina
    • family: Courant given: Judicaël
    • family: Filliatre given: Jean-Christophe
    • family: Gimenez given: Eduardo
    • family: Herbelin given: Hugo
    • family: Huet given: Gerard
    • family: Munoz given: Cesar
    • family: Murthy given: Chetan
    • literal: others issued:
    • year: '1997' title: 'The coq proof assistant reference manual: Version 6.1' title-short: The coq proof assistant reference manual publisher: Inria genre: PhD thesis

  • id: ethsplit type: article-journal author:

  • id: daofork type: article-journal author:

    • family: Castillo given: Michael dropping-particle: del issued:
    • year: '2016' title: Ethereum executes blockchain hard fork to return DAO funds publisher: Coindesk note: http://goo.gl/MpwrhS

  • id: icorush type: article-journal author:

    • family: Melendez given: Steven issued:
    • year: '2017' title: 'Inside the ico bubble: Why initial coin offerings have raised more than $1 billion since January' title-short: Inside the ico bubble publisher: Fast Company note: http://goo.gl/7b5nCd

  • id: hkg type: article-journal author:

  • id: paritymultisig type: article-journal author:

  • id: paritymultisig2 type: no-type author:

    • family: Steiner given: Jutta issued:
    • year: '2017' title: 'Security is a process: A postmortem on the parity multi-sig library self-destruct' title-short: Security is a process publisher: Ethcore note: http://goo.gl/LBh1vR

  • id: smartbillions type: no-type author:

  • id: mkr type: article-journal author:

  • id: eea type: article-journal author:

  • id: moser2013inquiry type: paper-conference author:

    • family: Moser given: Malte
    • family: Bohme given: Rainer
    • family: Breuker given: Dominic issued:
    • year: '2013' title: An inquiry into money laundering tools in the bitcoin ecosystem container-title: ECrime researchers summit (eCRS), 2013 publisher: IEEE page: '1-14'

  • id: coindeskformal type: article-journal author:

  • id: daian2016runtime type: paper-conference author:

    • family: Daian given: Philip
    • family: Guth given: Dwight
    • family: Hathhorn given: Chris
    • family: Li given: Yilong
    • family: Pek given: Edgar
    • family: Saxena given: Manasvi
    • family: Serbanuta given: Traian Florin
    • family: Rosu given: Grigore issued:
    • year: '2016' month: '09' title: 'Runtime verification at work: A tutorial' title-short: Runtime verification at work container-title: Runtime verification - 16th international conference, RV 2016 madrid, spain, september 23-30, 2016, proceedings collection-title: Lecture notes in computer science publisher: Springer page: '46-67' volume: '10012' DOI: http://dx.doi.org/10.1007/978-3-319-46982-9_5

  • id: ellison2012executable type: paper-conference author:

    • family: Ellison given: Chucky
    • family: Rosu given: Grigore issued:
    • year: '2012' month: 01 title: An executable formal semantics of c with applications container-title: Proceedings of the 39th acm sigplan-sigact symposium on principles of programming languages (popl’12) publisher: ACM page: '533-544' DOI: http://doi.acm.org/10.1145/2103656.2103719

  • id: thinkingsecurity type: article-journal author:

  • id: ethfoundationformal type: article-journal author:

  • id: ong2015evaluating type: article-journal author:

    • family: Ong given: Bobby
    • family: Lee given: Teik Ming
    • family: Li given: Guo
    • family: Chuen given: DLK issued:
    • year: '2015' title: Evaluating the potential of alternative cryptocurrencies container-title: 'Handbook of digital currency. Amsterdam: Elsevier' page: '81-135'

  • id: wilkinson2014storj type: article-journal author:

    • family: Wilkinson given: Shawn
    • family: Boshevski given: Tome
    • family: Brandoff given: Josh
    • family: Buterin given: Vitalik issued:
    • year: '2014' title: Storj a peer-to-peer cloud storage network publisher: Citeseer note: https://storj.io/storj.pdf

  • id: delmolino2016step type: paper-conference author:

    • family: Delmolino given: Kevin
    • family: Arnett given: Mitchell
    • family: Kosba given: Ahmed
    • family: Miller given: Andrew
    • family: Shi given: Elaine issued:
    • year: '2016' title: 'Step by step towards creating a safe smart contract: Lessons and insights from a cryptocurrency lab' title-short: Step by step towards creating a safe smart contract container-title: International conference on financial cryptography and data security publisher: Springer page: '79-94'

  • id: kogias2016enhancing type: paper-conference author:

    • family: Kogias given: Eleftherios Kokoris
    • family: Jovanovic given: Philipp
    • family: Gailly given: Nicolas
    • family: Khoffi given: Ismail
    • family: Gasser given: Linus
    • family: Ford given: Bryan issued:
    • year: '2016' title: Enhancing bitcoin security and performance with strong consistency via collective signing container-title: 25th USENIX security symposium (USENIX security 16) publisher: USENIX Association publisher-place: Austin, TX page: '279-296' URL: https://www.usenix.org/conference/usenixsecurity16/technical-sessions/presentation/kogias ISBN: '978-1-931971-32-4'

  • id: stefanescu-park-yuwen-li-rosu-2016-oopsla type: paper-conference author:

    • family: Ştefănescu given: Andrei
    • family: Park given: Daejun
    • family: Yuwen given: Shijiao
    • family: Li given: Yilong
    • family: Roşu given: Grigore issued:
    • year: '2016' month: '11' title: Semantics-based program verifiers for all languages container-title: Proceedings of the 31th conference on object-oriented programming, systems, languages, and applications (oopsla’16) publisher: ACM

  • id: rosu-serbanuta-2010-jlap type: article-journal author:

    • family: Roşu given: Grigore
    • family: Şerbănuţă given: Traian Florin issued:
    • year: '2010' title: An overview of the K semantic framework container-title: Journal of Logic and Algebraic Programming page: '397-434' volume: '79' issue: '6' note: https://kframework.org/ DOI: 10.1016/j.jlap.2010.03.012

  • id: serbanuta-rosu-2010-wrla type: paper-conference author:

    • family: Şerbanuţă given: Traian Florin
    • family: Roşu given: Grigore issued:
    • year: '2010' month: 03 title: 'K-Maude: A rewriting based tool for semantics of programming languages' title-short: K-Maude container-title: Proceedings of the 8th international workshop on rewriting logic and its applications (wrla’10) publisher: Springer page: '104-122' DOI: http://dx.doi.org/10.1007/978-3-642-16310-4_8

  • id: nakamoto2008bitcoin type: no-type author:

    • family: Nakamoto given: Satoshi issued:
    • year: '2008' title: 'Bitcoin: A peer-to-peer electronic cash system' title-short: Bitcoin note: https://bitcoin.org/bitcoin.pdf

  • id: dao-attack type: no-type author:

  • id: hathhorn-ellison-rosu-2015-pldi type: paper-conference author:

    • family: Hathhorn given: Chris
    • family: Ellison given: Chucky
    • family: Roşu given: Grigore issued:
    • year: '2015' month: 06 title: Defining the undefinedness of c container-title: Proceedings of the 36th acm sigplan conference on programming language design and implementation (pldi’15) publisher: ACM page: '336-345' DOI: http://dx.doi.org/10.1145/2813885.2737979

  • id: bogdanas-rosu-2015-popl type: paper-conference author:

    • family: Bogdănaş given: Denis
    • family: Roşu given: Grigore issued:
    • year: '2015' month: 01 title: '[K-Java: A Complete Semantics of Java]{.nocase}' container-title: Proceedings of the 42nd symposium on principles of programming languages (popl’15) publisher: ACM page: '445-456' DOI: http://dx.doi.org/10.1145/2676726.2676982

  • id: park-stefanescu-rosu-2015-pldi type: paper-conference author:

    • family: Park given: Daejun
    • family: Ştefănescu given: Andrei
    • family: Roşu given: Grigore issued:
    • year: '2015' month: 06 title: 'KJS: A complete formal semantics of JavaScript' title-short: KJS container-title: Proceedings of the 36th acm sigplan conference on programming language design and implementation (pldi’15) publisher: ACM page: '346-356' DOI: http://dx.doi.org/10.1145/2737924.2737991

  • id: ellison-2012-thesis type: thesis author:

    • family: Ellison given: Chucky issued:
    • year: '2012' month: 07 title: A formal semantics of C with applications publisher: University of Illinois genre: PhD thesis

  • id: stefanescu-ciobaca-mereuta-moore-serbanuta-rosu-2014-rta type: paper-conference author:

    • family: Ştefănescu given: Andrei
    • family: Ciobâcă given: Ştefan
    • family: Mereuţă given: Radu
    • family: Moore given: Brandon M.
    • family: Şerbănuţă given: Traian Florin
    • family: Roşu given: Grigore issued:
    • year: '2014' month: 07 title: All-path reachability logic container-title: Proceedings of the joint 25th international conference on rewriting techniques and applications and 12th international conference on typed lambda calculi and applications (rta-tlca’14) collection-title: LNCS publisher: Springer page: '425-440' volume: '8560' DOI: http://dx.doi.org/10.1007/978-3-319-08918-8_29

  • id: de2008z3 type: paper-conference author:

    • family: De Moura given: Leonardo
    • family: Bjørner given: Nikolaj issued:
    • year: '2008' title: 'Z3: An efficient smt solver' title-short: Z3 container-title: International conference on tools and algorithms for the construction and analysis of systems publisher: Springer Berlin Heidelberg page: '337-340'

  • id: guth-hathhorn-saxena-rosu-2016-cav type: paper-conference author:

    • family: Guth given: Dwight
    • family: Hathhorn given: Chris
    • family: Saxena given: Manasvi
    • family: Rosu given: Grigore issued:
    • year: '2016' month: 07 title: 'RV-Match: Practical semantics-based program analysis' title-short: RV-Match container-title: Computer aided verification - 28th international conference (CAV 2016), toronto, on, canada, july 17-23, 2016, proceedings, part I collection-title: LNCS publisher: Springer page: '447-453' volume: '9779' DOI: http://dx.doi.org/10.1007/978-3-319-41528-4_24

  • id: fstar-etaps type: paper-conference author:

    • family: Grishchenko given: Ilya
    • family: Maffei given: Matteo
    • family: Schneidewind given: Clara editor:
    • family: Bauer given: Lujo
    • family: Küsters given: Ralf issued:
    • year: '2018' title: A semantic framework for the security analysis of ethereum smart contracts container-title: Principles of security and trust publisher: Springer International Publishing publisher-place: Cham page: '243-269' abstract: 'Smart contracts are programs running on cryptocurrency (e.g., Ethereum) blockchains, whose popularity stem from the possibility to perform financial transactions, such as payments and auctions, in a distributed environment without need for any trusted third party. Given their financial nature, bugs or vulnerabilities in these programs may lead to catastrophic consequences, as witnessed by recent attacks. Unfortunately, programming smart contracts is a delicate task that requires strong expertise: Ethereum smart contracts are written in Solidity, a dedicated language resembling JavaScript, and shipped over the blockchain in the EVM bytecode format. In order to rigorously verify the security of smart contracts, it is of paramount importance to formalize their semantics as well as the security properties of interest, in particular at the level of the bytecode being executed.' ISBN: '978-3-319-89722-6'

  • id: fstar-tr type: article-journal author:

    • family: Grishchenko given: Ilya
    • family: Maffei given: Matteo
    • family: Schneidewind given: Clara issued:
    • year: '2018' title: A semantic framework for the security analysis of ethereum smart contracts. technical report. note: https://secpriv.tuwien.ac.at/tools/ethsemantics

  • id: wood2014ethereum type: article-journal author:

    • family: Wood given: Gavin issued:
    • year: '2014' title: 'Ethereum: A secure decentralised generalised transaction ledger' title-short: Ethereum note: (Updated for EIP-150 in 2017) http://yellowpaper.io/

  • id: solidity type: no-type author:

  • id: serpent type: no-type author:

  • id: ktoisabelle type: no-type author:

  • id: why3 type: chapter author:

    • family: Filliâtre given: Jean-Christophe
    • family: Paskevich given: Andrei editor:
    • family: Felleisen given: Matthias
    • family: Gardner given: Philippa issued:
    • year: '2013' title: Why3 — where programs meet provers container-title: 'Programming languages and systems: 22nd european symposium on programming, esop 2013, held as part of the european joint conferences on theory and practice of software, etaps 2013, rome, italy, march 16-24, 2013. proceedings' publisher: Springer Berlin Heidelberg publisher-place: Berlin, Heidelberg page: '125-128' URL: https://doi.org/10.1007/978-3-642-37036-6_8 DOI: 10.1007/978-3-642-37036-6_8 ISBN: '978-3-642-37036-6'

  • id: rosu-2015-rta type: article-journal author:

    • family: Roşu given: Grigore issued:
    • year: '2017' title: Matching logic container-title: Logical Methods in Computer Science volume: to appear DOI: http://arxiv.org/abs/1705.06312

  • id: meseguer-20-years-rewriting type: article-journal author:

    • family: Meseguer given: José issued:
    • year: '2012' title: Twenty years of rewriting logic container-title: The Journal of Logic and Algebraic Programming page: 721 - 781 volume: '81' issue: '7' note: Rewriting Logic and its Applications URL: http://www.sciencedirect.com/science/article/pii/S1567832612000707 DOI: http://dx.doi.org/10.1016/j.jlap.2012.06.003 ISSN: '1567-8326'

  • id: rosu-stefanescu-2012-fm type: paper-conference author:

    • family: Roşu given: Grigore
    • family: Ştefănescu given: Andrei issued:
    • year: '2012' month: '8' title: From Hoare Logic to Matching Logic Reachability container-title: Proceedings of the 18th international symposium on formal methods (fm’12) collection-title: LNCS publisher: Springer page: '387-402' volume: '7436' abstract: 'Matching logic reachability has been recently proposed as an alternative program verification approach. Unlike Hoare logic, where one defines a language-specific proof system that needs to be proved sound for each language separately, matching logic reachability provides a *language-independent* and *sound* proof system that directly uses the trusted operational semantics of the language as axioms. Matching logic reachability thus has a clear practical advantage: it eliminates the need for an additional semantics of the same language in order to reason about programs, and implicitly eliminates the need for tedious soundness proofs. What is not clear, however, is whether matching logic reachability is as powerful as Hoare logic. This paper introduces a technique to mechanically translate Hoare logic proof derivations into equivalent matching logic reachability proof derivations. The presented technique has two consequences: first, it suggests that matching logic reachability has no theoretical limitation over Hoare logic; and second, it provides a new approach to prove Hoare logics sound.' DOI: http://dx.doi.org/10.1007/978-3-642-32759-9_32

  • id: ethereum-abi type: no-type author:

  • id: viper-url type: no-type author:

  • id: viper-snapshot type: no-type author:

  • id: k-url type: no-type author:

  • id: evm-repo type: no-type author:

  • id: verified-smart-contracts type: no-type author:

  • id: yellowpaper-bug-136 type: no-type author:

    • literal: KEVM Team issued:
    • year: '2017' title: Yellowpaper Issue 136 publisher: Link to issues removed for double blind review

  • id: yellowpaper-bug-160 type: no-type author:

    • literal: KEVM Team issued:
    • year: '2017' title: Yellowpaper Issue 160 publisher: Link to issues removed for double blind review

  • id: yellowpaper-bug-216 type: no-type author:

    • literal: KEVM Team issued:
    • year: '2017' title: Yellowpaper Issue 216 publisher: Link to issues removed for double blind review

  • id: ViperBugsReported type: no-type author:

  • id: semantics-based-verifiers type: paper-conference author:

    • family: Ştefănescu given: Andrei
    • family: Park given: Daejun
    • family: Yuwen given: Shijao
    • family: Li given: Yilong
    • family: Roşu given: Grigore issued:
    • year: '2016' title: Semantics-based program verifiers for all languages container-title: OOPSLA publisher: ACM page: '74-91' DOI: 10.1145/2983990.2984027

  • id: k-tutorial-url type: no-type author:

  • id: trailofbits-manticore type: no-type author:

  • id: rosu-2017-lmcs type: article-journal author:

    • family: Roşu given: Grigore issued:
    • year: '2017' title: Matching logic container-title: Logical Methods in Computer Science DOI: http://arxiv.org/abs/1705.06312

  • id: erc-20-url type: no-type author:

  • id: ethereum-tests-url type: no-type author:

  • id: viper-docs-url type: no-type author:

  • id: jellopaper type: no-type author:

    • literal: KEVM Team issued:
    • year: '2017' title: The evm semantic “jello paper" publisher: https://jellopaper.org/

  • id: securify type: no-type author:

    • literal: Software Reliability Lab, ETH Zurich issued:
    • year: '2017' title: Securify formal verification of ethereum smart contracts note: https://securify.ch/

  • id: hildenbrandt-saxena-zhu-rodrigues-daian-guth-moore-zhang-park-rosu-2018-csf type: paper-conference author:

    • family: Hildenbrandt given: Everett
    • family: Saxena given: Manasvi
    • family: Zhu given: Xiaoran
    • family: Rodrigues given: Nishant
    • family: Daian given: Philip
    • family: Guth given: Dwight
    • family: Moore given: Brandon
    • family: Zhang given: Yi
    • family: Park given: Daejun
    • family: Ştefănescu given: Andrei
    • family: Roşu given: Grigore issued:
    • year: '2018' title: 'KEVM: A complete semantics of the ethereum virtual machine' title-short: KEVM container-title: Computer security foundations symposium abstract: 'A developing field of interest for the distributed systems and applied cryptography communities is that of smart contracts: self-executing financial instruments that synchronize their state, often through a blockchain. One such smart contract system that has seen widespread practical adoption is Ethereum, which has grown to a market capacity of 100 billion USD and clears an excess of 500,000 daily transactions.Unfortunately, the rise of these technologies has been marred by a series of costly bugs and exploits. Increasingly, the Ethereum community has turned to formal methods and rigorous program analysis tools. This trend holds great promise due to the relative simplicity of smart contracts and bounded-time deterministic execution inherent to the Ethereum Virtual Machine (EVM).Here we present KEVM, an executable formal specification of the EVM’s bytecode stack-based language built with the Framework, designed to serve as a solid foundation for further formal analyses. We empirically evaluate the correctness and performance of KEVM using the official Ethereum test suite [@ethereum-tests-url]ethereum-tests-url. To demonstrate the usability, several extensions of the semantics are presented and two different-language implementations of the ERC20 Standard Token are verified against the ERC20 specification. These results are encouraging for the executable semantics approach to language prototyping and specification.'