[GH-ISSUE #6854] [Bug] Obligation ledger verifies a changed owner using proof for the previous implementation #4193

Closed
opened 2026-10-31 00:47:35 +00:00 by bsakaguchi · 0 comments
Owner

Originally created by @coygeek on GitHub (Oct 23, 2026).
Original GitHub issue: https://github.com/morluto/rea/issues/6854

Before submitting

  • I searched the open and closed issues for a related report.
  • I removed credentials, tokens, private paths, and sensitive target data.

Area

Evidence, artifacts, or reconstruction

Observed behavior

A reconstruction obligation remains verified, and its ledger remains ready, after changing only the manifest owner's implementation digest while keeping proof Evidence explicitly associated with the previous digest.

The synthetic proof's authenticated subject.digest.sha256 and normalized_result.owner_sha256 both identify "1".repeat(64). Changing manifest.bindings[0].owner.owner_sha256 to "2".repeat(64) produces a new closure digest but no diagnostic. The proof, obligation, fixture, verifier and claim IDs are unchanged.

Observed through the production application service and the production CLI command registration hosted in a minimal Incur CLI. The CLI registration calls the same service at applicationCommands.ts. The installed executable and MCP transport were not exercised.

Reproduction

With this source revision and its locked dependencies already installed, save the following as /tmp/rea-owner-proof-repro.mjs. From the source checkout, run:

REA_ROOT="$PWD" node --import "$PWD/node_modules/tsx/dist/loader.mjs" /tmp/rea-owner-proof-repro.mjs

This constructs synthetic Evidence, invokes the actual registered build-reconstruction-obligation-ledger command, and writes the requests and replies beside the probe. No target, analysis provider, or declared verifier command executes.

import { writeFileSync } from 'node:fs';
import { join } from 'node:path';
import { pathToFileURL } from 'node:url';
const root = process.env.REA_ROOT;
if (!root) throw new Error('Set REA_ROOT to the REA source checkout');
const load = file => import(pathToFileURL(join(root, file)).href);
const { createEvidence } = await load('src/domain/evidence.ts');
const { createEvidenceBundle } = await load('src/domain/evidenceBundle.ts');
const { registerApplicationCommands } = await load('src/cli/applicationCommands.ts');
const { Cli } = await load('node_modules/incur/dist/index.js');
const { silentLogger } = await load('src/logger.ts');
const sha = c => c.repeat(64), id = 'review.sample';
const provider = { id: 'synthetic', name: 'Synthetic fixture', version: '1' };
const original = createEvidence(undefined, provider, {
  operation: 'observe', parameters: {}, result: { output: 1 },
  confidence: 'observed', authority: 'shipped-artifact'
});
const proof = createEvidence(
  { path: 'owner.js', sha256: sha('1'), format: 'javascript' }, provider, {
    predicateType: 'rea.reconstruction-proof',
    operation: 'verify_reconstruction_obligations', parameters: {},
    result: { passed: true, obligation_ids: [id], fixture_ids: ['fixture.positive'],
      case_kinds: ['positive'], verifier_ids: ['verifier.sample'],
      claim_ids: ['claim.sample'], owner_sha256: sha('1') },
    confidence: 'observed', authority: 'shipped-artifact'
  });
const request = {
  evidence_bundle: createEvidenceBundle([original, proof]),
  reviewed_obligations: [{
    obligation_id: id, obligation_version: 1, title: 'Sample output',
    application_layer: 'other', family: 'reviewed',
    target: { artifact_sha256: null, application_node_id: null,
      semantic_node_id: null, location: 'original.js' },
    required: true, required_case_kinds: ['positive'],
    required_original_authority: 'static', required_fixture_authority: 'unit',
    required_verifier_authority: 'unit', requires_parser_type: false,
    dependency_obligation_ids: [], residual_unknown_ids: [], unavailable_authority: [],
    required_next_evidence: [], disposition: 'active',
    review_evidence_ids: [original.evidence_id]
  }],
  manifest: { bindings: [{
    obligation_id: id, owner: { module_path: 'owner.js', symbol: 'sample', owner_sha256: sha('1') },
    parser_type: null, original_cases: [{ kind: 'positive',
      evidence_id: original.evidence_id, location: '/normalized_result/output' }],
    fixtures: [{ fixture_id: 'fixture.positive', case_kind: 'positive',
      authority: 'unit', evidence_ids: [proof.evidence_id] }],
    verifier: { verifier_id: 'verifier.sample', claim_id: 'claim.sample',
      command: 'synthetic verifier (not executed)', authority: 'unit', status: 'pass',
      result_evidence_id: proof.evidence_id, enumerated_obligation_ids: [id],
      nondeterminism: { mode: 'total-order', specification: 'Single output' } }
  }], contradictions: [] }
};
for (const [name, owner, omitVerifier] of [
  ['matching-owner', '1', false], ['changed-owner-old-proof', '2', false],
  ['clear-verifier-workaround', '2', true]
]) {
  const input = structuredClone(request), binding = input.manifest.bindings[0];
  binding.owner.owner_sha256 = sha(owner);
  if (omitVerifier) binding.verifier = null;
  writeFileSync(join(import.meta.dirname, name + '.reduced-request.json'), JSON.stringify(input, null, 2));
  const cli = Cli.create('rea', { sync: false, update: false });
  registerApplicationCommands(cli, silentLogger);
  let output = '', exitCode = 0;
  await cli.serve(['build-reconstruction-obligation-ledger', JSON.stringify(input), '--json'], {
    env: {}, stdout: text => { output += text; }, exit: code => { exitCode = code; }
  });
  writeFileSync(join(import.meta.dirname, name + '.reduced-cli.json'), output);
  const envelope = JSON.parse(output);
  const ledger = (envelope.normalized_result ? envelope : envelope.data).normalized_result;
  console.log(JSON.stringify({ name, exitCode, status: ledger.status,
    obligation: ledger.obligations[0].status, owner, proofOwner: proof.subject.digest.sha256[0],
    diagnostics: ledger.obligations[0].diagnostics.map(x => x.code) }));
}

The matching-owner and changed-owner behavior was observed in two small probe runs; the reduced script above was run once and also checks the workaround.

Expected behavior

The matching-owner request should remain ready. Proof explicitly identifying the old implementation should not verify a binding naming a different implementation digest. The changed-owner request should retain an incompatibility or missing-current-proof diagnostic and stay open until proof for the current owner is supplied.

The manifest and closure guide says that a binding names one owner and its exact implementation digest and requires authenticated, comparable fixture Evidence. The closure contract requires a passing verifier for a required obligation. An observation about the previous implementation does not establish that requirement for the changed owner.

Impact and scope

A routine implementation edit followed by rebuilding the ledger with retained proof can produce a clean verification result for code the proof does not describe. The result recomputes its identity, so a new ledger/closure digest does not establish that the new implementation was checked.

This is a bounded incorrect analysis result. No deployment incident, stored-data loss, or real-world frequency was established. The tested input has one reviewed static obligation and one required positive fixture; other obligation families were not exercised.

Workaround verified in the reduced probe: set the changed binding's verifier to null until new proof is available. It returns open, obligation implemented, and missing-verifier. This preserves the missing-verification state rather than retaining the previous passing claim.

REA version

rea-agents package version 6.7.0; immutable main source snapshot 96ea32b7e4e28d3c9cd79a1de4b8e1ba3b4244e9. The source snapshot, rather than the published package runtime, was tested.

Runtime and platform

Node.js v26.12.1; Linux 7.2.8-9-omarchy, x86_64; repository-locked tsx loader and Incur dependencies. Node.js satisfies this revision's declared engine range. No Hopper, Ghidra or other analysis engine is involved.

Target and artifact context

Synthetic authenticated Evidence only. One original static observation, one passing proof with an owner subject digest, one reviewed obligation, and one manifest binding. Digest strings are inert test data; owner.js is a synthetic subject label and no file at that path is executed or inspected.

Interface

CLI

Earliest failure stage

Native analysis or reconstruction

Relevant output or evidence

Actual reduced-probe stdout:

{"name":"matching-owner","exitCode":0,"status":"ready","obligation":"verified","owner":"1","proofOwner":"1","diagnostics":[]}
{"name":"changed-owner-old-proof","exitCode":0,"status":"ready","obligation":"verified","owner":"2","proofOwner":"1","diagnostics":[]}
{"name":"clear-verifier-workaround","exitCode":0,"status":"open","obligation":"implemented","owner":"2","proofOwner":"1","diagnostics":["missing-verifier"]}

owner and proofOwner show the first character of their full 64-character digests. The changed-owner request differs from the matching-owner request only in the manifest owner digest.

Source evidence: proof qualification checks authority, confidence, operation, passing status and enumerated IDs; fixture evaluation and verifier evaluation supply those IDs without the current owner identity.

Typed outcome or recovery expected

A typed diagnostic that the supplied proof does not establish the current implementation's fixture/verifier result, with obligation status below verified and ledger status below ready.

Analysis or suspected cause

Source-derived: ExpectedProof has no owner-digest field. evidenceAuthoritySupportsProof neither receives the current owner digest nor compares the Evidence subject digest with it. The current binding is serialized into the ledger, but both fixture and verifier qualification ignore its implementation identity. The observed synthetic mismatch therefore passes all existing qualification checks.

No implementation change or proposed public schema is included in this report.

Additional context

AI-assisted disclosure: an OpenAI Codex agent performed source review, wrote and ran the synthetic probes, and drafted this report. No human review is implied.

Duplicate searches covered both open and closed issues using owner_sha256, obligation_version, obligation owner proof, and ledger stale, plus the local open-issue title index. No matching owner/proof-digest report was found. Related reports address different contracts: #3363 and #6770 concern absent Evidence references; #4396 requests negative controls on verifier sensitivity. Here all references resolve, and an existing proof for one explicit owner digest is reused for another. The known coverage reports #3354, #3937, #3890 and #3889 are excluded.

Limitations: no full executable startup, MCP transport, real verifier execution, published-package runtime, or broad test suite was tested. The observed claim is acceptance of mismatched synthetic proof through production source workflow code and CLI registration.

Triage assessment

  • Impact level: P2
  • Assessment status: supported
  • Impact basis: The production workflow and CLI registration return ready/verified without diagnostics when only the exact implementation digest changes and the retained authenticated proof still identifies the previous digest. This is a bounded incorrect verification result; no downstream incident was observed.
  • Workaround status: available
  • Workaround basis: Clearing the verifier binding after the implementation change was observed to return open/implemented with missing-verifier, preventing false closure while fresh proof is obtained.
Originally created by @coygeek on GitHub (Oct 23, 2026). Original GitHub issue: https://github.com/morluto/rea/issues/6854 ### Before submitting - [x] I searched the open and closed issues for a related report. - [x] I removed credentials, tokens, private paths, and sensitive target data. ### Area Evidence, artifacts, or reconstruction ### Observed behavior A reconstruction obligation remains `verified`, and its ledger remains `ready`, after changing only the manifest owner's implementation digest while keeping proof Evidence explicitly associated with the previous digest. The synthetic proof's authenticated `subject.digest.sha256` and `normalized_result.owner_sha256` both identify `"1".repeat(64)`. Changing `manifest.bindings[0].owner.owner_sha256` to `"2".repeat(64)` produces a new closure digest but no diagnostic. The proof, obligation, fixture, verifier and claim IDs are unchanged. Observed through the production application service and the production CLI command registration hosted in a minimal Incur CLI. The CLI registration calls the same service at [applicationCommands.ts](https://github.com/morluto/rea/blob/96ea32b7e4e28d3c9cd79a1de4b8e1ba3b4244e9/src/cli/applicationCommands.ts#L123-L138). The installed executable and MCP transport were not exercised. ### Reproduction With this source revision and its locked dependencies already installed, save the following as `/tmp/rea-owner-proof-repro.mjs`. From the source checkout, run: ```sh REA_ROOT="$PWD" node --import "$PWD/node_modules/tsx/dist/loader.mjs" /tmp/rea-owner-proof-repro.mjs ``` This constructs synthetic Evidence, invokes the actual registered `build-reconstruction-obligation-ledger` command, and writes the requests and replies beside the probe. No target, analysis provider, or declared verifier command executes. ```js import { writeFileSync } from 'node:fs'; import { join } from 'node:path'; import { pathToFileURL } from 'node:url'; const root = process.env.REA_ROOT; if (!root) throw new Error('Set REA_ROOT to the REA source checkout'); const load = file => import(pathToFileURL(join(root, file)).href); const { createEvidence } = await load('src/domain/evidence.ts'); const { createEvidenceBundle } = await load('src/domain/evidenceBundle.ts'); const { registerApplicationCommands } = await load('src/cli/applicationCommands.ts'); const { Cli } = await load('node_modules/incur/dist/index.js'); const { silentLogger } = await load('src/logger.ts'); const sha = c => c.repeat(64), id = 'review.sample'; const provider = { id: 'synthetic', name: 'Synthetic fixture', version: '1' }; const original = createEvidence(undefined, provider, { operation: 'observe', parameters: {}, result: { output: 1 }, confidence: 'observed', authority: 'shipped-artifact' }); const proof = createEvidence( { path: 'owner.js', sha256: sha('1'), format: 'javascript' }, provider, { predicateType: 'rea.reconstruction-proof', operation: 'verify_reconstruction_obligations', parameters: {}, result: { passed: true, obligation_ids: [id], fixture_ids: ['fixture.positive'], case_kinds: ['positive'], verifier_ids: ['verifier.sample'], claim_ids: ['claim.sample'], owner_sha256: sha('1') }, confidence: 'observed', authority: 'shipped-artifact' }); const request = { evidence_bundle: createEvidenceBundle([original, proof]), reviewed_obligations: [{ obligation_id: id, obligation_version: 1, title: 'Sample output', application_layer: 'other', family: 'reviewed', target: { artifact_sha256: null, application_node_id: null, semantic_node_id: null, location: 'original.js' }, required: true, required_case_kinds: ['positive'], required_original_authority: 'static', required_fixture_authority: 'unit', required_verifier_authority: 'unit', requires_parser_type: false, dependency_obligation_ids: [], residual_unknown_ids: [], unavailable_authority: [], required_next_evidence: [], disposition: 'active', review_evidence_ids: [original.evidence_id] }], manifest: { bindings: [{ obligation_id: id, owner: { module_path: 'owner.js', symbol: 'sample', owner_sha256: sha('1') }, parser_type: null, original_cases: [{ kind: 'positive', evidence_id: original.evidence_id, location: '/normalized_result/output' }], fixtures: [{ fixture_id: 'fixture.positive', case_kind: 'positive', authority: 'unit', evidence_ids: [proof.evidence_id] }], verifier: { verifier_id: 'verifier.sample', claim_id: 'claim.sample', command: 'synthetic verifier (not executed)', authority: 'unit', status: 'pass', result_evidence_id: proof.evidence_id, enumerated_obligation_ids: [id], nondeterminism: { mode: 'total-order', specification: 'Single output' } } }], contradictions: [] } }; for (const [name, owner, omitVerifier] of [ ['matching-owner', '1', false], ['changed-owner-old-proof', '2', false], ['clear-verifier-workaround', '2', true] ]) { const input = structuredClone(request), binding = input.manifest.bindings[0]; binding.owner.owner_sha256 = sha(owner); if (omitVerifier) binding.verifier = null; writeFileSync(join(import.meta.dirname, name + '.reduced-request.json'), JSON.stringify(input, null, 2)); const cli = Cli.create('rea', { sync: false, update: false }); registerApplicationCommands(cli, silentLogger); let output = '', exitCode = 0; await cli.serve(['build-reconstruction-obligation-ledger', JSON.stringify(input), '--json'], { env: {}, stdout: text => { output += text; }, exit: code => { exitCode = code; } }); writeFileSync(join(import.meta.dirname, name + '.reduced-cli.json'), output); const envelope = JSON.parse(output); const ledger = (envelope.normalized_result ? envelope : envelope.data).normalized_result; console.log(JSON.stringify({ name, exitCode, status: ledger.status, obligation: ledger.obligations[0].status, owner, proofOwner: proof.subject.digest.sha256[0], diagnostics: ledger.obligations[0].diagnostics.map(x => x.code) })); } ``` The matching-owner and changed-owner behavior was observed in two small probe runs; the reduced script above was run once and also checks the workaround. ### Expected behavior The matching-owner request should remain `ready`. Proof explicitly identifying the old implementation should not verify a binding naming a different implementation digest. The changed-owner request should retain an incompatibility or missing-current-proof diagnostic and stay open until proof for the current owner is supplied. The [manifest and closure guide](https://github.com/morluto/rea/blob/96ea32b7e4e28d3c9cd79a1de4b8e1ba3b4244e9/docs/reconstruction-obligation-ledgers.md#L226-L231) says that a binding names one owner and its exact implementation digest and requires authenticated, comparable fixture Evidence. The [closure contract](https://github.com/morluto/rea/blob/96ea32b7e4e28d3c9cd79a1de4b8e1ba3b4244e9/docs/reconstruction-obligation-ledgers.md#L10-L18) requires a passing verifier for a required obligation. An observation about the previous implementation does not establish that requirement for the changed owner. ### Impact and scope A routine implementation edit followed by rebuilding the ledger with retained proof can produce a clean verification result for code the proof does not describe. The result recomputes its identity, so a new ledger/closure digest does not establish that the new implementation was checked. This is a bounded incorrect analysis result. No deployment incident, stored-data loss, or real-world frequency was established. The tested input has one reviewed static obligation and one required positive fixture; other obligation families were not exercised. Workaround verified in the reduced probe: set the changed binding's `verifier` to `null` until new proof is available. It returns `open`, obligation `implemented`, and `missing-verifier`. This preserves the missing-verification state rather than retaining the previous passing claim. ### REA version `rea-agents` package version `6.7.0`; immutable main source snapshot `96ea32b7e4e28d3c9cd79a1de4b8e1ba3b4244e9`. The source snapshot, rather than the published package runtime, was tested. ### Runtime and platform Node.js `v26.12.1`; Linux `7.2.8-9-omarchy`, x86_64; repository-locked `tsx` loader and Incur dependencies. Node.js satisfies this revision's declared engine range. No Hopper, Ghidra or other analysis engine is involved. ### Target and artifact context Synthetic authenticated Evidence only. One original static observation, one passing proof with an owner subject digest, one reviewed obligation, and one manifest binding. Digest strings are inert test data; `owner.js` is a synthetic subject label and no file at that path is executed or inspected. ### Interface CLI ### Earliest failure stage Native analysis or reconstruction ### Relevant output or evidence Actual reduced-probe stdout: ```json {"name":"matching-owner","exitCode":0,"status":"ready","obligation":"verified","owner":"1","proofOwner":"1","diagnostics":[]} {"name":"changed-owner-old-proof","exitCode":0,"status":"ready","obligation":"verified","owner":"2","proofOwner":"1","diagnostics":[]} {"name":"clear-verifier-workaround","exitCode":0,"status":"open","obligation":"implemented","owner":"2","proofOwner":"1","diagnostics":["missing-verifier"]} ``` `owner` and `proofOwner` show the first character of their full 64-character digests. The changed-owner request differs from the matching-owner request only in the manifest owner digest. Source evidence: [proof qualification](https://github.com/morluto/rea/blob/96ea32b7e4e28d3c9cd79a1de4b8e1ba3b4244e9/src/application/ReconstructionObligationAuthority.ts#L63-L90) checks authority, confidence, operation, passing status and enumerated IDs; [fixture evaluation](https://github.com/morluto/rea/blob/96ea32b7e4e28d3c9cd79a1de4b8e1ba3b4244e9/src/application/ReconstructionObligationLedgerEvaluation.ts#L275-L292) and [verifier evaluation](https://github.com/morluto/rea/blob/96ea32b7e4e28d3c9cd79a1de4b8e1ba3b4244e9/src/application/ReconstructionObligationLedgerEvaluation.ts#L325-L342) supply those IDs without the current owner identity. ### Typed outcome or recovery expected A typed diagnostic that the supplied proof does not establish the current implementation's fixture/verifier result, with obligation status below `verified` and ledger status below `ready`. ### Analysis or suspected cause Source-derived: [`ExpectedProof`](https://github.com/morluto/rea/blob/96ea32b7e4e28d3c9cd79a1de4b8e1ba3b4244e9/src/application/ReconstructionObligationAuthority.ts#L7-L13) has no owner-digest field. `evidenceAuthoritySupportsProof` neither receives the current owner digest nor compares the Evidence subject digest with it. The current binding is serialized into the ledger, but both fixture and verifier qualification ignore its implementation identity. The observed synthetic mismatch therefore passes all existing qualification checks. No implementation change or proposed public schema is included in this report. ### Additional context AI-assisted disclosure: an OpenAI Codex agent performed source review, wrote and ran the synthetic probes, and drafted this report. No human review is implied. Duplicate searches covered both open and closed issues using `owner_sha256`, `obligation_version`, `obligation owner proof`, and `ledger stale`, plus the local open-issue title index. No matching owner/proof-digest report was found. Related reports address different contracts: [#3363](https://github.com/morluto/rea/issues/3363) and [#6770](https://github.com/morluto/rea/issues/6770) concern absent Evidence references; [#4396](https://github.com/morluto/rea/issues/4396) requests negative controls on verifier sensitivity. Here all references resolve, and an existing proof for one explicit owner digest is reused for another. The known coverage reports #3354, #3937, #3890 and #3889 are excluded. Limitations: no full executable startup, MCP transport, real verifier execution, published-package runtime, or broad test suite was tested. The observed claim is acceptance of mismatched synthetic proof through production source workflow code and CLI registration. ## Triage assessment - Impact level: P2 - Assessment status: supported - Impact basis: The production workflow and CLI registration return ready/verified without diagnostics when only the exact implementation digest changes and the retained authenticated proof still identifies the previous digest. This is a bounded incorrect verification result; no downstream incident was observed. - Workaround status: available - Workaround basis: Clearing the verifier binding after the implementation change was observed to return open/implemented with missing-verifier, preventing false closure while fresh proof is obtained.
Sign in to join this conversation.
No milestone
No project
No assignees
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference
morluto/rea#4193
No description provided.