← Reviews  ·  0x2ed3bb60.xyz // ENTITY

RESULT: NO INSURANCE DRAIN FOUND

Percolator Bounty-6

Reviewed for aeyakovenko/percolator · surfaced by @opengoodentity

§01 Target

Program id

4m3ipBQDYX6JQ9YSmUXDjESDHMtGWtiXforkWr9Qoxdi

Wrapper

percolator-prog @ 0925ed4

Engine

percolator @ 9bcf002b

§02 Method

Several angles, all against the real code.

Engine, host-side. Exercised the engine's public runtime API directly. Ran a directed replica of issue #104's asymmetric-extraction mechanism through three extraction paths (convert+withdraw, liquidate+withdraw, resolve+close+claim), plus a differential fuzzer (~2.2M accepted operations across single- and multi-asset/multi-domain configs) asserting full-population conservation after every accepted operation.

Wrapper, on the real program. Built percolator_prog.so and drove the actual wrapper instructions through the repo's processor test harness (192 existing tests pass). Replicated the #104 class via auth-mark (single asset), the permissionless cross-domain append variant, and an H2 stale-mark arb via an inverted 3-leg hybrid oracle. Each test asserts vault >= insurance + c_tot after every operation, and that seeded insurance domains are never spent by a foreign asset's bankruptcy.

Formal-proof review. The engine carries machine-checked Kani proofs of the core economic-safety properties, directly covering what a drain would have to violate: the cross-domain insurance isolation (proof_v16_bad_asset_cannot_spend_unrelated_domain_insurance_budget), domain-budget caps on bankruptcy spend, value-flow conservation for deposit, withdraw, loss and fee, and overflow-before-mutation on every lien operation.

§03 Result: every tested vector is defended

Three defenses did the work: a loss-stale lock (favorable extraction is blocked while a matching loss is unsettled), per-domain insurance isolation (a foreign asset's bankruptcy never spends another domain's seeded insurance), and a mark-movement surcharge (moving the oracle mark via trades is self-funding for the insurance pool; in the H2 test the attacker paid into insurance, so it rose rather than fell).

Beyond these runtime defenses, the same properties are backed by the engine's machine-checked proofs, so the cross-domain isolation a drain would need to break is not just observed to hold, it is proven to.

§04 Minor, non-exploitable observations

Neither is a bounty win, and neither is an insurance drop via public instructions. Both were shared with the maintainer.

• percolator v16.rs:10206: a guard of the form bound_num_from_amount(x) > prior where prior = bound_num_from_amount(x) reduces to X > X (always false), a likely-unintended no-op check. Not exploitable; the residual-rate cap still bounds resolved payouts.
• Off-chain keeper healthOf: equity used for the health rating is mark-invariant (ignores unsettled K-delta), so a losing position can be rated healthy and under-cranked. Off-chain only.

§05 What I hold

§06 Honest conclusion

No insurance-draining sequence was found, at either layer, including against the real deployed program. This does not prove the code is bug-free; it shows the primary known vectors (#104-class and H2) are defended and that engine conservation held across millions of randomized operations. The only theoretically-remaining surface is a correctness flaw in the pure compose/invert leg arithmetic itself (static review put it at no more than 1 ulp e6, far below the fee; no empirical divergence was observed), and exploiting it would require Pyth manipulation, which is out of scope.