research-article

Securify: Practical Security Analysis of Smart Contracts

Authors:

Dana Drachsler-Cohen,

Arthur Gervais,

Florian Bünzli,

Martin VechevAuthors Info & Claims

CCS '18: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security

Pages 67 - 82

https://doi.org/10.1145/3243734.3243780

Published: 15 October 2018 Publication History

Abstract

Permissionless blockchains allow the execution of arbitrary programs (called smart contracts), enabling mutually untrusted entities to interact without relying on trusted third parties. Despite their potential, repeated security concerns have shaken the trust in handling billions of USD by smart contracts. To address this problem, we present Securify, a security analyzer for Ethereum smart contracts that is scalable, fully automated, and able to prove contract behaviors as safe/unsafe with respect to a given property. Securify's analysis consists of two steps. First, it symbolically analyzes the contract's dependency graph to extract precise semantic information from the code. Then, it checks compliance and violation patterns that capture sufficient conditions for proving if a property holds or not. To enable extensibility, all patterns are specified in a designated domain-specific language. Securify is publicly released, it has analyzed >18K contracts submitted by its users, and is regularly used to conduct security audits by experts. We present an extensive evaluation of Securify over real-world Ethereum smart contracts and demonstrate that it can effectively prove the correctness of smart contracts and discover critical violations.

Supplementary Material

MP4 File (p67-tsankov.mp4)

Download
432.28 MB

References

[1]

2016. The DAO Attacked: Code Issue Leads to 60 Million Ether Theft. (2016).

[2]

2016. Etherdice. (2016). Available from: https://etherdice.io/.

[3]

2016. King of Ether. (2016). Available from: https://github.com/kieranelby/ KingOfTheEtherThrone/blob/v0.4.0/contracts/KingOfTheEtherThrone.sol.

[4]

2016. King of Ether, Postmortem. (2016). Available from: https://www. kingoftheether.com/postmortem.html.

[5]

2016. Reentrancy Woes in Smart Contracts. (2016). Available from: http: //hackingdistributed.com/2016/07/13/reentrancy-woes/.

[6]

2016. theDAO. (2016). Available from: https://etherscan.io/address/ 0xbb9bc244d798123fde783fcc1c72d3bb8c189413.

[7]

2017. Accidental bug may have frozen $280 million worth of digital coin ether in a cryptocurrency wallet. (2017). Available from: https://www.cnbc.com/2017/11/ 08/accidental-bug-may-have-frozen...

[8]

2017. Blockchain is empowering the future of insurance. (2017). Available from: https://techcrunch.com/2016/10/29/ blockchain-is-empowering-the-future-of-insurance/.

[9]

2017. ETHLance. (2017). Available from: http://ethlance.com/.

[10]

2017. An In-Depth Look at the Parity Multisig Bug. (2017). Available from: http://hackxingdistributed.com/2017/07/22/deep-dive-parity-bug.

[11]

2017. Northern Trust uses blockchain for private equity recordkeeping. (2017). Available from: http://www.reuters.com/article/ nthern-trust-ibm-blockchain-idUSL1N1G61TX.

[12]

2017. Parity Ethereum Client. (2017). Available from: https://github.com/ paritytech/parity.

[13]

2017. Security Alert. (2017). Available from: https://paritytech.io/blog/ security-alert.html.

[14]

2017. Submarine Sends: IC3's Plan to Clamp Down on ICO Cheats. (2017). Available from: https://www.coindesk.com/ submarine-sends-inside-ic3s-plan-to-clamp-...

[15]

2018. Ethereum Smart Contract Security Best Practices. (2018). Available from: https://consensys.github.io/smart-contract-best-practices/.

[16]

2018. Mythril. (2018). Available from: https://github.com/ConsenSys/mythril.

[17]

2018. Parity Wallet Library. (2018). Available from: https://github.com/ paritytech/parity/blob/4d08e7b0aec46443bf26547b17d10cb302672835/js/src/ contracts/snippets/enhanced-wallet.sol.

[18]

2018. Solidity, high-level language for writing smart contracts. (2018). Available from: https://solidity.readthedocs.io/en/develop/.

[19]

Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli. 2017. A Survey of Attacks on Ethereum Smart Contracts (SoK). In Principles of Security and Trust - 6th International Conference, POST. 164--186.

Digital Library

[20]

Massimo Bartoletti, Salvatore Carta, Tiziana Cimoli, and Roberto Saia. 2017. Dissecting Ponzi schemes on Ethereum: identification, analysis, and impact. CoRR abs/1703.03779 (2017).

[21]

Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Anitha Gollamudi, Georges Gonthier, Nadim Kobeissi, Natalia Kulatova, Aseem Rastogi, Thomas Sibut-Pinote, Nikhil Swamy, and Santiago Zanella-Béguelin. 2016. Formal Verification of Smart Contracts: Short Paper. In Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security (PLAS). 91--96.

Digital Library

[22]

Giancarlo Bigi, Andrea Bracciali, Giovanni Meacci, and Emilio Tuosto. 2015. Validation of Decentralised Smart Contracts Through Game Theory and Formal Methods. In Programming Languages with Applications to Biology and Security. 142--161.

[23]

Martin Bravenboer and Yannis Smaragdakis. 2009. Strictly Declarative Specification of Sophisticated Points-to Analyses. In Proceedings of the 24th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA). 243--262.

Digital Library

[24]

Vitalik Buterin. 2013. Ethereum: a next generation smart contract and decentralized application platform. (2013). Available from: https://github.com/ethereum/ wiki/wiki/White-Paper.

[25]

Vitalik Buterin. 2016. Thinking About Smart Contract Security. (2016). Available from: https://blog.ethereum.org/2016/06/19/thinking-smart-contract-security/.

[26]

Pawel Bylica. 2017. How to Find $10M Just by Reading the Blockchain. (Apr 2017). Available from: https://blog.golemproject.net/ how-to-find-10m-by-just-reading-blockchain-6ae9d39fcd95.

[27]

Ting Chen, Xiaoqi Li, Xiapu Luo, and Xiaosong Zhang. 2017. Under-optimized smart contracts devour your money. In Software Analysis, Evolution and Reengineering (SANER). 442--446.

[28]

Kevin Delmolino, Mitchell Arnett, Ahmed Kosba, Andrew Miller, and Elaine Shi. 2016. Step by Step Towards Creating a Safe Smart Contract: Lessons and Insights from a Cryptocurrency Lab. In Financial Cryptography and Data Security (FC). 79--94.

[29]

Yoshihiko Futamura. 1999. Partial Evaluation of Computation Process - An Approach to a Compiler-Compiler. Higher-Order and Symbolic Computation 12, 4 (1999), 381--391.

Digital Library

[30]

Ilya Grishchenko, Matteo Maffei, and Clara Schneidewind. 2018. A Semantic Framework for the Security Analysis of Ethereum Smart Contracts. In Principles of Security and Trust - 7th International Conference (POST). 243--269.

[31]

Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar. 2018. Online detection of effectively callback free objects with applications to smart contracts. PACMPL 2, POPL (2018), 48:1--48:28.

Digital Library

[32]

Everett Hildenbrandt, Manasvi Saxena, Nishant Rodrigues, Xiaoran Zhu, Philip Daian, Dwight Guth, Brandon M. Moore, Daejun Park, Yi Zhang, Andrei Stefanescu, and Grigore Rosu. 2018. KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine. In 31st IEEE Computer Security Foundations Symposium (CSF). 204--217.

[33]

Yoichi Hirai. 2016. Formal verification of Deed contract in Ethereum name service. Technical Report. Available from: https://yoichihirai.com/deed.pdf.

[34]

Yoichi Hirai. 2017. Defining the Ethereum Virtual Machine for Interactive Theorem Provers. In Financial Cryptography and Data Security (FC). 520--535.

[35]

Andrew Johnson, LucasWaye, Scott Moore, and Stephen Chong. 2015. Exploring and Enforcing Security Guarantees via Program Dependence Graphs. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 291--302.

Digital Library

[36]

Herbert Jordan, Bernhard Scholz, and Pavle Subotic. 2016. Soufflé: On Synthesis of Program Analyzers. In Computer Aided Verification - 28th International Conference (CAV). 422--430.

[37]

Sukrit Kalra, Seep Goel, Mohan Dhawan, and Subodh Sharma. 2018. ZEUS: Analyzing Safety of Smart Contracts. In 25th Annual Network and Distributed System Security Symposium (NDSS).

[38]

Ahmed E. Kosba, Andrew Miller, Elaine Shi, Zikai Wen, and Charalampos Papamanthou. 2016. Hawk: The Blockchain Model of Cryptography and Privacy- Preserving Smart Contracts. In IEEE Symposium on Security and Privacy (SP). 839--858.

[39]

Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor. 2016. Making Smart Contracts Smarter. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (CCS). 254--269.

Digital Library

[40]

Magnus Madsen, Ming-Ho Yee, and Ondrej Lhoták. 2016. From Datalog to flix: a declarative language for fixed points on lattices. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 194--208.

Digital Library

[41]

Ravi Mangal, Xin Zhang, Aditya V. Nori, and Mayur Naik. 2015. A user-guided approach to program analysis. In Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering (ESEC/FSE). 462--473.

Digital Library

[42]

Michael C. Martin, V. Benjamin Livshits, and Monica S. Lam. 2005. Finding application errors and security flaws using PQL: a program query language. In Proceedings of the 20th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA). 365--383.

Digital Library

[43]

Satoshi Nakamoto. 2008. Bitcoin: A peer-to-peer electronic cash system. (2008).

[44]

Ivica Nikolic, Aashish Kolluri, Ilya Sergey, Prateek Saxena, and Aquinas Hobor. 2018. Finding The Greedy, Prodigal, and Suicidal Contracts at Scale. CoRR abs/1802.06038 (2018).

[45]

Todd A. Proebsting and Scott A.Watterson. 1997. Krakatoa: Decompilation in Java (Does Bytecode Reveal Source?). In Third USENIX Conference on Object-Oriented Technologies and Systems (COOTS). 185--198.

Digital Library

[46]

Grigore Roşu and Traian Florin Şerbănută. 2010. An Overview of the K Semantic Framework. Journal of Logic and Algebraic Programming 79, 6 (2010), 397--434.

[47]

Pablo Lamela Seijas, Simon Thompson, and Darryl McAdams. 2016. Scripting smart contracts for distributed ledger technology. IACR Cryptology ePrint Archive 2016 (2016).

[48]

Gagandeep Singh, Markus Püschel, and Martin Vechev. 2017. Fast Polyhedra Abstract Domain. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). 46--59.

Digital Library

[49]

Yannis Smaragdakis and Martin Bravenboer. 2010. Using Datalog for Fast and Easy Program Analysis. In Datalog Reloaded - First International Workshop, Datalog. 245--251.

Digital Library

[50]

Jeffrey D. Ullman. 1988. Principles of Database and Knowledge-base Systems, Vol. I. Principles of computer science series, Vol. 14.

Digital Library

[51]

Raja Vallee-Rai and Laurie J. Hendren. 1998. Jimple: Simplifying Java Bytecode for Analyses and Transformations. (1998).

[52]

Gavin Wood. 2014. Ethereum: A secure decentralised generalised transaction ledger. Ethereum Project Yellow Paper (2014).

[53]

Xin Zhang, Ravi Mangal, Radu Grigore, Mayur Naik, and Hongseok Yang. 2014. On abstraction refinement for program analyses in Datalog. In ACM SIGPLAN Conference on Programming Language Design and Implementation, (PLDI). 239-- 248.

Digital Library

Cited By

Park JChoi J(2025)Towards Effective Guidance of Smart Contract Fuzz Testing Based on Static AnalysisElectronics10.3390/electronics1404080614:4(806)Online publication date: 19-Feb-2025
https://doi.org/10.3390/electronics14040806
Wang ZChen JZheng PZhang YZhang WZheng Z(2025)Unity is Strength: Enhancing Precision in Reentrancy Vulnerability Detection of Smart Contract Analysis ToolsIEEE Transactions on Software Engineering10.1109/TSE.2024.342732151:1(1-13)Online publication date: Jan-2025
https://doi.org/10.1109/TSE.2024.3427321
Lian WBao ZZhang XJia BZhang Y(2025)A Universal and Efficient Multi-Modal Smart Contract Vulnerability Detection Framework for Big DataIEEE Transactions on Big Data10.1109/TBDATA.2024.340337611:1(190-207)Online publication date: Feb-2025
https://doi.org/10.1109/TBDATA.2024.3403376
Show More Cited By

Index Terms

Securify: Practical Security Analysis of Smart Contracts
1. Security and privacy
  1. Formal methods and theory of security
    1. Logic and verification
  2. Software and application security

Recommendations

Security Analysis of Smart Contracts in Datalog
Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice
Abstract
Smart contracts enable mutually untrusted entities to interact without relying on trusted third parties. Despite their potential, repeated security concerns have shaken the trust in handling billions of USD by smart contracts. To address this ...
Formal Modeling and Verification of Smart Contracts
ICSCA '18: Proceedings of the 2018 7th International Conference on Software and Computer Applications

Smart contracts can automatically perform the contract terms according to the received information, and it is one of the most important research fields in digital society. The core of smart contracts is algorithm contract, that is, the parties reach an ...
sVerify: Verifying Smart Contracts Through Lazy Annotation and Learning
Leveraging Applications of Formal Methods, Verification and Validation
Abstract
Smart contracts have recently attracted much attention from industry as they aim to assure anonymous distributed secure transactions. It also becomes clear that they are not immune to code vulnerabilities. As smart contracts cannot be patched once ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CCS '18: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security

October 2018

2359 pages

ISBN:9781450356930

DOI:10.1145/3243734

General Chairs:
David Lie
University of Toronto
,
Mohammad Mannan
Concordia University
,
Program Chairs:
Michael Backes
CISPA Helmholtz Center i.G.
,
XiaoFeng Wang
Indiana University

Copyright © 2018 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGSAC: ACM Special Interest Group on Security, Audit, and Control

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 15 October 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

ERC Starting Grant

Conference

CCS '18

Sponsor:

SIGSAC

CCS '18: 2018 ACM SIGSAC Conference on Computer and Communications Security

October 15 - 19, 2018

Toronto, Canada

Acceptance Rates

CCS '18 Paper Acceptance Rate 134 of 809 submissions, 17%;

Overall Acceptance Rate 1,261 of 6,999 submissions, 18%

Upcoming Conference

CCS '25

Sponsor:
sigsac

ACM SIGSAC Conference on Computer and Communications Security

October 13 - 17, 2025

Taipei , Taiwan

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

655
Total Citations
View Citations
4,486
Total Downloads

Downloads (Last 12 months)503
Downloads (Last 6 weeks)45

Reflects downloads up to 23 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Park JChoi J(2025)Towards Effective Guidance of Smart Contract Fuzz Testing Based on Static AnalysisElectronics10.3390/electronics1404080614:4(806)Online publication date: 19-Feb-2025
https://doi.org/10.3390/electronics14040806
Wang ZChen JZheng PZhang YZhang WZheng Z(2025)Unity is Strength: Enhancing Precision in Reentrancy Vulnerability Detection of Smart Contract Analysis ToolsIEEE Transactions on Software Engineering10.1109/TSE.2024.342732151:1(1-13)Online publication date: Jan-2025
https://doi.org/10.1109/TSE.2024.3427321
Lian WBao ZZhang XJia BZhang Y(2025)A Universal and Efficient Multi-Modal Smart Contract Vulnerability Detection Framework for Big DataIEEE Transactions on Big Data10.1109/TBDATA.2024.340337611:1(190-207)Online publication date: Feb-2025
https://doi.org/10.1109/TBDATA.2024.3403376
Bresil MPrasad PSayeed MBukar U(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
https://doi.org/10.1109/ACCESS.2025.3532326
Osei SHuang RMa Z(2025)An Attention-based Wide and Deep Neural Network for Reentrancy Vulnerability Detection in Smart ContractsJournal of Systems and Software10.1016/j.jss.2025.112361223(112361)Online publication date: May-2025
https://doi.org/10.1016/j.jss.2025.112361
Hejazi NLashkari A(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
https://doi.org/10.1016/j.jnca.2025.104142
Ding HLiu YPiao XSong HJi Z(2025)SmartGuard: An LLM-enhanced framework for smart contract vulnerability detectionExpert Systems with Applications10.1016/j.eswa.2025.126479269(126479)Online publication date: Apr-2025
https://doi.org/10.1016/j.eswa.2025.126479
Xu SHe HMihaljević MZhang SShao WWang Q(2025)DBC-MulBiLSTM: A DistilBERT-CNN Feature Fusion Framework enhanced by multi-head self-attention and BiLSTM for smart contract vulnerability detectionComputers and Electrical Engineering10.1016/j.compeleceng.2025.110096123(110096)Online publication date: Apr-2025
https://doi.org/10.1016/j.compeleceng.2025.110096
Fadi OBahaj AZkik KEl Ghazi AGhogho MBoulmalf M(2025)Smart contract anomaly detection: The Contrastive Learning ParadigmComputer Networks10.1016/j.comnet.2025.111121260(111121)Online publication date: Apr-2025
https://doi.org/10.1016/j.comnet.2025.111121
Li PWang GXing XZhu JGu WZhang Y(2025)EAOS: Exposing attacks in smart contracts through analyzing opcode sequences with operandsComputer Networks10.1016/j.comnet.2024.110959257(110959)Online publication date: Feb-2025
https://doi.org/10.1016/j.comnet.2024.110959
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten