docs: state the per-page temporal replay boundary in its true form (#142) - #160
Merged
Conversation
Closes #142 (I153). The design spec's §9 documented "no rollback/replay resistance" for one case: an attacker who substitutes a WHOLLY OLDER, validly-signed database image. The actual weakness is strictly stronger, and the gap between the two mattered. Page AAD is `page_id` and nothing else, so a sealed page authenticates WHERE it belongs but not WHEN. An attacker holding an older copy of the file can splice INDIVIDUAL stale pages into the current one — each verifies under the current DEK, at the correct page id. What comes out is a mixed state that never existed at any commit: a stale freemap or interior tree page beside current siblings, which the engine may walk as though it were consistent. Neither of the spec's Provided claims covered this, and both read as though they did. "Cryptographic tamper-detection" and "anti-relocation" are SPATIAL guarantees: relocation is about moving a page to the wrong place, replay about moving it to the wrong time. §9 now says so in as many words, since that distinction is the whole finding. Stated in three places, because they have different readers: the spec §9 (the normative boundary), THEORY.md (the reader who never opens a spec), and `PageCipher::seal`'s doc comment (the maintainer who might otherwise "simplify" the AAD, or read anti-relocation as more than it is). Also records what does and does not bound the exposure: * `rekey` (ADR 0018) does not make a splice DETECTABLE, but it invalidates every page image sealed under the old DEK, so pages captured before a rotation cannot be spliced in after one. * The I148 positional page-type checks are a partial and accidental mitigation: a splice is caught whenever the stale page's type differs from the one expected at that position. It is silent only for a same-type splice — realistic for hot structural nodes, but not universal. Two corrections from review: * The first draft justified rejecting a commit-epoch AAD as "the write amplification shadow paging exists to avoid". Backwards: shadow paging ACCEPTS write amplification as the price of crash-safety-by-inspection — ADR 0001 lists it as a negative consequence and THEORY.md says the cost is taken with eyes open. The objection is amplification well beyond what that trade already buys, which is a different sentence. * "Corrupts structure silently" was stated flatly in two of the three places and hedged in the third. Hedged consistently now, and the type checks are named as the reason it is only sometimes silent. ADR 0015 stated both the old boundary and "bulk DEK rotation deferred". It is Accepted, so it gets an Addendum rather than an edit.
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
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.
Closes #142 (I153). Stacked on #159. Documentation only — 731 tests still pass.
The design spec's §9 documented "no rollback/replay resistance" for one case: an attacker who substitutes a wholly older, validly-signed database image. The actual weakness is strictly stronger, and the gap between the two mattered.
Page AAD is
page_idand nothing else, so a sealed page authenticates where it belongs but not when. An attacker holding an older copy of the file can splice individual stale pages into the current one — each verifies under the current DEK, at the correct page id. What comes out is a mixed state that never existed at any commit: a stale freemap or interior tree page beside current siblings, which the engine may walk as though it were consistent.Neither of the spec's Provided claims covered this, and both read as though they did:
§9 now says that in as many words, since the distinction is the whole finding.
Stated in three places, for three readers
THEORY.mdPageCipher::sealdoc commentWhat bounds the exposure
rekey(feat: bulk DEK rotation — re-encrypt a whole database under a fresh data key (#140) #159, ADR 0018) does not make a splice detectable, but it invalidates every page image sealed under the old DEK — so pages captured before a rotation cannot be spliced in after one. An operator who suspects file access has a way to draw a line.Three routes to actually closing it are listed with honest costs (external trust anchor / commit epoch in AAD / hash-chained page tags); none is implemented, and the issue stays the tracker for that.
Two corrections from review
THEORY.mdsays the cost is taken with eyes open. The real objection is amplification well beyond what that trade already buys, which is a different sentence. Fixed in both places.ADR 0015
It stated both the old boundary and "bulk DEK rotation deferred". It is Accepted, so it gets an
## Addendum (2026-08-04)pointing at ADR 0018 and the corrected boundary — not an in-place edit.