Security analysis of smart contracts in datalog

Abstract

Smart contracts enable 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 issue, we have developed Securify, a scalable and fully automated security analyzer for Ethereum smart contracts. A key technical insight behind the design of Securify is that whenever a smart contract violates a security property, it often also violates a simpler property that can be expressed on the contract’s data-flow graph. To leverage this insight, Securify symbolically encodes relevant control- and data-flow dependencies in stratified Datalog and uses scalable Datalog solvers to derive key semantic facts about the contract. Then, it inspects the inferred semantic facts to checks a set of compliance and violation patterns, which capture sufficient conditions for proving if a given security property holds or not.