AI helps you reading Science

AI generates interpretation videos

AI extracts and analyses the key points of the paper to generate videos automatically


pub
Go Generating

AI Traceability

AI parses the academic lineage of this thesis


Master Reading Tree
Generate MRT

AI Insight

AI extracts a summary of this paper


Weibo:
We devised compliance and violation patterns that can effectively prove whether real-world contracts are safe/unsafe with respect to relevant properties

Securify: Practical Security Analysis of Smart Contracts.

ACM Conference on Computer and Communications Security, (2018): 67-82

Cited by: 411|Views494
EI

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 pres...More

Code:

Data:

Introduction
  • Blockchain platforms, such as Nakamoto’s Bitcoin [43], enable the trade of crypto-currencies between mutually mistrusting parties.
  • To eliminate the need for trust, Nakomoto designed a peer-to-peer network that enables its peers to agree on the trading transactions.
  • Buterin [24] identified the applicability of decentralized computation beyond trading, and designed the Ethereum blockchain which supports the execution of programs, called smart contracts, written in Turing-complete languages.
Highlights
  • Blockchain platforms, such as Nakamoto’s Bitcoin [43], enable the trade of crypto-currencies between mutually mistrusting parties
  • To evaluate Securify, we conducted the following experiments: (i) evaluated Securify’s effectiveness in proving the correctness of and discovering violations in real-world contracts; manually inspected Securify’s results on smart contracts whose source code had been uploaded to Securify’s public interface; compared Securify to Oyente [39] and Mythril [16], two smart contract checkers based on symbolic execution; measured the success of Securify’s decompiler in resolving memory and storage offsets; (v) measured Securify’s time and memory consumption
  • Our first dataset, dubbed Ethereum Virtual Machine dataset, consists of 24, 594 smart contracts obtained by parsing create transactions using the parity client [12]
  • We presented Securify, a new lightweight and scalable verifier for Ethereum smart contracts
  • Securify leverages the domain-specific insight that violations of many practical properties for smart contracts violate simpler properties, which are significantly easier to check in a purely automated way
  • We devised compliance and violation patterns that can effectively prove whether real-world contracts are safe/unsafe with respect to relevant properties
Methods
  • In Programming Languages with Applications to Biology and Security.

    [23] Martin Bravenboer and Yannis Smaragdakis. 2009.
  • In Programming Languages with Applications to Biology and Security.
  • [23] Martin Bravenboer and Yannis Smaragdakis.
  • Declarative Specification of Sophisticated Points-to Analyses.
  • In Proceedings of the 24th Annual ACM.
  • SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and.
  • Ethereum: a generation smart contract and decentralized application platform.
  • Available from: https://github.com/ethereum/.
  • [25] Vitalik Buterin.
  • Thinking About Smart Contract Security.
  • Available from: https://blog.ethereum.org/2016/06/19/thinking-smart-contract-security/
Results
  • To evaluate Securify, the authors conducted the following experiments: (i) evaluated Securify’s effectiveness in proving the correctness of and discovering violations in real-world contracts; manually inspected Securify’s results on smart contracts whose source code had been uploaded to Securify’s public interface; compared Securify to Oyente [39] and Mythril [16], two smart contract checkers based on symbolic execution; measured the success of Securify’s decompiler in resolving memory and storage offsets; (v) measured Securify’s time and memory consumption.

    Datasets.
  • The authors' first dataset, dubbed EVM dataset, consists of 24, 594 smart contracts obtained by parsing create transactions using the parity client [12].
  • The authors obtained the EVM bytecode of these smart contracts.
  • The authors' second dataset, dubbed Solidity dataset, consists of 100 smart contracts written in Solidity which were uploaded to Securify’s public interface.
  • The authors restricted the selection to contracts with up to 200 lines of Solidity code
Conclusion
  • The authors presented Securify, a new lightweight and scalable verifier for Ethereum smart contracts.
  • Securify leverages the domain-specific insight that violations of many practical properties for smart contracts violate simpler properties, which are significantly easier to check in a purely automated way.
  • Based on this insight, the authors devised compliance and violation patterns that can effectively prove whether real-world contracts are safe/unsafe with respect to relevant properties.
  • Securify enjoys several important benefits: (i) it analyzes all contract behaviors to avoid undesirable false negatives; it reduces the user effort in classifying warnings into true positives and false alarms by guaranteeing that certain behaviors are actual errors; it supports a new domain-specific language that enables users to express new vulnerability patterns as they emerge; its analysis pipeline – from bytecode decompilation, optimizations, to checking of patterns – is fully automated using scalable, off-the-shelf Datalog solvers
Related work
  • We discuss some of the works that are most closely related to ours.

    Analysis of Smart Contracts. Smart contracts have been shown to be exposed to severe vulnerabilities [19, 25]. Hirai [33] was one of the firsts to formally verify smart contracts using the Isabelle proof assistant. In [34], Hirai defines a formal model for the Ethereum Virtual Machine using the Lem language. This model proves safety properties of smart contracts using existing interactive theorem provers. Formal semantics of the EVM have been defined by Grishchenko et al [30] using the F* framework and by Hildenbrandt et al [32] using the K framework [46]. These semantics are executable and were validated against the official Ethereum test suite. Further, they enable the formal specification and verification of properties. The main benefit of these frameworks is that they provide strong formal verification guarantees and are precise (no false positives). They target arbitrary properties, but are, unfortunately, nontrivial to fully automate. In contrast, Securify targets properties that can be proved/disproved by checking simpler properties that can be verified in a fully automated way.
Funding
  • The research leading to these results was partially supported by an ERC Starting Grant 680358
Reference
  • 2016. The DAO Attacked: Code Issue Leads to 60 Million Ether Theft. (2016).
    Google ScholarFindings
  • 2016. Etherdice. (2016). Available from: https://etherdice.io/.
    Findings
  • 2016. King of Ether. (2016). Available from: https://github.com/kieranelby/
    Findings
  • 2016. King of Ether, Postmortem. (2016). Available from: https://www.
    Findings
  • 2016. Reentrancy Woes in Smart Contracts. (2016). Available from: http:
    Google ScholarFindings
  • 201theDAO. (2016). Available from: https://etherscan.io/address/
    Findings
  • 201Accidental bug may have frozen 280 million worth of digital coin ether in a cryptocurrency wallet. (2017). Available from: https://www.cnbc.com/2017/11/ Available from: https://techcrunch.com/2016/10/29/
    Findings
  • [9] 2017. ETHLance. (2017). Available from: http://ethlance.com/.
    Findings
  • [10] 2017. An In-Depth Look at the Parity Multisig Bug. (2017). Available from: http://hackxingdistributed.com/2017/07/22/deep-dive-parity-bug.
    Findings
  • [11] 2017. Northern Trust uses blockchain for private equity recordkeeping. (2017). Available from: http://www.reuters.com/article/
    Findings
  • [12] 2017. Parity Ethereum Client. (2017). Available from: https://github.com/
    Findings
  • [13] 2017. Security Alert. (2017). Available from: https://paritytech.io/blog/ Available from: https://www.coindesk.com/
    Findings
  • [15] 2018. Ethereum Smart Contract Security Best Practices. (2018). Available from: https://consensys.github.io/smart-contract-best-practices/.
    Findings
  • [16] 2018. Mythril. (2018). Available from: https://github.com/ConsenSys/mythril.
    Findings
  • [17] 2018. Parity Wallet Library. (2018). Available from: https://github.com/ Solidity, high-level language for writing smart contracts. (2018). Available from: https://solidity.readthedocs.io/en/develop/.
    Findings
  • [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
    Google ScholarLocate open access versionFindings
  • [20] Massimo Bartoletti, Salvatore Carta, Tiziana Cimoli, and Roberto Saia. 20CoRR abs/1703.03779 (2017).
    Findings
  • [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
    Google ScholarLocate open access versionFindings
  • [22] Giancarlo Bigi, Andrea Bracciali, Giovanni Meacci, and Emilio Tuosto. 2015.
    Google ScholarFindings
  • [23] Martin Bravenboer and Yannis Smaragdakis. 2009. Strictly Declarative Specification of Sophisticated Points-to Analyses. In Proceedings of the 24th Annual ACM
    Google ScholarLocate open access versionFindings
  • [24] Vitalik Buterin. 2013. Ethereum: a next generation smart contract and decentralized application platform. (2013). Available from: https://github.com/ethereum/
    Findings
  • [25] Vitalik Buterin. 2016. Thinking About Smart Contract Security. (2016). Available from: https://blog.ethereum.org/2016/06/19/thinking-smart-contract-security/.
    Findings
  • [26] Pawel Bylica. 2017. Blockchain. (Apr 2017). Available from: https://blog.golemproject.net/
    Findings
  • [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.
    Google ScholarLocate open access versionFindings
  • [28] Kevin Delmolino, Mitchell Arnett, Ahmed Kosba, Andrew Miller, and Elaine Shi.
    Google ScholarFindings
  • 2016. Step by Step Towards Creating a Safe Smart Contract: Lessons and Insights from a Cryptocurrency Lab. In Financial Cryptography and Data Security (FC).
    Google ScholarFindings
  • [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.
    Google ScholarLocate open access versionFindings
  • [30] Ilya Grishchenko, Matteo Maffei, and Clara Schneidewind. 2018. A Semantic
    Google ScholarFindings
  • [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
    Google ScholarFindings
  • (2018), 48:1–48:28.
    Google ScholarFindings
  • [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
    Google ScholarFindings
  • [33] Yoichi Hirai. 2016. Formal verification of Deed contract in Ethereum name service. Technical Report. Available from: https://yoichihirai.com/deed.pdf.
    Findings
  • [34] Yoichi Hirai. 2017. Defining the Ethereum Virtual Machine for Interactive Theorem Provers. In Financial Cryptography and Data Security (FC). 520–535.
    Google ScholarLocate open access versionFindings
  • [35] Andrew Johnson, Lucas Waye, 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
    Google ScholarFindings
  • [36] Herbert Jordan, Bernhard Scholz, and Pavle Subotic. 2016. Soufflé: On Synthesis of
    Google ScholarLocate open access versionFindings
  • [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).
    Google ScholarLocate open access versionFindings
  • [38] Ahmed E. Kosba, Andrew Miller, Elaine Shi, Zikai Wen, and Charalampos Papamanthou. 2016. Hawk: The Blockchain Model of Cryptography and PrivacyPreserving Smart Contracts. In IEEE Symposium on Security and Privacy (SP). 839–858.
    Google ScholarLocate open access versionFindings
  • [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.
    Google ScholarLocate open access versionFindings
  • [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.
    Google ScholarLocate open access versionFindings
  • [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.
    Google ScholarLocate open access versionFindings
  • [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.
    Google ScholarFindings
  • [43] Satoshi Nakamoto. 2008. Bitcoin: A peer-to-peer electronic cash system. (2008).
    Google ScholarFindings
  • [44] Ivica Nikolic, Aashish Kolluri, Ilya Sergey, Prateek Saxena, and Aquinas Hobor.
    Google ScholarLocate open access versionFindings
  • 2018. Finding The Greedy, Prodigal, and Suicidal Contracts at Scale. CoRR abs/1802.06038 (2018).
    Findings
  • 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.
    Google ScholarLocate open access versionFindings
  • Grigore Roşu and Traian Florin Şerbănuţă. 2010. An Overview of the K Semantic Framework. Journal of Logic and Algebraic Programming 79, 6 (2010), 397–434.
    Google ScholarLocate open access versionFindings
  • Pablo Lamela Seijas, Simon Thompson, and Darryl McAdams. 2016. Scripting smart contracts for distributed ledger technology. IACR Cryptology ePrint Archive 2016 (2016).
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Yannis Smaragdakis and Martin Bravenboer. 2010. Using Datalog for Fast and Easy Program Analysis. In Datalog Reloaded - First International Workshop, Datalog. 245–251.
    Google ScholarLocate open access versionFindings
  • Jeffrey D. Ullman. 1988. Principles of Database and Knowledge-base Systems, Vol. I. Principles of computer science series, Vol. 14.
    Google ScholarFindings
  • Raja Vallee-Rai and Laurie J. Hendren. 1998. Jimple: Simplifying Java Bytecode for Analyses and Transformations. (1998).
    Google ScholarFindings
  • Gavin Wood. 2014. Ethereum: A secure decentralised generalised transaction ledger. Ethereum Project Yellow Paper (2014).
    Google ScholarLocate open access versionFindings
Your rating :
0

 

Tags
Comments
数据免责声明
页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果,我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问,可以通过电子邮件方式联系我们:report@aminer.cn
小科