Fix replay binding to source message#28
Open
juanbono wants to merge 2 commits into
Open
Conversation
The previous Inbox accepted any 32-byte transport nonce the attestor
quorum chose to sign over, with no on-chain link to a unique
source-chain event. This allowed a single `BridgeBurner.sendTo` to
produce two valid attested messages under different nonces, minting 2×
amount on the destination.
The fix derives the replay-protection nonce on-chain from a tuple that
identifies the source event uniquely:
nonce = keccak256(abi.encode(srcChain, srcOutbox, srcSender, srcSeq))
Outbox changes
- Adds a per-sender monotonic counter `nextSeq[msg.sender]`.
- `sendMessage` consumes the counter, derives the nonce on-chain, and
emits `MessageSent(sender, dstChain, dstRecipient, srcSeq, nonce, payload)`.
- Returns `(srcSeq, nonce)` so callers (e.g., BridgeBurner) can log them.
Wire format
- Transport message becomes
`(srcChain, srcOutbox, srcSender, srcSeq, dstChain, dstRecipient, payload)`.
- The nonce is no longer a separate field — attestors cannot pick it
independently of the source event.
Inbox changes
- New `srcOutboxes[srcChain] => address outbox` map authenticating the
canonical source Outbox per chain. Without a configured entry the
chain's messages are rejected (`UnknownSrcOutbox`).
- `setSrcOutbox` validates the candidate (zero-check, code-length,
ERC-165 advertisement of `IOutbox`) — mirrors `BridgeBurner.setOutbox`.
- Refuses to silently overwrite a non-zero entry (`SrcOutboxAlreadySet`).
Operators must explicitly clear with `setSrcOutbox(srcChain, 0)`
during a paused-and-drained window before pointing at a new Outbox.
- `recvMessage` decodes the new wire format, re-derives the nonce,
rejects stranger `srcOutbox` values, and uses the derived nonce as
the `usedNonces` replay key.
BridgeConfig
- Adds `SrcOutbox[]` to the Config struct, zero-checks each entry,
and calls `inbox.setSrcOutbox` during `configure`. The example
TOML and ConfigureBridge script will need a follow-up to add the
new section.
The PoC test (`test_NoncePoCBlockedByDerivedKey`) demonstrates that
re-attesting the same source event under any "fresh" nonce now fails
on the second receive — the derived key is identical and `usedNonces`
catches it. Stranger-outbox and unconfigured-srcChain cases are also
covered.
The H-04 commit changed the Inbox wire format and added the `srcOutboxes` authentication + on-chain nonce derivation, but did not update `Bridge.formal.t.sol`. Its `check_*` proofs are Halmos-only (forge test runs `test*`, so local `forge test` stayed green) and so the stale 6-field `_encodeMessage` slipped through until the CI Halmos job failed. Fix the InboxFormalTest proofs: - `_encodeMessage` now emits the 7-field layout (srcChain, srcOutbox, srcSender, srcSeq, dstChain, dstRecipient, payload); add `_deriveNonce` mirroring the Inbox's keccak derivation. - `InboxFormalTest.setUp` registers the canonical source Outbox for SRC_CHAIN so deliveries pass the new `srcOutboxes` check and reach the property under test. - Replay / delivery proofs are reparameterized on `srcSeq` (the nonce is now derived, not a free input) and assert on the derived key. - `check_wrongChainAlwaysReverts` varies only `dstChain` symbolically (the chain check is positionally first and field-independent); this also sidesteps a Halmos symbolic-CALLDATACOPY limitation when decoding a fully-symbolic envelope. - `zeroThreshold` / `singleSig` / `zeroSignatures` proofs configure the source Outbox so they reach the intended signature/threshold checks instead of short-circuiting at the srcOutbox guard. Verified locally: `halmos` 35/35 green (all formal + invariant suites), `forge test` bridge suite 79/79 green, forge fmt clean.
jrchatruc
approved these changes
May 26, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Problem: The previous Inbox accepted any 32-byte transport nonce the attestor quorum chose to sign over, with no on-chain link to a unique source-chain event.
Fix. Derive the replay-protection nonce on-chain from a tuple identifying the source event uniquely:
nonce = keccak256(abi.encode(srcChain, srcOutbox, srcSender, srcSeq)). The Outbox gains a per-sender monotonicnextSeq[msg.sender]counter and emitsMessageSent(sender, dstChain, dstRecipient, srcSeq, nonce, payload).