TY - GEN
T1 - Formal design, implementation and verification of blockchain languages
AU - Rosu, Grigore
N1 - Funding Information:
NSF CCF-1421575; NSF SBIR-II-1660186; IOHK grant; Ethereum Foundation grant.
Funding Information:
To enable the formal verification of smart contracts, in a project partially funded by the research and engineering company IOHK (http://iohk.io, the creators of the Cardano blockchain and the ADA cryptocurrency), we have formalized the semantics of the EVM [9]. Our K semantics of the EVM, which we refer to as KEVM, is as complete as it can be. We know this because we tested it by running the automatically generated interpreter (see Figure 1) against the comprehensive 40,000-program test suite that comes with the official C++ implementation of the EVM, which serves as a conformance suite for EVM implementations. Building upon KEVM, the startup Runtime Verification has formally verified several smart contracts as part of their commercial verification services (https: //runtimeverification.com/smartcontract/).
Publisher Copyright:
© Grigore Rosu; licensed under Creative Commons License CC-BY.
PY - 2018/7/1
Y1 - 2018/7/1
N2 - 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.
AB - 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.
KW - Blockchain
KW - Formal semantics
KW - Program verification
UR - http://www.scopus.com/inward/record.url?scp=85049810338&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85049810338&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.FSCD.2018.2
DO - 10.4230/LIPIcs.FSCD.2018.2
M3 - Conference contribution
AN - SCOPUS:85049810338
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018
A2 - Kirchner, Helene
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018
Y2 - 9 July 2018 through 12 July 2018
ER -