FORAY: Towards Effective Attack Synthesis against Deep Logical Vulnerabilities in DeFi Protocols

TL;DR

This work introduces FORAY, a highly effective attack synthesis framework against deep logical bugs in DeFi protocols and significantly outperforms Halmos and ItyFuzz, the state-of-the-art (SOTA) tools for smart contract vulnerability detection, in both effectiveness and efficiency.

Abstract

Blockchain adoption has surged with the rise of Decentralized Finance (DeFi) applications. However, the significant value of digital assets managed by DeFi protocols makes them prime targets for attacks. Current smart contract vulnerability detection tools struggle with DeFi protocols due to deep logical bugs arising from complex financial interactions between multiple smart contracts. These tools primarily analyze individual contracts and resort to brute-force methods for DeFi protocols crossing numerous smart contracts, leading to inefficiency. We introduce Foray, a highly effective attack synthesis framework against deep logical bugs in DeFi protocols. Foray proposes a novel attack sketch generation and completion framework. Specifically, instead of treating DeFis as regular programs, we design a domain-specific language (DSL) to lift the low-level smart contracts into their high-level financial operations. Based on our DSL, we first compile a given DeFi protocol into a token flow graph, our graphical representation of DeFi protocols. Then, we design an efficient sketch generation method to synthesize attack sketches for a certain attack goal (e.g., price manipulation, arbitrage, etc.). This algorithm strategically identifies candidate sketches by finding reachable paths in TFG, which is much more efficient than random enumeration. For each candidate sketch written in our DSL, Foray designs a domain-specific symbolic compilation to compile it into SMT constraints. Our compilation simplifies the constraints by removing redundant smart contract semantics. It maintains the usability of symbolic compilation, yet scales to problems orders of magnitude larger. Finally, the candidates are completed via existing solvers and are transformed into concrete attacks via direct syntax transformation.

Figures (9)

• Figure 1: Illustration of MUMUG and a concrete exploit against it. depth .1 IERC20().transferFrom and depth .1 IERC20().transfer are standard APIs that enable the withdraw and deposit of tokens for one address. depth .1 uniswap.getAmountIn and depth .1 uniswap.getAmountOut are depth .1 uniswap APIs that calculate the required amount to swap one type of token for another based on their current reserves.
• Figure 2: Overview of Foray with the demonstrated completed sketch for the example in \ref{['fig:motivating']}. In the sketch, depth .1 swap$^1$ refers to the depth .1 mn_bond function. depth .1 swap$^2$ is achieved through the depth .1 uniswap.swap function.
• Figure 3: Demonstration of token flow graph construction, graph reachability, and valid attack sketch of MUMUG in \ref{['fig:motivating']}. In the TFG, the token nodes (except $\epsilon\xspace$) represent tokens owned by the attacker and edges are financial operators (constructs in abstract financial language).
• Figure 4: Syntax for our abstract financial language.
• Figure 5: Flow predicates inference rules. $\bullet$ indicates a special address. Note that mint and burn has an implicit constraint that $a$ must belong to a set of authorized addresses.

Theorems & Definitions (1)

• definition 1: DeFi Attack Synthesis