Fetching the paper…
Reading the bibliography…
We introduce the Clockwork Finance Framework (CFF), a general purpose, formal verification framework for mechanized reasoning about the economic security properties of composed decentralized-finance (DeFi) smart contracts.
“A Formal Semantics of Findel in Coq (Short Paper)” arXiv:1909.05464 , 2019
Andrei Arusoaie · 1909
Earlier work this paper cites.
“Database transaction models”
Gottfried Vossen · 1995
Earlier work this paper cites.
“Z3: An Efficient SMT Solver”
Leonardo de Moura and Nikolaj Bjrner · 2008
Earlier work this paper cites.
“Formal verification of a realistic compiler”
Xavier Leroy · 2009
Earlier work this paper cites.
“Beware the middleman: Empirical analysis of Bitcoin-exchange risk”
Tyler Moore and Nicolas Christin · 2013
Earlier work this paper cites.
“Maximal sound predictive race detection with control flow abstraction”
Jeff Huang, Patrick’Neil Meredith and Grigore Rosu · 2014
Earlier work this paper cites.
“The inside story of Mt. Gox, Bitcoin’s $460 million disaster”
Robert McMillan · 2014
Earlier work this paper cites.
“Ethereum yellow paper” https://github.com/ethereum/yellowpaper , 2014
Gavin Wood · 2014
Earlier work this paper cites.
“Thinking about smart contract security” https://blog.ethereum.org/2016/06/19/thinking-smartcontract-security , 2016
Vitalik Buterin · 2016
Earlier work this paper cites.
“Hawk: The Blockchain Model of Cryptography and Privacy-Preserving Smart Contracts”
Ahmed Kosba et al · 2016
Earlier work this paper cites.
“Semantics-Based Program Verifiers for All Languages”
Andrei Stefanescu et al · 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.
“On Path Independence” https://vitalik.ca/general/2017/06/22/marketmakers.html , 2017
Vitalik Buterin · 2017
Earlier work this paper cites.
“Defining the Ethereum virtual machine for interactive theorem provers”
Yoichi Hirai · 2017
Earlier work this paper cites.
“Formal Verification of Financial Algorithms”
Grant Passmore and Denis Ignatovich · 2017
Earlier work this paper cites.
“A hacker stole $31M of Ether—how it happened, and what it means for Ethereum”
Haseeb Qureshi · 2017
Earlier work this paper cites.
“K: A semantic framework for programming languages and formal analysis tools”
Grigore Rosu · 2017
Cited alongside, same era.
“Towards verifying Ethereum smart contract bytecode in Isabelle/HOL”
Sidney Amani, Myriam B“’egel, Maksym Bortin and Mark Staples · 2018
Cited alongside, same era.
“Enter the hydra: Towards principled bug bounties and exploit-resistant smart contracts”
Lorenz Breidenbach, Phil Daian, Florian Tram“‘er and Ari Juels · 2018
Cited alongside, same era.
“A Language-Independent Program Verification Framework”
Xiaohong Chen and Grigore Rosu · 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.
“KEVM: A complete formal semantics of the Ethereum virtual machine”
Everett Hildenbrandt et al · 2018
“A Survey on Ethereum Systems Security: Vulnerabilities, Attacks, and Defenses”
Huashan Chen, Marcus Pendleton, Laurent Njilla and Shouhuai Xu · 2020
Later among the works it cites.
“Matching Logic Explained” http://hdl.handle.net/2142/107794 , 2020
Xiaohong Chen, Dorel Lucanu and Grigore Rosu · 2020
Later among the works it cites.
“Flash Boys 2.0: Frontrunning, Transaction Reordering, and Consensus Instability in Decentralized Exchanges”
Philip Daian et al · 2020
Later among the works it cites.
“Verified Smart Contracts” https://github.com/runtimeverification/verified-smart-contracts , 2020
Runtime Inc · 2020
Later among the works it cites.
“Post-Mortem [of the bZx Attack]” https://bzx.network/blog/postmortem-ethdenver , 2020
Kyle Kistner · 2020
Later among the works it cites.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Cited alongside, same era.
“Teether: Gnawing at Ethereum to automatically exploit smart contracts”
Johannes Krupp and Christian Rossow · 2018
Cited alongside, same era.
“QSYM: A practical concolic execution engine tailored for hybrid fuzzing”
Insu Yun et al · 2018
Cited alongside, same era.
“Formal Specification of Constant Product ( x × y = k ) (x\times y=k) Market Maker Model and Implementation” https://github.com/runtimeverification/verified-smart-contracts/blob/master/uniswap/x-y-k.pdf , 2018
Yi Zhang, Xiaohong Chen and Grigore Rosu · 2018
Cited alongside, same era.
“Uniswap” https://uniswap.org/docs , 2019
Hayden Adams · 2019
Cited alongside, same era.
“K vs. Coq as Language Verification Frameworks (Part 1 of 3)” https://runtimeverification.com/blog/k-vs-coq-as-language-verification-frameworks-part-1-of-3/ , 2019
Musab Alturki and Brandon Moore · 2019
Cited alongside, same era.
“ILC: A Calculus for Composable, Computational Cryptography”
Kevin Liao, Matthew. Hammer and Andrew Miller · 2019
Cited alongside, same era.
MakerDAO · 2020
Later among the works it cites.
“End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract”
Daejun Park, Yi Zhang and Grigore Rosu · 2020
Later among the works it cites.
“A Note on Bundle Profit Maximization” https://angeris.github.io/papers/flashbots-mev.pdf , 2021
Guillermo Angeris, Alex Evans and Tarun Chitra · 2021
Closest in time.
“The Analysis of the Array Finance Security Incident” https://blocksecteam.medium.com/the-analysis-of-the-array-finance-security-incident-bcab555326c1 , 2021
BlockSecTeam · 2021
Closest in time.
“PancakeBunny Incident: Root Cause Analysis” https://peckshield.medium.com/pancakebunny-incident-root-cause-analysis-7099f413cc9b , 2021
PeckShield · 2021
Closest in time.
“Attacking the DeFi Ecosystem with Flash Loans for Fun and Profit”
Kaihua Qin, Liyi Zhou, Benjamin Livshits and Arthur Gervais · 2021
Closest in time.
“High-Frequency Trading on Decentralized On-Chain Exchanges”
Liyi Zhou et al · 2021
Closest in time.
“On the Just-In-Time Discovery of Profit-Generating Transactions in DeFi Protocols”
Liyi Zhou et al · 2021
Closest in time.
“Someone Claims $1.1M from Ape Tokens Airdrop via Flash Loan” https://www.cryptotimes.io/someone-claims-1-1m-from-ape-tokens-airdrop-via-flash-loan/ , 2022
Ritu Lavania · 2022
Closest in time.
“Quantifying Blockchain Extractable Value: How dark is the forest?”
Kaihua Qin, Liyi Zhou and Arthur Gervais · 2022
Closest in time.