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

随着去中心化金融（DeFi）应用的兴起，区块链的应用已经激增。然而，由于DeFi协议管理的数字资产价值巨大，因此它们成为攻击的主要目标。由于多个智能合约之间的复杂金融交互引起的深层逻辑漏洞，目前的智能合约漏洞检测工具难以处理DeFi协议。这些工具主要分析单个合约，对于跨越多个智能合约的DeFi协议，采用暴力方法，导致效率低下。我们介绍了Foray，这是一个高效的攻击合成框架，用于针对DeFi协议中的深层逻辑漏洞。Foray提出了一种新颖的攻击草图生成和完成框架。具体来说，我们设计了一种领域特定语言（DSL），将低级智能合约提升到高级金融操作的水平，而不是将DeFi视为常规程序。基于我们的DSL，我们首先将给定的DeFi协议编译成代币流图，即我们对DeFi协议的图形表示。然后，我们设计了一种有效的草图生成方法，以合成特定攻击目标（例如价格操纵，套利等）的攻击草图。该算法通过在TFG中查找可达路径来策略性地识别候选草图，这比随机枚举要高效得多。对于我们DSL中编写的每个候选草图，Foray设计了一种领域特定符号编译，将其编译为SMT约束。我们的编译通过去除冗余的智能合约语义来简化约束。它保持了符号编译的可用性，但可以扩展到大量的问题。最后，通过现有的求解器完成候选草图，并通过直接语法转换将其转化为具体攻击。

提高智能合约漏洞检测工具的效率，以应对DeFi协议中复杂的金融交互逻辑所带来的深层次逻辑漏洞。

设计一种针对DeFi协议的攻击综合框架Foray，通过领域特定语言DSL将智能合约提升为高级金融操作，将DeFi协议编译成令牌流图TFG，使用高效的草图生成方法来合成攻击草图，通过DSL符号编译将草图编译成SMT约束，通过现有的求解器将候选草图完成并转化为具体攻击。

论文提出了一种针对DeFi协议的攻击综合框架，通过DSL将智能合约提升为高级金融操作，能够有效地解决DeFi协议中复杂的逻辑漏洞问题。论文在多个数据集上进行了实验，并与现有的工具进行了比较，结果表明Foray在效率和准确性方面都有显著提高。论文还开源了代码，方便其他研究者进行使用和改进。

相关研究包括但不限于：1. Mythril：一种智能合约安全分析工具；2. Securify：一种基于符号执行的智能合约安全分析工具；3. Maru：一种用于检测智能合约中的逻辑漏洞的工具。