Source-linked AI summary
Securify: Practical Security Analysis of Smart Contracts
Petar Tsankov, Andrei Dan, Dana Drachsler Cohen, Arthur Gervais, Florian Buenzli, Martin Vechev
TL;DR
Smart contracts require stronger security analysis because existing approaches can miss violations, produce false positives, and provide incomplete coverage. Securify symbolically analyzes contract dependency graphs and checks extensible compliance and violation patterns. The system can prove relevant behaviors safe or unsafe, has analyzed more than 18K contracts, and is used in commercial audits.
Problem
Existing smart-contract analyzers can miss critical violations, produce false positives, and fail to achieve sufficient code coverage on realistic contracts.
Method
Securify encodes contract dependency graphs in Datalog and checks compliance and violation patterns that provide sufficient conditions for proving properties or their negations.
Results
Securify can effectively prove the correctness of real-world contracts and discover violations, while reducing manually inspected warnings by 65.9% and up to 99.4% for some properties.
Takeaways & Limitations
Securify provides a lightweight, scalable, fully automated verifier that reports unsafe behaviors and supports extensible vulnerability patterns.
Takeaways & Limitations
Its generic properties may miss contract-specific vulnerabilities, and matching a compliance pattern does not guarantee that contract-specific requirements are correctly satisfied.
Abstract
from arXiv · showhide
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.
1 INTRODUCTION
Smart contracts enable trustless computation but remain difficult to secure because existing analyzers can miss violations, raise false positives, and provide limited coverage. Securify addresses these challenges with domain-specific compliance and violation patterns, automated semantic analysis, and extensive real-world use and evaluation.
- Smart-contract exploits have caused losses reaching millions of USD, including $150M from the DAO and $280M frozen in the Parity wallet.
- Key Challenges: Existing analyzers can miss critical violations, produce false positives, and achieve insufficient coverage, with Oyente reaching only 20.2% coverage on the Parity wallet.
- Securify: Domain-specific Verifier: Securify uses compliance patterns that imply a property holds and violation patterns that imply its negation, while unmatched behaviors become warnings.
- Securify symbolically analyzes contract dependency graphs, checks semantic facts with security patterns, and automates the analysis using scalable Datalog solvers and a pattern DSL.
- Reduced Manual Effort: 65.9% fewer warnings require manual inspection, reaching up to 99.4% for some properties, while Securify reports all unsafe behaviors.
- Auditing Smart Contracts: Securify has analyzed >18K user-submitted contracts and supported 38 detailed commercial smart-contract audits.
- Main Contributions: The paper contributes a dependency-graph decompiler, compliance and violation patterns, a fully automated implementation, and an evaluation showing effective correctness proofs and violation discovery.
2 MOTIVATING EXAMPLES
Securify illustrates two smart-contract vulnerabilities: unrestricted writes can let attackers seize funds, while library dependence can freeze deposited ether. It detects these issues by matching semantic dependency patterns against contract code.
- Stealing Ether: 30 million USD was stolen from Parity’s multi-signature wallet after an attacker exploited an initialization flaw.The wallet’s owner field could be written by any user, enabling the attacker to set their own address and withdraw all stored ether.
- Stealing Ether: The restricted-write property requires that not all users can make a transaction modifying a security-critical field such as owner.Securify proves violations by establishing that all users can reach a write, and satisfaction by showing that some user cannot modify the field.
- Stealing Ether: Securify detects the wallet flaw when the owner assignment does not depend on the caller instruction.Dependency analysis implies that any user can reach the assignment, matching the unrestricted-write violation pattern.
- Frozen Funds: ≈280 million USD was frozen when a wallet library was removed from the blockchain.The wallet depended on the library for ether withdrawal, so deleting the library prevented funds from being extracted.
- Frozen Funds: Securify identifies locked-funds risk when users can deposit ether and every ether-transfer call extracts zero ether.The conjunction of these facts implies that ether can enter the contract without a direct transfer path out.
3 THE SECURIFY SYSTEM
Securify analyzes contract bytecode by deriving semantic facts and checking extensible compliance and violation patterns. It reports violations, warnings, or compliance results, while remaining limited in numerical reasoning, reachability analysis, and property scope.
- Inputs: Securify accepts EVM bytecode and DSL-specified compliance and violation patterns as inputs.Solidity contracts can also be compiled to bytecode before analysis; the two pattern types provide sufficient conditions for satisfaction or violation.
- Analysis Pipeline: Securify decompiles EVM bytecode into stackless static-single-assignment form before analysis.It also identifies methods and partially evaluates memory and storage offsets and jump destinations.
- Analysis Pipeline: Securify infers data- and control-flow dependencies and other semantic facts using declarative stratified Datalog rules.The inference is fully automated and supports modular extension with additional facts and rules.
- Pattern Checking: Securify checks compliance and violation patterns written in a specialized DSL that security experts can extend with custom patterns.The DSL supports properties including restricted writes, exception handling, ether liquidity, and input validation.
- Pattern Checking: A restricted-write violation matches an sstore whose storage offset and stored value may not depend on the caller.For each violation match, Securify outputs the responsible instruction; unmatched compliance and violation patterns produce a warning.
- Limitations: Securify cannot currently reason about numerical properties such as overflows.The authors identify numerical analysis as planned future work.
- Limitations: Securify assumes all contract instructions are reachable and therefore does not reason about reachability.This assumption supports the formal correspondence between supported properties and the patterns used to prove or disprove them.
- Limitations: The supported properties often, but not always, capture violations exploitable by attackers.Security experts can address contract-specific needs by writing customized patterns in the DSL.
4 SEMANTIC FACTS
Securify represents contract instructions and control flow as Datalog facts, then derives semantic facts about execution dependencies through stratified rules. These facts capture flow and data-dependency relationships used later for security-property checking.
- Semantic-Fact Inference: Securify derives semantic facts automatically from the contract’s dependency graph and uses them as the basis for checking security properties.The analysis covers control- and data-flow dependencies and is introduced as a reusable inference process over EVM contracts.
- Stratified Datalog: Stratified Datalog supplies the declarative language for expressing facts and rules that infer additional contract semantics.Stratification ensures predicates used negatively are fully defined in lower strata, and models are computed through fixed points.
- Facts: Securify first extracts base facts describing contract instructions, labels, variables, constants, and control-flow relationships.Instruction facts encode operations and their arguments; Follow records consecutive instructions, while Join captures merged branches.
- Flow-Dependency Predicates: MayFollow and MustFollow summarize whether one instruction can follow another or must precede it across control-flow paths.MayFollow is inferred transitively from immediate Follow facts, while MustFollow requires attention to control-flow join points.
- Data-Dependency Predicates: Data-dependency predicates MayDepOn, Eq, and DetBy characterize relationships among instruction results, variables, constants, and tags.MayDepOn rules propagate dependencies through assignments, operations, and memory loads, including loads with constant or unknown offsets.
5 SECURITY PATTERNS
Securify expresses security properties as compliance and violation patterns over inferred semantic facts, using these patterns to prove properties, identify violations, and support custom auditing rules.
- Pattern Language: Securify defines a language for expressing patterns and interprets them over semantic facts derived from contracts.The language includes instruction predicates, dependency predicates, quantifiers, logical connectors, and shorthand forms.
- Pattern Semantics: Patterns are checked against a Datalog fixed-point, so a semantic fact holds exactly when it is contained in that fixed-point.Quantifiers and logical connectors are interpreted as usual, while flow- and data-dependency predicates use inferred facts.
- Security Properties: 35 security properties are approximated with compliance patterns implying satisfaction and violation patterns implying negation; unmatched cases produce warnings.The patterns do not precisely capture the properties, so neither pattern may match even when the property’s status is unknown.
- Security Properties: For no writes after calls, compliance checks that calls are not followed by storage writes, while violation checks for calls necessarily followed by writes.This property differs from reentrancy, which concerns re-entering the same function and reaching the call instruction.
- Security Properties: For restricted writes, compliance requires storage offsets to depend on the sender, while violation detects writes whose execution and offset are independent of the caller.The property can instead target critical writes, such as owner-field modifications, when unrestricted global writes are acceptable.
- Custom and Localized Patterns: Auditors can specify contract-specific patterns in Securify’s language, while instruction patterns localize violations and contract patterns flag whole-contract issues.Ether liquidity is given as an example of a contract pattern because its violation combines conditions involving stop and call instructions.
6 IMPLEMENTATION
Securify decompiles EVM bytecode, optimizes its control-flow representation, infers semantic facts with Datalog, and evaluates patterns to report vulnerabilities or warnings.
- Front End: Securify decompiles EVM bytecode into assembly and SSA instructions, then constructs a control-flow graph.The SSA conversion excludes stack operations while retaining the EVM instruction set’s other instructions.
- Datasets: Figure 10 reports statistics for two Ethereum datasets and identifies the relevant checks by contract, sstore-instruction, or call-instruction counts.Ether liquidity uses the number of contracts; restricted writes and validated arguments use sstore instructions; remaining properties use call instructions.
- Optimizations: Securify applies unused-instruction elimination, partial evaluation, and method inlining to improve analysis precision and scalability.Unused-instruction elimination reduces contract instructions by 44%, while partial evaluation resolves over 70% of storage and memory offsets.
- Fact Inference and Pattern Evaluation: Semantic facts are inferred with stratified Datalog and Souffle, which computes a fixed-point of the inferred facts.Pattern evaluation queries this fixed-point directly and iterates over instructions to handle quantifiers.
7 EVALUATION
Securify was evaluated on real-world EVM and Solidity contracts for proving security properties, finding violations, reducing warnings, and comparing against symbolic checkers. The results show broad coverage, substantial proof of safety and violations, and practical scalability, while effectiveness varies by property.
- Datasets: 24,594 contracts formed the EVM dataset, while the Solidity dataset contained 100 uploaded Solidity contracts.The datasets represent deployed bytecode and recently uploaded source contracts, respectively.
- Security analysis: 55.5% of relevant instructions were proved safe, 29.3% were definite violations, and 15.2% were warnings across security properties.For no writes after calls, 90.9% of calls were compliant, 6.5% violated the property, and 2.6% generated warnings.
- Security analysis: For handled exceptions, Securify proved violations for 29.9% of call instructions and compliance for the remaining 70.1%, with no warnings.At least one pattern matched every call instruction for this property.
- Limitations and future work: Pattern effectiveness varied by property, with restricted transfer and transaction-ordering properties producing roughly half false warnings.The authors identify harder-to-prove properties as candidates for additional patterns.
- Comparison: Oyente missed 72.9% of transaction-ordering violations, while Mythril missed 65.6% of restricted-transfer violations.Both symbolic tools missed actual vulnerabilities for all considered security properties except reentrancy.
- Performance: Partial evaluation correctly resolved 72.6% of memory and storage offsets on average, and Securify terminated for all contracts in 30 seconds per contract on average.The resolved offsets support inference of precise memory and storage writes.
8 RELATED WORK
Related work spans formal verification, symbolic execution, declarative analysis, domain-specific checking, and language-based security. Securify differs through all-behavior analysis, compliance and violation patterns, and an extensible DSL for smart-contract properties.
- Formal verification: Formal-verification systems model Ethereum or translate contracts into theorem-proving frameworks, but some reported no real-world contract evaluation.The cited approaches include Isabelle, Lem, F*, and other verification systems.
- Symbolic execution: Symbolic-execution tools such as Oyente, Mythril, and Maian can miss paths, encounter hard constraints, and produce low coverage or false positives.Securify is described as an abstract interpreter that explores all contract behaviors and can provide soundness guarantees over executions.
- Domain-specific analyzers: Zeus supports sound analysis and XACML properties, whereas Securify’s DSL targets data- and control-flow properties and includes violation patterns.A direct comparison was unavailable because Zeus and its benchmarks were not publicly available.
- Domain-specific analyzers: Securify covers a larger class of smart-contract properties than a dynamic linearizability checker and lets security experts extend the system with additional properties.The comparison concerns a reentrancy-focused checker by Grossman et al.
- Language-based security: Language-based tools such as PQL and Pidgin express program or dependence-graph patterns, while Securify focuses on Ethereum smart contracts.Both approaches use declarative analysis foundations for expressing security-relevant patterns.
- Declarative analysis: Declarative program-analysis systems use Datalog for static-analysis computations, paralleling Securify’s fact-inference engine.Doop is cited as a scalable declarative points-to analysis for Java.
9 CONCLUSION
Securify is a lightweight, scalable verifier that analyzes all contract behaviors, reduces warning-classification effort, and supports extensible vulnerability patterns. Its automated Datalog-based pipeline enables security experts to express new patterns as vulnerabilities emerge.
- Conclusion: Securify analyzes all contract behaviors to avoid undesirable false negatives.This benefit is presented as a central conclusion of the paper.
- Conclusion: Securify reduces user effort by guaranteeing that certain reported behaviors are actual errors rather than requiring classification of every report.Users still classify warnings into true positives and false alarms.
- Conclusion: Its domain-specific language lets users express new vulnerability patterns as they emerge.The extensibility applies to security patterns used by the verifier.
- Conclusion: The bytecode-decompilation, optimization, and pattern-checking pipeline is fully automated with scalable, off-the-shelf Datalog solvers.This automation spans the analysis pipeline described in the conclusion.