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

TL;DR

Foray introduces a novel framework for synthesizing effective attacks on deep logical vulnerabilities in DeFi protocols by leveraging a high-level domain-specific language, token flow graphs, and symbolic compilation, significantly improving efficiency over existing methods.

Contribution

The paper presents a new attack synthesis framework that models DeFi protocols with a domain-specific language and token flow graphs, enabling scalable and efficient attack generation.

Findings

Successfully synthesizes attacks for complex DeFi protocols.

Outperforms brute-force methods in efficiency and scalability.

Demonstrates effectiveness on real-world DeFi vulnerabilities.

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.