Showing 1–29 of 29 results for author: Gervais, A

Hunting DeFi Vulnerabilities via Context-Sensitive Concolic Verification

Authors: Yepeng Ding, Arthur Gervais, Roger Wattenhofer, Hiroyuki Sato

Abstract: Decentralized finance (DeFi) is revolutionizing the traditional centralized finance paradigm with its attractive features such as high availability, transparency, and tamper-proofing. However, attacks targeting DeFi services have severely damaged the DeFi market, as evidenced by our investigation of 80 real-world DeFi incidents from 2017 to 2022. Existing methods, based on symbolic execution, mode… ▽ More Decentralized finance (DeFi) is revolutionizing the traditional centralized finance paradigm with its attractive features such as high availability, transparency, and tamper-proofing. However, attacks targeting DeFi services have severely damaged the DeFi market, as evidenced by our investigation of 80 real-world DeFi incidents from 2017 to 2022. Existing methods, based on symbolic execution, model checking, semantic analysis, and fuzzing, fall short in identifying the most DeFi vulnerability types. To address the deficiency, we propose Context-Sensitive Concolic Verification (CSCV), a method of automating the DeFi vulnerability finding based on user-defined properties formulated in temporal logic. CSCV builds and optimizes contexts to guide verification processes that dynamically construct context-carrying transition systems in tandem with concolic executions. Furthermore, we demonstrate the effectiveness of CSCV through experiments on real-world DeFi services and qualitative comparison. The experiment results show that our CSCV prototype successfully detects 76.25% of the vulnerabilities from the investigated incidents with an average time of 253.06 seconds. △ Less

Submitted 16 April, 2024; originally announced April 2024.

What Drives the (In)stability of a Stablecoin?

Authors: Yu** Kwon, Kornrapat Pongmala, Kaihua Qin, Ariah Klages-Mundt, Philipp Jovanovic, Christine Parlour, Arthur Gervais, Dawn Song

Abstract: In May 2022, an apparent speculative attack, followed by market panic, led to the precipitous downfall of UST, one of the most popular stablecoins at that time. However, UST is not the only stablecoin to have been depegged in the past. Designing resilient and long-term stable coins, therefore, appears to present a hard challenge. To further scrutinize existing stablecoin designs and ultimately l… ▽ More In May 2022, an apparent speculative attack, followed by market panic, led to the precipitous downfall of UST, one of the most popular stablecoins at that time. However, UST is not the only stablecoin to have been depegged in the past. Designing resilient and long-term stable coins, therefore, appears to present a hard challenge. To further scrutinize existing stablecoin designs and ultimately lead to more robust systems, we need to understand where volatility emerges. Our work provides a game-theoretical model aiming to help identify why stablecoins suffer from a depeg. This game-theoretical model reveals that stablecoins have different price equilibria depending on the coin's architecture and mechanism to minimize volatility. Moreover, our theory is supported by extensive empirical data, spanning $1$ year. To that end, we collect daily prices for 22 stablecoins and on-chain data from five blockchains including the Ethereum and the Terra blockchain. △ Less

Submitted 25 July, 2023; v1 submitted 14 June, 2023; originally announced July 2023.

Do you still need a manual smart contract audit?

Authors: Isaac David, Liyi Zhou, Kaihua Qin, Dawn Song, Lorenzo Cavallaro, Arthur Gervais

Abstract: We investigate the feasibility of employing large language models (LLMs) for conducting the security audit of smart contracts, a traditionally time-consuming and costly process. Our research focuses on the optimization of prompt engineering for enhanced security analysis, and we evaluate the performance and accuracy of LLMs using a benchmark dataset comprising 52 Decentralized Finance (DeFi) smart… ▽ More We investigate the feasibility of employing large language models (LLMs) for conducting the security audit of smart contracts, a traditionally time-consuming and costly process. Our research focuses on the optimization of prompt engineering for enhanced security analysis, and we evaluate the performance and accuracy of LLMs using a benchmark dataset comprising 52 Decentralized Finance (DeFi) smart contracts that have previously been compromised. Our findings reveal that, when applied to vulnerable contracts, both GPT-4 and Claude models correctly identify the vulnerability type in 40% of the cases. However, these models also demonstrate a high false positive rate, necessitating continued involvement from manual auditors. The LLMs tested outperform a random model by 20% in terms of F1-score. To ensure the integrity of our study, we conduct mutation testing on five newly developed and ostensibly secure smart contracts, into which we manually insert two and 15 vulnerabilities each. This testing yielded a remarkable best-case 78.7% true positive rate for the GPT-4-32k model. We tested both, asking the models to perform a binary classification on whether a contract is vulnerable, and a non-binary prompt. We also examined the influence of model temperature variations and context length on the LLM's performance. Despite the potential for many further enhancements, this work lays the groundwork for a more efficient and economical approach to smart contract security audits. △ Less

Submitted 22 June, 2023; v1 submitted 21 June, 2023; originally announced June 2023.

Blockchain Censorship

Authors: Anton Wahrstätter, Jens Ernstberger, Aviv Yaish, Liyi Zhou, Kaihua Qin, Taro Tsuchiya, Sebastian Steinhorst, Davor Svetinovic, Nicolas Christin, Mikolaj Barczentewicz, Arthur Gervais

Abstract: Permissionless blockchains promise to be resilient against censorship by a single entity. This suggests that deterministic rules, and not third-party actors, are responsible for deciding if a transaction is appended to the blockchain or not. In 2022, the U.S. Office of Foreign Assets Control (OFAC) sanctioned a Bitcoin mixer and an Ethereum application, putting the neutrality of permissionless blo… ▽ More Permissionless blockchains promise to be resilient against censorship by a single entity. This suggests that deterministic rules, and not third-party actors, are responsible for deciding if a transaction is appended to the blockchain or not. In 2022, the U.S. Office of Foreign Assets Control (OFAC) sanctioned a Bitcoin mixer and an Ethereum application, putting the neutrality of permissionless blockchains to the test. In this paper, we formalize quantify and analyze the security impact of blockchain censorship. We start by defining censorship, followed by a quantitative assessment of current censorship practices. We find that 46% of Ethereum blocks were made by censoring actors that intend to comply with OFAC sanctions, indicating the significant impact of OFAC sanctions on the neutrality of public blockchains. We further uncover that censorship not only impacts neutrality, but also security. We show how after Ethereum's move to Proof-of-Stake (PoS) and adoption of Proposer-Builder Separation (PBS) the inclusion of censored transactions was delayed by an average of 85%. Inclusion delays compromise a transaction's security by, e.g., strengthening a sandwich adversary. Finally we prove a fundamental limitation of PoS and Proof-of-Work (PoW) protocols against censorship resilience. △ Less

Submitted 2 June, 2023; v1 submitted 29 May, 2023; originally announced May 2023.

Time to Bribe: Measuring Block Construction Market

Authors: Anton Wahrstätter, Liyi Zhou, Kaihua Qin, Davor Svetinovic, Arthur Gervais

Abstract: With the emergence of Miner Extractable Value (MEV), block construction markets on blockchains have evolved into a competitive arena. Following Ethereum's transition from Proof of Work (PoW) to Proof of Stake (PoS), the Proposer Builder Separation (PBS) mechanism has emerged as the dominant force in the Ethereum block construction market. This paper presents an in-depth longitudinal study of the… ▽ More With the emergence of Miner Extractable Value (MEV), block construction markets on blockchains have evolved into a competitive arena. Following Ethereum's transition from Proof of Work (PoW) to Proof of Stake (PoS), the Proposer Builder Separation (PBS) mechanism has emerged as the dominant force in the Ethereum block construction market. This paper presents an in-depth longitudinal study of the Ethereum block construction market, spanning from the introduction of PoS and PBS in September 2022 to May 2023. We analyze the market shares of builders and relays, their temporal changes, and the financial dynamics within the PBS system, including payments among builders and block proposers -- commonly referred to as bribes. We introduce an MEV-time law quantifying the expected MEV revenue wrt. the time elapsed since the last proposed block. We provide empirical evidence that moments of crisis (e.g. the FTX collapse, USDC stablecoin de-peg) coincide with significant spikes in MEV payments compared to the baseline. Despite the intention of the PBS architecture to enhance decentralization by separating actor roles, it remains unclear whether its design is optimal. Implicit trust assumptions and conflicts of interest may benefit particular parties and foster the need for vertical integration. MEV-Boost was explicitly designed to foster decentralization, causing the side effect of enabling risk-free sandwich extraction from unsuspecting users, potentially raising concerns for regulators. △ Less

Submitted 2 June, 2023; v1 submitted 25 May, 2023; originally announced May 2023.

Towards Automated Security Analysis of Smart Contracts based on Execution Property Graph

Authors: Kaihua Qin, Zhe Ye, Zhun Wang, Weilin Li, Liyi Zhou, Chao Zhang, Dawn Song, Arthur Gervais

Abstract: Identifying and mitigating vulnerabilities in smart contracts is crucial, especially considering the rapid growth and increasing complexity of Decentralized Finance (DeFi) platforms. To address the challenges associated with securing these contracts, we introduce a versatile dynamic analysis framework specifically designed for the Ethereum Virtual Machine (EVM). This comprehensive framework focuse… ▽ More Identifying and mitigating vulnerabilities in smart contracts is crucial, especially considering the rapid growth and increasing complexity of Decentralized Finance (DeFi) platforms. To address the challenges associated with securing these contracts, we introduce a versatile dynamic analysis framework specifically designed for the Ethereum Virtual Machine (EVM). This comprehensive framework focuses on tracking contract executions, capturing valuable runtime information, while introducing and employing the Execution Property Graph (EPG) to propose a unique graph traversal technique that swiftly detects potential smart contract attacks. Our approach showcases its efficacy with rapid average graph traversal time per transaction and high true positive rates. The successful identification of a zero-day vulnerability affecting Uniswap highlights the framework's potential to effectively uncover smart contract vulnerabilities in complex DeFi systems. △ Less

Submitted 24 May, 2023; v1 submitted 23 May, 2023; originally announced May 2023.

Blockchain Large Language Models

Authors: Yu Gai, Liyi Zhou, Kaihua Qin, Dawn Song, Arthur Gervais

Abstract: This paper presents a dynamic, real-time approach to detecting anomalous blockchain transactions. The proposed tool, BlockGPT, generates tracing representations of blockchain activity and trains from scratch a large language model to act as a real-time Intrusion Detection System. Unlike traditional methods, BlockGPT is designed to offer an unrestricted search space and does not rely on predefined… ▽ More This paper presents a dynamic, real-time approach to detecting anomalous blockchain transactions. The proposed tool, BlockGPT, generates tracing representations of blockchain activity and trains from scratch a large language model to act as a real-time Intrusion Detection System. Unlike traditional methods, BlockGPT is designed to offer an unrestricted search space and does not rely on predefined rules or patterns, enabling it to detect a broader range of anomalies. We demonstrate the effectiveness of BlockGPT through its use as an anomaly detection tool for Ethereum transactions. In our experiments, it effectively identifies abnormal transactions among a dataset of 68M transactions and has a batched throughput of 2284 transactions per second on average. Our results show that, BlockGPT identifies abnormal transactions by ranking 49 out of 124 attacks among the top-3 most abnormal transactions interacting with their victim contracts. This work makes contributions to the field of blockchain transaction analysis by introducing a custom data encoding compatible with the transformer architecture, a domain-specific tokenization technique, and a tree encoding method specifically crafted for the Ethereum Virtual Machine (EVM) trace representation. △ Less

Submitted 29 April, 2023; v1 submitted 25 April, 2023; originally announced April 2023.

Smart Contract and DeFi Security Tools: Do They Meet the Needs of Practitioners?

Authors: Stefanos Chaliasos, Marcos Antonios Charalambous, Liyi Zhou, Rafaila Galanopoulou, Arthur Gervais, Dimitris Mitropoulos, Ben Livshits

Abstract: The growth of the decentralized finance (DeFi) ecosystem built on blockchain technology and smart contracts has led to an increased demand for secure and reliable smart contract development. However, attacks targeting smart contracts are increasing, causing an estimated \… ▽ More The growth of the decentralized finance (DeFi) ecosystem built on blockchain technology and smart contracts has led to an increased demand for secure and reliable smart contract development. However, attacks targeting smart contracts are increasing, causing an estimated \$6.45 billion in financial losses. Researchers have proposed various automated security tools to detect vulnerabilities, but their real-world impact remains uncertain. In this paper, we aim to shed light on the effectiveness of automated security tools in identifying vulnerabilities that can lead to high-profile attacks, and their overall usage within the industry. Our comprehensive study encompasses an evaluation of five SoTA automated security tools, an analysis of 127 high-impact real-world attacks resulting in \$2.3 billion in losses, and a survey of 49 developers and auditors working in leading DeFi protocols. Our findings reveal a stark reality: the tools could have prevented a mere 8% of the attacks in our dataset, amounting to \$149 million out of the \$2.3 billion in losses. Notably, all preventable attacks were related to reentrancy vulnerabilities. Furthermore, practitioners distinguish logic-related bugs and protocol layer vulnerabilities as significant threats that are not adequately addressed by existing security tools. Our results emphasize the need to develop specialized tools catering to the distinct demands and expectations of developers and auditors. Further, our study highlights the necessity for continuous advancements in security tools to effectively tackle the ever-evolving challenges confronting the DeFi ecosystem. △ Less

Submitted 22 January, 2024; v1 submitted 6 April, 2023; originally announced April 2023.

The Blockchain Imitation Game

Authors: Kaihua Qin, Stefanos Chaliasos, Liyi Zhou, Benjamin Livshits, Dawn Song, Arthur Gervais

Abstract: The use of blockchains for automated and adversarial trading has become commonplace. However, due to the transparent nature of blockchains, an adversary is able to observe any pending, not-yet-mined transactions, along with their execution logic. This transparency further enables a new type of adversary, which copies and front-runs profitable pending transactions in real-time, yielding significant… ▽ More The use of blockchains for automated and adversarial trading has become commonplace. However, due to the transparent nature of blockchains, an adversary is able to observe any pending, not-yet-mined transactions, along with their execution logic. This transparency further enables a new type of adversary, which copies and front-runs profitable pending transactions in real-time, yielding significant financial gains. Shedding light on such "copy-paste" malpractice, this paper introduces the Blockchain Imitation Game and proposes a generalized imitation attack methodology called Ape. Leveraging dynamic program analysis techniques, Ape supports the automatic synthesis of adversarial smart contracts. Over a timeframe of one year (1st of August, 2021 to 31st of July, 2022), Ape could have yielded 148.96M USD in profit on Ethereum, and 42.70M USD on BNB Smart Chain (BSC). Not only as a malicious attack, we further show the potential of transaction and contract imitation as a defensive strategy. Within one year, we find that Ape could have successfully imitated 13 and 22 known Decentralized Finance (DeFi) attacks on Ethereum and BSC, respectively. Our findings suggest that blockchain validators can imitate attacks in real-time to prevent intrusions in DeFi. △ Less

Submitted 31 March, 2023; originally announced March 2023.

Mitigating Decentralized Finance Liquidations with Reversible Call Options

Authors: Kaihua Qin, Jens Ernstberger, Liyi Zhou, Philipp Jovanovic, Arthur Gervais

Abstract: Liquidations in Decentralized Finance (DeFi) are both a blessing and a curse -- whereas liquidations prevent lenders from capital loss, they simultaneously lead to liquidation spirals and system-wide failures. Since most lending and borrowing protocols assume liquidations are indispensable, there is an increased interest in alternative constructions that prevent immediate systemic-failure under un… ▽ More Liquidations in Decentralized Finance (DeFi) are both a blessing and a curse -- whereas liquidations prevent lenders from capital loss, they simultaneously lead to liquidation spirals and system-wide failures. Since most lending and borrowing protocols assume liquidations are indispensable, there is an increased interest in alternative constructions that prevent immediate systemic-failure under uncertain circumstances. In this work, we introduce reversible call options, a novel financial primitive that enables the seller of a call option to terminate it before maturity. We apply reversible call options to lending in DeFi and devise Miqado, a protocol for lending platforms to replace the liquidation mechanisms. To the best of our knowledge, Miqado is the first protocol that actively mitigates liquidations to reduce the risk of liquidation spirals. Instead of selling collateral, Miqado incentivizes external entities, so-called supporters, to top-up a borrowing position and grant the borrower additional time to rescue the debt. Our simulation shows that Miqado reduces the amount of liquidated collateral by 89.82% in a worst-case scenario. △ Less

Submitted 27 March, 2023; v1 submitted 10 February, 2023; originally announced March 2023.

Exploring the Advantages of Transformers for High-Frequency Trading

Authors: Fazl Barez, Paul Bilokon, Arthur Gervais, Nikita Lisitsyn

Abstract: This paper explores the novel deep learning Transformers architectures for high-frequency Bitcoin-USDT log-return forecasting and compares them to the traditional Long Short-Term Memory models. A hybrid Transformer model, called \textbf{HFformer}, is then introduced for time series forecasting which incorporates a Transformer encoder, linear decoder, spiking activations, and quantile loss function… ▽ More This paper explores the novel deep learning Transformers architectures for high-frequency Bitcoin-USDT log-return forecasting and compares them to the traditional Long Short-Term Memory models. A hybrid Transformer model, called \textbf{HFformer}, is then introduced for time series forecasting which incorporates a Transformer encoder, linear decoder, spiking activations, and quantile loss function, and does not use position encoding. Furthermore, possible high-frequency trading strategies for use with the HFformer model are discussed, including trade sizing, trading signal aggregation, and minimal trading threshold. Ultimately, the performance of the HFformer and Long Short-Term Memory models are assessed and results indicate that the HFformer achieves a higher cumulative PnL than the LSTM when trading with multiple signals during backtesting. △ Less

Submitted 20 February, 2023; originally announced February 2023.

SoK: Decentralized Finance (DeFi) Attacks

Authors: Liyi Zhou, Xihan Xiong, Jens Ernstberger, Stefanos Chaliasos, Zhipeng Wang, Ye Wang, Kaihua Qin, Roger Wattenhofer, Dawn Song, Arthur Gervais

Abstract: Within just four years, the blockchain-based Decentralized Finance (DeFi) ecosystem has accumulated a peak total value locked (TVL) of more than 253 billion USD. This surge in DeFi's popularity has, unfortunately, been accompanied by many impactful incidents. According to our data, users, liquidity providers, speculators, and protocol operators suffered a total loss of at least 3.24 billion USD fr… ▽ More Within just four years, the blockchain-based Decentralized Finance (DeFi) ecosystem has accumulated a peak total value locked (TVL) of more than 253 billion USD. This surge in DeFi's popularity has, unfortunately, been accompanied by many impactful incidents. According to our data, users, liquidity providers, speculators, and protocol operators suffered a total loss of at least 3.24 billion USD from Apr 30, 2018 to Apr 30, 2022. Given the blockchain's transparency and increasing incident frequency, two questions arise: How can we systematically measure, evaluate, and compare DeFi incidents? How can we learn from past attacks to strengthen DeFi security? In this paper, we introduce a common reference frame to systematically evaluate and compare DeFi incidents, including both attacks and accidents. We investigate 77 academic papers, 30 audit reports, and 181 real-world incidents. Our data reveals several gaps between academia and the practitioners' community. For example, few academic papers address "price oracle attacks" and "permissonless interactions", while our data suggests that they are the two most frequent incident types (15% and 10.5% correspondingly). We also investigate potential defenses, and find that: (i) 103 (56%) of the attacks are not executed atomically, granting a rescue time frame for defenders; (ii) SoTA bytecode similarity analysis can at least detect 31 vulnerable/23 adversarial contracts; and (iii) 33 (15.3%) of the adversaries leak potentially identifiable information by interacting with centralized exchanges. △ Less

Submitted 7 April, 2023; v1 submitted 27 August, 2022; originally announced August 2022.

On How Zero-Knowledge Proof Blockchain Mixers Improve, and Worsen User Privacy

Authors: Zhipeng Wang, Stefanos Chaliasos, Kaihua Qin, Liyi Zhou, Lifeng Gao, Pascal Berrang, Ben Livshits, Arthur Gervais

Abstract: Zero-knowledge proof (ZKP) mixers are one of the most widely-used blockchain privacy solutions, operating on top of smart contract-enabled blockchains. We find that ZKP mixers are tightly intertwined with the growing number of Decentralized Finance (DeFi) attacks and Blockchain Extractable Value (BEV) extractions. Through coin flow tracing, we discover that 205 blockchain attackers and 2,595 BEV e… ▽ More Zero-knowledge proof (ZKP) mixers are one of the most widely-used blockchain privacy solutions, operating on top of smart contract-enabled blockchains. We find that ZKP mixers are tightly intertwined with the growing number of Decentralized Finance (DeFi) attacks and Blockchain Extractable Value (BEV) extractions. Through coin flow tracing, we discover that 205 blockchain attackers and 2,595 BEV extractors leverage mixers as their source of funds, while depositing a total attack revenue of 412.87M USD. Moreover, the US OFAC sanctions against the largest ZKP mixer, Tornado.Cash, have reduced the mixer's daily deposits by more than 80%. Further, ZKP mixers advertise their level of privacy through a so-called anonymity set size, which similarly to k-anonymity allows a user to hide among a set of k other users. Through empirical measurements, we, however, find that these anonymity set claims are mostly inaccurate. For the most popular mixers on Ethereum (ETH) and Binance Smart Chain (BSC), we show how to reduce the anonymity set size on average by 27.34% and 46.02% respectively. Our empirical evidence is also the first to suggest a differing privacy-predilection of users on ETH and BSC. State-of-the-art ZKP mixers are moreover interwoven with the DeFi ecosystem by offering anonymity mining (AM) incentives, i.e., users receive monetary rewards for mixing coins. However, contrary to the claims of related work, we find that AM does not necessarily improve the quality of a mixer's anonymity set. Our findings indicate that AM attracts privacy-ignorant users, who then do not contribute to improving the privacy of other mixer users. △ Less

Submitted 6 March, 2023; v1 submitted 22 January, 2022; originally announced January 2022.

Proof of Steak

Authors: Jon Crowcroft, Hamed Haddadi, Arthur Gervais, Tristan Henderson

Abstract: We introduce Proof-of-Steak (PoS) as a fundamental net-zero block generation technique, often accompanied by Non-Frangipane Tokens. Genesis cut is gradually heated and minted (using the appropriate sauce), enabling the miners to redirect the extracted gold and the dissipated heat into the furnace, hence enabling the first fully-circular economy ever built using blockchain technology, utilising tam… ▽ More We introduce Proof-of-Steak (PoS) as a fundamental net-zero block generation technique, often accompanied by Non-Frangipane Tokens. Genesis cut is gradually heated and minted (using the appropriate sauce), enabling the miners to redirect the extracted gold and the dissipated heat into the furnace, hence enabling the first fully-circular economy ever built using blockchain technology, utilising tamper-evident steak haché. In this paper we present the basic ingredients for building Proof-of-Steak, assessing its global impact, and opportunities to save the world and beyond! △ Less

Submitted 13 December, 2021; originally announced December 2021.

Comments: This is a silly article

Towards Private On-Chain Algorithmic Trading

Authors: Ceren Kocaoğullar, Arthur Gervais, Benjamin Livshits

Abstract: While quantitative automation related to trading crypto-assets such as ERC-20 tokens has become relatively commonplace, with services such as 3Commas and Shrimpy offering user-friendly web-driven services for even the average crypto trader, we have not yet seen the emergence of on-chain trading as a phenomenon. We hypothesize that just like decentralized exchanges (DEXes) that by now are by some m… ▽ More While quantitative automation related to trading crypto-assets such as ERC-20 tokens has become relatively commonplace, with services such as 3Commas and Shrimpy offering user-friendly web-driven services for even the average crypto trader, we have not yet seen the emergence of on-chain trading as a phenomenon. We hypothesize that just like decentralized exchanges (DEXes) that by now are by some measures more popular than traditional exchanges, process in the space of decentralized finance (DeFi) may enable attractive online trading automation options. In this paper we present ChainBot, an approach for creating algorithmic trading bots with the help of blockchain technology. We show how to partition the computation into on- and off-chain components in a way that provides a measure of end-to-end integrity, while preserving the algorithmic "secret sauce". Our system is enabled with a careful use of algorithm partitioning, zero-knowledge proofs and smart contracts. We also show that with layer-2 (L2) technologies, trades can be kept private, which means that algorithmic parameters are difficult to recover by a chain observer. Our approach offers more transparent access to liquidity and better censorship-resistance compared to traditional off-chain trading approaches. We develop a sample ChainBot and train it on historical data, resulting in returns that are up to 2.4x the buy-and-hold strategy, which we use as our baseline. Our measurements show that across 1000 runs, the end-to-end average execution time for our system is 48.4 seconds. We demonstrate that the frequency of trading does not significantly affect the rate of return and Sharpe ratio, which indicates that we do not have to trade at every block, thereby significantly saving in terms of gas fees. In our implementation, a user who invests \$1,000 would earn \$105, and spend \$3 on gas; assuming a user pool of 1,000 subscribers. △ Less

Submitted 23 September, 2021; originally announced September 2021.

CeFi vs. DeFi -- Comparing Centralized to Decentralized Finance

Authors: Kaihua Qin, Liyi Zhou, Yaroslav Afonin, Ludovico Lazzaretti, Arthur Gervais

Abstract: To non-experts, the traditional Centralized Finance (CeFi) ecosystem may seem obscure, because users are typically not aware of the underlying rules or agreements of financial assets and products. Decentralized Finance (DeFi), however, is making its debut as an ecosystem claiming to offer transparency and control, which are partially attributable to the underlying integrity-protected blockchain, a… ▽ More To non-experts, the traditional Centralized Finance (CeFi) ecosystem may seem obscure, because users are typically not aware of the underlying rules or agreements of financial assets and products. Decentralized Finance (DeFi), however, is making its debut as an ecosystem claiming to offer transparency and control, which are partially attributable to the underlying integrity-protected blockchain, as well as currently higher financial asset yields than CeFi. Yet, the boundaries between CeFi and DeFi may not be always so clear cut. In this work, we systematically analyze the differences between CeFi and DeFi, covering legal, economic, security, privacy and market manipulation. We provide a structured methodology to differentiate between a CeFi and a DeFi service. Our findings show that certain DeFi assets (such as USDC or USDT stablecoins) do not necessarily classify as DeFi assets, and may endanger the economic security of intertwined DeFi protocols. We conclude this work with the exploration of possible synergies between CeFi and DeFi. △ Less

Submitted 16 June, 2021; v1 submitted 15 June, 2021; originally announced June 2021.

A2MM: Mitigating Frontrunning, Transaction Reordering and Consensus Instability in Decentralized Exchanges

Authors: Liyi Zhou, Kaihua Qin, Arthur Gervais

Abstract: The asset trading volume on blockchain-based exchanges (DEX) increased substantially since the advent of Automated Market Makers (AMM). Yet, AMMs and their forks compete on the same blockchain, incurring unnecessary network and block-space overhead, by attracting sandwich attackers and arbitrage competitions. Moreover, conceptually speaking, a blockchain is one database, and we find little reason… ▽ More The asset trading volume on blockchain-based exchanges (DEX) increased substantially since the advent of Automated Market Makers (AMM). Yet, AMMs and their forks compete on the same blockchain, incurring unnecessary network and block-space overhead, by attracting sandwich attackers and arbitrage competitions. Moreover, conceptually speaking, a blockchain is one database, and we find little reason to partition this database into multiple competing exchanges, which then necessarily require price synchronization through arbitrage. This paper shows that DEX arbitrage and trade routing among similar AMMs can be performed efficiently and atomically on-chain within smart contracts. These insights lead us to create a new AMM design, an Automated Arbitrage Market Maker, short A2MM DEX. A2MM aims to unite multiple AMMs to reduce overheads, costs and increase blockchain security. With respect to Miner Extractable Value (MEV), A2MM serves as a decentralized design for users to atomically collect MEV, mitigating the dangers of centralized MEV relay services. We show that A2MM offers essential security benefits. First, A2MM strengthens the blockchain consensus security by mitigating the competitive exploitation of MEV, therefore reducing the risks of consensus forks. A2MM reduces the network layer overhead of competitive transactions, improves network propagation, leading to less stale blocks and better blockchain security. Through trade routing, A2MM reduces the predatory risks of sandwich attacks by taking advantage of the minimum profitable victim input. A2MM also offers financial benefits to traders. Failed swap transactions from competitive trading occupy valuable block space, implying an upward pressure on transaction fees. Our evaluations shows that A2MM frees up 32.8% block-space of AMM-related transactions. In expectation, A2MM's revenue allows to reduce swap fees by 90%. △ Less

Submitted 17 June, 2021; v1 submitted 14 June, 2021; originally announced June 2021.

An Empirical Study of DeFi Liquidations: Incentives, Risks, and Instabilities

Authors: Kaihua Qin, Liyi Zhou, Pablo Gamito, Philipp Jovanovic, Arthur Gervais

Abstract: Financial speculators often seek to increase their potential gains with leverage. Debt is a popular form of leverage, and with over 39.88B USD of total value locked (TVL), the Decentralized Finance (DeFi) lending markets are thriving. Debts, however, entail the risks of liquidation, the process of selling the debt collateral at a discount to liquidators. Nevertheless, few quantitative insights are… ▽ More Financial speculators often seek to increase their potential gains with leverage. Debt is a popular form of leverage, and with over 39.88B USD of total value locked (TVL), the Decentralized Finance (DeFi) lending markets are thriving. Debts, however, entail the risks of liquidation, the process of selling the debt collateral at a discount to liquidators. Nevertheless, few quantitative insights are known about the existing liquidation mechanisms. In this paper, to the best of our knowledge, we are the first to study the breadth of the borrowing and lending markets of the Ethereum DeFi ecosystem. We focus on Aave, Compound, MakerDAO, and dYdX, which collectively represent over 85% of the lending market on Ethereum. Given extensive liquidation data measurements and insights, we systematize the prevalent liquidation mechanisms and are the first to provide a methodology to compare them objectively. We find that the existing liquidation designs well incentivize liquidators but sell excessive amounts of discounted collateral at the borrowers' expenses. We measure various risks that liquidation participants are exposed to and quantify the instabilities of existing lending protocols. Moreover, we propose an optimal strategy that allows liquidators to increase their liquidation profit, which may aggravate the loss of borrowers. △ Less

Submitted 1 October, 2021; v1 submitted 11 June, 2021; originally announced June 2021.

On the Just-In-Time Discovery of Profit-Generating Transactions in DeFi Protocols

Authors: Liyi Zhou, Kaihua Qin, Antoine Cully, Benjamin Livshits, Arthur Gervais

Abstract: In this paper, we investigate two methods that allow us to automatically create profitable DeFi trades, one well-suited to arbitrage and the other applicable to more complicated settings. We first adopt the Bellman-Ford-Moore algorithm with DEFIPOSER-ARB and then create logical DeFi protocol models for a theorem prover in DEFIPOSER-SMT. While DEFIPOSER-ARB focuses on DeFi transactions that form a… ▽ More In this paper, we investigate two methods that allow us to automatically create profitable DeFi trades, one well-suited to arbitrage and the other applicable to more complicated settings. We first adopt the Bellman-Ford-Moore algorithm with DEFIPOSER-ARB and then create logical DeFi protocol models for a theorem prover in DEFIPOSER-SMT. While DEFIPOSER-ARB focuses on DeFi transactions that form a cycle and performs very well for arbitrage, DEFIPOSER-SMT can detect more complicated profitable transactions. We estimate that DEFIPOSER-ARB and DEFIPOSER-SMT can generate an average weekly revenue of 191.48ETH (76,592USD) and 72.44ETH (28,976USD) respectively, with the highest transaction revenue being 81.31ETH(32,524USD) and22.40ETH (8,960USD) respectively. We further show that DEFIPOSER-SMT finds the known economic bZx attack from February 2020, which yields 0.48M USD. Our forensic investigations show that this opportunity existed for 69 days and could have yielded more revenue if exploited one day earlier. Our evaluation spans 150 days, given 96 DeFi protocol actions, and 25 assets. Looking beyond the financial gains mentioned above, forks deteriorate the blockchain consensus security, as they increase the risks of double-spending and selfish mining. We explore the implications of DEFIPOSER-ARB and DEFIPOSER-SMT on blockchain consensus. Specifically, we show that the trades identified by our tools exceed the Ethereum block reward by up to 874x. Given optimal adversarial strategies provided by a Markov Decision Process (MDP), we quantify the value threshold at which a profitable transaction qualifies as Miner ExtractableValue (MEV) and would incentivize MEV-aware miners to fork the blockchain. For instance, we find that on Ethereum, a miner with a hash rate of 10% would fork the blockchain if an MEV opportunity exceeds 4x the block reward. △ Less

Submitted 3 March, 2021; originally announced March 2021.

The Eye of Horus: Spotting and Analyzing Attacks on Ethereum Smart Contracts

Authors: Christof Ferreira Torres, Antonio Ken Iannillo, Arthur Gervais, Radu State

Abstract: In recent years, Ethereum gained tremendously in popularity, growing from a daily transaction average of 10K in January 2016 to an average of 500K in January 2020. Similarly, smart contracts began to carry more value, making them appealing targets for attackers. As a result, they started to become victims of attacks, costing millions of dollars. In response to these attacks, both academia and indu… ▽ More In recent years, Ethereum gained tremendously in popularity, growing from a daily transaction average of 10K in January 2016 to an average of 500K in January 2020. Similarly, smart contracts began to carry more value, making them appealing targets for attackers. As a result, they started to become victims of attacks, costing millions of dollars. In response to these attacks, both academia and industry proposed a plethora of tools to scan smart contracts for vulnerabilities before deploying them on the blockchain. However, most of these tools solely focus on detecting vulnerabilities and not attacks, let alone quantifying or tracing the number of stolen assets. In this paper, we present Horus, a framework that empowers the automated detection and investigation of smart contract attacks based on logic-driven and graph-driven analysis of transactions. Horus provides quick means to quantify and trace the flow of stolen assets across the Ethereum blockchain. We perform a large-scale analysis of all the smart contracts deployed on Ethereum until May 2020. We identified 1,888 attacked smart contracts and 8,095 adversarial transactions in the wild. Our investigation shows that the number of attacks did not necessarily decrease over the past few years, but for some vulnerabilities remained constant. Finally, we also demonstrate the practicality of our framework via an in-depth analysis on the recent Uniswap and Lendf.me attacks. △ Less

Submitted 15 January, 2021; originally announced January 2021.

Quantifying Blockchain Extractable Value: How dark is the forest?

Authors: Kaihua Qin, Liyi Zhou, Arthur Gervais

Abstract: Permissionless blockchains such as Bitcoin have excelled at financial services. Yet, opportunistic traders extract monetary value from the mesh of decentralized finance (DeFi) smart contracts through so-called blockchain extractable value (BEV). The recent emergence of centralized BEV relayer portrays BEV as a positive additional revenue source. Because BEV was quantitatively shown to deteriorate… ▽ More Permissionless blockchains such as Bitcoin have excelled at financial services. Yet, opportunistic traders extract monetary value from the mesh of decentralized finance (DeFi) smart contracts through so-called blockchain extractable value (BEV). The recent emergence of centralized BEV relayer portrays BEV as a positive additional revenue source. Because BEV was quantitatively shown to deteriorate the blockchain's consensus security, BEV relayers endanger the ledger security by incentivizing rational miners to fork the chain. For example, a rational miner with a 10% hashrate will fork Ethereum if a BEV opportunity exceeds 4x the block reward. However, related work is currently missing quantitative insights on past BEV extraction to assess the practical risks of BEV objectively. In this work, we allow to quantify the BEV danger by deriving the USD extracted from sandwich attacks, liquidations, and decentralized exchange arbitrage. We estimate that over 32 months, BEV yielded 540.54M USD in profit, divided among 11,289 addresses when capturing 49,691 cryptocurrencies and 60,830 on-chain markets. The highest BEV instance we find amounts to 4.1M USD, 616.6x the Ethereum block reward. Moreover, while the practitioner's community has discussed the existence of generalized trading bots, we are, to our knowledge, the first to provide a concrete algorithm. Our algorithm can replace unconfirmed transactions without the need to understand the victim transactions' underlying logic, which we estimate to have yielded a profit of 57,037.32 ETH (35.37M USD) over 32 months of past blockchain data. Finally, we formalize and analyze emerging BEV relay systems, where miners accept BEV transactions from a centralized relay server instead of the peer-to-peer (P2P) network. We find that such relay systems aggravate the consensus layer attacks and therefore further endanger blockchain security. △ Less

Submitted 10 December, 2021; v1 submitted 14 January, 2021; originally announced January 2021.

AMR:Autonomous Coin Mixer with Privacy Preserving Reward Distribution

Authors: Duc V. Le, Arthur Gervais

Abstract: It is well known that users on open blockchains are tracked by an industry providing services to governments, law enforcement, secret services, and alike. While most blockchains do not protect their users' privacy and allow external observers to link transactions and addresses, a growing research interest attempts to design add-on privacy solutions to help users regain their privacy on non-private… ▽ More It is well known that users on open blockchains are tracked by an industry providing services to governments, law enforcement, secret services, and alike. While most blockchains do not protect their users' privacy and allow external observers to link transactions and addresses, a growing research interest attempts to design add-on privacy solutions to help users regain their privacy on non-private blockchains. In this work, we propose to our knowledge the first censorship resilient mixer, which can reward its users in a privacy-preserving manner for participating in the system. Increasing the anonymity set size, and diversity of users, is, as we believe, an important endeavor to raise a mixer's contributed privacy in practice. The paid-out rewards can take the form of governance tokens to decentralize the voting on system parameters, similar to how popular "DeFi farming" protocols operate. Moreover, by leveraging existing "Defi" lending platforms, AMR is the first mixer design that allows participating clients to earn financial interests on their deposited funds. Our system AMR is autonomous as it does not rely on any external server or third party. The evaluation of our AMR implementation shows that the system supports today on Ethereum anonymity set sizes beyond thousands of users, and a capacity of over $66,000$ deposits per day, at constant system costs. We provide a formal specification of our zksnark-based AMR system, a privacy and security analysis, implementation, and evaluation with both the MiMC and Poseidon hash functions. △ Less

Submitted 7 June, 2021; v1 submitted 2 October, 2020; originally announced October 2020.

High-Frequency Trading on Decentralized On-Chain Exchanges

Authors: Liyi Zhou, Kaihua Qin, Christof Ferreira Torres, Duc V Le, Arthur Gervais

Abstract: Decentralized exchanges (DEXs) allow parties to participate in financial markets while retaining full custody of their funds. However, the transparency of blockchain-based DEX in combination with the latency for transactions to be processed, makes market-manipulation feasible. For instance, adversaries could perform front-running -- the practice of exploiting (typically non-public) information tha… ▽ More Decentralized exchanges (DEXs) allow parties to participate in financial markets while retaining full custody of their funds. However, the transparency of blockchain-based DEX in combination with the latency for transactions to be processed, makes market-manipulation feasible. For instance, adversaries could perform front-running -- the practice of exploiting (typically non-public) information that may change the price of an asset for financial gain. In this work we formalize, analytically exposit and empirically evaluate an augmented variant of front-running: sandwich attacks, which involve front- and back-running victim transactions on a blockchain-based DEX. We quantify the probability of an adversarial trader being able to undertake the attack, based on the relative positioning of a transaction within a blockchain block. We find that a single adversarial trader can earn a daily revenue of over several thousand USD when performing sandwich attacks on one particular DEX -- Uniswap, an exchange with over 5M USD daily trading volume by June 2020. In addition to a single-adversary game, we simulate the outcome of sandwich attacks under multiple competing adversaries, to account for the real-world trading environment. △ Less

Submitted 29 September, 2020; originally announced September 2020.

FileBounty: Fair Data Exchange

Authors: Simon Janin, Kaihua Qin, Akaki Mamageishvili, Arthur Gervais

Abstract: Digital contents are typically sold online through centralized and custodian marketplaces, which requires the trading partners to trust a central entity. We present FileBounty, a fair protocol which, assuming the cryptographic hash of the file of interest is known to the buyer, is trust-free and lets a buyer purchase data for a previously agreed monetary amount, while guaranteeing the integrity of… ▽ More Digital contents are typically sold online through centralized and custodian marketplaces, which requires the trading partners to trust a central entity. We present FileBounty, a fair protocol which, assuming the cryptographic hash of the file of interest is known to the buyer, is trust-free and lets a buyer purchase data for a previously agreed monetary amount, while guaranteeing the integrity of the contents. To prevent misbehavior, FileBounty guarantees that any deviation from the expected participants' behavior results in a negative financial payoff; i.e. we show that honest behavior corresponds to a subgame perfect Nash equilibrium. Our novel deposit refunding scheme is resistant to extortion attacks under rational adversaries. If buyer and seller behave honestly, FileBounty's execution requires only three on-chain transactions, while the actual data is exchanged off-chain in an efficient and privacy-preserving manner. We moreover show how FileBounty enables a flexible peer-to-peer setting where multiple parties fairly sell a file to a buyer. △ Less

Submitted 9 July, 2021; v1 submitted 25 August, 2020; originally announced August 2020.

Comments: Simon Janin and Kaihua Qin contributed equally to this work

Applying Private Information Retrieval to Lightweight Bitcoin Clients

Authors: Kaihua Qin, Henryk Hadass, Arthur Gervais, Joel Reardon

Abstract: Lightweight Bitcoin clients execute a Simple Payment Verification (SPV) protocol to verify the validity of transactions related to a particular user. Currently, lightweight clients use Bloom filters to significantly reduce the amount of bandwidth required to validate a particular transaction. This is despite the fact that research has shown that Bloom filters are insufficient at preserving the pri… ▽ More Lightweight Bitcoin clients execute a Simple Payment Verification (SPV) protocol to verify the validity of transactions related to a particular user. Currently, lightweight clients use Bloom filters to significantly reduce the amount of bandwidth required to validate a particular transaction. This is despite the fact that research has shown that Bloom filters are insufficient at preserving the privacy of clients' queries. In this paper we describe our design of an SPV protocol that leverages Private Information Retrieval (PIR) to create fully private and performant queries. We show that our protocol has a low bandwidth and latency cost; properties that make our protocol a viable alternative for lightweight Bitcoin clients and other cryptocurrencies with a similar SPV model. In contract to Bloom filters, our PIR-based approach offers deterministic privacy to the user. Among our results, we show that in the worst case, clients who would like to verify 100 transactions occurring in the past week incurs a bandwidth cost of 33.54 MB with an associated latency of approximately 4.8 minutes, when using our protocol. The same query executed using the Bloom-filter-based SPV protocol incurs a bandwidth cost of 12.85 MB; this is a modest overhead considering the privacy guarantees it provides. △ Less

Submitted 25 August, 2020; originally announced August 2020.

ConFuzzius: A Data Dependency-Aware Hybrid Fuzzer for Smart Contracts

Authors: Christof Ferreira Torres, Antonio Ken Iannillo, Arthur Gervais, Radu State

Abstract: Smart contracts are Turing-complete programs that are executed across a blockchain. Unlike traditional programs, once deployed, they cannot be modified. As smart contracts carry more value, they become more of an exciting target for attackers. Over the last years, they suffered from exploits costing millions of dollars due to simple programming mistakes. As a result, a variety of tools for detecti… ▽ More Smart contracts are Turing-complete programs that are executed across a blockchain. Unlike traditional programs, once deployed, they cannot be modified. As smart contracts carry more value, they become more of an exciting target for attackers. Over the last years, they suffered from exploits costing millions of dollars due to simple programming mistakes. As a result, a variety of tools for detecting bugs have been proposed. Most of these tools rely on symbolic execution, which may yield false positives due to over-approximation. Recently, many fuzzers have been proposed to detect bugs in smart contracts. However, these tend to be more effective in finding shallow bugs and less effective in finding bugs that lie deep in the execution, therefore achieving low code coverage and many false negatives. An alternative that has proven to achieve good results in traditional programs is hybrid fuzzing, a combination of symbolic execution and fuzzing. In this work, we study hybrid fuzzing on smart contracts and present ConFuzzius, the first hybrid fuzzer for smart contracts. ConFuzzius uses evolutionary fuzzing to exercise shallow parts of a smart contract and constraint solving to generate inputs that satisfy complex conditions that prevent evolutionary fuzzing from exploring deeper parts. Moreover, ConFuzzius leverages dynamic data dependency analysis to efficiently generate sequences of transactions that are more likely to result in contract states in which bugs may be hidden. We evaluate the effectiveness of ConFuzzius by comparing it with state-of-the-art symbolic execution tools and fuzzers for smart contracts. Our evaluation on a curated dataset of 128 contracts and 21K real-world contracts shows that our hybrid approach detects more bugs (up to 23%) while outperforming state-of-the-art in terms of code coverage (up to 69%), and that data dependency analysis boosts bug detection up to 18%. △ Less

Submitted 10 March, 2021; v1 submitted 25 May, 2020; originally announced May 2020.

Attacking the DeFi Ecosystem with Flash Loans for Fun and Profit

Authors: Kaihua Qin, Liyi Zhou, Benjamin Livshits, Arthur Gervais

Abstract: Credit allows a lender to loan out surplus capital to a borrower. In the traditional economy, credit bears the risk that the borrower may default on its debt, the lender hence requires upfront collateral from the borrower, plus interest fee payments. Due to the atomicity of blockchain transactions, lenders can offer flash loans, i.e., loans that are only valid within one transaction and must be re… ▽ More Credit allows a lender to loan out surplus capital to a borrower. In the traditional economy, credit bears the risk that the borrower may default on its debt, the lender hence requires upfront collateral from the borrower, plus interest fee payments. Due to the atomicity of blockchain transactions, lenders can offer flash loans, i.e., loans that are only valid within one transaction and must be repaid by the end of that transaction. This concept has lead to a number of interesting attack possibilities, some of which were exploited in February 2020. This paper is the first to explore the implication of transaction atomicity and flash loans for the nascent decentralized finance (DeFi) ecosystem. We show quantitatively how transaction atomicity increases the arbitrage revenue. We moreover analyze two existing attacks with ROIs beyond 500k%. We formulate finding the attack parameters as an optimization problem over the state of the underlying Ethereum blockchain and the state of the DeFi ecosystem. We show how malicious adversaries can efficiently maximize an attack profit and hence damage the DeFi ecosystem further. Specifically, we present how two previously executed attacks can be "boosted" to result in a profit of 829.5k USD and 1.1M USD, respectively, which is a boost of 2.37x and 1.73x, respectively. △ Less

Submitted 20 March, 2021; v1 submitted 8 March, 2020; originally announced March 2020.

The Decentralized Financial Crisis

Authors: Lewis Gudgeon, Daniel Perez, Dominik Harz, Benjamin Livshits, Arthur Gervais

Abstract: The Global Financial Crisis of 2008, caused by the accumulation of excessive financial risk, inspired Satoshi Nakamoto to create Bitcoin. Now, more than ten years later, Decentralized Finance (DeFi), a peer-to-peer financial paradigm which leverages blockchain-based smart contracts to ensure its integrity and security, contains over 702m USD of capital as of April 15th, 2020. As this ecosystem dev… ▽ More The Global Financial Crisis of 2008, caused by the accumulation of excessive financial risk, inspired Satoshi Nakamoto to create Bitcoin. Now, more than ten years later, Decentralized Finance (DeFi), a peer-to-peer financial paradigm which leverages blockchain-based smart contracts to ensure its integrity and security, contains over 702m USD of capital as of April 15th, 2020. As this ecosystem develops, it is at risk of the very sort of financial meltdown it is supposed to be preventing. In this paper we explore how design weaknesses and price fluctuations in DeFi protocols could lead to a DeFi crisis. We focus on DeFi lending protocols as they currently constitute most of the DeFi ecosystem with a 76% market share by capital as of April 15th, 2020. First, we demonstrate the feasibility of attacking Maker's governance design to take full control of the protocol, the largest DeFi protocol by market share, which would have allowed the theft of 0.5bn USD of collateral and the minting of an unlimited supply of DAI tokens. In doing so, we present a novel strategy utilizing so-called flash loans that would have in principle allowed the execution of the governance attack in just two transactions and without the need to lock any assets. Approximately two weeks after we disclosed the attack details, Maker modified the governance parameters mitigating the attack vectors. Second, we turn to a central component of financial risk in DeFi lending protocols. Inspired by stress-testing as performed by central banks, we develop a stress-testing framework for a stylized DeFi lending protocol, focusing our attention on the impact of a drying-up of liquidity on protocol solvency. Based on our parameters, we find that with sufficiently illiquidity a lending protocol with a total debt of 400m USD could become undercollateralized within 19 days. △ Less

Submitted 27 June, 2020; v1 submitted 19 February, 2020; originally announced February 2020.

Securify: Practical Security Analysis of Smart Contracts

Authors: Petar Tsankov, Andrei Dan, Dana Drachsler Cohen, Arthur Gervais, Florian Buenzli, Martin Vechev

Abstract: Permissionless blockchains allow the execution of arbitrary programs (called smart contracts), enabling 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 problem, we present Securify, a security analyzer for Ethereum smart contr… ▽ More Permissionless blockchains allow the execution of arbitrary programs (called smart contracts), enabling 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 problem, we present Securify, a security analyzer for Ethereum smart contracts that is scalable, fully automated, and able to prove contract behaviors as safe/unsafe with respect to a given property. Securify's analysis consists of two steps. First, it symbolically analyzes the contract's dependency graph to extract precise semantic information from the code. Then, it checks compliance and violation patterns that capture sufficient conditions for proving if a property holds or not. To enable extensibility, all patterns are specified in a designated domain-specific language. Securify is publicly released, it has analyzed >18K contracts submitted by its users, and is regularly used to conduct security audits by experts. We present an extensive evaluation of Securify over real-world Ethereum smart contracts and demonstrate that it can effectively prove the correctness of smart contracts and discover critical violations. △ Less

Submitted 24 August, 2018; v1 submitted 4 June, 2018; originally announced June 2018.