percolator-bounty5-v16

Engine validate_account_source_credit_shape admits empty source-domain capacity

Invariantvalidate_account_source_credit_shape admits empty source-domain capacity

Affected code

• Engine: src/v16.rs:11912 — validate_account_source_credit_shape
• Engine pin: 23de295039360182338e8675315103b7cf25e15b
• Wrapper guard: v16_program.rs:9437 — ensure_portfolio_storage_for_market_slots
• Wrapper pin: af8cf46

Description

The function reads configured_domains but never compares it against account_domain_capacity. An account whose source-domain Vec is empty (capacity 0) skips all per-domain checks and passes validation, even when the configured market requires 2 * max_market_slots domains.

Distinct from issue #104 (0x-SquidSol): that finding attacks accrue_asset_to_not_atomic K-state asymmetry to inflate pnl_pos_bound_tot and drain insurance via attacker bankruptcy. This finding is an upstream validation gap — orthogonal layer of the engine, independent root cause, no current insurance impact.

Impact

As-is: none observed. The wrapper auto-realloc absorbs any byte-level truncation before the engine validates.

Latent risk: if the wrapper ensure_portfolio_storage_for_market_slots is ever removed, simplified, or replaced with a check that does not trigger realloc, the engine bug becomes a direct state-corruption primitive admitting portfolios with source_domain_capacity != configured_domain_count into post-validation flow.

Layer 3 — Symbolic verification (Kani)

✓ Counterexample found (bug confirmed by symbolic execution)

Layer 4 — On-chain BPF reproduction

Not reproduced (wrapper-side defenses caught it OR test setup didn't reach buggy state)

Reproduction

L2 + L2.5: cargo test --features test --test test_hyp1_portfolio_preflight_lazy_deser_bypass panics with "got Ok(()) — bug present".

L3 Kani (~8.6s): cargo kani --tests --features fuzz --harness proof_hyp1_portfolio_preflight_empty_source_domain_must_reject returns VERIFICATION:- FAILED (1 of 2335 checks, 164 unreachable).

L4 LiteSVM: cargo test --test v16_cu v16_bpf_l4_hyp1_portfolio_preflight_truncated_source_domain -- --nocapture shows wrapper auto-realloc-ed truncated portfolio with zero-fill; engine bug not reached via this path.

Recommended fix

Add an upfront check in validate_account_source_credit_shape at the top of the function: if account_domain_capacity != configured_domains return Err(V16Error::HiddenLeg). Engine becomes self-defending; the wrapper auto-realloc remains a separate defense layer.

Layer 2 — Concrete proof of concept (engine-direct)

#[test]
fn hyp1_portfolio_preflight_lazy_deser_bypass_fires() {
    // 1. Construct engine state.
    let market_group_id = [0u8; 32];
    let cfg = config_for_hyp1_portfolio_preflight_lazy_deser_bypass();
    let mut group =
        MarketGroupV16::new(market_group_id, cfg).expect("MarketGroupV16::new must succeed");

    // 2. Build a portfolio account with a well-formed header + owner, but whose
    //    source-domain vectors are empty (zero capacity) — simulating a
    //    "corrupt source-domain tail" that a lazy-deser path would not read.
    let owner: [u8; 32] = [1u8; 32];
    let account_id: [u8; 32] = [2u8; 32];
    let provenance = ProvenanceHeaderV16::new(market_group_id, account_id, owner);

    // PortfolioAccountV16::empty leaves all source-domain Vecs with len == 0,
    // which is below the configured domain count (2 assets * 2 = 4 domains).
    let account = PortfolioAccountV16::empty(provenance);

    // 3. Verify the configured domain count requires source-domain capacity.
    let required_domain_count =
        v16_domain_count_for_market_slots(cfg.max_market_slots).expect("domain count");
    // An empty PortfolioAccountV16 has source_domain_capacity() == 0.
    assert_eq!(
        account.source_claim_market_id.len(),
        0,
        "empty account has zero source-domain capacity"
    );
    assert!(
        required_domain_count > 0,
        "configured domain count must be positive"
    );

    // 4a. The "preflight" (lazy-deser path) only checks header + owner — PASSES.
    let preflight_result = preflight_owner_check(&market_group_id, &account);
    assert!(
        preflight_result.is_ok(),
        "preflight (header-only check) must accept a well-formed header: {:?}",
        preflight_result
    );

    // 4b. The full boxed read (validate_account_shape / read_portfolio_boxed_for_market_slots)
    //     checks that source_domain_capacity >= configured_domain_count — FAILS.
    let full_result = group.validate_account_shape(&account);
    assert!(
        full_result.is_err(),
        "full shape validation must REJECT an account whose source-domain capacity ({}) \
         is below the required domain count ({}); got Ok(()) — bug present",
        account.source_claim_market_id.len(),
        required_domain_count
    );

    // 5. The atomicity gap: preflight says Ok but full read says Err.
    //    If the engine were fixed (preflight also validated domain capacity), both
    //    would return the same error.  The assertion below captures the discrepancy.
    //    It FAILS (panics) when the bug is present because we assert the two results
    //    are EQUAL — but they are not (preflight Ok, full Err).
    let preflight_ok = preflight_owner_check(&market_group_id, &account).is_ok();
    let full_ok = group.validate_account_shape(&account).is_ok();

    // BUG WITNESS: preflight passes but full validation rejects.
    // When patched, preflight must also reject, making preflight_ok == full_ok == false.
    assert_eq!(
        preflight_ok, full_ok,
        "HYPOTHESIS CONFIRMED: lazy-deser preflight (ok={}) disagrees with full boxed \
         read (ok={}) for an account with corrupt/zero source-domain tail — \
         a wrapper that commits state based on preflight before doing the full read \
         can be bypassed",
        preflight_ok, full_ok
    );
}

Layer P3 — Proposed structural fix (patch diff)

--- /tmp/v16_clean.rs	2026-05-25 20:01:25.289480086 +0000
+++ /root/audit_runs/bounty5-v16/target/engine/src/v16.rs	2026-05-25 20:03:36.073811440 +0000
@@ -11912,6 +11912,13 @@
     fn validate_account_source_credit_shape(&self, account: &PortfolioAccountV16) -> V16Result<()> {
         let configured_domains = self.configured_domain_count()?;
         let account_domain_capacity = account.source_domain_capacity();
+        // SECURITY FIX (HYP1): reject portfolios whose source-domain capacity does not
+        // match the configured domain count. Previously, an account with zero-capacity
+        // source-domain Vec would pass this function unchecked because the loop body
+        // below never executes when capacity == 0.
+        if account_domain_capacity != configured_domains {
+            return Err(V16Error::HiddenLeg);
+        }
         let mut d = 0;
         while d < account_domain_capacity {
             let numeric_zero_source_domain = account.source_claim_bound_num[d] == 0

References

• L3 Kani harness: tests/proofs_hyp1_portfolio_preflight_empty_source_domain.rs
• L2 PoC: tests/engine/test_hyp1_portfolio_preflight_lazy_deser_bypass.rs
• L4 LiteSVM test: target/wrapper/tests/v16_cu.rs (v16_bpf_l4_hyp1_portfolio_preflight_truncated_source_domain)

Engine validate_account_shape accepts leg with rewritten asset binding

InvariantMulti-leg oracle composite accepts oracle_accounts as a caller-supplied list. Verify each account's feed_id is bound to the expected leg index via cryptographic feed_id equality (not just account order). Find any path where leg account ordering can be swapped without detection.

Affected code

• Engine: src/v16.rs:11791 — leg validation loop inside validate_account_shape
• Engine pin: 23de295039360182338e8675315103b7cf25e15b
• Wrapper guard: state::read_portfolio rejects malformed bytes with Custom(0x9)
• Wrapper pin: af8cf46

Description

The only post-attach check is that (leg.asset_index, leg.market_id) is internally consistent against self.assets[]. An attacker who can write to the on-chain PortfolioAccountV16 bytes can change both fields together without engine detection. The leg k_snap, f_snap, b_snap, epoch_snap would still reflect the original asset state but the engine would settle them against the swapped asset.

Distinct from issue #104 (0x-SquidSol): that finding attacks accrue_asset_to_not_atomic K-state asymmetry. This finding is at the validation layer — orthogonal root cause, no current insurance impact.

Impact

As-is: none observed. The wrapper rejects the byte-rewrite vector with Custom(0x9).

Latent risk: if exploitable, an attacker could open a position on asset A, observe the price move, then rewrite the leg to point at asset B — settling against B K/F state while having opened against A. This breaks K/F accounting invariants and could enable PnL extraction across markets.

Layer 3 — Symbolic verification (Kani)

✓ Counterexample found (bug confirmed by symbolic execution)

Layer 4 — On-chain BPF reproduction

Not reproduced (wrapper-side defenses caught it OR test setup didn't reach buggy state)

Reproduction

L2 + L2.5: cargo test --features test --test test_o7_leg_account_ordering_not_bound panics with "swap accepted by validate_account_shape without any cryptographic feed_id check".

L3 Kani (~74s): cargo kani --tests --features fuzz --harness proof_o7_leg_index_swap_consistent_market_id_must_reject returns VERIFICATION:- FAILED (1 of 2412 checks, 128 unreachable).

L4 LiteSVM: cargo test --test v16_cu v16_bpf_l4_o7_leg_index_rewrite_then_read -- --nocapture shows wrapper rejected byte-rewrite with Custom(0x9).

Recommended fix

The supplied patch adds a partial mitigation: bind the leg to its asset via side-epoch. leg.epoch_snap must match the current asset epoch on the leg side (epoch_long or epoch_short).

Partial coverage: catches swaps where source and target assets have different side epochs (production scenario after retire/reactivate cycles, side resets, recovery transitions). Does NOT catch swaps between two freshly-initialized assets where both still have epoch_long = epoch_short = 0.

Full mitigation requires a dedicated binding-attestation field on PortfolioLegV16, e.g. attached_market_id_at_open: u64 captured in attach_leg and verified in validate_account_shape. That is a larger surgical change requiring synchronized updates to attach_leg, validate_account_shape, and any pathway that mutates legs.

Layer 2 — Concrete proof of concept (engine-direct)

#[test]
fn o7_leg_account_ordering_not_bound_fires() {
    let market_group_id = [0u8; 32];
    let mut group =
        MarketGroupV16::new(market_group_id, config_for_o7()).expect("MarketGroupV16::new");

    // Activate two asset slots so we have two distinct market_ids.
    {
        let asset = &mut group.assets[0];
        asset.lifecycle = AssetLifecycleV16::Active;
        asset.raw_oracle_target_price = 1_000_000;
        asset.effective_price = 1_000_000;
        asset.fund_px_last = 1_000_000;
        asset.slot_last = 1;
        asset.a_long = percolator::ADL_ONE;
        asset.a_short = percolator::ADL_ONE;
    }
    group.current_slot = group.current_slot.max(1);
    {
        let asset = &mut group.assets[1];
        asset.lifecycle = AssetLifecycleV16::Active;
        asset.raw_oracle_target_price = 2_000_000;
        asset.effective_price = 2_000_000;
        asset.fund_px_last = 2_000_000;
        asset.slot_last = 2;
        asset.a_long = percolator::ADL_ONE;
        asset.a_short = percolator::ADL_ONE;
    }
    group.current_slot = group.current_slot.max(2);

    let market_id_0 = group.assets[0].market_id;
    let market_id_1 = group.assets[1].market_id;
    assert_ne!(market_id_0, market_id_1, "assets must have distinct market_ids");

    // Build account A: long on asset 0.
    let owner_a = [1u8; 32];
    let id_a = [2u8; 32];
    let prov_a = ProvenanceHeaderV16::new(market_group_id, id_a, owner_a);
    let mut account_a = PortfolioAccountV16::empty(prov_a);
    account_a.ensure_source_domain_capacity(
        group.assets.len() * 2,
    );

    group
        .deposit_not_atomic(&mut account_a, 1_000_000_000)
        .expect("deposit A");

    let prices = vec![1_000_000u64; group.assets.len()];

    group
        .attach_leg(&mut account_a, 0, SideV16::Long, 500_000)
        .expect("attach leg to asset 0");

    // Refresh so health cert is valid.
    group
        .full_account_refresh(&mut account_a, &prices)
        .expect("refresh A");


    // Find the active leg slot for asset 0.
    let leg_slot = {
        let mut found = None;
        for s in 0..16usize {
            if account_a.legs[s].active && account_a.legs[s].asset_index == 0 {
                found = Some(s);
                break;
            }
        }
        found.expect("leg for asset 0 must exist")
    };

    // Save the original state so we can restore and compare.
    let original_asset_index = account_a.legs[leg_slot].asset_index;
    let original_market_id = account_a.legs[leg_slot].market_id;

    // Perform the swap: point the leg at asset slot 1 with asset 1's market_id.
    // This is the attacker's reordering: same leg, different oracle feed slot.
    account_a.legs[leg_slot].asset_index = 1;
    account_a.legs[leg_slot].market_id = market_id_1;

    // Invalidate health cert (the swap changed the bitmap-consistent state).
    account_a.health_cert.valid = false;

    let result_after_swap = group.validate_account_shape(&account_a);

    // Restore original state.
    account_a.legs[leg_slot].asset_index = original_asset_index;
    account_a.legs[leg_slot].market_id = original_market_id;
    account_a.health_cert.valid = false;

    let result_original = group.validate_account_shape(&account_a);

    // The original configuration must be valid.
    assert!(
        result_original.is_ok(),
        "original leg-asset binding must be valid: {:?}",
        result_original
    );

    // BUG WITNESS: if the swapped configuration is ALSO Ok, the engine has
    assert!(
        result_after_swap.is_err(),
        "BUG O7: swapping leg asset_index from {} to {} (market_id {} → {}) \
         was accepted by validate_account_shape without any cryptographic \
         feed_id check — oracle account ordering is not bound. \
         Expected Err, got Ok.",
        original_asset_index,
        1,
        original_market_id,
        market_id_1,
    );
}

Layer P3 — Proposed structural fix (patch diff)

--- /tmp/v16_clean.rs	2026-05-25 20:01:25.289480086 +0000
+++ /root/audit_runs/bounty5-v16/target/engine/src/v16.rs	2026-05-25 20:03:36.113811541 +0000
@@ -11800,6 +11800,18 @@
                 {
                     return Err(V16Error::HiddenLeg);
                 }
+                // SECURITY FIX (O7) — partial mitigation: bind the leg to its asset via
+                // the side-epoch snapshot. Catches attacks where the new asset has a
+                // different epoch (post-retire/reactivate, post-side-reset). Does NOT
+                // catch the case where both assets start at epoch 0 — a full mitigation
+                // requires adding a dedicated binding-attestation field on PortfolioLegV16.
+                let _asset_epoch = match leg.side {
+                    SideV16::Long => self.assets[asset_index].epoch_long,
+                    SideV16::Short => self.assets[asset_index].epoch_short,
+                };
+                if leg.epoch_snap != _asset_epoch {
+                    return Err(V16Error::HiddenLeg);
+                }
             }
         }
         if account.close_progress.active {

References

• L3 Kani harness: tests/proofs_o7_leg_index_swap_consistent_market_id.rs
• L2 PoC: tests/engine/test_o7_leg_account_ordering_not_bound.rs
• L4 LiteSVM test: target/wrapper/tests/v16_cu.rs (v16_bpf_l4_o7_leg_index_rewrite_then_read)