Precise Attack Synthesis for Smart Contracts

Unleashing mayhem on binary code

Original

Sang Kil Cha, Thanassis Avgerinos, Alexandre Rebert, and David Brumley · 1902

Earlier work this paper cites.

Symbolic execution and program testing

James C King · 1976

Earlier work this paper cites.

Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints

Patrick Cousot and Radhia Cousot · 1977

Earlier work this paper cites.

AEG: automatic exploit generation

Thanassis Avgerinos, Sang Kil Cha, Brent Lim Tze Hao, and David Brumley · 2011

Earlier work this paper cites.

A lightweight symbolic virtual machine for solver-aided host languages

Emina Torlak and Rastislav Bodík · 2014

Earlier work this paper cites.

SMACK: decoupling source language details from verifier implementations

Zvonimir Rakamaric and Michael Emmi · 2014

Earlier work this paper cites.

Boolector 2.0 system description

Aina Niemetz, Mathias Preiner, and Armin Biere · 2015

Earlier work this paper cites.

Making smart contracts smarter

Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor · 2016

Earlier work this paper cites.

A survey of attacks on ethereum smart contracts (sok)

Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli · 2017

Earlier work this paper cites.

Defining the ethereum virtual machine for interactive theorem provers

Yoichi Hirai · 2017

Earlier work this paper cites.

Securify: Practical security analysis of smart contracts

Petar Tsankov, Andrei Marian Dan, Dana Drachsler-Cohen, Arthur Gervais, Florian Bünzli, and Martin T. Vechev · 2018

Earlier work this paper cites.

Contractfuzzer: fuzzing smart contracts for vulnerability detection

Bo Jiang, Ye Liu, and W. K. Chan · 2018

Earlier work this paper cites.

Madmax: surviving out-of-gas conditions in ethereum smart contracts

Neville Grech, Michael Kong, Anton Jurisevic, Lexi Brent, Bernhard Scholz, and Yannis Smaragdakis · 2018

Earlier work this paper cites.

ZEUS: analyzing safety of smart contracts

Sukrit Kalra, Seep Goel, Mohan Dhawan, and Subodh Sharma · 2018

Earlier work this paper cites.

teether: Gnawing at ethereum to automatically exploit smart contracts

Johannes Krupp and Christian Rossow · 2018

Earlier work this paper cites.

https://github.com/ConsenSys/mythril-classic , 2018

Mythril classic · 2018

Earlier work this paper cites.

Online detection of effectively callback free objects with applications to smart contracts

Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar · 2018

Cited alongside, same era.

A semantic framework for the security analysis of ethereum smart contracts

Ilya Grishchenko, Matteo Maffei, and Clara Schneidewind · 2018

Cited alongside, same era.

Erays: Reverse engineering ethereum’s opaque smart contracts

Yi Zhou, Deepak Kumar, Surya Bakshi, Joshua Mason, Andrew Miller, and Michael Bailey · 2018

Cited alongside, same era.

https://bitcoin.org/ , 2019

Bitcoin · 2019

Cited alongside, same era.

https://www.ethereum.org/ , 2019

Ethereum · 2019

Cited alongside, same era.

https://solidity.readthedocs.io/en/v0.5.1/ , 2019

Solidity · 2019

Cited alongside, same era.

https://github.com/ethereum/serpent , 2019

Serpent · 2019

Closest in time.

https://github.com/ethereum/vyper , 2019

Vyper · 2019

Closest in time.

https://tinyurl.com/y7tkoggh , 2019

Transaction 0x45725e88bcbfd30afacf184a58b1ea… · 2019

Closest in time.

https://tinyurl.com/yb6eo6r9 , 2018

Batchoverflow exploit creates trillions of ethereum tokens, major exchanges halt erc20 deposits · 2019

Closest in time.

https://racket-lang.org/ , 2017

The racket language · 2019

Closest in time.

https://en.wikipedia.org/wiki/Non-interference_(security) , 2018

Non-interference (security) · 2019

Closest in time.

https://dasp.co/#item-4 , 2018

Unchecked return values for low level calls · 2019