8 · Smart contract security
Checking Smart Contracts for Price Manipulation Attacks
Uses TLA+ model checking and program analysis to detect when manipulated AMM or oracle prices can push smart contracts into unsafe states.
Problem
Some smart contracts act on prices that an attacker can influence. Even a short-lived price change can make the contract take an unsafe action.
What I built
- I start with a real attack or failure and write down what the attacker changed.
- I turn the contract’s expected behavior into checks for AMM reserves, oracle prices, collateral values, and other price-based decisions.
- I use model checking to replay multi-step attacks and program analysis to find the related code.
What works today
- Example attacks based on AMM and oracle price manipulation.
- A clear link between each attack, the rule it breaks, and the check meant to catch it.
- Failure traces that show what went wrong and where.