amadan
Bind checker readonly mode to a closed checkpoint handoff
2 files changed,
+55
−18
implementation/compatibility-checker/proposal.json+36 −18implementation/compatibility-checker/review-revision.json+19 −0
CI passed — run details
diff --git a/implementation/compatibility-checker/proposal.json b/implementation/compatibility-checker/proposal.json| index e5e5300..0c30622 100644 |
| --- a/implementation/compatibility-checker/proposal.json |
| +++ b/implementation/compatibility-checker/proposal.json |
| @@ -1,6 +1,6 @@ |
| { |
| - "version": 1, |
| - "status": "UNAPPROVED DESIGN PROPOSAL; no runtime implementation or authority conferred", |
| + "version": 2, |
| + "status": "UNAPPROVED amended design after Fable REQUEST CHANGES on2214be1; no runtime authority conferred", |
| "home_revision": "7e282e2a363b9cc90cd74dd97809e6613a699af8", |
| "audit": "audit.json", |
| "audit_sha256": "0625d33bb795c1cf415e1e213d8e572e65f8ae4ebcf71ab52adf264c076e8b60", |
| @@ -54,7 +54,7 @@ |
| { |
| "key": "HOME_DEK", |
| "credential_database_proof": "Authenticate every existing signin_links.sealed_address with signin.address and every credential operator sealed result with operator.result/v1/<origin>/<operation>/<action>. Discard plaintext immediately; no echo or persistence. This proves those stored ciphertexts, not key history when none remain.", |
| - "directory_database_proof": "Authenticate every teams.sealed_name with directory.team-name/<id> and every directory operator sealed result using existing purpose; validate resulting format with existing pure validators.", |
| + "directory_database_proof": "Authenticate every teams.sealed_name with directory.team-name/<id>, every directory operator sealed result with operator.result/v1/<origin>/<operation>/<action>, every oficina_handoff_pending.sealed_path with handoff.path.<stored secret_hash>, and every oficina_handoff_inbox.sealed_token with handoff.token.<stored handle_hash>. Read-only scan includes expired rows too; no sweep/Finish/Verify that consumes replay. Validate stored purpose/hash shape and bounded path representation using shared current fresh-prefix/SafePath rules; token decryption proves at-rest authentication, not current token validity or authority (expired tokens do not fail solely on expiry). Never emit plaintext or invoke handoff.Finish; discard per-row plaintext. Roster cursors and assertion intent are client-held, not persisted witnesses.", |
| "required_even_if_ciphertexts_exist": "Exact trusted enrolled fingerprint equality. Missing ciphertexts do not allow omission. No newly sealed self-test blob counts as compatibility evidence." |
| }, |
| { |
| @@ -86,7 +86,7 @@ |
| "not_claimed": "Fingerprint comparison proves continuity with enrollment, not that enrollment was correct. Ciphertext checks prove present data compatibility only. Signing key validation proves current configured keypair math and expected public binding, not independent key-custody attestation." |
| }, |
| "database_acceptance": { |
| - "common": "Exact existing regular database identity from verified launch; exact role-specific schema and trusted instance enrollment. Never create missing file or invoke general migrator. Check sqlite integrity_check result exactly ok and foreign_key_check empty within deadline. Refuse unknown extra/missing/modified schema, corrupt rows or contradictory binding.", |
| + "common": "Exact existing regular database identity and role enrollment from verified closed-checkpoint handoff; exact role-specific schema; no creation/migration repair. Run read-only foreign_key_check within deadline and rely on fresh platform integrity/checkpoint receipt for whole-file integrity; avoid duplicating integrity_check. Corrupt schema/rows/ciphertexts or contradictory binding still refuse app compatibility.", |
| "credential_set": "migrate.Merge(home.BootSchema, operator.CredentialSchema) from selected release. At7e BootSchema = sessions.Schema + passkey.Schema + home.Schema; CredentialSchema namespace oficina_credential_operator with0001_operator and0002_operator_key_identity.", |
| "directory_set": "migrate.Merge(directorySchema, directorydata.OperatorSchema, operator.DirectorySchema) from selected release. directorySchema = sessions.Schema + oficina_handoff migrations + directorydata.Schema + directorydata.RosterSchema. Operator bindings namespace oficina_directory_operator_bindings; DirectorySchema namespace oficina_directory_operator with0001_operator,0002_owner_receipts,0003_operator_key_identity.", |
| "current_gap": "Runtime.Schema currently omits operator.CredentialSchema/operator.DirectorySchema and directorydata.OperatorSchema. Checker never fixes that. Separately reviewed additive deployment must install required sets before the checker can succeed.", |
| @@ -95,22 +95,35 @@ |
| "credential_identity": "No directory/team/roster namespace; people refs and blind indexes retain their current shape. If operator_state exists, exact origin/installation/registry/device/key identity must match trusted enrollment and sequence/head/completion must match approved expected state constraints. Do not infer app identity from table names alone.", |
| "directory_identity": "No people/signin/passkey credential namespace; exact operator origin/installation/registry/device/key identity when initialized; generation and existing owner/team memberships agree with trusted baseline expectations. Validate team sqid/label, purpose-bound name, bounded epochs, and existing registry/provisioning references using current pure validators. No new generation, team or owner creation.", |
| "empty_policy": "No default empty DB success. Missing file, empty schema, missing ledger or untrusted role binding always refuse. A schema-complete but authority-empty initial role is accepted ONLY with a separately enrolled explicit baseline profile binding exact DB identity, role/origins, required schema, expected absence of operator state/generation/teams/people and key fingerprints. This permits planned first initialization without inventing ownership, but that baseline profile must be reviewed/enrolled; a caller boolean or just current count=0 is insufficient. Initialized profile requires exact expected state presence and at least its enrolled durable identity witnesses; zero rows unexpectedly refuses.", |
| - "bounded_scan": "Single read transaction over all compatibility-relevant rows; proposed deadline min(launch deadline,30seconds), at most100000 rows and64MiB authenticated ciphertext cumulatively, per-value bounds from schema. Exceeding limits returns unavailable, never success from sampling. Do not allocate plaintext corpus; scan/discard one value at a time. Larger deployments need separately reviewed limits.", |
| + "bounded_scan": "Single read transaction over all compatibility-relevant rows; proposed deadline min(launch deadline,30seconds), at most100000 rows and64MiB authenticated ciphertext cumulatively, per-value bounds from schema. Exceeding limits returns unavailable, never success from sampling. Do not allocate plaintext corpus; scan/discard one value at a time. Larger deployments need separately reviewed limits. Main byte hashing has separate256MiB per-pass cap and shared30second invocation deadline; these limits are conservative refusal limits, not a completeness claim for larger deployments.", |
| "concurrent_state": "No serving/replication writer is allowed during checker under platform fence/retained lease. Read snapshot is not a substitute for that ownership proof." |
| }, |
| "database_opening": { |
| - "decision": "Require a reviewed read-only variant of existing actual-descriptor connector, not current newBoundDatabase and not a bare sql.Open(mode=ro).", |
| - "identity": "Retain nofollow ancestor walk, single hardlink/device/inode pins, actual driver-open descriptor inventory and checks during all queries/rows/close. Adapt expected main descriptor to O_RDONLY; pin any main/WAL/SHM identities before and after actual open. No fallback to mode=rw or path-only proof; no immutable=1 because it suppresses change/WAL handling assumptions.", |
| - "os_boundary": "Run selected command with DB directory/files read-only in its reviewed process namespace and prohibit arbitrary writable regular inherited descriptors. Private result is anonymous pipe. Sandbox setup belongs to reviewed launch integration; merely setting PRAGMA query_only is insufficient.", |
| - "wal_shm": "Main and WAL bytes/presence/identity must not change; SHM bytes/presence/identity must also remain unchanged by checker. Locks/descriptor offsets may change but are not stored data. Open coherent pre-existing sidecars read-only if SQLite supports the actual state; missing sidecars or recovery requiring writes must refuse. No checkpoint, SHM rebuild, journal mode change, deletion or creation in checker. Platform may perform its separately authorized checked checkpoint before invocation, then rebind the observed files; checker cannot request implicit repair.", |
| - "actual_driver_gate": "This is a proposed dependency, not a proven capability of pinned modernc. Prove readonly hot-WAL and checkpointed WAL-mode cases on exact driver/kernel; if coherent readonly open cannot meet constraints, refuse and return design for review rather than silently allow housekeeping writes.", |
| - "root_probe": "probe/readonly_probe_test.go and overlay.json show current connector + query_only + SELECT can change main SHA and remove WAL/SHM at close. Observational test passes; it proves current helper is unsuitable, not checker safety.", |
| - "postcondition": "Close must complete successfully and pinned identity/no-change checks must pass before success result is released. Output assembled privately but withheld until all DB handles are closed and final evidence checked." |
| + "decision": "A checker-only actual-descriptor connector using mode=ro&immutable=1 is proposed exclusively for a verified closed-checkpoint handoff. No generic readonly fallback or mutable operator change. Absent handoff proof refuses before database opening.", |
| + "explicit_upstream_amendment": "home-operator-open.md line21 fixes mutable operator DSN to mode=rw/default VFS. This revision REQUESTS a separately reviewed checker-only exception mode=ro&immutable=1; it does not amend the mutable operator connector or claim its existing approval covers this path. The previously proposed checker no-immutable rule is replaced only under the preconditions below.", |
| + "worker_order": [ |
| + "Verify exact approved resume operation, exclusive operation execution and same primary/artifact/environment/DB identities. Install durable/local admission fence. Obtain checked old main+sidecar death, cgroup emptiness and old replication Close evidence BEFORE acquiring the maintenance Held lease.", |
| + "Under the same retained healthy Held lease and exclusive worker execution, invoke the existing reviewed Held.Checkpoint protocol: temporary replica store SyncAndWait then checked Close; final lease health check. No Release or second owner. All store/SQLite handles used by checkpoint must be closed. Failure or uncertain close refuses handoff.", |
| + "Checkpoint receipt alone does not prove filesystem state. Verify main exists, one link and exact pinned identity, and WAL/SHM/rollback-journal are ABSENT by nofollow relative inspection of pinned parent directory. Any sidecar including zero-length WAL/SHM refuses; never delete sidecars to make the check pass. Normal closed checkpoint is the supported positive state. If actual checkpoint leaves sidecars, remain fenced/unavailable until a separately reviewed preparation path exists.", |
| + "After closure and before checker launch, bind main length and SHA256 from an exact bounded scan to fresh attempt-specific private handoff evidence, alongside checkpoint receipt, old-writer/replica stop evidence, retained lease identity and current guard generation. Recheck absence/identity and healthy lease before dispatch.", |
| + "Launch only the exact selected checker artifact under immutable protected environment and reviewed read-only data namespace. Verify fresh handoff evidence through the platform launch verifier. The checker cannot mint evidence from a path, env flag, lease timestamp or its own observation.", |
| + "No writer, checkpoint, replication reopen, adoption or other checker may overlap this handoff interval. Worker retains lease/exclusive execution through checker closure, final evidence and resume transition. Any failure remains fenced. Existing ResumeFenced still owns subsequent compatible serving/replication handoff; checker never releases ownership." |
| + ], |
| + "executor_recovery": "A fresh lease, empty app cgroup or RecoverClaim alone does not prove an earlier maintenance executor is dead. Paused workerA could later checkpoint/reopen/publish while B checks immutable state. Takeover unavailable unless independently reviewed exclusive operation execution and predecessor executor quiescence/death/exclusion proof hold. No automatic timeout-based recovery or reuse of old handoff receipt.", |
| + "identity": "Retain existing nofollow ancestor walk, pinned parent and one-hardlink main device/inode, actual driver-open descriptor inventory, checks before/after every query/row and close. Expected driver main descriptor must be O_RDONLY and match the retained main identity. URI built by code with only fixed mode=ro,immutable=1,defaultVFS; no caller query params/hooks/extensions. Refuse O_RDWR/O_WRONLY, extra database, unexpected file descriptor, reconnect overlap, changed path or unlinked main. Immutable is safe only because separately proved ownership excludes ALL writers; it is not evidence that no writers exist.", |
| + "os_boundary": "OS-readonly main and data namespace, including parent directory, are mandatory in addition to immutable mode. No writable regular inherited descriptors, application globals or SQLite hooks. App stdout is private anonymous pipe. This restricts this checker only; exclusion of other processes comes from verified fence/lease/executor protocol, never the mount alone.", |
| + "wal_shm": "Require WAL, SHM and rollback journal absent throughout before/during/after open; their appearance is refusal even if zero bytes. No SHM is opened or written, so there are no reader read-marks to classify as allowed changes. No sidecar creation/deletion, recovery, checkpoint, journal mode changes or writer repair in checker. Do not admit hot WAL or manufacture absent-sidecar state by removing files.", |
| + "byte_evidence": "Max main size256MiB, positive file length; bound exact each-pass byte count before reading and recheck EOF/length. SHA256 before SQLite open and after successful SQLite close, each at most256MiB, plus identity/size/sidecar absence checks. Worker prelaunch hash is also max256MiB; total required hash IO across worker+checker is at most768MiB. Use fixed64KiB streaming buffers, never os.ReadFile or full-file allocation. No stat-only equality claim: device/inode/size detect identity, cryptographic byte equality detects content.", |
| + "descriptor_lifetime": "Checker acquires and retains read-only pinned main descriptor before driver construction; prehash via that descriptor before SQL open and posthash via the SAME descriptor only after all SQLite connections close. Never open/close a second main-file descriptor while SQLite locks may exist. Use ReadAt/Seek on retained descriptor rather than reopening path. Keep it until hash/identity/sidecar checks finish. Close failure, partial scan, unexpected EOF/growth, deadline or mismatch prevents success. Worker independent observer holds its own stable descriptor and closes outside any local SQLite active connection.", |
| + "deadline": "Entire invocation including both checker hashes and SQL scan is bounded by min(verified launch deadline,30seconds) and conservative retained-lease deadline. Check context between64KiB reads; blocking kernel IO is supervised by platform containment/deadline and failure cannot be reported as checked stop. No success emitted if cleanup/posthash cannot finish within deadline. Larger/slower DB refuses, never sampling or extending lease authority.", |
| + "postcondition": "Before emitting any success bytes, verify driver close succeeded, exact pre/post main hashes match the fresh worker handoff hash, identity/size still match and all three sidecars remain absent. Worker accepts result only for exact live attempt with retained healthy lease and exclusive ownership, and independently rechecks identity/absence before resume. A hash is byte evidence under the no-writer protocol, not proof against a hostile trusted worker that changes and restores bytes.", |
| + "actual_driver_gate": "Required empirical positive: exact pinned modernc/native Linux, WAL-mode header but cleanly checkpointed/closed main with no sidecars, actual mode=ro&immutable=1 O_RDONLY inode descriptor, byte preservation and no sidecar creation. Negative: current mode=rw+query_only housekeeping probe, missing handoff, hot/empty WAL, SHM, journal, stale lease/worker, inode replacement and >256MiB all refuse. No VFS/unsafe introspection/dependency fork; failure means unsupported, not fallback.", |
| + "root_probe": "Historical probe/observation.json demonstrates current mutable connector changes main/removes WAL+SHM despite only SELECT/query_only. It remains a negative control; it does not prove the proposed immutable connector or worker handoff exists." |
| }, |
| "launch_and_result": { |
| - "required_input_binding": "Verified platform launch pins request/attempt/guard generation, account/app/primary host, selected immutable executable digest, immutable config snapshot binding, existing DB device/inode, role/origin and enrolled expected-state digest. Exact fields/API come from reviewed launch contract; application cannot self-authorize or accept raw env equivalents.", |
| + "required_input_binding": "Verified platform launch pins request/attempt/guard generation, account/app/primary host, selected immutable executable digest, immutable config snapshot binding, existing DB device/inode, role/origin and enrolled expected-state digest. Exact fields/API come from reviewed launch contract; application cannot self-authorize or accept raw env equivalents. Additionally require fresh verified closed-checkpoint handoff evidence binding main identity/length/SHA256, absent WAL/SHM/journal, old writer/replica stop proof and same retained lease/exclusive executor. Evidence format belongs to reviewed platform launch adapter; this checker design requests required semantics, not a new self-signed authorization.", |
| "freshness": "One process invocation per platform-approved checker attempt, deadline enforced throughout parsing/open/scans/close/output. Invocation does not mutate any replay ledger; platform owns attempt freshness and accepts only result from the exact captured child pipe under retained fence/lease.", |
| - "result": "Proposed bounded private JSON version1/purpose oficina/home/compatibility/v1, role, exact origins, role-labelled public fingerprints, credential manifest digest or null, schema-profile digest, verified expected-state digest, and binding identifiers copied only from verified launch. Success contains no subjects, labels, addresses, ciphertext, private keys, secret fingerprints, tokens or SQL. Secret fingerprint comparison yields only overall success. This is plain captured private result, not a new signed Home output protocol.", |
| + "result": "Proposed bounded private JSON version1/purpose oficina/home/compatibility/v1, role, exact origins, role-labelled public fingerprints, credential manifest digest or null, schema-profile digest, verified expected-state digest, and binding identifiers copied only from verified launch. Success contains no subjects, labels, addresses, ciphertext, private keys, secret fingerprints, tokens or SQL. Secret fingerprint comparison yields only overall success. This is plain captured private result, not a new signed Home output protocol. Include private checked main SHA256/length and opaque handoff evidence digest solely for exact worker comparison, never public logging or release metadata.", |
| "limits": "Maximum16KiB success result. Failure writes no partial success JSON and uses generic nonzero exit; no config values, DB row values or driver SQL/error strings in stderr/logs. Platform capture limit remains authoritative if lower.", |
| "consumer": "Platform verifies exact attempt/artifact/config/DB/result binding before resume-ready; provisioner compares facts to its enrolled expected evidence. Receipt or earlier checker result cannot satisfy a later resume. Source build identity comes from verified selected artifact, not an untrusted self-reported version." |
| }, |
| @@ -138,7 +151,6 @@ |
| "All active/accepted public key roles accounted for; collisions, wrong role/pin, absent private config refuse; canaries prove no private bytes in result/errors/logs.", |
| "No listener, mail send, session mint, authority journal mutation, migration or DB creation; actual subprocess with denied network and controlled inherited descriptors.", |
| "Synthetic existing credential/directory DBs: correct role/schema/key passes; wrong role/origin/key, partial/future/corrupt ledger refuses; existing identities/owners/generation/sequence unchanged.", |
| - "Actual DB/WAL/SHM before/after evidence matches reviewed no-write contract, including hot WAL, readonly permissions and failed checks.", |
| "Replacement-path/open-restore race, hardlinks, expired deadline and actual descriptor mismatch refuse using existing connector proof or explicitly reviewed extension.", |
| "Selected artifact/environment/attempt mismatch and stale checker output cannot resume; prior action success and HTTP health cannot bypass checker.", |
| "Mutations removing schema/key verification, role separation or digest comparison must fail meaningful tests.", |
| @@ -147,10 +159,16 @@ |
| "Explicit baseline-empty profile cannot be enabled by request boolean, current count or missing enrollment; initialized profile cannot downgrade to empty.", |
| "Mutations allowing missing operator migration, future ledger ID, extra trigger, wrong role set, sampled scan completion, mode=rw fallback or early output must be killed.", |
| "Actual root housekeeping probe becomes negative control: forbidden current connector fails readonly invariant, reviewed connector preserves main/WAL/SHM bytes and identities or refuses without modifications.", |
| - "No changes to sessions, people, owners, memberships, generation, operator heads/results, secret files or config; private canaries absent from logs/results and raw files/WAL." |
| + "No changes to sessions, people, owners, memberships, generation, operator heads/results, secret files or config; private canaries absent from logs/results and raw files/WAL.", |
| + "Exact cleanly closed WAL-mode main without sidecars succeeds under verified handoff and readonly immutable actual driver; current mode=rw probe remains a forbidden negative control. Preserve main bytes and sidecar absence at all observations.", |
| + "Every present sidecar (including zero-byte WAL/SHM and rollback journal), missing receipt, mismatched main hash/identity/length or writable main descriptor refuses before success. No cleanup deletion to manufacture acceptance.", |
| + "Interleave paused previous executorA with attempted fresh takeoverB: B cannot launch even with empty app cgroup/new lease until A is independently excluded. Interleave rogue reopen between checkpoint/launch: guard/executor enforcement prevents it, not hash timing alone.", |
| + "Handoff rows: wrong key, purpose or moved ciphertext refuses; legitimate expired token still decrypts without mint/consume/sweep; raw DB/session/replay/authority rows unchanged.", |
| + "Main256MiB exact-bound scans, over-bound refusal, short read, file growth, same-size mutation, inode swap, close/posthash failure and deadline cancellation all prevent any success bytes. Demonstrate no second main-descriptor open/close while SQL active.", |
| + "Remove immutable restriction-to-verified-handoff, sidecar absence, final byte comparison or handoff ciphertext checks in meaningful mutations: each must be killed." |
| ], |
| "unresolved_review_dependencies": [ |
| - "Readonly actual-descriptor connector and process namespace support require separate focused implementation review and empirical proof; no query_only shortcut.", |
| + "Checker-only exception to approved mutable operator mode=rw contract, reviewed immutable readonly descriptor connector and verified closed-checkpoint launch evidence are required. No existing Checkpoint receipt alone asserts absent sidecars or exclusive predecessor executor death; integrations must implement and prove those facts. Unsupported state remains unavailable.", |
| "Protected launch and selected artifact verifier remains separately reviewed platform dependency, not supplied by Home7e.", |
| "Typed operator runtime configuration is not mounted in Home7e; checker and actual operator must share it, not collect imaginary pins.", |
| "Trusted enrollment currently has one DataKey fingerprint, not explicit pepper/signin/MAC expected fields or role-state baseline. Proposed additions need review and authenticated collection before use.", |
| @@ -382,5 +400,5 @@ |
| "sha256": "6ab9ea1dd6c63916f8d1984cf4a7c3a7cdf05e4705e807a34c58f7da5e537824" |
| } |
| ], |
| - "review_note": "All concrete choices here are proposals; source reuse does not approve new key enrollment, readonly semantics, private protocol or platform authority." |
| + "review_note": "Revision2 addresses Fable2214be1 findings; all changed semantics await explicit rereview. Closed-checkpoint and immutable exception are proposed dependencies, not claimed current platform/runtime authority." |
| } |
diff --git a/implementation/compatibility-checker/review-revision.json b/implementation/compatibility-checker/review-revision.json| new file mode 100644 |
| index 0000000..fc8e2c6 |
| --- /dev/null |
| +++ b/implementation/compatibility-checker/review-revision.json |
| @@ -0,0 +1,19 @@ |
| +{ |
| + "prior_design": "2214be15c9768dc3ba57dbcd33861c7e388a4909", |
| + "prior_review": "REQUEST CHANGES, claude-fable-5-1, session5a362663-1e97-49c5-8199-753d93684ec6", |
| + "status": "Unapproved revised design; no runtime changes", |
| + "resolved_findings": { |
| + "1": "Explicit closed-checkpoint no-writer handoff admits absent sidecars; narrowly proposed mode=ro&immutable=1 exception", |
| + "2": "SHM always absent and OS writes denied; no readmark allowance", |
| + "3": "Purpose-bound pending/inbox handoff ciphertext scans added", |
| + "4": "Exact bounded256MiB main SHA256 pre/post with retained descriptor, no duplicate-open lock hazard" |
| + }, |
| + "nonblocking": "Platform integrity receipt replaces duplicate integrity_check; no other policy changes", |
| + "source_addition": { |
| + "file": "handoff/store.go", |
| + "sha256": "a834c7c7ddbaabb59d40f81935e266bec09cbb76e53ea956b6d4334b8f36ad07", |
| + "line": 343, |
| + "end_line": 364, |
| + "excerpt": "\ttoken, e := s.sealer.Open(\"handoff.token.\"+handleHash, sealedToken)\n\tif e != nil {\n\t\treturn zero, \"\", ErrRefused\n\t}\n\tclaims, e := s.verifier.Verify(string(token), now)\n\tif e != nil {\n\t\treturn zero, \"\", ErrRefused\n\t}\n\tif subtle.ConstantTimeCompare([]byte(nonceHash), []byte(digest(claims.Nonce))) != 1 || existingSubject != \"\" && existingSubject != claims.Subject {\n\t\treturn zero, \"\", ErrRefused\n\t}\n\tpath, e := s.sealer.Open(\"handoff.path.\"+secretHash, sealedPath)\n\tif e != nil {\n\t\treturn zero, \"\", ErrRefused\n\t}\n\tfresh := strings.HasPrefix(string(path), freshPathPrefix)\n\tif fresh {\n\t\tpath = path[len(freshPathPrefix):]\n\t}\n\tif !SafePath(string(path)) {\n\t\treturn zero, \"\", ErrRefused\n\t}" |
| + } |
| +} |