Securify: Practical Security Analysis of Smart Contracts

By Petar Tsankov, Andrei Marian Dan, Dana Drachsler-Cohen, Arthur Gervais, Florian Buenzli, Martin T. Vechev. Conference on Computer and Communications Security, 2018

1,151 citations recorded by the source corpus.

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.

Subfields: Artificial Intelligence, Information Systems, Signal Processing

View Paper: https://www.semanticscholar.org/paper/272850f06a2aa8c0831f68cf832412852aab5dc8

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Information Systems

In Signal Processing

Citations in the corpus

Sereum: Protecting Existing Smart Contracts Against Re-Entrancy Attacks (2018, methodology): “We compare our ﬁndings with state-of-the-art academic analysis tools such as Oyente [29], [34] and Se-curify [42].”
Smart Contract Development: Challenges and Opportunities (2021, background): “developed Securify to detect several kinds of security bugs by inspecting whether or not smart contract behavior violated certain semantic patterns derived from controland data-flow dependencies within smart contract [144], [143].”
Slither: A Static Analysis Framework for Smart Contracts (2019, methodology): “Securify is one of these tools [27], developed by the SRI Systems Lab (ETH Zurich).”
Dissecting Ponzi schemes on Ethereum: identification, analysis, and impact (2017, methodology): “To counteract these vulnerabilities, researchers have started to develop tools for automatically analysing Ethereum contracts [23, 30, 31, 32, 33].”
A Survey on Ethereum Systems Security (2019, background): “Securify [176] (D15) defines a set of compliance and violation patterns to characterize how contract comply and violate security properties extracted from some known vulnerabilities, such as the reentrancy vulnerability (V1), the delegatecall injection vulnerability (V2), and the frozen Ether vulner”
Osiris: Hunting for Integer Bugs in Ethereum Smart Contracts (2018, methodology): “Hence, we only scratched the tip of the iceberg, by analysing only 495 of them.”
Survey on blockchain based smart contracts: Applications, opportunities and challenges (2021, background): “Identification of such vulnerabilities save money, time and safeguards the entire blockchain ecosystem • Security analysis [242], [243], [244], [245], [246], [247] • Vulnerability identification [248], [249] • Automated security testing [250], [251] , [252] • Symbolic analysis [253] • Security bug i”
A Survey on Consensus Mechanisms and Mining Strategy Management in Blockchain Networks (2018, background): “Extending from the basic scenarios in [127] and [217], various tools of mechanism design, e.”
Combining Graph Neural Networks With Expert Knowledge for Smart Contract Vulnerability Detection (2021, methodology): “We empirically checked the Vulnerable contract using the state-of-the-art tools including Oyente [8], Securify [18], Smartcheck [16], Slither [53], and Mythril [52], and manually inspected their generated reports.”
An Overview on Smart Contracts: Challenges, Advances and Platforms (2019, neutral): “Meanwhile [84] symbolically analyzed the contract dependency graph to extract precise semantic information from the code.”
Empirical Review of Automated Analysis Tools on 47,587 Ethereum Smart Contracts (2019, methodology): “There has been some effort from the research community to develop automated analysis tools that locate and eliminate vulnerabilities in smart contracts [18, 27, 39, 42].”