2018

Vandal: A Scalable Security Analysis Framework for Smart Contracts

Brent, Lexi, Jurisevic, Anton, Kong, Michael et al.

Understand

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.

Built on

doi: 10.1145/115372.115320
Cytron R, Ferrante J, Rosen BK, Wegman MN, Zadeck FK. Efficiently Computing Static Single Assignment Form and the Control Dependence Graph. ACM Trans. Program. Lang. Syst · 1991
Earlier work this paper cites.
2nd ed. 2007
Aho AV, Lam MS, Sethi R, Ullman JD. Compilers: Principles, Techniques, & Tools with Gradiance · 2007
Earlier work this paper cites.
Nakamoto S. Bitcoin: A Peer-to-Peer Electronic Cash System. https://www.bitcoin.org/bitcoin.pdf ; 2009
2009
Earlier work this paper cites.
Bravenboer M, Smaragdakis Y. Strictly Declarative Specification of Sophisticated Points-to Analyses. In: OOPSLA ’09. ACM. ACM; 2009; New York, NY, USA: 243–262
2009
Earlier work this paper cites.
Hoder K, Bjørner N, Moura dLM. Z
2011
Earlier work this paper cites.
Buterin V. A Next-Generation Smart Contract and Decentralized Application Platform. https://github.com/ethereum/wiki/wiki/White-Paper ; 2013
2013
Earlier work this paper cites.
Flood MD, Goodenough OR. Contract as automaton: the computational representation of financial agreements. https://dx.doi.org/10.2139/ssrn.2648460 ; 2015
2015
Earlier work this paper cites.
doi: 10.1145/2644805
Livshits B, Sridharan M, Smaragdakis Y, et al. In Defense of Soundiness: A Manifesto. Commun. ACM · 2015
Earlier work this paper cites.
London : Portfolio Penguin, 2016: Penguin
Tapscott D, Tapscott A. Blockchain Revolution: How the Technology Behind Bitcoin Is Changing Money, Business, and the World · 2016
Earlier work this paper cites.
Science fUKGO. Distributed ledger technology: beyond block chain. https://www.gov.uk/government/publications/distributed-ledger-technology-blackett-review ; 2016
2016
Earlier work this paper cites.
Luu L, Chu DH, Olickel H, Saxena P, Hobor A. Making Smart Contracts Smarter. In: CCS ’16. ACM. ACM; 2016; New York, NY, USA: 254–269
2016
Earlier work this paper cites.
Zikai AW, Miller A. Scanning Live Ethereum Contracts for the “Unchecked-Send”
2016
Earlier work this paper cites.
Bhargavan K, Delignat-Lavaud A, Fournet C, et al. Formal Verification of Smart Contracts: Short Paper. In: PLAS ’16. ACM. ACM; 2016; New York, NY, USA: 91–96
2016
Earlier work this paper cites.
R3 Consortium . Corda—an open-source distributed ledger platform. https://www.corda.net/; 2017
2017
Earlier work this paper cites.
Leising M. The Ether Thief. https://www.bloomberg.com/features/2017-the-ether-thief/ ; 2017
2017
Earlier work this paper cites.
Accessed: 2017-08-22
BlockCAT . On the Parity Multi-Sig Wallet Attack. https://medium.com/@BlockCAT/on-the-parity-multi-sig-wallet-attack-83fb5e7f4b8c ; 2017 · 2017
Earlier work this paper cites.
Accessed: 2017-08-22
Qureshi H. A hacker stole $31M of Ether—how it happened and what it means for Ethereum. http://haseebq.com/a-hacker-stole-31m-of-ether/ ; 2017 · 2017
Earlier work this paper cites.

Similar

Atzei N, Bartoletti M, Cimoli T. A Survey of Attacks on Ethereum Smart Contracts. In: Springer-Verlag New York, Inc. Springer-Verlag New York, Inc.; 2017; New York, NY, USA: 164–186
2017
Cited alongside, same era.
Chen T, Li X, Luo X, Zhang X. Under-optimized smart contracts devour your money. In: IEEE. ; 2017: 442-446
2017
Cited alongside, same era.
doi: 10.1145/3158136
Grossman S, Abraham I, Golan-Gueta G, et al. Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts. Proc. ACM Program. Lang · 2017
Cited alongside, same era.
Hildenbrandt E, Zhu X, Rodrigues N. KEVM: A Complete Semantics of the Ethereum Virtual Machine. In: Everett Hildenbrandt and Xiaoran Zhu and Nishant Rodrigues. ; 2017
2017
Cited alongside, same era.
Hirai Y. Defining the Ethereum Virtual Machine for Interactive Theorem Provers. In: Brenner M, Rohloff K, Bonneau J, et al. , eds. Financial Cryptography and Data Security
2017
Cited alongside, same era.
Bartoletti M, Carta S, Cimoli T, Saia R. Dissecting Ponzi schemes on Ethereum: identification, analysis, and impact. https://arxiv.org/pdf/1703.03779.pdf ; 2017
Original
2017
Cited alongside, same era.
Accessed: 2018-09-11
web.archive.org . Ethereum (ETH) price, charts, market cap, and other metrics — CoinMarketCap. https://web.archive.org/web/20180911060543/https://coinmarketcap.com/currencies/ethereum/ ; 2018 · 2018
Cited alongside, same era.
Accessed: 2018-04-17
Various . GitHub - ethereum/solidity: The Solidity Contract-Oriented Programming Language. https://github.com/ethereum/solidity ; 2018 · 2018
Cited alongside, same era.
Accessed: 2018-03-15
wired.com . A $50 Million Hack Just Showed That the DAO Was All Too Human. https://www.wired.com/2016/06/50-million-hack-just-showed-dao-human/ ; 2018 · 2018
Cited alongside, same era.
Accessed: 2018-06-28
blog.zeppelin.solutions . The Parity Wallet Hack Explained – Zeppelin Blog. https://blog.zeppelin.solutions/on-the-parity-wallet-multisig-hack-405a8c12e8f7 ; 2018 · 2018
Cited alongside, same era.
Accessed: 2018-06-28
medium.com . Another Parity Wallet hack explained – Sergey Petrov – Medium. https://medium.com/@Pr0Ger/another-parity-wallet-hack-explained-847ca46a2e1c ; 2018 · 2018
Cited alongside, same era.
Accessed: 2018-06-28
steemit.com . Proof of Weak Hands (PoWH) Coin hacked, 866 eth stolen. https://steemit.com/cryptocurrency/@bitburner/proof-of-weak-hands-powh-coin-hacked-866-eth-stolen ; 2018 · 2018
Cited alongside, same era.

Then

Albert E, Gordillo P, Livshits B, Rubio A, Sergey I. EthIR: A Framework for High-Level Analysis of Ethereum Bytecode. In: Springer. Springer; 2018
2018
Closest in time.
The 9th annual HITB Security Conference
Mueller B. Smashing Ethereum Smart Contracts for Fun and Real Profit. https://github.com/b-mueller/smashing-smart-contracts/raw/master/smashing-smart-contracts-1of1.pdf ; 2018 · 2018
Closest in time.
Accessed: 2018-08-24
Various . Rattle – An EVM Binary Static Analysis Framework. https://github.com/trailofbits/rattle ; 2018 · 2018
Closest in time.
Accessed: 2018-03-16
github.com . GitHub - usyd-blockchain/vandal: Static program analysis framework for Ethereum smart contract bytecode. https://github.com/usyd-blockchain/vandal ; · 2018
Closest in time.
Accessed: 2018-03-15
parity.io . Parity. https://www.parity.io/ ; 2018 · 2018
Closest in time.
Accessed: 2018-08-24
Various . Porosity – a decompiler for EVM bytecode into readable Solidity-syntax contracts. https://github.com/comaeio/porosity ; 2018 · 2018
Closest in time.
Krupp J, Rossow C. teEther: Gnawing at Ethereum to Automatically Exploit Smart Contracts. In: USENIX Association. USENIX Association; 2018; Baltimore, MD: 1317–1333
2018
Closest in time.
Grishchenko I, Maffei M, Schneidewind C. A Semantic Framework for the Security Analysis of Ethereum smart contracts. CoRR
Original
2018
Closest in time.
Accessed: 2018-04-17
Why3 . Why3. http://why3.lri.fr/ ; 2018 · 2018
Closest in time.
Amani S, Bégel M, Bortin M, Staples M. Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL. In: CPP 2018. ACM. ACM; 2018; New York, NY, USA: 66–77
2018
Closest in time.
Accessed: 2018-04-17
Isabelle . Isabelle. https://isabelle.in.tum.de/ ; 2018 · 2018
Closest in time.
Accessed: 2018-04-17
FStarLang . F*: A Higher-Order Effectful Language Designed for Program Verification. https://www.fstar-lang.org/ ; 2018 · 2018
Closest in time.
Accessed: 2018-04-17
K Framework . K Framework. http://www.kframework.org/index.php/Main_Page ; 2018 · 2018
Closest in time.
Mavridou A, Laszka A. Designing Secure Ethereum Smart Contracts: A Finite State Machine Based Approach. http://aronlaszka.com/papers/mavridou2018designing.pdf ; 2018
2018
Closest in time.
Accessed: 2018-04-17
LLVM . The LLVM Compiler Infrastructure Project. https://llvm.org/ ; 2018 · 2018
Closest in time.
Accessed: 2018-04-17
SeaHorn . SeaHorn — A Verification Framework. http://seahorn.github.io/ ; 2018 · 2018
Closest in time.
Grech N, Kong M, Jurisevic A, Brent L, Scholz B, Smaragdakis Y. MadMax: Surviving Out-of-Gas Conditions in Ethereum Smart Contracts. Proc. ACM Program. Lang
2018
Closest in time.

Beyond the bibliography

alphaXiv searches the wider corpus for related work and actual follow-ups.

Open on alphaXiv

alphaXiv is searching for related work…

Reading the bibliography…