diff --git a/docs/ida-provider.md b/docs/ida-provider.md index ddcaaef4b..b22a35cce 100644 --- a/docs/ida-provider.md +++ b/docs/ida-provider.md @@ -138,6 +138,8 @@ Run `npm run verify:ida -- --target /absolute/path/to/program --procedure main` Native verification requires `--second-procedure other_function --second-marker unique_second_body_text`; these options remain optional for the other profiles. The marker must occur in the second function's pseudocode and be absent from the first; the verifier also checks that returning to the first restores its text. +The verifier requires the resolved procedure in both inventory and procedure search, then compares address, assembly, pseudocode, instruction windows and relationship results with the CLI/MCP dossier. Supply `--expected-string known_literal` to check a known positive string inventory/search result and `--expected-xref 0xSOURCE` to check a known reference source address. Choose those oracles independently from the operation under test. Without them, string and xref correctness are listed in `unverified`; valid output shapes alone do not establish those behaviors. Callee parity does not independently establish semantic completeness. Native callee successes must report an explicit truncation marker; missing markers remain protocol failures. + The initial real workflows use stdio registrations for the legacy Windows GUI profile and a Windows x64 headless supervisor with IDA 9.3. The headless workflow has also passed on macOS arm64 with IDA Professional 9.1 (build 9.1.250226) against the same upstream commit `c133c3853faa111a9b00ee615c013b720d0c4acd`, using a source-built arm64 Mach-O fixture; Mach-O C symbols carry a leading underscore, so the procedure name is `_rea_fixture_add`. Streamable HTTP is tested against a loopback MCP fixture with the pinned client SDK; a real IDA HTTP-supervisor workflow remains unverified. Linux headless engine operation, other IDA releases, architectures, and modern attached GUI tools require their corresponding real workflows before support is claimed. Native Windows verification uses IDA Pro 9.3 with the public two-function fixture and Windows `whoami.exe`, using upstream `c9d15d98e8a143fc74f6e14037c48f63889b6d6c` with a loopback-listener change. It covers production CLI/MCP parity, distinct-function switching, identity and connection cleanup. See the [correctness and performance measurements](https://github.com/morluto/rea/blob/main/experiments/analysis-efficiency/ida-native-windows.md). This follow-up did not run Windows IDA Free or native macOS. diff --git a/experiments/analysis-efficiency/ida-native-windows.md b/experiments/analysis-efficiency/ida-native-windows.md index 835662fc4..9adbd2143 100644 --- a/experiments/analysis-efficiency/ida-native-windows.md +++ b/experiments/analysis-efficiency/ida-native-windows.md @@ -23,6 +23,25 @@ connecting. Dossier relationship coverage remains unknown when direct callers are unavailable, while standalone callee coverage retains its own observed state. It preserves the attached GUI database. +The later verification follow-up rejects native callee successes without an +explicit truncation marker, checks positive procedure inventory/search and +compares normalized function results. String and xref correctness require +independent positive oracles; runs without those oracles label them unverified. +Earlier reports established contract validity for these operations and did not +by themselves establish string/xref semantic correctness. + +The follow-up passed eight production checks with a known CRT literal confirmed +in the unchanged fixture bytes and a reference source address independently +identified from `main` assembly matching the C source. A loopback response-only +proxy in front of the real IDA Pro provider reproduced the earlier verifier +passing empty function inventories and xrefs. The corrected verifier rejected +those replies with positive oracles, empty string results and missing native +callee truncation markers. The comparison used verifier source `d1aaeee40` +with the same current adapter runtime; it is a verifier comparison, not an +engine performance comparison. Only response payloads were modified; the original +input digest stayed unchanged, the target was never executed, and the attached +GUI database was preserved. + The real application was a digest-verified, unchanged copy of Windows `whoami.exe`: 94,208 bytes, 243 recognized functions, and 314 upstream C-string observations. The selected 1,741-byte function had 20 resolved diff --git a/scripts/verify-real-ida.mjs b/scripts/verify-real-ida.mjs index c2d4d55cc..cedbf5076 100644 --- a/scripts/verify-real-ida.mjs +++ b/scripts/verify-real-ida.mjs @@ -18,6 +18,8 @@ const { values } = parseArgs({ procedure: { type: "string", default: "rea_fixture_add" }, "second-procedure": { type: "string" }, "second-marker": { type: "string" }, + "expected-string": { type: "string" }, + "expected-xref": { type: "string" }, "package-root": { type: "string" }, report: { type: "string" }, }, @@ -34,6 +36,8 @@ if ( throw new Error( "IDA verification requires --second-procedure and a nonempty --second-marker together; choose a marker unique to the second function's pseudocode.", ); +if (values["expected-string"] === "" || values["expected-xref"] === "") + throw new Error("IDA verification oracles must be nonempty."); const packageRoot = resolve( values["package-root"] ?? fileURLToPath(new URL("..", import.meta.url)), ); @@ -47,12 +51,14 @@ const [ { functionDossierSchema }, { readIdaConfiguration }, { createIdaMcpConnection }, + { idaAddressSchema }, ] = await Promise.all([ importBuilt("contracts/toolContracts.js"), importBuilt("domain/evidence.js"), importBuilt("domain/hopperValues.js"), importBuilt("ida/IdaConfiguration.js"), importBuilt("ida/IdaMcpConnection.js"), + importBuilt("ida/IdaProtocolValues.js"), ]); const registration = readIdaConfiguration(process.env.REA_IDA_MCP_CONFIG); if (!registration.ok) throw registration.error; @@ -79,7 +85,12 @@ const report = { config.protocol ?? (config.mode === "attached" ? "legacy" : "modern"), checks: [], observations: [], + unverified: [], }; +const expectedXref = + values["expected-xref"] === undefined + ? undefined + : idaAddressSchema.parse(values["expected-xref"]); let phase = "target admission"; const workspaces = new Set(); const databases = new Set(); @@ -184,12 +195,85 @@ const mcp = async (cliDossier) => { ["search_procedures", { pattern: dossier.procedure.name }], ["procedure_pseudo_code", { procedure: dossier.procedure.address }], ["read_function_instructions", { procedure: dossier.procedure.address }], - ["search_strings", { pattern: "a.b", mode: "literal" }], + [ + "search_strings", + { + pattern: values["expected-string"] ?? "a.b", + mode: "literal", + case_sensitive: true, + }, + ], ["xrefs", { address: dossier.procedure.address }], ]) { const result = await call(name, args); - observe(result); + const value = observe(result); + switch (name) { + case "list_procedures": + case "search_procedures": + assert.ok( + value.some( + (item) => + item.address === dossier.procedure.address && + item.value === dossier.procedure.name, + ), + `${name} omitted the resolved procedure.`, + ); + break; + case "procedure_address": + assert.equal(value, dossier.procedure.address); + break; + case "procedure_assembly": + assert.equal(value, dossier.assembly.join("\n")); + break; + case "procedure_pseudo_code": + assert.equal(value, dossier.pseudocode); + break; + case "procedure_callers": + case "procedure_callees": { + const expected = + name === "procedure_callers" ? dossier.callers : dossier.callees; + assert.deepEqual( + [...value].sort(), + expected.map((item) => item.address).sort(), + ); + break; + } + case "read_function_instructions": + assert.deepEqual(value.procedure.address, dossier.procedure.address); + assert.deepEqual(value.instructions, dossier.assembly); + break; + case "list_strings": + case "search_strings": + if (values["expected-string"] !== undefined) + assert.ok( + value.some((item) => + item.value.includes(values["expected-string"]), + ), + `${name} omitted the expected literal.`, + ); + break; + case "xrefs": + if (expectedXref !== undefined) + assert.ok( + value.includes(expectedXref), + "xrefs omitted the expected source address.", + ); + break; + } } + if (values["expected-string"] === undefined) + report.unverified.push( + "String inventory/search correctness: no independent expected literal supplied.", + ); + else + report.checks.push( + "string inventory and literal search contain the expected literal", + ); + if (expectedXref === undefined) + report.unverified.push( + "Xref correctness: no independent expected source address supplied.", + ); + else report.checks.push("xrefs contain the expected source address"); if (values["second-procedure"] !== undefined) { const secondAddress = observe( await call("procedure_address", { @@ -231,10 +315,10 @@ const mcp = async (cliDossier) => { await call("close_binary", {}); opened = false; report.checks.push( - "one MCP connection, target selection, analysis/search/xrefs, invalid input, and close", + "one MCP connection, positive procedure inventory/search, contract-valid tool results, invalid input, and close", ); report.checks.push( - "CLI/MCP function identity, pseudocode, assembly, and raw Evidence parity", + "CLI/MCP function identity, pseudocode, assembly, instructions, and relationship parity", ); } finally { const completedPhase = phase; @@ -300,6 +384,7 @@ try { passed: report.passed, mode: report.mode, checks: report.checks, + unverified: report.unverified, ...(report.passed ? {} : { diff --git a/src/ghidra/GhidraInstallation.test.ts b/src/ghidra/GhidraInstallation.test.ts index 185c71973..21c4195ad 100644 --- a/src/ghidra/GhidraInstallation.test.ts +++ b/src/ghidra/GhidraInstallation.test.ts @@ -5,6 +5,7 @@ import { projectGhidraDoctorInspection } from "./GhidraDoctor.js"; import { ghidraJavaEnvironment, inspectGhidraInstallation, + type GhidraExecutableHeaderProbe, type GhidraInstallationHost, type GhidraJavaObservation, } from "./GhidraInstallation.js"; @@ -23,6 +24,11 @@ const WINDOWS_PROPERTIES = `${WINDOWS_INSTALL}\\Ghidra\\application.properties`; const WINDOWS_HEADLESS = `${WINDOWS_INSTALL}\\support\\analyzeHeadless.bat`; const WINDOWS_DECOMPILER = `${WINDOWS_INSTALL}\\Ghidra\\Features\\Decompiler\\os\\win_x86_64\\decompile.exe`; +const headerProbe = (bytes: Buffer): GhidraExecutableHeaderProbe => ({ + bytes, + size: bytes.length, +}); + const JAVA: GhidraJavaObservation = { version: "21.0.11", major: SUPPORTED_GHIDRA_JAVA_MAJOR, @@ -543,7 +549,7 @@ describe("Ghidra FAT native decompiler admission", () => { platform: "darwin", architecture: "arm64", }, - host({ executableHeader: () => ({ bytes, size: bytes.length }) }), + host({ executableHeader: () => headerProbe(bytes) }), ); expect(result.status).toBe(status); expect( @@ -561,7 +567,7 @@ describe("Ghidra FAT native decompiler admission", () => { platform: "darwin", architecture: "arm64", }, - host({ executableHeader: () => ({ bytes, size: bytes.length }) }), + host({ executableHeader: () => headerProbe(bytes) }), ); expect(result.status).toBe("available"); expect( @@ -581,9 +587,7 @@ describe("Ghidra native decompiler admission", () => { architecture: "x64" as const, }, executableHeader: (path: string) => - path === LINUX_DECOMPILER - ? { bytes: elf(1, 1, 8), size: 52 } - : undefined, + path === LINUX_DECOMPILER ? headerProbe(elf(1, 1, 8)) : undefined, }, { name: "a Linux x86-64 decompiler at the macOS arm64 path", @@ -594,9 +598,7 @@ describe("Ghidra native decompiler admission", () => { architecture: "arm64" as const, }, executableHeader: (path: string) => - path === MAC_DECOMPILER - ? { bytes: elf(2, 1, 62), size: 52 } - : undefined, + path === MAC_DECOMPILER ? headerProbe(elf(2, 1, 62)) : undefined, }, { name: "a macOS arm64 decompiler at the Linux x64 path", @@ -608,7 +610,7 @@ describe("Ghidra native decompiler admission", () => { }, executableHeader: (path: string) => path === LINUX_DECOMPILER - ? { bytes: thinMach(0xcffaedfe, 0x0100000c), size: 32 } + ? headerProbe(thinMach(0xcffaedfe, 0x0100000c)) : undefined, }, ])("distinguishes $name", ({ options, executableHeader }) => { @@ -632,9 +634,7 @@ describe("Ghidra native decompiler admission", () => { }, host({ executableHeader: (path: string) => - path === LINUX_DECOMPILER - ? { bytes: elf(2, 1, 62), size: 52 } - : undefined, + path === LINUX_DECOMPILER ? headerProbe(elf(2, 1, 62)) : undefined, }), ); expect(result.status).toBe("available"); @@ -678,7 +678,7 @@ describe("Ghidra native decompiler admission", () => { }, host({ executableHeader: (path: string) => - path === MAC_DECOMPILER ? { bytes, size: bytes.length } : undefined, + path === MAC_DECOMPILER ? headerProbe(bytes) : undefined, }), ); expect(result.status).toBe("available"); @@ -701,9 +701,7 @@ describe("Ghidra native decompiler admission", () => { }, host({ executableHeader: (path: string) => - path === MAC_DECOMPILER - ? { bytes: elf(2, 1, 62), size: 52 } - : undefined, + path === MAC_DECOMPILER ? headerProbe(elf(2, 1, 62)) : undefined, }), ); expect(result.status).toBe("unavailable"); diff --git a/src/ida/IdaNativeProtocol.test.ts b/src/ida/IdaNativeProtocol.test.ts index f90673031..d59f598dd 100644 --- a/src/ida/IdaNativeProtocol.test.ts +++ b/src/ida/IdaNativeProtocol.test.ts @@ -375,6 +375,42 @@ describe("native IDA query identity", () => { ); }); +describe("native IDA callee truncation", () => { + it("rejects native successes without an explicit truncation marker and preserves upstream failures", async () => { + const { client, producer } = await fixture(); + const previous = producer.overrideCall; + try { + producer.overrideCall = (name, args) => + name === "callees" + ? [{ callees: [], error: null }] + : previous?.(name, args); + for (const operation of [ + "procedure_callees", + "analyze_function", + ] as const) { + const result = await client.execute(operation, { procedure: "main" }); + expect(result.ok).toBe(false); + if (!result.ok) { + expect(result.error).toBeInstanceOf(AnalysisProtocolError); + expect(result.error.message).toContain("truncation marker"); + } + } + producer.overrideCall = (name, args) => + name === "callees" + ? [{ callees: null, error: "callee database failure" }] + : previous?.(name, args); + const result = await client.execute("procedure_callees", { + procedure: "main", + }); + expect(result.ok).toBe(false); + if (!result.ok) + expect(result.error.message).toContain("callee database failure"); + } finally { + await client.close(); + } + }); +}); + describe("native IDA callee lookup batches", () => { it("batches unique callees and binds reordered replies to their source queries", async () => { const { client, producer } = await fixture(); diff --git a/src/ida/IdaNativeProtocol.ts b/src/ida/IdaNativeProtocol.ts index 711383f8e..a7ac782d5 100644 --- a/src/ida/IdaNativeProtocol.ts +++ b/src/ida/IdaNativeProtocol.ts @@ -63,7 +63,21 @@ const nativeErrorSchema = z .nullish() .transform((value) => value ?? undefined); export const nativeCalleesSchema = z - .array(modernCalleesSchema.element.extend({ error: nativeErrorSchema })) + .array( + modernCalleesSchema.element + .extend({ error: nativeErrorSchema }) + .transform((page) => { + if ( + page.error === undefined && + page.callees !== null && + page.more === undefined + ) + throw new AnalysisProtocolError( + "Native IDA callees omitted an explicit truncation marker.", + ); + return page; + }), + ) .length(1); export const nativeXrefsSchema = z .array(modernXrefsSchema.element.extend({ error: nativeErrorSchema })) diff --git a/tests/boundary/providers/ida/verifierObservations.test.ts b/tests/boundary/providers/ida/verifierObservations.test.ts new file mode 100644 index 000000000..56376174d --- /dev/null +++ b/tests/boundary/providers/ida/verifierObservations.test.ts @@ -0,0 +1,271 @@ +import { randomUUID } from "node:crypto"; +import { readFile, rm, writeFile } from "node:fs/promises"; +import { createServer } from "node:http"; +import { join } from "node:path"; +import { expect, it } from "vitest"; +import { z } from "zod"; +import { + jsonValueSchema, + type JsonValue, +} from "../../../../src/domain/jsonValue.js"; +import { nativeTools } from "../../../../src/ida/IdaNativeProtocol.js"; +import { + OwnedCommandFailure, + runOwnedCommand, +} from "../../../../src/process/OwnedCommand.js"; +import { createIdaTarget } from "../../../fixtures/idaMcp.js"; + +const requestSchema = z.object({ + id: z.union([z.string(), z.number()]).optional(), + method: z.string(), + params: z + .object({ + protocolVersion: z.string().optional(), + name: z.string().optional(), + arguments: z.record(z.string(), jsonValueSchema).optional(), + }) + .passthrough() + .optional(), +}); + +const fn = (address: string) => ({ + addr: address, + name: address === "0x1000" ? "main" : "helper", + size: "0x20", +}); +const observation = ( + name: string, + args: Readonly>, + scenario: { readonly empty: readonly string[]; readonly omitMore: boolean }, +): JsonValue => { + switch (name) { + case "lookup_funcs": + return z + .array(z.string()) + .parse(args.queries) + .map((query) => ({ + query, + fn: fn( + query === "helper" || query === "0x2000" ? "0x2000" : "0x1000", + ), + error: null, + })); + case "list_funcs": + return [ + { + data: scenario.empty.includes(name) ? [] : [fn("0x1000")], + next_offset: null, + }, + ]; + case "find_regex": + return { + matches: scenario.empty.includes(name) + ? [] + : [{ addr: "0x3000", string: "a.b" }], + cursor: { done: true }, + }; + case "decompile": { + const addr = z.string().parse(args.addr); + return { + addr, + ok: true, + pseudocode: + addr === "0x1000" + ? "int main(void) { return 42; }" + : "int helper(void) { return 55; }", + lines: 1, + }; + } + case "disasm": + return { + asm: { + name: "main", + start_ea: "0x1000", + lines: "main (.text @ 0x1000):\n1000 ret", + }, + cursor: { done: true }, + }; + case "callees": + return [ + { + callees: [], + error: null, + ...(scenario.omitMore ? {} : { more: false }), + }, + ]; + case "xrefs_to": + return [ + { + xrefs: scenario.empty.includes(name) + ? [] + : [{ addr: "0x1004", type: "code", fn: null }], + more: false, + error: null, + }, + ]; + default: + throw new Error(`Unexpected fixture operation ${name}`); + } +}; + +const fixture = async (empty: readonly string[], omitMore: boolean) => { + const { root, target } = await createIdaTarget(); + const server = createServer(async (request, response) => { + try { + let body = ""; + for await (const chunk of request) body += String(chunk); + const input = requestSchema.parse(JSON.parse(body)); + if (input.id === undefined) { + response.writeHead(202).end(); + return; + } + const result = + input.method === "initialize" + ? { + protocolVersion: input.params?.protocolVersion, + capabilities: { tools: {}, resources: {} }, + serverInfo: { name: "native-verifier-fixture", version: "1" }, + } + : input.method === "tools/list" + ? { + tools: nativeTools.map((name) => ({ + name, + inputSchema: { type: "object" }, + })), + } + : input.method === "resources/read" + ? { + contents: [ + { + uri: "ida://idb/metadata", + mimeType: "application/json", + text: JSON.stringify({ + path: `${target.path}.i64`, + sha256: target.sha256, + base: "0x1000", + module: "target.elf", + }), + }, + ], + } + : { + content: [ + { + type: "text", + text: JSON.stringify( + observation( + z.string().parse(input.params?.name), + input.params?.arguments ?? {}, + { empty, omitMore }, + ), + ), + }, + ], + }; + response + .writeHead(200, { "Content-Type": "application/json" }) + .end(JSON.stringify({ jsonrpc: "2.0", id: input.id, result })); + } catch { + response.writeHead(500).end(); + } + }); + await new Promise((resolve) => server.listen(0, "127.0.0.1", resolve)); + const address = server.address(); + if (address === null || typeof address === "string") + throw new Error("No fixture address"); + const config = join(root, "native.json"); + await writeFile( + config, + JSON.stringify({ + url: `http://127.0.0.1:${address.port}/mcp`, + protocol: "native", + timeoutMs: 30000, + }), + ); + return { + root, + target, + config, + close: async (removeWorkspace: boolean) => { + server.closeAllConnections(); + await new Promise((resolve, reject) => + server.close((error) => + error === undefined ? resolve() : reject(error), + ), + ); + if (removeWorkspace) await rm(root, { recursive: true, force: true }); + }, + }; +}; + +it.each([ + { empty: [], omitMore: false, oracles: true, passed: true }, + { empty: ["list_funcs"], omitMore: false, oracles: true, passed: false }, + { empty: ["find_regex"], omitMore: false, oracles: true, passed: false }, + { empty: ["xrefs_to"], omitMore: false, oracles: true, passed: false }, + { empty: [], omitMore: true, oracles: true, passed: false }, + { + empty: ["find_regex", "xrefs_to"], + omitMore: false, + oracles: false, + passed: true, + }, +])( + "checks real-verifier values for $empty / omitted more=$omitMore / oracles=$oracles", + async ({ empty, omitMore, oracles, passed }) => { + const upstream = await fixture(empty, omitMore); + let cleanupConfirmed = false; + try { + const reportPath = join(upstream.root, "report.json"); + const result = await runOwnedCommand( + { + command: process.execPath, + arguments: [ + "scripts/verify-real-ida.mjs", + "--target", + upstream.target.path, + "--procedure", + "main", + "--second-procedure", + "helper", + "--second-marker", + "55", + "--report", + reportPath, + ...(oracles + ? ["--expected-string", "a.b", "--expected-xref", "0x1004"] + : []), + ], + runId: `rea-ida-verifier-${randomUUID()}`, + cwd: process.cwd(), + env: { + REA_IDA_MCP_CONFIG: upstream.config, + NODE_OPTIONS: "--max-old-space-size=1024", + }, + }, + { timeoutMs: 90000, diagnosticBytes: 16384, acceptNonZeroExit: true }, + ); + cleanupConfirmed = true; + const report = z + .object({ passed: z.boolean(), unverified: z.array(z.string()) }) + .parse(JSON.parse(await readFile(reportPath, "utf8"))); + expect(report.passed, result.stdout.text + result.stderr.text).toBe( + passed, + ); + expect(result.exitCode).toBe(passed ? 0 : 1); + if (!oracles) + expect(report.unverified).toEqual([ + "String inventory/search correctness: no independent expected literal supplied.", + "Xref correctness: no independent expected source address supplied.", + ]); + else expect(report.unverified).toEqual([]); + } catch (cause) { + if (cause instanceof OwnedCommandFailure && cause.cleanupFailure === null) + cleanupConfirmed = true; + throw cause; + } finally { + await upstream.close(cleanupConfirmed); + } + }, + 120000, +);