A routine upgrade left one Euler function free to reduce collateral with no health check at the end. A custom detector flags exactly that omission at commit time.
Pre-Mortem is a weekly series by Kostas Ferles, CTO of AuditHub. This article looks at a solvency check that every fund-moving function ran except one, and the automated pass that catches the omission before deployment. New breakdown every week. Find Kostas at @KFerles.
Jon Stephens just covered this bug in the Auditor’s Take: how a senior auditor catches the one Euler function missing the health check the rest of the functions had. That article prompted this one. If an auditor can catch that by reading the code, a detector should catch it automatically, on every commit. So here is the deep dive from the AuditHub side: could a static analyzer have flagged the missing check before it ever reached audit?
TL;DR
- Euler’s
donateToReservescut a caller’s collateral without thecheckLiquiditycall every other function ran. - Vanguard flags any function that writes a balance without reaching the
checkLiquiditycall. - Run on Euler’s EToken contract, the detector returns exactly one function:
donateToReserves. - The detector is configurable per protocol and re-runs on every commit, before production.
What is the AuditHub Approach
The AuditHub Approach is how we systematically catch the classes of bugs that manual review struggles to reason about exhaustively. It lets a team define automated checks tailored to their own protocol, in code, so the reasoning a reviewer does once keeps running. For a lending protocol like Euler, it rests on two pillars.
The first is custom static analysis: per-protocol detectors that flag suspicious structural patterns at commit time. The second is specification-guided fuzzing: running a formal invariant against real contract state to confirm whether a flagged pattern is actually exploitable.
Static analysis is fast and exhaustive, but it works at the structural layer, so it tells you where a bug could be, not whether it is. Fuzzing works at the execution layer and answers exploitability, but it is slow without a target to aim at. The combination is the point, though which pillar carries a given case depends on the bug. The SuperRare bug in an earlier Pre-Mortem was source-shaped, and one static pass settled it. Euler’s donateToReserves is the same kind of case: the detector below settles exactly where the check is missing.
How Vanguard flags the missing check
Vanguard analyzes Solidity without running it, matching patterns defined in a detector written for the protocol’s own logic. The property is simple to state: any externally callable function that changes a user’s balance has to reach a checkLiquidity call before it returns. The detector encodes exactly that and flags any function that violates it.
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
FIND Function f IN Contract c, StorageWrite w IN f.reachable WHERE c.name == "EToken", f.isExternallyCallable, regexMatch(w.location, ".*users.*balance"), !EXISTS InternalCall liq IN f.reachable WHERE { liq.callee.name == "checkLiquidity" } AS contract = c, function = f, balanceWrite = w, |
The query keeps every externally callable function on the EToken contract that writes a user’s balance and does not reach a checkLiquidity call anywhere in its execution. This is interprocedural: it follows the balance write and the check across function boundaries, not just within one body. Run against that contract, the detector reports a single function:
|
1 2 3 |
Function EToken.donateToReserves writes the user balance without any reachable checkLiquidity call. |
What static analysis cannot tell you is whether that missing check actually leads to a loss. A function can skip a guard and still be safe if nothing downstream can push the account past the boundary. For Euler, that comes down to leverage and liquidation elsewhere in the protocol, which the companion Auditor’s Take walks through in full.
A takeaway for developers
Any protocol that enforces a safety invariant by having each function remember to call the same check is one commit away from the same failure. The moment someone adds an entry point and forgets the call, the invariant holds everywhere else but not on that new function.
A custom Vanguard detector written for this invariant catches the same mistake the next time it happens, flagging any new function that touches a balance without reaching the guard, on every commit. Pair it with a V Spec run against the deployed market, so what the detector flags is confirmed exploitable before user funds arrive, not after. Better still, enforce the invariant by construction: route the health check through a single point every state-changing path has to cross, so no new function can skip it. Euler itself moved in that direction in a later version.
Run these on every commit, not once, because of timing. An audit is a snapshot of the code the reviewers saw, and donateToReserves landed in an upgrade well after Euler’s core was first audited. The code keeps changing; the invariant does not. So the check belongs on every push, not in a single review.
Want checks like this running on your codebase?
One missing call turned a donation function into a $197M drain. If you want a detector like this, and the fuzzing that confirms it, running on your protocol on every commit, try AuditHub for free or book a demo.
