Securify: Practical Security Analysis of Smart Contracts
Petar Tsankov, Andrei Dan, Dana Drachsler Cohen, Arthur Gervais,, Florian Buenzli, Martin Vechev

TL;DR
Securify is a scalable, automated tool for analyzing Ethereum smart contracts' security, capable of proving safety or identifying violations through pattern-based analysis, aiding in trust and security in blockchain applications.
Contribution
It introduces Securify, a novel security analyzer that uses pattern-based analysis and a domain-specific language for extensibility, improving smart contract security assessments.
Findings
Analyzed over 18,000 contracts with Securify.
Effectively proved correctness and identified violations.
Used by security experts for audits.
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsBlockchain Technology Applications and Security · Advanced Malware Detection Techniques · Security and Verification in Computing
