Formal Multi-Protocol DeFi Vulnerability Detection
Like a compound eye that sees from many angles simultaneously, this tool analyzes DeFi protocol interactions from multiple perspectives to detect vulnerabilities invisible to single-contract analyzers.
Current security tools detect only ~8% of DeFi attacks (research). Why?
- Single-contract focus: Slither, Mythril analyze one contract at a time
- Two-contract limit: DeFiTail only handles 2 contracts
- No formal semantics: Tools use pattern matching/ML, missing novel attack vectors
- Static-only: Flash loan attacks exploit dynamic, runtime composability
Example attack current tools miss:
1. Flash loan WETH from Aave
2. Swap WETH→Token on Uniswap (moves price)
3. Borrow Token on Compound (uses manipulated price)
4. Price returns to normal
5. Liquidate own position, profit from price delta
6. Repay flash loan
This crosses 3+ protocols with complex economic dependencies.
Compound Eye is a Rust-based formal analyzer that:
- Models DeFi primitives formally - Not bytecode patterns, but semantic operations
- Builds multi-protocol dependency graphs - Track how protocols interact
- Uses symbolic execution - Find attack paths across protocol boundaries
- Detects economic vulnerabilities - Price manipulation, oracle attacks, liquidation exploits
# Clone the repository
git clone https://github.com/luishsr/compound-eye-defi
cd compound-eye
# Build release version
cargo build --release
# The binary will be at ./target/release/compound-eye- Rust 1.75+
- (Optional) Z3 SMT solver for advanced symbolic execution
# List available protocol models
compound-eye list
# Analyze protocol interactions
compound-eye analyze --protocols aave-v3 uniswap-v3 chainlink
# Initialize a custom protocol specification
compound-eye init "My Protocol" Lending ./
# Visualize dependency graph
compound-eye graph --protocols aave-v3 compound-v3 chainlink -o deps.dot$ compound-eye analyze --protocols aave-v3 uniswap-v3 chainlink
Compound Eye - DeFi Composability Vulnerability Analyzer
Starting analysis...
→ Loading 3 protocol(s)
→ Building dependency graph...
4 protocols, 3 dependencies
✓ Analysis completed in 0.12s
2 vulnerabilities found (1 critical, 1 high)
[CRITICAL] Oracle Price Manipulation → Liquidation
Path:
1. Flash loan 10,000 ETH from Aave
2. Swap ETH→USDC on Uniswap (moves TWAP)
3. Aave reads Uniswap TWAP for ETH price
4. Positions become undercollateralized
5. Liquidate positions, extract profit
6. Repay flash loan
Mitigation: Use Chainlink oracle instead of Uniswap TWAP
[HIGH] Shared Oracle Liquidation Risk
Multiple lending protocols share the same oracle...
┌────────────────────────────────────────────────────────────────────────┐
│ Compound Eye │
├────────────────────────────────────────────────────────────────────────┤
│ ┌─────────────────┐ ┌─────────────────┐ ┌─────────────────────┐ │
│ │ Protocol │ │ Dependency │ │ Vulnerability │ │
│ │ Modeler │──▶│ Graph Builder │──▶│ Detector │ │
│ │ (DeFi DSL) │ │ (Multi-proto) │ │ (Symbolic exec) │ │
│ └─────────────────┘ └─────────────────┘ └─────────────────────┘ │
└────────────────────────────────────────────────────────────────────────┘
| Crate | Description |
|---|---|
compound-eye-core |
DeFi DSL, protocol abstractions, dependency graph |
compound-eye-models |
Protocol implementations (Aave, Uniswap, Chainlink, etc.) |
compound-eye-analyzer |
Vulnerability patterns, symbolic execution engine |
compound-eye-indexer |
On-chain data fetching and state reconstruction |
compound-eye-cli |
Command-line interface |
- Aave V3
- Compound V3
- MakerDAO
- Uniswap V3
- Curve Finance
- Chainlink
Create a TOML specification file:
# my-protocol.toml
id = "my-protocol"
name = "My Protocol"
protocol_type = "Lending"
version = "1.0"
chain_id = 1
[[contracts]]
name = "Main"
address = "0x..."
[[assets]]
symbol = "TOKEN"
address = "0x..."
decimals = 18
is_collateral = true
[[dependencies]]
target = "chainlink"
dep_type = "OraclePrice"
description = "Uses Chainlink for price feeds"Then analyze:
compound-eye analyze --protocols ./my-protocol.toml chainlinkCompound Eye detects these attack patterns:
| Pattern | Description |
|---|---|
| Oracle Manipulation | DEX-based oracles that can be manipulated via swaps |
| Flash Loan Amplification | Attacks amplified by flash loan capital |
| Liquidation Cascades | Shared oracle dependencies causing mass liquidations |
| Cross-Protocol Reentrancy | Callback-based reentrancy across protocol boundaries |
# Run tests
cargo test
# Run with debug logging
RUST_LOG=debug cargo run -- analyze --protocols aave-v3
# Build documentation
cargo doc --open| Tool | Approach | Contracts | Formal? | Open Source |
|---|---|---|---|---|
| Slither | Static analysis | 1 | No | Yes |
| DeFiTail | Deep learning | 2 | No | No |
| FlashSyn | Attack synthesis | N | No | Research |
| Compound Eye | Formal semantics + symbolic | Unlimited | Yes | Yes |
- Core DSL and protocol abstractions
- Multi-protocol dependency graph
- Pattern-based vulnerability detection
- Symbolic execution engine
- Real-time monitoring mode
- Historical exploit replay validation
- Web dashboard
- Additional protocol models
Contributions are welcome! Please see CONTRIBUTING.md for guidelines.
Licensed under either of:
- Apache License, Version 2.0 (LICENSE-APACHE or http://www.apache.org/licenses/LICENSE-2.0)
- MIT license (LICENSE-MIT or http://opensource.org/licenses/MIT)
at your option.
This project builds on research from:
This tool is for security research and educational purposes. Always obtain proper authorization before testing on live systems.