[GH-ISSUE #5903] [Bug] Partial managed/native verification coverage is omitted from residual unknowns #3581

New issue

Closed

opened 2026-10-31 00:42:05 +00:00 by bsakaguchi · 0 comments

bsakaguchi commented

2026-10-31 00:42:05 +00:00

Owner

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

Before submitting

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

Area

MCP or agent integration

Observed behavior

verify_managed_native_boundaries returns successful Evidence with coverage.status: "partial" but creates no residual unknown when summary.unresolved, summary.contradicted and summary.native_body_unresolved are all zero. A subsequent MCP list_unknowns request filtered to managed-native-verification returns total: 0.

This reproduced for three inputs: unavailable boundary inspection from a native PE without CLI metadata; unavailable inspection from corrupt managed metadata; and one successfully verified P/Invoke with an additional unsupported native observation. The returned Evidence correctly retains partial coverage and its limitation. The omission is in automatic session unknown registration.

Reproduction

Executed a focused test through the repository's in-memory MCP harness, which uses production server registration. The first two inputs come from the actual static byte inspector and repository PE fixture builders, then are authenticated with createEvidence. The inspection MCP command itself was not invoked. Verification and unknown listing both use real MCP requests. Native observations are simulated; no native analysis provider or target code executes.

Save this test as tests/boundary/mcp/managedNativeCoverageRepro.test.ts in the source checkout and run:

./node_modules/.bin/vitest run --project mcp-boundary tests/boundary/mcp/managedNativeCoverageRepro.test.ts --maxWorkers 1

import { expect, it } from "vitest";
import { MANAGED_NATIVE_VERIFICATION_EXAMPLE as example } from "../../../src/contracts/managed/managedWorkflowExamples.js";
import { createEvidence, parseEvidence } from "../../../src/domain/evidence.js";
import { managedNativeVerificationResultSchema } from "../../../src/domain/managed/managedNativeVerificationSchemas.js";
import { inspectManagedNativeBoundariesBytes } from "../../../src/dotnet/ManagedNativeBoundaryInspector.js";
import { buildManagedPeFixture, buildNativePeFixture, managedPeFixtureTarget } from "../../../src/dotnet/ManagedPe.fixture.js";
import { createApplicationMcpHarness } from "../../fixtures/applicationMcpHarness.js";
import { createTestBinarySession } from "../../fixtures/binarySession.js";

const unavailable = (malformed: boolean) => {
  const bytes = malformed
    ? buildManagedPeFixture({ corruptMetadataSignature: true })
    : buildNativePeFixture();
  const result = inspectManagedNativeBoundariesBytes(bytes, managedPeFixtureTarget(bytes));
  expect(result.coverage.state).toBe("unavailable");
  return createEvidence(undefined, example.managed_boundaries.provider, {
    operation: "inspect_managed_native_boundaries", parameters: {}, result,
    limitations: result.limitations,
  });
};
const unsupported = createEvidence(undefined,
  { id: "fixture-native", name: "Fixture native", version: "1" },
  { operation: "inspect_signature", parameters: {}, result: { signed: true },
    limitations: ["Synthetic native observation; no provider executed."] });

for (const scenario of ["complete", "native-pe", "malformed-metadata", "unsupported-extra", "unresolved-control"] as const) {
  it(`records coverage unknowns: ${scenario}`, async () => {
    const harness = await createApplicationMcpHarness({ session: createTestBinarySession(() => {
      throw new Error("No provider should execute");
    }) });
    try {
      const managed = scenario === "native-pe" ? unavailable(false)
        : scenario === "malformed-metadata" ? unavailable(true) : example.managed_boundaries;
      const response = await harness.client.callTool({ name: "verify_managed_native_boundaries", arguments: {
        managed_boundaries: managed,
        native_observations: scenario === "unsupported-extra" ? [...example.native_observations, unsupported]
          : scenario === "unresolved-control" ? [unsupported] : example.native_observations,
      } });
      expect(response.isError, JSON.stringify(response.content)).not.toBe(true);
      const result = managedNativeVerificationResultSchema.parse(parseEvidence(response.structuredContent).normalized_result);
      const unknowns = await harness.client.callTool({ name: "list_unknowns", arguments: { domain: "managed-native-verification" } });
      expect(unknowns.isError, JSON.stringify(unknowns.content)).not.toBe(true);
      const total = (unknowns.structuredContent as { result: { total: number } }).result.total;
      console.log(JSON.stringify({ scenario, summary: result.summary, coverage: result.coverage,
        native: result.native_observations, unknowns: total }));
      expect(result.coverage.status).toBe(scenario === "complete" ? "complete-within-inputs" : "partial");
      if (scenario !== "unresolved-control") expect(result.summary).toMatchObject({ unresolved: 0, contradicted: 0, native_body_unresolved: 0 });
      expect(total).toBe(scenario === "complete" ? 0 : 1);
    } finally { await harness.close(); }
  });
}

All five scenarios ran once. The three coverage-only cases fail the final expectation with expected +0 to be 1; both controls pass. All calls succeed and their coverage/count assertions pass before that expectation.

Expected behavior

Partial verification coverage should register a residual coverage question even when every observed declaration matches, or no declarations could be admitted. Zero observed unresolved items does not establish a complete inventory.

The tool design contract requires missing coverage to remain unknown. The verification domain explicitly marks incomplete managed inputs and unsupported native observations as partial. The export-shape workflow already includes incomplete coverage when deciding whether to register an unknown.

Impact and scope

P2: session consumers relying on the residual unknown registry miss a coverage gap. A caller can work around this by examining the returned verification Evidence's coverage and limitations. No incorrect symbol match, target mutation or security boundary crossing was observed.

Observed scope is the three synthetic input shapes above over MCP. A genuinely unresolved declaration still records an unknown, and complete verification correctly leaves none. Real-artifact frequency and other platforms were not measured. CLI verification does not exercise this MCP session-registration path.

REA version

6.7.0; source revision 52415975942a4b9c53a817915b313ccc404f280e.

Runtime and platform

macOS 27.0.1 arm64; Node.js v26.12.0; repository-pinned Vitest 5.0.3. No Hopper, Ghidra, IDA or CLR execution.

Target and artifact context

Repository-generated PE fixtures without CLI metadata or with a corrupt metadata signature; the shipped managed/native verification example with one P/Invoke and a matching Mach-O export; and authenticated synthetic inspect_signature Evidence supplying no native symbols.

Interface

MCP

Earliest failure stage

Artifact or evidence registration

Relevant output or evidence

Observed public MCP results, with counts reduced to the fields relevant to this issue:

Scenario	verified	unresolved	coverage.status	list_unknowns total
Complete control	1	0	complete-within-inputs	0
Native PE, no CLI metadata	0	0	partial	0
Corrupt metadata signature	0	0	partial	0
Matched declaration plus unsupported observation	1	0	partial	0
Unresolved control	0	1	partial	1

The mixed-observation case reports native_observations: { total: 2, accepted: 1, unsupported: 1, symbols: 1 }. Vitest reports three failed assertions and two passing controls. Each harness closes in a finally block.

Typed outcome or recovery expected

Keep returning the successful verification Evidence and its existing limitations, and register a residual unknown linked to that result whenever verification coverage is partial. Preserve the complete and unresolved controls and exact-repeat behavior. No fix or restoration was tested.

Analysis or suspected cause

Source-derived explanation: the MCP registration checks only three summary counts before choosing plain Evidence recording versus Evidence-with-unknown recording. It ignores verification.coverage.status.

The domain coverage computation sets partial coverage whenever managed coverage is not complete or any observation is unsupported. The boundary inspector returns empty arrays with unavailable coverage when no CLI metadata is admitted. These cases can therefore have zero unresolved item counts while still requiring a residual coverage question.

Additional context

Fetched upstream before preparing this report. The relevant registration, domain and boundary-inspector files are unchanged between the tested revision and origin/main at c324d31b45fcab77e4ed7320ed60f0bf5a4ba188. Execution on that later revision is not claimed.

Related reports checked: #3333 concerns collisions between distinct already-unresolved requests; #4055 concerns runtime-provided methods being counted as unresolved native bodies; #4639 concerns rejection of unsupported observations; #5468 concerns empty import names failing output validation; #558 concerns other incomplete-comparison facets; #4057 requests additional native symbol sources. None describes this coverage-only omission. The residual audit prompt was not executed.

Originally created by @coygeek on GitHub (Oct 21, 2026). Original GitHub issue: https://github.com/morluto/rea/issues/5903 ### 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 MCP or agent integration ### Observed behavior `verify_managed_native_boundaries` returns successful Evidence with `coverage.status: "partial"` but creates no residual unknown when `summary.unresolved`, `summary.contradicted` and `summary.native_body_unresolved` are all zero. A subsequent MCP `list_unknowns` request filtered to `managed-native-verification` returns `total: 0`. This reproduced for three inputs: unavailable boundary inspection from a native PE without CLI metadata; unavailable inspection from corrupt managed metadata; and one successfully verified P/Invoke with an additional unsupported native observation. The returned Evidence correctly retains partial coverage and its limitation. The omission is in automatic session unknown registration. ### Reproduction Executed a focused test through the repository's in-memory MCP harness, which uses production server registration. The first two inputs come from the actual static byte inspector and repository PE fixture builders, then are authenticated with `createEvidence`. The inspection MCP command itself was not invoked. Verification and unknown listing both use real MCP requests. Native observations are simulated; no native analysis provider or target code executes. Save this test as `tests/boundary/mcp/managedNativeCoverageRepro.test.ts` in the source checkout and run: ```sh ./node_modules/.bin/vitest run --project mcp-boundary tests/boundary/mcp/managedNativeCoverageRepro.test.ts --maxWorkers 1 ``` ```ts import { expect, it } from "vitest"; import { MANAGED_NATIVE_VERIFICATION_EXAMPLE as example } from "../../../src/contracts/managed/managedWorkflowExamples.js"; import { createEvidence, parseEvidence } from "../../../src/domain/evidence.js"; import { managedNativeVerificationResultSchema } from "../../../src/domain/managed/managedNativeVerificationSchemas.js"; import { inspectManagedNativeBoundariesBytes } from "../../../src/dotnet/ManagedNativeBoundaryInspector.js"; import { buildManagedPeFixture, buildNativePeFixture, managedPeFixtureTarget } from "../../../src/dotnet/ManagedPe.fixture.js"; import { createApplicationMcpHarness } from "../../fixtures/applicationMcpHarness.js"; import { createTestBinarySession } from "../../fixtures/binarySession.js"; const unavailable = (malformed: boolean) => { const bytes = malformed ? buildManagedPeFixture({ corruptMetadataSignature: true }) : buildNativePeFixture(); const result = inspectManagedNativeBoundariesBytes(bytes, managedPeFixtureTarget(bytes)); expect(result.coverage.state).toBe("unavailable"); return createEvidence(undefined, example.managed_boundaries.provider, { operation: "inspect_managed_native_boundaries", parameters: {}, result, limitations: result.limitations, }); }; const unsupported = createEvidence(undefined, { id: "fixture-native", name: "Fixture native", version: "1" }, { operation: "inspect_signature", parameters: {}, result: { signed: true }, limitations: ["Synthetic native observation; no provider executed."] }); for (const scenario of ["complete", "native-pe", "malformed-metadata", "unsupported-extra", "unresolved-control"] as const) { it(`records coverage unknowns: ${scenario}`, async () => { const harness = await createApplicationMcpHarness({ session: createTestBinarySession(() => { throw new Error("No provider should execute"); }) }); try { const managed = scenario === "native-pe" ? unavailable(false) : scenario === "malformed-metadata" ? unavailable(true) : example.managed_boundaries; const response = await harness.client.callTool({ name: "verify_managed_native_boundaries", arguments: { managed_boundaries: managed, native_observations: scenario === "unsupported-extra" ? [...example.native_observations, unsupported] : scenario === "unresolved-control" ? [unsupported] : example.native_observations, } }); expect(response.isError, JSON.stringify(response.content)).not.toBe(true); const result = managedNativeVerificationResultSchema.parse(parseEvidence(response.structuredContent).normalized_result); const unknowns = await harness.client.callTool({ name: "list_unknowns", arguments: { domain: "managed-native-verification" } }); expect(unknowns.isError, JSON.stringify(unknowns.content)).not.toBe(true); const total = (unknowns.structuredContent as { result: { total: number } }).result.total; console.log(JSON.stringify({ scenario, summary: result.summary, coverage: result.coverage, native: result.native_observations, unknowns: total })); expect(result.coverage.status).toBe(scenario === "complete" ? "complete-within-inputs" : "partial"); if (scenario !== "unresolved-control") expect(result.summary).toMatchObject({ unresolved: 0, contradicted: 0, native_body_unresolved: 0 }); expect(total).toBe(scenario === "complete" ? 0 : 1); } finally { await harness.close(); } }); } ``` All five scenarios ran once. The three coverage-only cases fail the final expectation with `expected +0 to be 1`; both controls pass. All calls succeed and their coverage/count assertions pass before that expectation. ### Expected behavior Partial verification coverage should register a residual coverage question even when every observed declaration matches, or no declarations could be admitted. Zero observed unresolved items does not establish a complete inventory. The [tool design contract](https://github.com/morluto/rea/blob/52415975942a4b9c53a817915b313ccc404f280e/docs/tool-design.md#L49-L58) requires missing coverage to remain unknown. The verification domain explicitly marks incomplete managed inputs and unsupported native observations as partial. The [export-shape workflow](https://github.com/morluto/rea/blob/52415975942a4b9c53a817915b313ccc404f280e/src/server/registerApplicationTools/compareExportShapes.ts#L53-L64) already includes incomplete coverage when deciding whether to register an unknown. ### Impact and scope P2: session consumers relying on the residual unknown registry miss a coverage gap. A caller can work around this by examining the returned verification Evidence's coverage and limitations. No incorrect symbol match, target mutation or security boundary crossing was observed. Observed scope is the three synthetic input shapes above over MCP. A genuinely unresolved declaration still records an unknown, and complete verification correctly leaves none. Real-artifact frequency and other platforms were not measured. CLI verification does not exercise this MCP session-registration path. ### REA version 6.7.0; source revision `52415975942a4b9c53a817915b313ccc404f280e`. ### Runtime and platform macOS 27.0.1 arm64; Node.js v26.12.0; repository-pinned Vitest 5.0.3. No Hopper, Ghidra, IDA or CLR execution. ### Target and artifact context Repository-generated PE fixtures without CLI metadata or with a corrupt metadata signature; the shipped managed/native verification example with one P/Invoke and a matching Mach-O export; and authenticated synthetic `inspect_signature` Evidence supplying no native symbols. ### Interface MCP ### Earliest failure stage Artifact or evidence registration ### Relevant output or evidence Observed public MCP results, with counts reduced to the fields relevant to this issue: | Scenario | verified | unresolved | contradicted | native_body_unresolved | coverage.status | list_unknowns total | | --- | ---: | ---: | ---: | ---: | --- | ---: | | Complete control | 1 | 0 | 0 | 0 | complete-within-inputs | 0 | | Native PE, no CLI metadata | 0 | 0 | 0 | 0 | partial | 0 | | Corrupt metadata signature | 0 | 0 | 0 | 0 | partial | 0 | | Matched declaration plus unsupported observation | 1 | 0 | 0 | 0 | partial | 0 | | Unresolved control | 0 | 1 | 0 | 0 | partial | 1 | The mixed-observation case reports `native_observations: { total: 2, accepted: 1, unsupported: 1, symbols: 1 }`. Vitest reports three failed assertions and two passing controls. Each harness closes in a `finally` block. ### Typed outcome or recovery expected Keep returning the successful verification Evidence and its existing limitations, and register a residual unknown linked to that result whenever verification coverage is partial. Preserve the complete and unresolved controls and exact-repeat behavior. No fix or restoration was tested. ### Analysis or suspected cause Source-derived explanation: the [MCP registration](https://github.com/morluto/rea/blob/52415975942a4b9c53a817915b313ccc404f280e/src/server/registerManagedWorkflowTools/verifyManagedNativeBoundaries.ts#L80-L119) checks only three summary counts before choosing plain Evidence recording versus Evidence-with-unknown recording. It ignores `verification.coverage.status`. The [domain coverage computation](https://github.com/morluto/rea/blob/52415975942a4b9c53a817915b313ccc404f280e/src/domain/managed/managedNativeVerificationMatch.ts#L381-L390) sets partial coverage whenever managed coverage is not complete or any observation is unsupported. The [boundary inspector](https://github.com/morluto/rea/blob/52415975942a4b9c53a817915b313ccc404f280e/src/dotnet/ManagedNativeBoundaryInspector.ts#L41-L94) returns empty arrays with unavailable coverage when no CLI metadata is admitted. These cases can therefore have zero unresolved item counts while still requiring a residual coverage question. ### Additional context Fetched upstream before preparing this report. The relevant registration, domain and boundary-inspector files are unchanged between the tested revision and `origin/main` at `c324d31b45fcab77e4ed7320ed60f0bf5a4ba188`. Execution on that later revision is not claimed. Related reports checked: #3333 concerns collisions between distinct already-unresolved requests; #4055 concerns runtime-provided methods being counted as unresolved native bodies; #4639 concerns rejection of unsupported observations; #5468 concerns empty import names failing output validation; #558 concerns other incomplete-comparison facets; #4057 requests additional native symbol sources. None describes this coverage-only omission. The residual audit prompt was not executed.

bsakaguchi closed this issue

2026-10-31 00:42:05 +00:00

bsakaguchi referenced this issue

2026-10-31 01:09:48 +00:00

[PR #3581] feat(apktool): harden AAPT2 inspection and rebuild experiment #5838