VeriSolid: Correct-by-Design Smart Contracts for Ethereum

Anastasia Mavridou, Aron Laszka, Emmanouela Stachtiari, Abhishek Dubey

Research output: Chapter in Book/Report/Conference proceedingConference contribution

72 Scopus citations

Abstract

The adoption of blockchain based distributed ledgers is growing fast due to their ability to provide reliability, integrity, and auditability without trusted entities. One of the key capabilities of these emerging platforms is the ability to create self-enforcing smart contracts. However, the development of smart contracts has proven to be error-prone in practice, and as a result, contracts deployed on public platforms are often riddled with security vulnerabilities. This issue is exacerbated by the design of these platforms, which forbids updating contract code and rolling back malicious transactions. In light of this, it is crucial to ensure that a smart contract is secure before deploying it and trusting it with significant amounts of cryptocurrency. To this end, we introduce the VeriSolid framework for the formal verification of contracts that are specified using a transition-system based model with rigorous operational semantics. Our model-based approach allows developers to reason about and verify contract behavior at a high level of abstraction. VeriSolid allows the generation of Solidity code from the verified models, which enables the correct-by-design development of smart contracts.

Original languageEnglish (US)
Title of host publicationFinancial Cryptography and Data Security - 23rd International Conference, FC 2019, Revised Selected Papers
EditorsIan Goldberg, Tyler Moore
PublisherSpringer
Pages446-465
Number of pages20
ISBN (Print)9783030321000
DOIs
StatePublished - 2019
Event23rd International Conference on Financial Cryptography and Data Security, FC 2019 - St. Kitts, Saint Kitts and Nevis
Duration: Feb 18 2019Feb 22 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11598 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference23rd International Conference on Financial Cryptography and Data Security, FC 2019
Country/TerritorySaint Kitts and Nevis
CitySt. Kitts
Period2/18/192/22/19

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'VeriSolid: Correct-by-Design Smart Contracts for Ethereum'. Together they form a unique fingerprint.

Cite this