TY  - GEN
ID  - discovery10182340
N2  - 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.
UR  - https://doi.org/10.1145/3243734.3243780
PB  - ACM
CY  - Toronto, Canada
KW  - Smart contracts; Security analysis; Stratified Datalog
A1  - Tsankov, Petar
A1  - Dan, Andrei
A1  - Drachsler-Cohen, Dana
A1  - Gervais, Arthur
A1  - Bünzli, Florian
A1  - Vechev, Martin
TI  - Securify: Practical Security Analysis of Smart Contracts
EP  - 82
Y1  - 2018/10/15/
AV  - public
SP  - 67
N1  - This version is the author accepted manuscript. For information on re-use, please refer to the publisher?s terms and conditions.
ER  -