LIPIcs.FSCD.2018.2.pdf
- Filesize: 393 kB
- 6 pages
Document
Formal Design, Implementation and Verification of Blockchain Languages (Invited Talk)
Author
-
Part of:
Volume:
3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Formal Structures for Computation and Deduction (FSCD) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2018-07-04
Cite As Get BibTex
Grigore Rosu. Formal Design, Implementation and Verification of Blockchain Languages (Invited Talk). In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 2:1-2:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.FSCD.2018.2
Abstract
This invited paper describes recent, ongoing and planned work on the use of the rewrite-based semantic framework K to formally design, implement and verify blockchain languages and virtual machines. Both academic and commercial endeavors are discussed, as well as thoughts and directions for future research and development.
Subject Classification
ACM Subject Classification
- Security and privacy → Logic and verification
- Software and its engineering → Software verification
- Theory of computation → Logic and verification
Keywords
- Formal semantics
- Program verification
- Blockchain
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli. A survey of attacks on Ethereum smart contracts. IACR Cryptology ePrint Archive, 2016:1007, 2016.
-
Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In Formal Methods for Components and Objects (FMCO'05), volume 4111 of LNCS, pages 364-387, 2006.
- Lorenz Breidenbach, Phil Daian, Ari Juels, and Emin Gün Sirer. An in-depth look at the parity multisig bug, 2017. URL: http://hackingdistributed.com/2017/07/22/deep-dive-parity-bug/.
- Vitalik Buterin. Thinking about smart contract security, 2016. URL: https://blog.ethereum.org/2016/06/19/thinking-smart-contract-security/.
-
Andrei Ştefănescu, Daejun Park, Shijiao Yuwen, Yilong Li, and Grigore Roşu. Semantics-based program verifiers for all languages. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'16). ACM, Nov 2016.
- Phil Daian. DAO attack, 2016. URL: http://hackingdistributed.com/2016/06/18/analysis-of-the-dao-exploit/.
- Etherscan. Ethereum transactions, 2018. URL: https://etherscan.io/.
-
Jean-Christophe Filliâtre and Claude Marché. The why/krakatoa/caduceus platform for deductive program verification. In CAV, volume 4590 of LNCS, pages 173-177, 2007.
- Everett Hildenbrandt, Manasvi Saxena, Xiaoran Zhu, Nishant Rodrigues, Philip Daian, Dwight Guth, Brandon Moore, Yi Zhang, Daejun Park, Andrei Ştefănescu, and Grigore Roşu. KEVM: A Complete Semantics of the Ethereum Virtual Machine. In Computer Security Foundations Symposium (CSF'18), 2018. URL: http://jellopaper.org.
- The Coq development team. The Coq proof assistant reference manual. LogiCal Project, 2004. Version 8.0. URL: http://coq.inria.fr.
-
Grigore Roşu and Traian Florin Şerbănuţă. An overview of the K semantic framework. Journal of Logic and Algebraic Programming, 79(6):397-434, 2010.
- Jutta Steiner. Security is a process: A postmortem on the parity multi-sig library self-destruct, 2017. URL: https://blog.ethcore.io/security-is-a-process-a-postmortem-on-the-parity-multi-sig-library-self-destruct/.
- The Isabelle development team. Isabelle, 2018. URL: https://isabelle.in.tum.de/.
- Gavin Wood. Ethereum: A secure decentralised generalised transaction ledger, 2014. (Updated for EIP-150 in 2017) URL: http://yellowpaper.io/.