Description
Abstract: This work 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.
We implement Over based on the *Slither* static analysis tool in *Python* for Solidity based smart contracts. To solve the optimization problems, we leverage the SMT solver *Z3*.
We answer three research questions.
- Are current control parameters of Defi protocols safe under large oracle deviations?
- Can Over efficiently analyze various Defi protocols that use oracles?
- Can Over assist developers to design safe Defi protocols that use oracles?
Empirical results show current parameters utilized in the majority of benchmarks are inadequate to ensure safety when confronted with significant oracle deviations. Over can successfully analyze all 10 benchmarks collected, which encompass a diverse range of DeFi protocols. The results also demonstrate how Over can help developers to design safe protocols.
Replication file for conference paper published in ICSE '24: Proceedings of the IEEE/ACM 46th International Conference on Software Engineering. Paper published online April 12, 2024. When citing this dataset, please also cite the associated article. A sample Publication Citation is provided below.
We implement Over based on the *Slither* static analysis tool in *Python* for Solidity based smart contracts. To solve the optimization problems, we leverage the SMT solver *Z3*.
We answer three research questions.
- Are current control parameters of Defi protocols safe under large oracle deviations?
- Can Over efficiently analyze various Defi protocols that use oracles?
- Can Over assist developers to design safe Defi protocols that use oracles?
Empirical results show current parameters utilized in the majority of benchmarks are inadequate to ensure safety when confronted with significant oracle deviations. Over can successfully analyze all 10 benchmarks collected, which encompass a diverse range of DeFi protocols. The results also demonstrate how Over can help developers to design safe protocols.
Replication file for conference paper published in ICSE '24: Proceedings of the IEEE/ACM 46th International Conference on Software Engineering. Paper published online April 12, 2024. When citing this dataset, please also cite the associated article. A sample Publication Citation is provided below.