fix(validator): reject a manifest that reuses one key for both signing roles - #1185
Merged
tcoratger merged 2 commits intoJul 6, 2026
Merged
Conversation
…g roles ValidatorEntry documents that the attestation and proposal keys must be separate so a validator can sign both a proposal and an attestation in the same slot without one-time-signature state reuse. Nothing enforced it: the registry loader assigned keys without comparing them, so a manifest carrying the same key in both fields loaded silently. Both signatures then advanced their own copy of the shared key from the pre-advance state, consuming overlapping XMSS one-time state — a key-compromise-class failure that stayed invisible because both loads and both signatures verify individually. Reject the misconfiguration at load time by comparing the manifest's two public keys, which leaves the secret bytes untouched. This turns the docstring invariant into a client-checkable rule and discharges the formal model's distinctness assumption at construction. Closes leanEthereum#1184
The one-validator fixture manifest reused one placeholder public key for both roles. The registry loader now rejects that, so make the two keys differ, as a real manifest does.
tcoratger
approved these changes
Jul 6, 2026
adust09
added a commit
to NyxFoundation/formal-leanSpec
that referenced
this pull request
Jul 20, 2026
…#59) Upstream leanEthereum/leanSpec#1185 (closes #1184) now rejects a manifest whose attestation and proposal public keys coincide, at load time and without touching secret bytes. The model's addChecked previously compared PRF seeds as a placeholder for the invited fix; re-align it with the merged shape: - addChecked now compares public keys, with the Arklib-side derivation entering as the publicKeyOf parameter (the repo's crypto-as-parameter pattern). - addChecked_wellFormed holds for every derivation: distinct public keys imply distinct secret keys by congruence alone. - addChecked_seed_distinct keeps the OTS-reuse core of #1184: for seed-fingerprinting derivations an accepted entry's keys have distinct master seeds. - Registry.lean and catalog docstrings drop the stale 'upstream does not enforce' caveat: WellFormed is established by construction since #1185.
adust09
added a commit
to NyxFoundation/formal-leanSpec
that referenced
this pull request
Jul 20, 2026
* feat(val): re-align VAL-2 checked insertion with merged leanSpec#1185 Upstream leanEthereum/leanSpec#1185 (closes #1184) now rejects a manifest whose attestation and proposal public keys coincide, at load time and without touching secret bytes. The model's addChecked previously compared PRF seeds as a placeholder for the invited fix; re-align it with the merged shape: - addChecked now compares public keys, with the Arklib-side derivation entering as the publicKeyOf parameter (the repo's crypto-as-parameter pattern). - addChecked_wellFormed holds for every derivation: distinct public keys imply distinct secret keys by congruence alone. - addChecked_seed_distinct keeps the OTS-reuse core of #1184: for seed-fingerprinting derivations an accepted entry's keys have distinct master seeds. - Registry.lean and catalog docstrings drop the stale 'upstream does not enforce' caveat: WellFormed is established by construction since #1185. * feat(st): prove ST-7 checkpoint replacement is strictly forward ST-3/ST-6 bound only the checkpoint slots, so they still admitted a transition that swaps latest_justified / latest_finalized to a different root at the same slot. ST-7 closes that gap at the STF level: across a successful transition each checkpoint is either unchanged as a whole value (root included) or replaced by one at a strictly higher slot, mirroring Checkpoint.advance_to's strict comparison and the finalized < source.slot finalization guard. - New LeanSpec/Forks/Lstar/CheckpointForward.lean with the per-phase chain applyJustification_forward -> processAttestation_forward -> foldlM -> processAttestations_forward, plus processBlockHeader_checkpoints_of_ne_zero (past genesis anchoring the header stage leaves both checkpoints untouched) and the top-level checkpoint_forward. - Genesis anchoring (the first block filling in its parent root at slot 0) is the one designed same-slot replacement; it is excluded by the latestBlockHeader.slot != 0 hypothesis and documented in the catalog entry. - Root ancestry across branches stays a store invariant per upstream leanSpec#1182's Checkpoint.advance_to / Store.latest_finalized notes; it is future FC work, not an STF property. - Catalog: ST-7 entry added, progress table now 31 proved / 1 axiom.
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.
Summary
ValidatorEntrydocuments that the attestation and proposal keys are separate "so one validator can sign both within the same slot without OTS conflict" — but nothing enforced it. The registry loader assigned keys without comparing them, andfrom_yamlnever compared the two keys it loaded. A node whose manifest carried the same key in both fields signed a block proposal and an attestation for the same slot with the same stateful XMSS key — the one-time-signature state reuse the separation exists to prevent — and nothing surfaced it.With identical key material in both fields, each signing path advanced its own field's copy from the pre-advance state, so the two signatures consumed overlapping OTS state (a key-compromise-class failure for hash-based schemes). Both loads succeeded and both signatures verified individually, so the misconfiguration stayed invisible.
Fix
Reject the misconfiguration at load time by comparing the manifest's two public keys, which leaves the secret bytes untouched and fires before any key file is decoded. This turns the docstring invariant into a client-checkable rule and discharges the formal model's
WellFormeddistinctness assumption at construction — the same shape as #1179 did for the store invariants.Real manifests are unaffected: production key generation derives the attestation and proposal keypairs from two independent
key_gencalls, so their public keys always differ.Testing
test_same_key_for_both_roles_raises, which asserts the full error message and writes no key files, proving the check fires before any decode.uv run pytest tests/node/validator/— 78 passed.Closes #1184