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

• URL: http://arxiv.org/abs/2407.06348v2
• Date: Sat, 31 Aug 2024 01:48:25 GMT
• Title: FORAY: Towards Effective Attack Synthesis against Deep Logical Vulnerabilities in DeFi Protocols
• Authors: Hongbo Wen, Hanzhi Liu, Jiaxin Song, Yanju Chen, Wenbo Guo, Yu Feng,
• Abstract summary: We introduce Foray, a highly effective attack synthesis framework against deep logical bugs in DeFi protocols. 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.
• Score: 7.413607595641641
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• A Realistic Threat Model for Large Language Model Jailbreaks [87.64278063236847]
  In this work, we propose a unified threat model for the principled comparison of jailbreak attacks. Our threat model combines constraints in perplexity, measuring how far a jailbreak deviates from natural text. We adapt popular attacks to this new, realistic threat model, with which we, for the first time, benchmark these attacks on equal footing.
  arXiv  Detail & Related papers  (2024-10-21T17:27:01Z)
• ZKFault: Fault attack analysis on zero-knowledge based post-quantum digital signature schemes [0.32248805768155825]
  We show that we can recover the entire secret key of LESS and CROSS using as little as a single fault. In this work, we first analyze the LESS signature scheme and devise our attack. Furthermore, we showed how this attack can be extended to the CROSS signature scheme.
  arXiv  Detail & Related papers  (2024-09-11T09:54:45Z)
• Theorem-Carrying-Transaction: Runtime Certification to Ensure Safety for Smart Contract Transactions [8.32630869646569]
  We present a viable technological roadmap for the community toward this ambitious goal. Our technology, called Theorem-Carrying-Transaction (TCT), combines the benefits of concrete execution and symbolic proofs. Our prototype incurs a negligible runtime overhead, two orders of magnitude lower than a state-of-the-art approach.
  arXiv  Detail & Related papers  (2024-08-12T20:27:41Z)
• Effective Targeted Testing of Smart Contracts [0.0]
  Since smart contracts are immutable, their bugs cannot be fixed, which may lead to significant monetary losses. Our framework, Griffin, tackles this deficiency by employing a targeted symbolic execution technique for generating test data. This paper discusses how smart contracts differ from legacy software in targeted symbolic execution and how these differences can affect the tool structure.
  arXiv  Detail & Related papers  (2024-07-05T04:38:11Z)
• LookAhead: Preventing DeFi Attacks via Unveiling Adversarial Contracts [15.071155232677643]
  Decentralized Finance (DeFi) incidents have resulted in financial damages exceeding 3 billion US dollars. Current detection tools face significant challenges in identifying attack activities effectively. We propose a new direction for detecting DeFi attacks that focuses on identifying adversarial contracts.
  arXiv  Detail & Related papers  (2024-01-14T11:39:33Z)
• Versatile Weight Attack via Flipping Limited Bits [68.45224286690932]
  We study a novel attack paradigm, which modifies model parameters in the deployment stage. Considering the effectiveness and stealthiness goals, we provide a general formulation to perform the bit-flip based weight attack. We present two cases of the general formulation with different malicious purposes, i.e., single sample attack (SSA) and triggered samples attack (TSA)
  arXiv  Detail & Related papers  (2022-07-25T03:24:58Z)
• Detecting DeFi Securities Violations from Token Smart Contract Code [0.4263043028086136]
  Decentralized Finance (DeFi) is a system of financial products and services built and delivered through smart contracts on various blockchains. This study aims to uncover whether we can identify DeFi projects potentially engaging in securities violations based on their tokens' smart contract code.
  arXiv  Detail & Related papers  (2021-12-06T01:44:08Z)
• Transferable Sparse Adversarial Attack [62.134905824604104]
  We introduce a generator architecture to alleviate the overfitting issue and thus efficiently craft transferable sparse adversarial examples. Our method achieves superior inference speed, 700$times$ faster than other optimization-based methods.
  arXiv  Detail & Related papers  (2021-05-31T06:44:58Z)
• ESCORT: Ethereum Smart COntRacTs Vulnerability Detection using Deep Neural Network and Transfer Learning [80.85273827468063]
  Existing machine learning-based vulnerability detection methods are limited and only inspect whether the smart contract is vulnerable. We propose ESCORT, the first Deep Neural Network (DNN)-based vulnerability detection framework for smart contracts. We show that ESCORT achieves an average F1-score of 95% on six vulnerability types and the detection time is 0.02 seconds per contract.
  arXiv  Detail & Related papers  (2021-03-23T15:04:44Z)
• Online Adversarial Attacks [57.448101834579624]
  We formalize the online adversarial attack problem, emphasizing two key elements found in real-world use-cases. We first rigorously analyze a deterministic variant of the online threat model. We then propose algoname, a simple yet practical algorithm yielding a provably better competitive ratio for $k=2$ over the current best single threshold algorithm.
  arXiv  Detail & Related papers  (2021-03-02T20:36:04Z)
• Composite Adversarial Attacks [57.293211764569996]
  Adversarial attack is a technique for deceiving Machine Learning (ML) models. In this paper, a new procedure called Composite Adrial Attack (CAA) is proposed for automatically searching the best combination of attack algorithms. CAA beats 10 top attackers on 11 diverse defenses with less elapsed time.
  arXiv  Detail & Related papers  (2020-12-10T03:21:16Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.