[GH-ISSUE #6758] [Bug] Managed/native verification equates distinct explicit PE module extensions #4117

New issue

Closed

opened 2026-10-31 00:46:57 +00:00 by bsakaguchi · 0 comments

bsakaguchi commented

2026-10-31 00:46:57 +00:00

Owner

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

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

executeManagedNativeBoundaries, the shared application entry for verify_managed_native_boundaries, verifies an import from nativehelper.dll using a function observation whose PE module is nativehelper.exe or nativehelper.node. It returns status: "verified", basis: "exact-function-name", and confidence: "observed" for these distinct explicit module names. The generated managed PE metadata has complete coverage. Native function Evidence is synthetic; no native provider or CLR loading was executed.

Reproduction

From a locked-dependency source checkout, save the following as /tmp/module-extension.mts, then run node --import tsx /tmp/module-extension.mts from the checkout root. This is the application-boundary fixture actually executed, with two failing extension cases and three controls. It creates only in-memory fixture metadata and authenticated synthetic function Evidence.

import assert from 'node:assert/strict';
import { pathToFileURL } from 'node:url';
const root = process.argv[2] ?? process.cwd();
const load = (path: string) => import(pathToFileURL(`${root}/${path}`).href);
const { buildManagedPeFixture, managedPeFixtureTarget } = await load('src/dotnet/ManagedPe.fixture.ts');
const { inspectManagedNativeBoundariesBytes } = await load('src/dotnet/ManagedNativeBoundaryInspector.ts');
const { executeManagedNativeBoundaries } = await load('src/application/managed/ManagedNativeVerificationService.ts');
const { createEvidence } = await load('src/domain/evidence.ts');
const { functionDossierSchema } = await load('src/domain/hopperValues.ts');
const { MANAGED_NATIVE_VERIFICATION_EXAMPLE } = await load('src/contracts/managed/managedWorkflowExamples.ts');
const provider = MANAGED_NATIVE_VERIFICATION_EXAMPLE.managed_boundaries.provider;
const nativeProvider = MANAGED_NATIVE_VERIFICATION_EXAMPLE.native_observations[0].provider;
const dossier = functionDossierSchema.parse({
  procedure: { address: '0x1000', name: 'open_native',
    classification: { external: false, thunk: false, thunk_target: null, provenance: 'synthetic-provider' },
    body: { available: false, reason: 'Generated local fixture; no native provider invoked' }, signature: null, locals: [] },
  pseudocode: '', assembly: [], comments: [], callers: [], callees: [],
  incoming_references: [], outgoing_references: [], referenced_strings: [], referenced_names: [],
  basic_blocks: [], native_api: null, native_value_flow: null, limitations: []
});
for (const [scope, modulePath, expectedStatus] of [
  ['nativehelper.dll', '/tmp/nativehelper.dll', 'verified'],
  ['nativehelper.dll', '/tmp/nativehelper.exe', 'contradicted'],
  ['nativehelper.dll', '/tmp/nativehelper.node', 'contradicted'],
  ['nativehelper.dll', '/tmp/other.dll', 'contradicted'],
  ['nativehelper', '/tmp/nativehelper.dll', 'verified'],
] as const) {
  const bytes = buildManagedPeFixture({ pinvoke: { moduleName: scope, importName: 'open_native' } });
  const inspected = inspectManagedNativeBoundariesBytes(bytes, managedPeFixtureTarget(bytes));
  assert.equal(inspected.coverage.state, 'complete');
  assert.equal(inspected.pinvoke_imports[0].import_scope_name, scope);
  const managed = createEvidence(undefined, provider, {
    operation: 'inspect_managed_native_boundaries', parameters: {}, result: inspected, rawResult: null
  });
  const native = createEvidence({ path: modulePath, sha256: '8'.repeat(64), format: 'pe' }, nativeProvider, {
    operation: 'analyze_function', parameters: {}, result: dossier, rawResult: null
  });
  const execution = executeManagedNativeBoundaries({ managed_boundaries: managed, native_observations: [native] });
  assert.equal(execution.ok, true);
  if (!execution.ok) throw execution.error;
  const result = execution.value.evidence.normalized_result;
  const observed = result.pinvoke_imports[0];
  console.log(JSON.stringify({ scope, modulePath, expectedStatus,
    status: observed.status, basis: observed.basis, confidence: observed.confidence,
    summary: result.summary }));
}

Expected behavior

Distinct explicit PE module filenames must not become an observed declaration correspondence merely because their stems match. For the .dll versus .exe/.node cases, preserve the module mismatch, or leave correspondence unresolved if there is insufficient information; do not assert verified correspondence without evidence of a mapping. Retain exact-name matching and the extensionless-name control.

docs/managed-code-analysis.md:455–463 defines comparison of declared module and entry-point identities. tests/conformance/providers/managed/managedNativeVerification.test.ts:252–294 demonstrates that a matching function from a different named module is contradicted with module-mismatch. Microsoft's native-library loading rules add .dll on Windows only when the name does not already end with .dll or .exe; they do not establish substitution between these explicit names.

Impact and scope

Both demonstrated extension mismatches produced false positive verification in the single fixture run; all three controls produced the expected classifications. This can make supplied native evidence appear to satisfy a managed import declared against a different module. The observed defect is declaration correspondence, not an observed CLR loading failure. The result retains the original import scope and matched module path, so callers can manually compare those explicit filenames. Real-provider and transport behavior were not tested.

REA version

6.7.0, source commit 2bcd7e6d13f0a8118d6619718254255e84f75d86; the latest npm release was confirmed before this investigation.

Runtime and platform

Node.js v26.12.1; Linux x86_64; locked dependencies installed with npm ci --ignore-scripts; source loaded with tsx. No Hopper or Ghidra process ran.

Target and artifact context

Generated local PE/CLI metadata with one P/Invoke import; authenticated synthetic analyze_function Evidence with PE module filenames and an unavailable function body. No private target data or live configuration was used.

Interface

Other

Earliest failure stage

Native analysis or reconstruction

Relevant output or evidence

Actual fixture output, exit status 0:

{"scope":"nativehelper.dll","modulePath":"/tmp/nativehelper.dll","expectedStatus":"verified","status":"verified","basis":"exact-function-name","confidence":"observed","summary":{"verified":1,"inferred":0,"unresolved":0,"contradicted":0,"native_body_unresolved":0}}
{"scope":"nativehelper.dll","modulePath":"/tmp/nativehelper.exe","expectedStatus":"contradicted","status":"verified","basis":"exact-function-name","confidence":"observed","summary":{"verified":1,"inferred":0,"unresolved":0,"contradicted":0,"native_body_unresolved":0}}
{"scope":"nativehelper.dll","modulePath":"/tmp/nativehelper.node","expectedStatus":"contradicted","status":"verified","basis":"exact-function-name","confidence":"observed","summary":{"verified":1,"inferred":0,"unresolved":0,"contradicted":0,"native_body_unresolved":0}}
{"scope":"nativehelper.dll","modulePath":"/tmp/other.dll","expectedStatus":"contradicted","status":"contradicted","basis":"module-mismatch","confidence":"unknown","summary":{"verified":0,"inferred":0,"unresolved":0,"contradicted":1,"native_body_unresolved":0}}
{"scope":"nativehelper","modulePath":"/tmp/nativehelper.dll","expectedStatus":"verified","status":"verified","basis":"exact-function-name","confidence":"observed","summary":{"verified":1,"inferred":0,"unresolved":0,"contradicted":0,"native_body_unresolved":0}}

The direct application call authenticates and parses both inputs, then creates the returned verification Evidence. Source reachability is ManagedNativeVerificationService.ts:18–29 → managedNativeVerification.ts:20–43 → managedNativeVerificationMatch.ts:55–98,175–239. CLI/MCP transport execution and real native-provider observations remain unexecuted.

Typed outcome or recovery expected

Preserve the candidate and its explicit filename, with contradicted/module-mismatch for the demonstrated known difference, or an explicitly unresolved correspondence where the comparison cannot be established. Keep exact .dll and extensionless-name controls working.

Analysis or suspected cause

Source inspection shows normalizeModule strips .dll, .dylib, .so, .node, and .exe indiscriminately. moduleValueCompatibility accepts matching stems before inspecting the native format, so distinct explicit filenames become a match. A matching function name then promotes the result to verified. This is source-supported reasoning consistent with the executed controls.

Additional context

Open and closed searches included repo:morluto/rea is:issue in:title managed module extension, repo:morluto/rea is:issue in:title P/Invoke, repo:morluto/rea is:issue in:title pinvoke, and repo:morluto/rea is:issue in:title "module" "verification". Related reports #3351, #6652, and #5467 concern path syntax, case, and missing identity respectively; this trigger uses known PE identities differing in explicit suffix.

Three interpretations were considered: accept every shared stem, mark ambiguous aliases unresolved, or preserve explicit filenames while admitting supported platform aliases. Preserving explicit names is strongest because both filename facts are known and no custom resolver or mapping is supplied. A custom resolver could establish a separate correspondence; this report does not claim .exe or .node files can never hold loadable native code. Independent review inspected the fixture and controls before drafting and found no blocking premise gap. No implementation change was made.

Triage assessment

Impact level: P2
Assessment status: supported
Impact basis: Two distinct explicit PE module-name mismatches were classified as observed verified declarations in the executed application fixture; exact-name and different-stem controls discriminate the failure.
Workaround status: available
Workaround basis: The returned import scope and matched native module path preserve the differing explicit filenames, allowing the caller to reject the false correspondence manually.

Originally created by @coygeek on GitHub (Oct 23, 2026). Original GitHub issue: https://github.com/morluto/rea/issues/6758 ## 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 `executeManagedNativeBoundaries`, the shared application entry for `verify_managed_native_boundaries`, verifies an import from `nativehelper.dll` using a function observation whose PE module is `nativehelper.exe` or `nativehelper.node`. It returns `status: "verified"`, `basis: "exact-function-name"`, and `confidence: "observed"` for these distinct explicit module names. The generated managed PE metadata has complete coverage. Native function Evidence is synthetic; no native provider or CLR loading was executed. ## Reproduction From a locked-dependency source checkout, save the following as `/tmp/module-extension.mts`, then run `node --import tsx /tmp/module-extension.mts` from the checkout root. This is the application-boundary fixture actually executed, with two failing extension cases and three controls. It creates only in-memory fixture metadata and authenticated synthetic function Evidence. ```typescript import assert from 'node:assert/strict'; import { pathToFileURL } from 'node:url'; const root = process.argv[2] ?? process.cwd(); const load = (path: string) => import(pathToFileURL(`${root}/${path}`).href); const { buildManagedPeFixture, managedPeFixtureTarget } = await load('src/dotnet/ManagedPe.fixture.ts'); const { inspectManagedNativeBoundariesBytes } = await load('src/dotnet/ManagedNativeBoundaryInspector.ts'); const { executeManagedNativeBoundaries } = await load('src/application/managed/ManagedNativeVerificationService.ts'); const { createEvidence } = await load('src/domain/evidence.ts'); const { functionDossierSchema } = await load('src/domain/hopperValues.ts'); const { MANAGED_NATIVE_VERIFICATION_EXAMPLE } = await load('src/contracts/managed/managedWorkflowExamples.ts'); const provider = MANAGED_NATIVE_VERIFICATION_EXAMPLE.managed_boundaries.provider; const nativeProvider = MANAGED_NATIVE_VERIFICATION_EXAMPLE.native_observations[0].provider; const dossier = functionDossierSchema.parse({ procedure: { address: '0x1000', name: 'open_native', classification: { external: false, thunk: false, thunk_target: null, provenance: 'synthetic-provider' }, body: { available: false, reason: 'Generated local fixture; no native provider invoked' }, signature: null, locals: [] }, pseudocode: '', assembly: [], comments: [], callers: [], callees: [], incoming_references: [], outgoing_references: [], referenced_strings: [], referenced_names: [], basic_blocks: [], native_api: null, native_value_flow: null, limitations: [] }); for (const [scope, modulePath, expectedStatus] of [ ['nativehelper.dll', '/tmp/nativehelper.dll', 'verified'], ['nativehelper.dll', '/tmp/nativehelper.exe', 'contradicted'], ['nativehelper.dll', '/tmp/nativehelper.node', 'contradicted'], ['nativehelper.dll', '/tmp/other.dll', 'contradicted'], ['nativehelper', '/tmp/nativehelper.dll', 'verified'], ] as const) { const bytes = buildManagedPeFixture({ pinvoke: { moduleName: scope, importName: 'open_native' } }); const inspected = inspectManagedNativeBoundariesBytes(bytes, managedPeFixtureTarget(bytes)); assert.equal(inspected.coverage.state, 'complete'); assert.equal(inspected.pinvoke_imports[0].import_scope_name, scope); const managed = createEvidence(undefined, provider, { operation: 'inspect_managed_native_boundaries', parameters: {}, result: inspected, rawResult: null }); const native = createEvidence({ path: modulePath, sha256: '8'.repeat(64), format: 'pe' }, nativeProvider, { operation: 'analyze_function', parameters: {}, result: dossier, rawResult: null }); const execution = executeManagedNativeBoundaries({ managed_boundaries: managed, native_observations: [native] }); assert.equal(execution.ok, true); if (!execution.ok) throw execution.error; const result = execution.value.evidence.normalized_result; const observed = result.pinvoke_imports[0]; console.log(JSON.stringify({ scope, modulePath, expectedStatus, status: observed.status, basis: observed.basis, confidence: observed.confidence, summary: result.summary })); } ``` ## Expected behavior Distinct explicit PE module filenames must not become an observed declaration correspondence merely because their stems match. For the `.dll` versus `.exe`/`.node` cases, preserve the module mismatch, or leave correspondence unresolved if there is insufficient information; do not assert verified correspondence without evidence of a mapping. Retain exact-name matching and the extensionless-name control. `docs/managed-code-analysis.md:455–463` defines comparison of declared module and entry-point identities. `tests/conformance/providers/managed/managedNativeVerification.test.ts:252–294` demonstrates that a matching function from a different named module is `contradicted` with `module-mismatch`. Microsoft's [native-library loading rules](https://learn.microsoft.com/en-us/dotnet/standard/native-interop/native-library-loading#library-name-variations) add `.dll` on Windows only when the name does not already end with `.dll` or `.exe`; they do not establish substitution between these explicit names. ## Impact and scope Both demonstrated extension mismatches produced false positive verification in the single fixture run; all three controls produced the expected classifications. This can make supplied native evidence appear to satisfy a managed import declared against a different module. The observed defect is declaration correspondence, not an observed CLR loading failure. The result retains the original import scope and matched module path, so callers can manually compare those explicit filenames. Real-provider and transport behavior were not tested. ## REA version 6.7.0, source commit `2bcd7e6d13f0a8118d6619718254255e84f75d86`; the latest npm release was confirmed before this investigation. ## Runtime and platform Node.js v26.12.1; Linux x86_64; locked dependencies installed with `npm ci --ignore-scripts`; source loaded with tsx. No Hopper or Ghidra process ran. ## Target and artifact context Generated local PE/CLI metadata with one P/Invoke import; authenticated synthetic `analyze_function` Evidence with PE module filenames and an unavailable function body. No private target data or live configuration was used. ## Interface Other ## Earliest failure stage Native analysis or reconstruction ## Relevant output or evidence Actual fixture output, exit status 0: ```jsonl {"scope":"nativehelper.dll","modulePath":"/tmp/nativehelper.dll","expectedStatus":"verified","status":"verified","basis":"exact-function-name","confidence":"observed","summary":{"verified":1,"inferred":0,"unresolved":0,"contradicted":0,"native_body_unresolved":0}} {"scope":"nativehelper.dll","modulePath":"/tmp/nativehelper.exe","expectedStatus":"contradicted","status":"verified","basis":"exact-function-name","confidence":"observed","summary":{"verified":1,"inferred":0,"unresolved":0,"contradicted":0,"native_body_unresolved":0}} {"scope":"nativehelper.dll","modulePath":"/tmp/nativehelper.node","expectedStatus":"contradicted","status":"verified","basis":"exact-function-name","confidence":"observed","summary":{"verified":1,"inferred":0,"unresolved":0,"contradicted":0,"native_body_unresolved":0}} {"scope":"nativehelper.dll","modulePath":"/tmp/other.dll","expectedStatus":"contradicted","status":"contradicted","basis":"module-mismatch","confidence":"unknown","summary":{"verified":0,"inferred":0,"unresolved":0,"contradicted":1,"native_body_unresolved":0}} {"scope":"nativehelper","modulePath":"/tmp/nativehelper.dll","expectedStatus":"verified","status":"verified","basis":"exact-function-name","confidence":"observed","summary":{"verified":1,"inferred":0,"unresolved":0,"contradicted":0,"native_body_unresolved":0}} ``` The direct application call authenticates and parses both inputs, then creates the returned verification Evidence. Source reachability is `ManagedNativeVerificationService.ts:18–29` → `managedNativeVerification.ts:20–43` → `managedNativeVerificationMatch.ts:55–98,175–239`. CLI/MCP transport execution and real native-provider observations remain unexecuted. ## Typed outcome or recovery expected Preserve the candidate and its explicit filename, with `contradicted`/`module-mismatch` for the demonstrated known difference, or an explicitly unresolved correspondence where the comparison cannot be established. Keep exact `.dll` and extensionless-name controls working. ## Analysis or suspected cause Source inspection shows `normalizeModule` strips `.dll`, `.dylib`, `.so`, `.node`, and `.exe` indiscriminately. `moduleValueCompatibility` accepts matching stems before inspecting the native format, so distinct explicit filenames become a match. A matching function name then promotes the result to verified. This is source-supported reasoning consistent with the executed controls. ## Additional context Open and closed searches included `repo:morluto/rea is:issue in:title managed module extension`, `repo:morluto/rea is:issue in:title P/Invoke`, `repo:morluto/rea is:issue in:title pinvoke`, and `repo:morluto/rea is:issue in:title "module" "verification"`. Related reports [#3351](https://github.com/morluto/rea/issues/3351), [#6652](https://github.com/morluto/rea/issues/6652), and [#5467](https://github.com/morluto/rea/issues/5467) concern path syntax, case, and missing identity respectively; this trigger uses known PE identities differing in explicit suffix. Three interpretations were considered: accept every shared stem, mark ambiguous aliases unresolved, or preserve explicit filenames while admitting supported platform aliases. Preserving explicit names is strongest because both filename facts are known and no custom resolver or mapping is supplied. A custom resolver could establish a separate correspondence; this report does not claim `.exe` or `.node` files can never hold loadable native code. Independent review inspected the fixture and controls before drafting and found no blocking premise gap. No implementation change was made. ## Triage assessment - Impact level: P2 - Assessment status: supported - Impact basis: Two distinct explicit PE module-name mismatches were classified as observed verified declarations in the executed application fixture; exact-name and different-stem controls discriminate the failure. - Workaround status: available - Workaround basis: The returned import scope and matched native module path preserve the differing explicit filenames, allowing the caller to reject the false correspondence manually.

bsakaguchi closed this issue

2026-10-31 00:46:57 +00:00

bsakaguchi referenced this issue

2026-10-31 01:11:36 +00:00

[PR #4117] [MERGED] fix(verifiers): align WABT operation timeout #6067