一句话：提出 OVer 框架，用符号分析与 SMT 求解自动分析预言机偏差下的 DeFi 协议安全性并生成防护语句。
本文针对 DeFi 协议中预言机输入被操纵或发生显著偏差时的安全问题，提出自动分析框架 OVer。OVer 首先对给定合约进行符号分析，构建约束模型，再借助 SMT 求解器搜索能使协议保持安全运行的参数；对于依赖预言机取值的智能合约，还可生成 guard 语句，以阻止预言机操纵攻击。作者在 10 个涵盖多种 DeFi 协议的基准上评估 OVer，结果显示其均能成功分析。论文进一步表明，多数基准当前采用的参数在预言机大幅偏差时不足以保障安全，而引入延迟等临时控制机制往往无效甚至有害。
This paper presents OVer, a framework designed to automatically analyze the behavior of decentralized finance (DeFi) protocols when subjected to a "skewed" oracle input. OVer firstly performs symbolic analysis on the given contract and constructs a model of constraints. Then, the framework leverages an SMT solver to identify parameters that allow its secure operation. Furthermore, guard statements may be generated for smart contracts that may use the oracle values, thus effectively preventing oracle manipulation attacks. Empirical results show that OVer can successfully analyze all 10 benchmarks collected, which encompass a diverse range of DeFi protocols. Additionally, this paper illustrates that current parameters utilized in the majority of benchmarks are inadequate to ensure safety when confronted with significant oracle deviations. It shows that existing ad-hoc control mechanisms such as introducing delays are often in-sufficient or even detrimental to protect the DeFi protocols against the oracle deviation in the real-world.
@inproceedings{paperbot11305,
title = {Safeguarding DeFi Smart Contracts against Oracle Deviations},
author = {Xun Deng and Sidi Mohamed Beillahi and Cyrus Minwalla and Han Du and Andreas Veneris and Fan Long},
booktitle = {ICSE},
year = {2024},
doi = {10.1145/3597503.3639225}
}