Protocol Security
Tutorial - Real-World Integration
Hardening a lending protocol.
Tutorial: Hardening a Lending Protocol
In this tutorial, we will add a Solvency Check to a lending market.
Goal: Ensure that no transaction can leave the protocol with TotalDebt > TotalCollateral.
Prerequisites
- A deployed Lending Market contract (we'll use a mock address).
- Matador CLI.
Solvency checks protect the whole market
This guard applies to every user action, so solvency remains enforced even if core logic changes.
Step 1: Write the Solvency Policy
solvency.matador:
import "abis/MarketLens.json" as Market;
permission SolvencyGuard -> 1.0.0 {
parameters: {
market: address,
minCollateralRatioBps: uint256
}
when: {
context.target == parameters.market,
Market.getTotalCollateral() >= parameters.minCollateralRatioBps,
Market.getTotalDebt() > 0
}
}Step 2: Compile
matador compile solvency.matador --out ./outStep 3: Install
We attach this policy to the User Role. Every user interaction (borrow, withdraw, transfer) must pass this check.
Step 4: Verification
- Scenario A (Safe Borrow): User borrows 50 USDC against 100 ETH.
- Post-state: Collateral >> Debt.
- Result: Approved.
- Scenario B (Exploit Attempt): User finds a bug that lets them withdraw all collateral without repaying debt.
- Execution happens (in simulation).
- Matador runs
check_after. - Post-state:
TotalCollateralis 0.TotalDebtis > 0. - Invariant fails.
- Result: REVERT.
The protocol is saved from the exploit, even though the exploit existed in the Solidity code.