TY - GEN
T1 - VeriSolid
T2 - 23rd International Conference on Financial Cryptography and Data Security, FC 2019
AU - Mavridou, Anastasia
AU - Laszka, Aron
AU - Stachtiari, Emmanouela
AU - Dubey, Abhishek
N1 - Publisher Copyright:
© 2019, International Financial Cryptography Association.
PY - 2019
Y1 - 2019
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85068817163&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85068817163&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-32101-7_27
DO - 10.1007/978-3-030-32101-7_27
M3 - Conference contribution
AN - SCOPUS:85068817163
SN - 9783030321000
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 446
EP - 465
BT - Financial Cryptography and Data Security - 23rd International Conference, FC 2019, Revised Selected Papers
A2 - Goldberg, Ian
A2 - Moore, Tyler
PB - Springer
Y2 - 18 February 2019 through 22 February 2019
ER -