Last week’s Auditor’s Take walked through the ResupplyFi bug in detail: an ERC-4626 oracle vulnerable to share-price inflation, a division that rounded down to zero, a solvency check that read the zero as “safe.” $9.6M lost in a single transaction.
This post asks a different question. Could a static analyzer have flagged the pattern before audit? Could a fuzzer have confirmed the exploit before the market opened? With the AuditHub Approach, yes.
What is the AuditHub Approach
The AuditHub Approach is our systematic detection approach for the classes of vulnerabilities manual review is hard to reason about in an exhaustive way. Generally, this method allows development teams to define automated checks tailored to their protocol in a programmatic way. For DeFi protocol, like ResupplyFi, this is manifested with the following 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 formal invariants against real contract state to confirm whether a flagged pattern is actually exploitable.
Static analysis is fast and exhaustive but produces false positives. It tells you where a bug could be, not whether it is. Fuzzing is precise but slow without a target. The combination is what makes the method work, and it is what catches bugs of the shape that drained ResupplyFi.
TL;DR
- Vanguard, our static analyzer, can flag the suspicious structure: division feeding multiplication through a storage variable in a critical solvency check.
- Static-analyzer warnings are not always real bugs. Confirming exploitability needs a dynamic technique like fuzzing.
- OrCa, our fuzzer, confirms the bug by exercising the deployed market state against an invariant expressed in our V specification language, producing a counter-example.
- Custom static detectors plus specification-guided fuzzing closes the gap between “this code looks suspicious” and “this code is exploitable.”
- Both checks are configurable per protocol and re-runnable on every commit.
How Vanguard can flag the pattern
Vanguard analyzes Solidity code without running it, matching patterns defined in a user-written detector tailored to the protocol’s logic. For the ResupplyFi class, the shape is roughly: a division whose result eventually feeds a multiplication through a state variable. Here is the custom detector:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 |
FIND Contract c, -- Find a division that writes into a storage variable Function divFunction IN c, DivideExpression div IN divFunction, Expression expr IN div.forwardSlices, StorageWrite writeEffect IN expr, -- Find a multiplication that depends on a storage read Function mulFunction IN c, Expression readExpr IN mulFunction, StorageRead readEffect IN readExpr, MultiplyExpression mul IN readExpr.interprocForwardSlices WHERE writeEffect.location == readEffect.location |
A generic “division before multiplication” detector exists in many Solidity static analyzers. None would have caught this one. They only report the pattern when it appears within a single function on local state. The custom detector above looks across functions and follows the data through a storage variable, both of which are necessary to see the ResupplyFi bug:
|
1 2 3 4 |
Divide-before-multiply through storage variable exchangeRateInfo.exchangeRate Result of division operation ResupplyPairCore._updateExchangeRate @ src/protocol/pair/ResupplyPairCore.sol:573:25 is used in multiplication operation ResupplyPairCore._isSolvent @ src/protocol/pair/ResupplyPairCore.sol:282:26 via storage variable exchangeRateInfo.exchangeRate |
Static analysis detects suspicious structural patterns by exhaustively exploring all execution paths in a program. It does not run the code, so it cannot tell you whether the suspicious shape is exploitable, or whether the surrounding logic protects against a potential attack. Some warnings will be false positives.
That is the cost of working at the structural layer rather than the execution layer. The benefit is that the check runs in seconds on every commit, which is the right cadence for a rate-or-solvency code path that should be considered high-risk by default. Let’s now see how a fuzzer can help us confirm that the above warning is indeed exploitable.
How OrCa confirms the exploit
OrCa is our fuzzer. It runs against a V Spec, a formal statement of an invariant the contract should preserve. For ResupplyFi, the invariant is straightforward: no borrow should succeed when the resulting loan-to-value ratio exceeds the configured maximum.
|
1 2 3 4 5 6 7 8 9 10 11 12 13 |
# One should never be able to remove collateral or borrow such that their loan-to-value ratio (LTV) exceeds the maximum allowed LTV. vars: ResupplyPair r, MockOracle o spec: []!( finished(r.removeCollateral, r.userBorrowShares(sender) * r.EXCHANGE_PRECISION() > o.price() * r.userCollateralBalance(sender) && r.maxLTV() <= 10000 ) || finished(r.removeCollateralVault, r.userBorrowShares(sender) * r.EXCHANGE_PRECISION() > o.price() * r.userCollateralBalance(sender) && r.maxLTV() <= 10000 ) || finished(r.borrow, r.userBorrowShares(sender) * r.EXCHANGE_PRECISION() > o.price() * r.userCollateralBalance(sender) && r.maxLTV() <= 10000 ) ) |
The V Spec above is exactly what OrCa ran. It says a user should never complete a borrow or remove-collateral operation where the value of their borrow exceeds the value of their collateral.
For the ResupplyFi market on local deployment, OrCa found a violation to the loan-to-value ratio invariant in under 10 minutes. More on V Spec syntax in the AuditHub documentation. Anyone with the source code and the V Spec can reproduce that locally. Static analysis points at the suspicious path. Fuzzing confirms whether the worry was justified.
A takeaway for developers
Every lending protocol that prices collateral through an ERC-4626 vault is exposed to the same pattern. Two parts: an oracle path that lets share-price inflation reach the rate calculation, and a solvency check that reads a degenerate rate as safe.
Both parts are checkable with tooling. Write a custom Vanguard detector for the rate-and-solvency path so any future change to that math is flagged at every commit. Express the LTV invariant as a V Spec and run OrCa against the deployed market before user funds arrive. The alternative is to launch on mainnet after a handful of auditors went over the code in a time-boxed engagement.
Audit firms can run the same method to scale coverage without scaling the team. If you want to set this up for your protocol, try AuditHub or book a demo to walk through the configuration for your specific market architecture.