skip to main content
10.1145/2993600.2993611acmconferencesArticle/Chapter ViewAbstractPublication PagespldiConference Proceedingsconference-collections
short-paper
Open access

Formal Verification of Smart Contracts: Short Paper

Published: 24 October 2016 Publication History

Abstract

Ethereum is a framework for cryptocurrencies which uses blockchain technology to provide an open global computing platform, called the Ethereum Virtual Machine (EVM). EVM executes bytecode on a simple stack machine. Programmers do not usually write EVM code; instead, they can program in a JavaScript-like language, called Solidity, that compiles to bytecode. Since the main purpose of EVM is to execute smart contracts that manage and transfer digital assets (called Ether), security is of paramount importance. However, writing secure smart contracts can be extremely difficult: due to the openness of Ethereum, both programs and pseudonymous users can call into the public methods of other programs, leading to potentially dangerous compositions of trusted and untrusted code. This risk was recently illustrated by an attack on TheDAO contract that exploited subtle details of the EVM semantics to transfer roughly $50M worth of Ether into the control of an attacker.
In this paper, we outline a framework to analyze and verify both the runtime safety and the functional correctness of Ethereum contracts by translation to F*, a functional programming language aimed at program verification.

References

[1]
G. Barthe, C. Fournet, B. Grégoire, P.-Y. Strub, N. Swamy, and S. Zanella-Béguelin. Probabilistic relational verification for cryptographic implementations. In ph41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pages 193--205. ACM, 2014.
[2]
V. Buterin. Critical update re: Dao vulnerability. https://blog.ethereum.org/2016/06/17/critical-update-re-dao-vulnerability, 2016.
[3]
Ethereum. Solidity documentation -- Release 0.2.0. http://solidity.readthedocs.io/, 2016.
[4]
Ethereum. Solidity-browser. https://ethereum.github.io/browser-solidity, 2016.
[5]
J.-C. Filliâtre and A. Paskevich. Why3 -- where programs meet provers. In 22nd European Symposium on Programming, ESOP '13, volume 7792 of phLecture Notes in Computer Science, pages 125--128. Springer, 2013.
[6]
L. Luu, D.-H. Chu, H. Olickel, P. Saxena, and A. Hobor. Making smart contracts smarter. Cryptology ePrint Archive, Report 2016/633, 2016. http://eprint.iacr.org/2016/633.
[7]
S. Nakamoto. Bitcoin: A peer-to-peer electronic cash system. http://bitcoin.org/bitcoin.pdf.
[8]
N. Swamy, C. Fournet, A. Rastogi, K. Bhargavan, J. Chen, P. Strub, and G. M. Bierman. Gradual typing embedded securely in javascript. In POPL '14, pages 425--438. ACM, 2014.
[9]
N. Swamy, C. Hritcu, C. Keller, A. Rastogi, A. Delignat-Lavaud, S. Forest, K. Bhargavan, C. Fournet, P.-Y. Strub, M. Kohlweiss, J.-K. Zinzindohoué, and S. Zanella-Béguelin. Dependent types and multi-monadic effects in F*. In ph43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '16, pages 256--270. ACM, 2016.
[10]
G. Wood. Ethereum: A secure decentralised generalised transaction ledger. http://gavwood.com/paper.pdf.

Cited By

View all
  • (2025)RTMS: A Smart Contract Vulnerability Detection Method Based on Feature Fusion and Vulnerability CorrelationsElectronics10.3390/electronics1404076814:4(768)Online publication date: 16-Feb-2025
  • (2025)Deep Learning-Based Vulnerability Detection Solutions in Smart Contracts: A Comparative and Meta-Analysis of Existing ApproachesIEEE Access10.1109/ACCESS.2025.353232613(28894-28919)Online publication date: 2025
  • (2025)Deductive Verification of Solidity Smart Contracts with SSCalcScience of Computer Programming10.1016/j.scico.2025.103267(103267)Online publication date: Jan-2025
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
PLAS '16: Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security
October 2016
116 pages
ISBN:9781450345743
DOI:10.1145/2993600
© 2016 Association for Computing Machinery. ACM acknowledges that this contribution was authored or co-authored by an employee, contractor or affiliate of a national government. As such, the Government retains a nonexclusive, royalty-free right to publish or reproduce this article, or to allow others to do so, for Government purposes only.

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 24 October 2016

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. EVM
  2. ethereum
  3. formal verification
  4. smart contracts
  5. solidity

Qualifiers

  • Short-paper

Conference

CCS'16
Sponsor:

Acceptance Rates

PLAS '16 Paper Acceptance Rate 6 of 11 submissions, 55%;
Overall Acceptance Rate 43 of 77 submissions, 56%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)1,148
  • Downloads (Last 6 weeks)117
Reflects downloads up to 20 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2025)RTMS: A Smart Contract Vulnerability Detection Method Based on Feature Fusion and Vulnerability CorrelationsElectronics10.3390/electronics1404076814:4(768)Online publication date: 16-Feb-2025
  • (2025)Deep Learning-Based Vulnerability Detection Solutions in Smart Contracts: A Comparative and Meta-Analysis of Existing ApproachesIEEE Access10.1109/ACCESS.2025.353232613(28894-28919)Online publication date: 2025
  • (2025)Deductive Verification of Solidity Smart Contracts with SSCalcScience of Computer Programming10.1016/j.scico.2025.103267(103267)Online publication date: Jan-2025
  • (2025)A Comprehensive Survey of Smart Contracts Vulnerability Detection Tools: Techniques and MethodologiesJournal of Network and Computer Applications10.1016/j.jnca.2025.104142237(104142)Online publication date: May-2025
  • (2025)Smart contract anomaly detection: The Contrastive Learning ParadigmComputer Networks10.1016/j.comnet.2025.111121260(111121)Online publication date: Apr-2025
  • (2025)CSAFuzzer: Fuzzing smart contracts combining with static analysisEmpirical Software Engineering10.1007/s10664-025-10623-330:3Online publication date: 10-Feb-2025
  • (2024)Advanced Security Auditing Methods for Solidity-Based Smart ContractsElectronics10.3390/electronics1320409313:20(4093)Online publication date: 17-Oct-2024
  • (2024)Access Control Verification in Smart Contracts Using Colored Petri NetsComputers10.3390/computers1311027413:11(274)Online publication date: 22-Oct-2024
  • (2024)Smart contract life-cycle management: an engineering framework for the generation of robust and verifiable smart contractsFrontiers in Blockchain10.3389/fbloc.2023.12762336Online publication date: 8-Jan-2024
  • (2024)Portable Blockchain for System Testing of Solana Smart ContractsProceedings of the 2024 7th International Conference on Blockchain Technology and Applications10.1145/3708622.3708633(49-54)Online publication date: 6-Dec-2024
  • Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media