Smart contract vulnerabilities represent a critical security challenge in blockchain systems, with numerous high-profile exploits resulting in significant financial losses. Traditional approaches like code reviews and automated vulnerability detection have limitations. VeriSolid addresses this by enabling developers to specify contract behavior at a high level of abstraction and automatically generate correct implementations verified against formal properties.
This paper introduces VeriSolid, a framework for correct-by-design development of Ethereum smart contracts. The work combines model-driven development with formal verification to enable developers to specify smart contract behavior as transition systems and automatically generate verified Solidity code with formal guarantees.
The paper presents VeriSolid's design and verification workflow, supporting specification of safety, liveness, and deadlock-freedom properties. The framework is evaluated on multiple smart contract models including blind auction and resource allocation contracts, demonstrating automatic generation of correct Solidity code with formal guarantees against specified vulnerabilities.
@inproceedings{Mavridou2019,
author = {Mavridou, Anastasia and Laszka, Aron and Stachtiari, Emmanouela and Dubey, Abhishek},
booktitle = {Financial Cryptography and Data Security - 23rd International Conference, {FC} 2019, Frigate Bay, St. Kitts and Nevis, Revised Selected Papers},
title = {VeriSolid: Correct-by-Design Smart Contracts for Ethereum},
year = {2019},
pages = {446--465},
acceptance = {21.9},
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.},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/bib/conf/fc/MavridouLSD19},
category = {selectiveconference},
contribution = {colab},
doi = {10.1007/978-3-030-32101-7\_27},
file = {:Mavridou2019-VeriSolid_Correct_by_Design_Smart_Contracts_for_Ethereum.pdf:PDF},
keywords = {smart contracts, formal verification, Ethereum, blockchain, correct-by-design, model-driven development},
project = {cps-blockchains},
tag = {platform,decentralization},
timestamp = {Mon, 14 Oct 2019 14:51:20 +0200},
url = {https://doi.org/10.1007/978-3-030-32101-7\_27}
}