Safeguarding DeFi Smart Contracts against Oracle Deviations

TL;DR

This paper tackles the problem that DeFi protocols depend on external oracle values, which can deviate and jeopardize safety. It introduces OVer, a framework that performs symbolic analysis of smart contract code, summarizes complex loops with a novel accumulation-based approach, and builds SMT-based models to compute safe oracle-deviation bounds and parameter settings, optionally inserting guard statements. The authors present a new loop-summarization technique, demonstrate soundness through formal constraint extraction, and validate OVer on nine real-world DeFi protocols plus a fictional one, showing that default parameters are often unsafe under historical deviations. The work provides developers with a practical tool to derive robust risk controls and improve the resilience of DeFi protocols against oracle manipulation.

Abstract

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 also illustrates that current parameters utilized in the majority of benchmarks are inadequate to ensure safety when confronted with significant oracle deviations.

Figures (4)

• Figure 1: Compound protocol borrow logic simplified.
• Figure 2: Compound analysis summary
• Figure 3: Overview of the proposed framework
• Figure 4: Function summary extraction rules.