  The rise of modern blockchains has facilitated the emergence of smart
contracts: autonomous programs that live and run on the blockchain. Smart
contracts have seen a rapid climb to prominence, with applications predicted in
law, business, commerce, and governance.
  Smart contracts are commonly written in a high-level language such as
Ethereum's Solidity, and translated to compact low-level bytecode for
deployment on the blockchain. Once deployed, the bytecode is autonomously
executed, usually by a %Turing-complete virtual machine. As with all programs,
smart contracts can be highly vulnerable to malicious attacks due to deficient
programming methodologies, languages, and toolchains, including buggy
compilers. At the same time, smart contracts are also high-value targets, often
commanding large amounts of cryptocurrency. Hence, developers and auditors need
security frameworks capable of analysing low-level bytecode to detect potential
security vulnerabilities.
  In this paper, we present Vandal: a security analysis framework for Ethereum
smart contracts. Vandal consists of an analysis pipeline that converts
low-level Ethereum Virtual Machine (EVM) bytecode to semantic logic relations.
Users of the framework can express security analyses in a declarative fashion:
a security analysis is expressed in a logic specification written in the
\souffle language. We conduct a large-scale empirical study for a set of common
smart contract security vulnerabilities, and show the effectiveness and
efficiency of Vandal. Vandal is both fast and robust, successfully analysing
over 95\% of all 141k unique contracts with an average runtime of 4.15 seconds;
outperforming the current state of the art tools---Oyente, EthIR, Mythril, and
Rattle---under equivalent conditions.
