mirror of
https://github.com/morluto/rea.git
synced 2026-10-11 21:39:55 +00:00
fix(ghidra): recover evidenced switch cases and default targets (#579)
Correlate typed labels with recovered block entries and one indirect dispatch. Preserve ambiguous and nonexact integer associations as unknown with raw diagnostics. Expose defaults separately, collect backing load metadata, and invalidate old profiles. Add independent compiler-byte CLI/MCP acceptance and actual Ghidra model controls. Assisted-by: Kogasa (gensokyo-skills:kogasa-surprise-testing) Assisted-by: Suika (gensokyo-skills:suika-scatter-gather-planning)
This commit is contained in:
N0zoM1z0
@@ -48,6 +48,8 @@ import ghidra.app.decompiler.DecompInterface;
|
||||
import ghidra.app.decompiler.DecompileOptions;
|
||||
import ghidra.app.decompiler.DecompileResults;
|
||||
import ghidra.app.decompiler.DecompiledFunction;
|
||||
import ghidra.app.decompiler.ClangCaseToken;
|
||||
import ghidra.app.decompiler.ClangNode;
|
||||
import ghidra.framework.Application;
|
||||
import ghidra.program.model.address.Address;
|
||||
import ghidra.program.model.address.AddressSpace;
|
||||
@@ -84,6 +86,8 @@ import ghidra.program.model.pcode.HighSymbol;
|
||||
import ghidra.program.model.pcode.JumpTable;
|
||||
import ghidra.program.model.pcode.PcodeOp;
|
||||
import ghidra.program.model.pcode.PcodeOpAST;
|
||||
import ghidra.program.model.pcode.PcodeBlock;
|
||||
import ghidra.program.model.pcode.PcodeBlockBasic;
|
||||
import ghidra.program.model.pcode.Varnode;
|
||||
import ghidra.program.model.pcode.VarnodeAST;
|
||||
|
||||
@@ -374,6 +378,7 @@ public final class ReaGhidraBridge extends HeadlessScript {
|
||||
decompiler.setOptions(options);
|
||||
decompiler.toggleCCode(true);
|
||||
decompiler.toggleSyntaxTree(true);
|
||||
decompiler.toggleJumpLoads(true);
|
||||
if (!decompiler.openProgram(currentProgram)) {
|
||||
throw new IllegalStateException("Ghidra decompiler could not open the imported Program");
|
||||
}
|
||||
@@ -1354,8 +1359,12 @@ public final class ReaGhidraBridge extends HeadlessScript {
|
||||
}
|
||||
|
||||
JumpTable[] recoveredJumpTables = highFunction.getJumpTables();
|
||||
List<ClangNode> caseTokens = new ArrayList<>();
|
||||
if (decompilation.getCCodeMarkup() != null) {
|
||||
decompilation.getCCodeMarkup().flatten(caseTokens);
|
||||
}
|
||||
for (int index = 0; index < recoveredJumpTables.length; index += 1) {
|
||||
jumpTables.add(inferredJumpTable(recoveredJumpTables[index]));
|
||||
jumpTables.add(inferredJumpTable(recoveredJumpTables[index], caseTokens));
|
||||
}
|
||||
return result;
|
||||
}
|
||||
@@ -1451,7 +1460,10 @@ public final class ReaGhidraBridge extends HeadlessScript {
|
||||
return result;
|
||||
}
|
||||
|
||||
private JsonObject inferredJumpTable(JumpTable jumpTable) throws Exception {
|
||||
private JsonObject inferredJumpTable(
|
||||
JumpTable jumpTable,
|
||||
List<ClangNode> caseTokens
|
||||
) throws Exception {
|
||||
JsonObject result = new JsonObject();
|
||||
result.addProperty(
|
||||
"dispatch_address",
|
||||
@@ -1550,13 +1562,33 @@ public final class ReaGhidraBridge extends HeadlessScript {
|
||||
}
|
||||
result.add("data_sources", dataSources);
|
||||
Address[] targets = jumpTable.getCases();
|
||||
Integer[] labels = jumpTable.getLabelValues();
|
||||
boolean labelsAligned = labels != null && labels.length == targets.length;
|
||||
TypedJumpTableCases typedCases = typedJumpTableCases(jumpTable, caseTokens);
|
||||
JsonArray mappings = new JsonArray();
|
||||
JsonArray defaultTargets = new JsonArray();
|
||||
for (Address target : typedCases.defaults) {
|
||||
defaultTargets.add(typedJumpTableTarget(target, jumpTable, "Typed default label"));
|
||||
}
|
||||
Set<Address> coveredTargets = new HashSet<>(typedCases.cases.values());
|
||||
coveredTargets.addAll(typedCases.defaults);
|
||||
if (recoveredAArch64 != null) {
|
||||
for (int index = 0; index < recoveredAArch64.mappings.size(); index += 1) {
|
||||
monitor.checkCancelled();
|
||||
RecoveredAArch64Mapping recovered = recoveredAArch64.mappings.get(index);
|
||||
if (
|
||||
typedCases.unknownTargets.contains(recovered.targetAddress) ||
|
||||
typedCases.ambiguousValues.contains((long) recovered.caseValue)
|
||||
) continue;
|
||||
Address typedTarget = typedCases.cases.get((long) recovered.caseValue);
|
||||
if (typedTarget != null && !typedTarget.equals(recovered.targetAddress)) {
|
||||
typedCases.cases.remove((long) recovered.caseValue);
|
||||
typedCases.ambiguousValues.add((long) recovered.caseValue);
|
||||
typedCases.unknownTargets.add(typedTarget);
|
||||
typedCases.unknownTargets.add(recovered.targetAddress);
|
||||
typedCases.limitations.add(
|
||||
"Typed case evidence and the verified relative table disagree on a destination; both destinations remain unknown for that case."
|
||||
);
|
||||
continue;
|
||||
}
|
||||
JsonObject mapping = new JsonObject();
|
||||
mapping.addProperty("case_value", recovered.caseValue);
|
||||
String targetAddress = canonicalAddress(recovered.targetAddress);
|
||||
@@ -1574,57 +1606,60 @@ public final class ReaGhidraBridge extends HeadlessScript {
|
||||
)
|
||||
);
|
||||
mapping.add("evidence", evidence);
|
||||
mappings.add(mapping);
|
||||
if (!typedCases.cases.containsKey((long) recovered.caseValue)) {
|
||||
mappings.add(mapping);
|
||||
}
|
||||
coveredTargets.add(recovered.targetAddress);
|
||||
}
|
||||
}
|
||||
else {
|
||||
for (Map.Entry<Long, Address> entry : typedCases.cases.entrySet()) {
|
||||
JsonObject mapping = typedJumpTableTarget(
|
||||
entry.getValue(),
|
||||
jumpTable,
|
||||
"Typed case value " + entry.getKey()
|
||||
);
|
||||
mapping.addProperty("case_value", entry.getKey());
|
||||
mappings.add(mapping);
|
||||
}
|
||||
Set<Address> emittedUnknownTargets = new HashSet<>();
|
||||
for (int index = 0; index < targets.length; index += 1) {
|
||||
monitor.checkCancelled();
|
||||
boolean unresolvedToken = typedCases.unknownTargets.contains(targets[index]);
|
||||
if (coveredTargets.contains(targets[index]) && !unresolvedToken) continue;
|
||||
if (!emittedUnknownTargets.add(targets[index])) continue;
|
||||
JsonObject mapping = new JsonObject();
|
||||
if (!labelsAligned || labels[index] == null) {
|
||||
mapping.add("case_value", JsonNull.INSTANCE);
|
||||
}
|
||||
else {
|
||||
mapping.addProperty("case_value", labels[index]);
|
||||
}
|
||||
mapping.add("case_value", JsonNull.INSTANCE);
|
||||
String targetAddress = canonicalAddress(targets[index]);
|
||||
mapping.addProperty("target_address", targetAddress);
|
||||
// Ghidra's recovered case-to-target relation does not identify
|
||||
// which backing load table produced an individual case. Keep the
|
||||
// table inventory and recovered mappings separate instead of
|
||||
// attaching every table address to every target.
|
||||
mapping.addProperty(
|
||||
"confidence",
|
||||
labelsAligned && labels[index] != null
|
||||
? "high"
|
||||
: "medium"
|
||||
);
|
||||
mapping.addProperty("confidence", "medium");
|
||||
JsonArray evidence = new JsonArray();
|
||||
evidence.add(
|
||||
inferenceEvidence(
|
||||
"jump-table",
|
||||
"ghidra-high-function",
|
||||
labelsAligned && labels[index] != null
|
||||
? "Ghidra paired case value " +
|
||||
labels[index] +
|
||||
" with target " +
|
||||
"Ghidra recovered target " +
|
||||
targetAddress +
|
||||
" at dispatch " +
|
||||
canonicalAddress(jumpTable.getSwitchAddress()) +
|
||||
"."
|
||||
: "Ghidra recovered target " +
|
||||
targetAddress +
|
||||
" at dispatch " +
|
||||
canonicalAddress(jumpTable.getSwitchAddress()) +
|
||||
", but no aligned case value was available."
|
||||
", but no unambiguous, exactly representable case label or default relationship was available."
|
||||
)
|
||||
);
|
||||
mapping.add("evidence", evidence);
|
||||
mappings.add(mapping);
|
||||
}
|
||||
}
|
||||
result.add("mappings", mappings);
|
||||
result.add("default_targets", defaultTargets);
|
||||
JsonArray limitations = new JsonArray();
|
||||
for (String limitation : typedCases.limitations) limitations.add(limitation);
|
||||
if (defaultTargets.isEmpty()) {
|
||||
limitations.add(
|
||||
"Ghidra exposed no typed default label with an unambiguous relationship to a recovered destination of this dispatch; default or out-of-range handling remains unknown."
|
||||
);
|
||||
}
|
||||
if (loadTables.length == 0 && referencedDataAddresses.isEmpty()) {
|
||||
limitations.add(
|
||||
"Ghidra recovered targets but exposed no backing load-table or dispatch-block data address."
|
||||
@@ -1639,9 +1674,9 @@ public final class ReaGhidraBridge extends HeadlessScript {
|
||||
"Load-table metadata was absent; table-level candidate ownership is inferred from typed data references in the dispatch block and its immediate control-flow predecessors, but candidates are not assigned to individual mappings."
|
||||
);
|
||||
}
|
||||
if (recoveredAArch64 == null && !labelsAligned) {
|
||||
if (!emittedUnknownTargets.isEmpty()) {
|
||||
limitations.add(
|
||||
"Case-label and target counts differ or labels are unavailable; all case values are left unknown because index alignment cannot be established."
|
||||
"Some recovered destinations lack an unambiguous, exactly representable case/default relationship; their case values remain unknown. Unequal label and destination arrays are never paired by index."
|
||||
);
|
||||
}
|
||||
if (recoveredAArch64 == null && loadTables.length == 0 && currentProgram.getLanguageID().getIdAsString().startsWith("AARCH64:")) {
|
||||
@@ -1656,6 +1691,124 @@ public final class ReaGhidraBridge extends HeadlessScript {
|
||||
return result;
|
||||
}
|
||||
|
||||
private static final class TypedJumpTableCases {
|
||||
private final Map<Long, Address> cases = new TreeMap<>();
|
||||
private final Set<Address> defaults = new java.util.TreeSet<>();
|
||||
private final Set<Address> unknownTargets = new HashSet<>();
|
||||
private final Set<Long> ambiguousValues = new HashSet<>();
|
||||
private final Set<String> limitations = new java.util.LinkedHashSet<>();
|
||||
}
|
||||
|
||||
private TypedJumpTableCases typedJumpTableCases(
|
||||
JumpTable jumpTable,
|
||||
List<ClangNode> tokens
|
||||
) throws Exception {
|
||||
TypedJumpTableCases result = new TypedJumpTableCases();
|
||||
Set<Address> targets = new HashSet<>();
|
||||
for (Address target : jumpTable.getCases()) targets.add(target);
|
||||
for (ClangNode node : tokens) {
|
||||
monitor.checkCancelled();
|
||||
if (!(node instanceof ClangCaseToken token)) continue;
|
||||
PcodeOp operation = token.getPcodeOp();
|
||||
if (operation == null || operation.getParent() == null) continue;
|
||||
PcodeBlockBasic block = operation.getParent();
|
||||
Address target = block.getStart();
|
||||
if (!targets.contains(target)) continue;
|
||||
PcodeOp dispatch = null;
|
||||
boolean ambiguousDispatch = false;
|
||||
boolean includesDispatch = false;
|
||||
for (int index = 0; index < block.getInSize(); index += 1) {
|
||||
PcodeBlock predecessor = block.getIn(index);
|
||||
if (!(predecessor instanceof PcodeBlockBasic basic)) continue;
|
||||
PcodeOp last = basic.getLastOp();
|
||||
if (last == null || last.getOpcode() != PcodeOp.BRANCHIND) continue;
|
||||
if (last.getSeqnum().getTarget().equals(jumpTable.getSwitchAddress())) {
|
||||
includesDispatch = true;
|
||||
}
|
||||
if (dispatch != null && dispatch != last) ambiguousDispatch = true;
|
||||
dispatch = last;
|
||||
}
|
||||
if (!includesDispatch) continue;
|
||||
if (ambiguousDispatch) {
|
||||
result.unknownTargets.add(target);
|
||||
result.limitations.add(
|
||||
"A typed case/default block has multiple indirect dispatch predecessors; REA cannot attribute its label to one switch."
|
||||
);
|
||||
continue;
|
||||
}
|
||||
// Default is a typed label role, not an OFF sentinel: Ghidra can
|
||||
// encode a default token with an ordinary in-range case value.
|
||||
if ("default".equals(token.getText())) {
|
||||
result.defaults.add(target);
|
||||
continue;
|
||||
}
|
||||
Long value = exactTypedCaseValue(token);
|
||||
if (value == null) {
|
||||
result.unknownTargets.add(target);
|
||||
result.limitations.add(
|
||||
"Typed case label " + token.getText() +
|
||||
" has encoded unsigned magnitude " + Long.toUnsignedString(token.getValue()) +
|
||||
" at recovered target " + canonicalAddress(target) +
|
||||
" for dispatch " + canonicalAddress(jumpTable.getSwitchAddress()) +
|
||||
"; the label is nonliteral, inconsistent with its encoded magnitude, or outside the exact JSON integer range, so its numeric case value remains unknown."
|
||||
);
|
||||
continue;
|
||||
}
|
||||
if (result.ambiguousValues.contains(value)) {
|
||||
result.unknownTargets.add(target);
|
||||
continue;
|
||||
}
|
||||
Address previous = result.cases.putIfAbsent(value, target);
|
||||
if (previous != null && !previous.equals(target)) {
|
||||
result.cases.remove(value);
|
||||
result.ambiguousValues.add(value);
|
||||
result.unknownTargets.add(previous);
|
||||
result.unknownTargets.add(target);
|
||||
result.limitations.add(
|
||||
"Typed tokens assign one case value to different recovered destinations; that case remains unknown."
|
||||
);
|
||||
}
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
private static Long exactTypedCaseValue(ClangCaseToken token) {
|
||||
String text = token.getText();
|
||||
if (text == null || !text.matches("-?(?:0[xX][0-9a-fA-F]+|[0-9]+)")) return null;
|
||||
boolean negative = text.startsWith("-");
|
||||
String literal = negative ? text.substring(1) : text;
|
||||
BigInteger magnitude = literal.startsWith("0x") || literal.startsWith("0X")
|
||||
? new BigInteger(literal.substring(2), 16)
|
||||
: new BigInteger(literal, 10);
|
||||
// Negative numeric tokens carry an unsigned magnitude in OFF, so
|
||||
// getValue()/getScalar() alone would incorrectly emit positive cases.
|
||||
if (!magnitude.equals(new BigInteger(Long.toUnsignedString(token.getValue())))) return null;
|
||||
BigInteger value = negative ? magnitude.negate() : magnitude;
|
||||
if (value.abs().compareTo(BigInteger.valueOf(9007199254740991L)) > 0) return null;
|
||||
return value.longValueExact();
|
||||
}
|
||||
|
||||
private static JsonObject typedJumpTableTarget(
|
||||
Address target,
|
||||
JumpTable table,
|
||||
String label
|
||||
) {
|
||||
JsonObject result = new JsonObject();
|
||||
String address = canonicalAddress(target);
|
||||
result.addProperty("target_address", address);
|
||||
result.addProperty("confidence", "high");
|
||||
JsonArray evidence = new JsonArray();
|
||||
evidence.add(inferenceEvidence(
|
||||
"jump-table",
|
||||
"ghidra-clang-case-token",
|
||||
label + " belongs to the p-code block starting at recovered target " +
|
||||
address + "; its unique indirect dispatch predecessor is " +
|
||||
canonicalAddress(table.getSwitchAddress()) + "."
|
||||
));
|
||||
result.add("evidence", evidence);
|
||||
return result;
|
||||
}
|
||||
|
||||
private static final class RecoveredAArch64Mapping {
|
||||
private final int caseValue;
|
||||
private final Address targetAddress;
|
||||
|
||||
@@ -96,6 +96,21 @@ The provider dossier itself retains up to 3,000 p-code operations, 64 inputs per
|
||||
operation and 12,000 def-use edges, with explicit omitted counts. A `STORE`
|
||||
may describe stack memory and does not itself prove persistent state.
|
||||
|
||||
Jump-table evidence keeps numeric `mappings`, explicit `default_targets`, and
|
||||
backing `data_sources` separate. A null case value denotes an unresolved
|
||||
case, never a known default. Ghidra pairs typed case/default tokens with the
|
||||
recovered block entry and its unique indirect dispatch predecessor; it does
|
||||
not zip unequal label and destination arrays. Shared case bodies retain each
|
||||
label. Negative numeric tokens are checked against their encoded magnitude;
|
||||
nonliteral, ambiguous, or nonexact JSON integer labels remain unknown.
|
||||
Unknown-label diagnostics retain the token text, encoded unsigned magnitude,
|
||||
target and dispatch so callers can inspect the original observations.
|
||||
Decompiler load-table metadata supplies observed entry sizes and counts
|
||||
without assigning every backing table to each mapping. These observations
|
||||
describe the decompiler's recovered switch, not guaranteed original source.
|
||||
Legacy records without `default_targets` normalize to an empty array and
|
||||
retain their existing unresolved mappings.
|
||||
|
||||
AArch64 jump-table recovery additionally verifies byte and halfword relative
|
||||
forms from unsigned bounds, register definitions, table loads, branch bases,
|
||||
scaled ADD/BR instructions and the recovered target set. It reads exactly the
|
||||
|
||||
@@ -521,9 +521,9 @@
|
||||
"mcp_prompts": 6
|
||||
},
|
||||
"digests": {
|
||||
"tools_sha256": "ff29fddb875d335c400902e846377990fa4276f04e4494a255dd3986a0fd7896",
|
||||
"tools_sha256": "e14cff8d23b94644dda1c1d0c28dbcf3e8140f05daa06f4bd5f1bde1f1e2ec9b",
|
||||
"prompts_sha256": "4762db348821fec787a5b8c6423f2c48a71f6f0ec2afee97b16ad69030ec504b",
|
||||
"combined_sha256": "73a4cdf4fc83b1728426931ff89e2113f1c8beb1b3bf337c179f2c349ce3c0f2",
|
||||
"combined_sha256": "93e02e0675739b3049b010eabe96745957e29267759a7028a66057677d1f4d92",
|
||||
"providers_sha256": "2ae8b85b20be338739e500549d275e78e875aaa10235d2ca283f0ade7787da90"
|
||||
}
|
||||
}
|
||||
|
||||
@@ -98,6 +98,7 @@ that a host or target is covered when it was skipped.
|
||||
| Ghidra lane | Supported runner/target | Additional local tools |
|
||||
| ------------------------------------------ | ---------------------------------------------------------------------------------- | ------------------------------------------------------------------- |
|
||||
| `npm run verify:ghidra` | Linux x64 ELF or macOS x64/arm64 Mach-O | Host C compiler, Ghidra 12.1.4, and full JDK 21 |
|
||||
| `npm run verify:ghidra:switch` | Linux x64 ELF; GCC/Clang optimized and stripped switch fixtures | GCC, Clang, GNU nm/objdump/strip, Ghidra 12.1.4, and full JDK 21 |
|
||||
| `npm run verify:ghidra:aarch64-jump-table` | Any supported Ghidra host; AArch64 ELF; byte/halfword tables; host ARM64 Mach-O | Clang with AArch64 target support, Ghidra 12.1.4, and full JDK 21 |
|
||||
| `npm run verify:ghidra:cross-format` | Any supported Ghidra host; also analyzes AArch64 ELF, x86-64 PE, and x86-64 Mach-O | `clang`, LLD, and `lld-link` in addition to host-lane prerequisites |
|
||||
| `npm run verify:ghidra:windows` | Controlled Windows x64 with native x86-64 PE | Ghidra 12.1.4, full JDK 21, and the Windows P0 fixture toolchain |
|
||||
@@ -107,6 +108,25 @@ production CLI and a separate stdio MCP process. It compares complete dependency
|
||||
graphs, validates Evidence and upstream/workflow profiles, checks capability
|
||||
discovery, and closes the MCP session. No provider or transport is mocked.
|
||||
|
||||
The Linux switch lane checks dense, sparse-with-holes, shared-body, nonzero,
|
||||
negative, and nonexact JSON integer labels plus a comparison-only control.
|
||||
Independent source labels, ELF file bytes, table slots, and bounds branches
|
||||
define expected case/default destinations. Production CLI and MCP must agree;
|
||||
debug labels must retain their signed values. For stripped negative fixtures,
|
||||
the independently checked 32-bit dispatch permits equivalent unsigned labels
|
||||
only alongside the reported low-confidence `undefined4` parameter; original
|
||||
source signedness remains unknown and the ABI residual must remain visible.
|
||||
unsafe labels remain unresolved and every recovered destination is retained.
|
||||
The compiler oracle also injects malformed records to check that its assertions
|
||||
reject missing/default-confused labels, wrong destinations, and numeric guesses.
|
||||
It also invokes the actual bridge methods on detached Ghidra model objects to
|
||||
check ambiguous dispatches, signed literals, precision bounds, shared targets,
|
||||
and conflicting labels. This reflection fixture depends on the pinned Ghidra
|
||||
model and does not claim a compiler produced those synthetic graph shapes.
|
||||
Pass `--entrypoint /path/to/installed/rea-agents/scripts/rea.mjs` directly to
|
||||
`scripts/verify-real-ghidra-switch.mjs` to verify an installed package through
|
||||
the same compiler oracles and CLI/MCP checks.
|
||||
|
||||
The cross-format Ghidra lane also analyzes an optimized AArch64 ELF switch
|
||||
fixture. It checks the recovered case values against the source cases and
|
||||
requires unresolved table bounds or case mappings to remain visible as
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
{
|
||||
"manifest_id": "ecm_c47e33ff69b099583ff6a3b19cb06b602040ecc735351cbac21b897501c4cffe",
|
||||
"manifest_id": "ecm_77a62ada2f566c17638950d2c7339364f131d0b384264204a7f8d89a9f90068f",
|
||||
"verifier": {
|
||||
"id": "rea-managed-conformance",
|
||||
"version": "1"
|
||||
@@ -13,7 +13,7 @@
|
||||
"skill_digests": [
|
||||
{
|
||||
"skill_id": "reverse-engineer-anything",
|
||||
"sha256": "54490266ef46ed8e57354dbca8cc1ad74ab6b7f21d38116bebfc87a04bfb55a5"
|
||||
"sha256": "ec130bedea71c202213535025cf32e9943ef309326ad29a55da511cab5f7ad45"
|
||||
}
|
||||
],
|
||||
"claims": [
|
||||
|
||||
@@ -121,6 +121,7 @@
|
||||
"verify:native-ui": "npm run build:cached && node scripts/verify-native-ui.mjs",
|
||||
"verify:keyed-archive": "npm run build:cached && node scripts/verify-keyed-archive.mjs",
|
||||
"verify:ghidra": "npm run build:cached && node scripts/verify-real-ghidra.mjs",
|
||||
"verify:ghidra:switch": "npm run build:cached && node scripts/verify-real-ghidra-switch.mjs",
|
||||
"verify:ghidra:dos": "npm run build:cached && node scripts/verify-real-ghidra-dos.mjs",
|
||||
"verify:ghidra:aarch64-jump-table": "npm run build:cached && node scripts/verify-real-ghidra.mjs --aarch64-jump-table",
|
||||
"verify:interface-builder": "npm run build:cached && node scripts/verify-interface-builder.mjs",
|
||||
|
||||
@@ -1,3 +1,5 @@
|
||||
import { hasTypedSwitchEvidence } from "./verify-real-ghidra-switch-assertions.mjs";
|
||||
|
||||
import { access } from "node:fs/promises";
|
||||
|
||||
import { parseBinaryTarget } from "../dist/application/BinaryTargetResolver.js";
|
||||
@@ -107,6 +109,14 @@ export function assertDenseSwitchDossier(dossier, address) {
|
||||
);
|
||||
if (
|
||||
denseTable === undefined ||
|
||||
denseTable.default_targets.length !== 1 ||
|
||||
denseTable.default_targets[0].confidence !== "high" ||
|
||||
!hasTypedSwitchEvidence(
|
||||
denseTable.default_targets[0].evidence,
|
||||
"Typed default label",
|
||||
denseTable.default_targets[0].target_address,
|
||||
denseTable.dispatch_address,
|
||||
) ||
|
||||
denseTable.mappings.some(
|
||||
({ target_address: target, evidence }) =>
|
||||
!/^0x[0-9a-f]+$/u.test(target) ||
|
||||
@@ -146,9 +156,8 @@ function assertNativeApiBoundary(observed, requireJumpTable) {
|
||||
) &&
|
||||
mappings.length > 0 &&
|
||||
mappings.every(
|
||||
({ target_address: target, data_addresses: addresses, evidence }) =>
|
||||
({ target_address: target, evidence }) =>
|
||||
/^0x[0-9a-f]+$/u.test(target) &&
|
||||
addresses.every((address) => /^0x[0-9a-f]+$/u.test(address)) &&
|
||||
evidence.some(({ kind }) => kind === "jump-table"),
|
||||
),
|
||||
)
|
||||
|
||||
@@ -613,3 +613,37 @@ export async function verifyNativeValueTrace(client, procedures, target) {
|
||||
const global = requireProcedure(names, "rea_ghidra_inventory_global");
|
||||
return verifyNativeValueE2e(target, entry.address, global.address);
|
||||
}
|
||||
|
||||
/** Match the source default's -1 assignment in supported native compiler encodings. */
|
||||
export async function verifyDenseDefaultReturn(client, targetAddress) {
|
||||
const instruction = await functionCall(client, "inspect_native_instruction", {
|
||||
address: targetAddress,
|
||||
});
|
||||
if (
|
||||
instruction.status !== "decoded" ||
|
||||
!isDefaultMinusOneAssignment(instruction)
|
||||
)
|
||||
throw new Error(
|
||||
`Dense default target lacks the source -1 assignment (x86 register/stack MOV or AArch64 W-register MOVN): ${JSON.stringify(instruction)}`,
|
||||
);
|
||||
return {
|
||||
target_address: targetAddress,
|
||||
instruction_bytes: instruction.bytes,
|
||||
};
|
||||
}
|
||||
|
||||
function isDefaultMinusOneAssignment(instruction) {
|
||||
if (instruction.architecture.startsWith("x86:"))
|
||||
return (
|
||||
instruction.bytes === "b8ffffffff" ||
|
||||
/^c745[0-9a-f]{2}ffffffff$/u.test(instruction.bytes)
|
||||
);
|
||||
if (
|
||||
instruction.architecture.startsWith("AARCH64:") &&
|
||||
instruction.bytes.length === 8
|
||||
) {
|
||||
const word = Buffer.from(instruction.bytes, "hex").readUInt32LE();
|
||||
return (word & 0xffffffe0) === 0x12800000;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
@@ -0,0 +1,420 @@
|
||||
import assert from "node:assert/strict";
|
||||
|
||||
/** Verify numeric/default evidence against independent compiler-byte/source oracles. */
|
||||
export function assertSwitchBoundary(boundary, fixture) {
|
||||
assert.equal(boundary.available, true);
|
||||
assert.equal(boundary.provenance, "ghidra-high-function");
|
||||
assert.ok(
|
||||
boundary.limitations.length > 0,
|
||||
"Provider observation scope must remain explicit",
|
||||
);
|
||||
if (!fixture.table) {
|
||||
assert.deepEqual(
|
||||
boundary.jump_tables,
|
||||
[],
|
||||
"Comparison-only control fabricated a jump table",
|
||||
);
|
||||
return { numeric_cases: 0, default_targets: 0, unknowns: 0 };
|
||||
}
|
||||
assert.equal(
|
||||
boundary.jump_tables.length,
|
||||
1,
|
||||
`Expected one source-owned switch: ${fixture.name}`,
|
||||
);
|
||||
const table = boundary.jump_tables[0];
|
||||
if (fixture.allow_unsigned_32_labels === true) {
|
||||
assert.equal(fixture.discriminator_size_bytes, 4);
|
||||
assert.equal(boundary.parameters.length, 1);
|
||||
assert.equal(boundary.parameters[0].data_type, "undefined4");
|
||||
assert.equal(boundary.parameters[0].size_bytes, 4);
|
||||
assert.equal(boundary.parameters[0].confidence, "low");
|
||||
}
|
||||
assert.equal(
|
||||
table.dispatch_address,
|
||||
fixture.dispatch_address,
|
||||
"Dispatch does not identify the independently byte-proven indirect jump",
|
||||
);
|
||||
const numericCount = assertCaseMappings(table, fixture);
|
||||
assert.equal(
|
||||
table.default_targets.length,
|
||||
1,
|
||||
"Default target must be separate from numeric cases/unknowns",
|
||||
);
|
||||
const defaultTarget = table.default_targets[0];
|
||||
assert.equal(
|
||||
defaultTarget.target_address,
|
||||
fixture.default_address,
|
||||
"Default does not enter the independently byte-proven default block",
|
||||
);
|
||||
assert.equal(defaultTarget.confidence, "high");
|
||||
assert.ok(
|
||||
hasTypedSwitchEvidence(
|
||||
defaultTarget.evidence,
|
||||
"Typed default label",
|
||||
defaultTarget.target_address,
|
||||
table.dispatch_address,
|
||||
),
|
||||
"Default omitted typed label/block/dispatch evidence",
|
||||
);
|
||||
assert.ok(
|
||||
table.data_sources.some(
|
||||
({ address, entry_size_bytes: size, entry_count: count }) =>
|
||||
address === fixture.table_address &&
|
||||
size === 8 &&
|
||||
count === fixture.slots.length,
|
||||
),
|
||||
"Recovered backing-table observation disagrees with independently decoded bytes",
|
||||
);
|
||||
return {
|
||||
numeric_cases: numericCount,
|
||||
default_targets: 1,
|
||||
unknowns: fixture.unsafe_integer ? table.mappings.length : 0,
|
||||
};
|
||||
}
|
||||
|
||||
function assertCaseMappings(table, fixture) {
|
||||
const explicit = fixture.slots.filter(({ explicit_case }) => explicit_case);
|
||||
const numeric = table.mappings.filter(
|
||||
({ case_value }) => typeof case_value === "number",
|
||||
);
|
||||
if (fixture.unsafe_integer) {
|
||||
assert.equal(
|
||||
numeric.length,
|
||||
0,
|
||||
"Unsafe integer labels were rounded, truncated or replaced by table indices",
|
||||
);
|
||||
assert.equal(
|
||||
table.mappings.length,
|
||||
fixture.blocks.length,
|
||||
"Unsafe labels must retain every independently byte-proven target",
|
||||
);
|
||||
assert.deepEqual(
|
||||
table.mappings.map(({ target_address }) => target_address).sort(),
|
||||
fixture.blocks.map(({ address }) => address).sort(),
|
||||
);
|
||||
for (const mapping of table.mappings) {
|
||||
assert.equal(mapping.case_value, null);
|
||||
assert.ok(
|
||||
["low", "medium"].includes(mapping.confidence),
|
||||
"Unknown numeric association must not claim high confidence",
|
||||
);
|
||||
assertUnknownTargetEvidence(
|
||||
mapping.evidence,
|
||||
mapping.target_address,
|
||||
table.dispatch_address,
|
||||
);
|
||||
}
|
||||
} else {
|
||||
assert.equal(
|
||||
table.mappings.length,
|
||||
numeric.length,
|
||||
"Complete public fixture has unresolved/misclassified numeric case rows",
|
||||
);
|
||||
const matchedValues = new Set();
|
||||
for (const mapping of numeric) {
|
||||
const expected = fixture.slots.find(
|
||||
({ value }) =>
|
||||
value === mapping.case_value ||
|
||||
(fixture.allow_unsigned_32_labels === true &&
|
||||
Number(BigInt.asUintN(32, BigInt(value))) === mapping.case_value),
|
||||
);
|
||||
assert.ok(expected, `Fabricated out-of-range case ${mapping.case_value}`);
|
||||
assert.ok(
|
||||
!matchedValues.has(expected.value),
|
||||
"Duplicate discriminator bit pattern",
|
||||
);
|
||||
matchedValues.add(expected.value);
|
||||
assert.equal(
|
||||
mapping.target_address,
|
||||
expected.target_address,
|
||||
`Wrong case→target ${fixture.name}:${mapping.case_value}`,
|
||||
);
|
||||
assert.equal(mapping.confidence, "high");
|
||||
assert.ok(
|
||||
hasTypedSwitchEvidence(
|
||||
mapping.evidence,
|
||||
`Typed case value ${mapping.case_value}`,
|
||||
mapping.target_address,
|
||||
table.dispatch_address,
|
||||
),
|
||||
"Numeric mapping omitted typed case/block/dispatch evidence",
|
||||
);
|
||||
}
|
||||
for (const { value } of explicit)
|
||||
assert.ok(
|
||||
matchedValues.has(value),
|
||||
`Omitted source case ${fixture.name}:${value}`,
|
||||
);
|
||||
}
|
||||
return numeric.length;
|
||||
}
|
||||
|
||||
/** Match typed labels to their explicitly evidenced block and unique dispatch. */
|
||||
export function hasTypedSwitchEvidence(evidence, label, target, dispatch) {
|
||||
return evidence.some(
|
||||
({ kind, source, detail }) =>
|
||||
kind === "jump-table" &&
|
||||
source === "ghidra-clang-case-token" &&
|
||||
typeof detail === "string" &&
|
||||
detail.trim().length > 0 &&
|
||||
detail.startsWith(
|
||||
`${label} belongs to the p-code block starting at recovered target ${target};`,
|
||||
) &&
|
||||
detail.includes(
|
||||
`its unique indirect dispatch predecessor is ${dispatch}.`,
|
||||
),
|
||||
);
|
||||
}
|
||||
function assertUnknownTargetEvidence(evidence, target, dispatch) {
|
||||
assert.ok(
|
||||
evidence.some(
|
||||
({ kind, source, detail }) =>
|
||||
kind === "jump-table" &&
|
||||
source === "ghidra-high-function" &&
|
||||
typeof detail === "string" &&
|
||||
detail.trim().length > 0 &&
|
||||
detail.startsWith(
|
||||
`Ghidra recovered target ${target} at dispatch ${dispatch},`,
|
||||
) &&
|
||||
detail.includes(
|
||||
"no unambiguous, exactly representable case label or default relationship",
|
||||
),
|
||||
),
|
||||
"Unknown mapping omitted recovered target/dispatch and unavailable label evidence",
|
||||
);
|
||||
}
|
||||
|
||||
/** Fault-injected guard controls only; these records are not real provider acceptance. */
|
||||
export function assertSwitchOracleControls(fixtures) {
|
||||
const fixture = fixtures.find(({ name }) => name === "holes_shared");
|
||||
assert.ok(fixture);
|
||||
const boundary = guardBoundary(fixture);
|
||||
const evidence = boundary.jump_tables[0].default_targets[0].evidence;
|
||||
assertSwitchBoundary(boundary, fixture);
|
||||
const faults = {
|
||||
consistently_wrong_dispatch: (table) => {
|
||||
const previous = table.dispatch_address;
|
||||
table.dispatch_address = "0xff";
|
||||
for (const row of [...table.mappings, ...table.default_targets])
|
||||
for (const evidence of row.evidence)
|
||||
evidence.detail = evidence.detail.replace(previous, "0xff");
|
||||
},
|
||||
wrong_numeric_evidence_source: (table) => {
|
||||
table.mappings[0].evidence[0].source = "unrelated-source";
|
||||
},
|
||||
wrong_default_evidence_source: (table) => {
|
||||
table.default_targets[0].evidence[0].source = "ghidra-high-function";
|
||||
},
|
||||
empty_default_evidence_detail: (table) => {
|
||||
table.default_targets[0].evidence[0].detail = "";
|
||||
},
|
||||
wrong_typed_dispatch: (table) => {
|
||||
table.mappings[0].evidence[0].detail =
|
||||
table.mappings[0].evidence[0].detail.replace(
|
||||
`predecessor is ${fixture.dispatch_address}.`,
|
||||
"predecessor is 0xff.",
|
||||
);
|
||||
},
|
||||
missing_default: (table) => {
|
||||
table.default_targets = [];
|
||||
},
|
||||
default_misclassified_as_unknown: (table) => {
|
||||
table.default_targets = [];
|
||||
table.mappings.push({
|
||||
case_value: null,
|
||||
target_address: fixture.default_address,
|
||||
confidence: "low",
|
||||
evidence,
|
||||
});
|
||||
},
|
||||
wrong_shared_target: (table) => {
|
||||
table.mappings.find(({ case_value }) => case_value === 3).target_address =
|
||||
fixture.blocks[0].address;
|
||||
},
|
||||
positional_label_guess: (table) => {
|
||||
table.mappings.find(({ case_value }) => case_value === 9).case_value = 99;
|
||||
},
|
||||
omitted_case: (table) => {
|
||||
table.mappings = table.mappings.filter(
|
||||
({ case_value }) => case_value !== 2,
|
||||
);
|
||||
},
|
||||
wrong_default_target: (table) => {
|
||||
table.default_targets[0].target_address = fixture.blocks[0].address;
|
||||
},
|
||||
wrong_backing_extent: (table) => {
|
||||
table.data_sources[0].entry_count--;
|
||||
},
|
||||
};
|
||||
for (const [name, inject] of Object.entries(faults)) {
|
||||
const damaged = structuredClone(boundary);
|
||||
inject(damaged.jump_tables[0]);
|
||||
assert.throws(
|
||||
() => assertSwitchBoundary(damaged, fixture),
|
||||
undefined,
|
||||
`Oracle failed to reject ${name}`,
|
||||
);
|
||||
}
|
||||
const negative = fixtures.find(({ name }) => name === "negative");
|
||||
assert.ok(negative);
|
||||
const signed = guardBoundary(negative);
|
||||
assertSwitchBoundary(signed, negative);
|
||||
signed.jump_tables[0].mappings = signed.jump_tables[0].mappings.map(
|
||||
(mapping) => ({ ...mapping, case_value: Math.abs(mapping.case_value) }),
|
||||
);
|
||||
assert.throws(
|
||||
() => assertSwitchBoundary(signed, negative),
|
||||
undefined,
|
||||
"Lost unary minus in a signed case label",
|
||||
);
|
||||
const unsignedControls = assertStrippedSignednessControls(negative);
|
||||
const comparison = fixtures.find(({ name }) => name === "comparison");
|
||||
assert.ok(comparison);
|
||||
assertSwitchBoundary({ ...boundary, jump_tables: [] }, comparison);
|
||||
assert.throws(
|
||||
() => assertSwitchBoundary(boundary, comparison),
|
||||
undefined,
|
||||
"Fabricated table for comparison-only control",
|
||||
);
|
||||
return [
|
||||
...assertUnsafeGuardControls(fixtures),
|
||||
...unsignedControls,
|
||||
...Object.keys(faults),
|
||||
"signed_label_magnitude",
|
||||
"fabricated_comparison_table",
|
||||
];
|
||||
}
|
||||
|
||||
function assertStrippedSignednessControls(fixture) {
|
||||
const strippedFixture = { ...fixture, allow_unsigned_32_labels: true };
|
||||
const signed = guardBoundary(fixture);
|
||||
const unsigned = structuredClone(signed);
|
||||
unsigned.parameters = [
|
||||
{ data_type: "undefined4", size_bytes: 4, confidence: "low" },
|
||||
];
|
||||
for (const mapping of unsigned.jump_tables[0].mappings) {
|
||||
const previous = mapping.case_value;
|
||||
mapping.case_value = Number(BigInt.asUintN(32, BigInt(previous)));
|
||||
mapping.evidence[0].detail = mapping.evidence[0].detail.replace(
|
||||
`Typed case value ${previous} `,
|
||||
`Typed case value ${mapping.case_value} `,
|
||||
);
|
||||
}
|
||||
assertSwitchBoundary(unsigned, strippedFixture);
|
||||
assert.throws(
|
||||
() => assertSwitchBoundary(unsigned, fixture),
|
||||
undefined,
|
||||
"Known signed source labels were replaced by unsigned values",
|
||||
);
|
||||
const faults = {
|
||||
stripped_signedness_promoted: (record) => {
|
||||
record.parameters[0].confidence = "high";
|
||||
},
|
||||
stripped_wrong_discriminator_width: (record) => {
|
||||
record.parameters[0].size_bytes = 8;
|
||||
},
|
||||
stripped_wrong_bit_pattern_target: (record) => {
|
||||
record.jump_tables[0].mappings[0].target_address =
|
||||
fixture.blocks[1].address;
|
||||
},
|
||||
stripped_duplicate_bit_pattern: (record) => {
|
||||
record.jump_tables[0].mappings.push(signed.jump_tables[0].mappings[0]);
|
||||
},
|
||||
};
|
||||
for (const [name, inject] of Object.entries(faults)) {
|
||||
const damaged = structuredClone(unsigned);
|
||||
inject(damaged);
|
||||
assert.throws(
|
||||
() => assertSwitchBoundary(damaged, strippedFixture),
|
||||
undefined,
|
||||
`Oracle failed to reject ${name}`,
|
||||
);
|
||||
}
|
||||
return ["known_signed_labels_must_stay_signed", ...Object.keys(faults)];
|
||||
}
|
||||
|
||||
function assertUnsafeGuardControls(fixtures) {
|
||||
const unsafe = fixtures.find(({ name }) => name === "unsafe_integer");
|
||||
assert.ok(unsafe);
|
||||
const unknown = guardBoundary(unsafe, true);
|
||||
assertSwitchBoundary(unknown, unsafe);
|
||||
for (const labels of [
|
||||
unsafe.slots.map(({ value }) => Number(BigInt(value) & 0xffffffffn)),
|
||||
unsafe.slots.map((_, index) => index),
|
||||
unsafe.slots.map(({ value }) => Number(value)),
|
||||
]) {
|
||||
const fabricated = structuredClone(unknown);
|
||||
fabricated.jump_tables[0].mappings = fabricated.jump_tables[0].mappings.map(
|
||||
(mapping, index) => ({
|
||||
...mapping,
|
||||
case_value: labels[index],
|
||||
confidence: "high",
|
||||
}),
|
||||
);
|
||||
assert.throws(
|
||||
() => assertSwitchBoundary(fabricated, unsafe),
|
||||
undefined,
|
||||
"Unsafe label rounding/truncation/index fallback accepted",
|
||||
);
|
||||
}
|
||||
return [
|
||||
"unsafe_label_signed32_truncation",
|
||||
"unsafe_label_index_fallback",
|
||||
"unsafe_label_float_rounding",
|
||||
];
|
||||
}
|
||||
function guardBoundary(fixture, unresolved = false) {
|
||||
const typedEvidence = (label, target) => [
|
||||
{
|
||||
kind: "jump-table",
|
||||
source: "ghidra-clang-case-token",
|
||||
detail: `${label} belongs to the p-code block starting at recovered target ${target}; its unique indirect dispatch predecessor is ${fixture.dispatch_address}.`,
|
||||
},
|
||||
];
|
||||
const unknownEvidence = (target) => [
|
||||
{
|
||||
kind: "jump-table",
|
||||
source: "ghidra-high-function",
|
||||
detail: `Ghidra recovered target ${target} at dispatch ${fixture.dispatch_address}, but no unambiguous, exactly representable case label or default relationship was available.`,
|
||||
},
|
||||
];
|
||||
return {
|
||||
available: true,
|
||||
provenance: "ghidra-high-function",
|
||||
limitations: ["Guard control only"],
|
||||
jump_tables: [
|
||||
{
|
||||
dispatch_address: fixture.dispatch_address,
|
||||
data_sources: [
|
||||
{
|
||||
address: fixture.table_address,
|
||||
entry_size_bytes: 8,
|
||||
entry_count: fixture.slots.length,
|
||||
},
|
||||
],
|
||||
mappings: fixture.slots.map(({ value, target_address }, index) => ({
|
||||
case_value: unresolved ? null : value,
|
||||
target_address,
|
||||
confidence: unresolved
|
||||
? index % 2 === 0
|
||||
? "medium"
|
||||
: "low"
|
||||
: "high",
|
||||
evidence: unresolved
|
||||
? unknownEvidence(target_address)
|
||||
: typedEvidence(`Typed case value ${value}`, target_address),
|
||||
})),
|
||||
default_targets: [
|
||||
{
|
||||
target_address: fixture.default_address,
|
||||
confidence: "high",
|
||||
evidence: typedEvidence(
|
||||
"Typed default label",
|
||||
fixture.default_address,
|
||||
),
|
||||
},
|
||||
],
|
||||
},
|
||||
],
|
||||
};
|
||||
}
|
||||
@@ -0,0 +1,156 @@
|
||||
import assert from "node:assert/strict";
|
||||
import { createHash } from "node:crypto";
|
||||
import { mkdir, readFile, realpath } from "node:fs/promises";
|
||||
import { dirname, join } from "node:path";
|
||||
import { fileURLToPath } from "node:url";
|
||||
|
||||
const EXPECTED_CHECKS = [
|
||||
"positive_decimal",
|
||||
"unsigned32_literal_not_rewritten",
|
||||
"negative_embedded_token_sign",
|
||||
"negative_hex",
|
||||
"zero",
|
||||
"magnitude_mismatch_unknown",
|
||||
"signed_encoding_is_not_magnitude",
|
||||
"symbol_label_unknown",
|
||||
"compound_label_unknown",
|
||||
"safe_positive_boundary",
|
||||
"safe_negative_boundary",
|
||||
"safe_hex_boundary",
|
||||
"unsafe_positive_unknown",
|
||||
"unsafe_negative_unknown",
|
||||
"unsigned64_unknown",
|
||||
"no_dispatch_not_attributed",
|
||||
"unique_dispatch_block_start",
|
||||
"instruction_offset_is_not_destination",
|
||||
"wrong_dispatch_not_attributed",
|
||||
"target_not_in_table_not_attributed",
|
||||
"signed_and_positive_distinct",
|
||||
"shared_destination_keeps_all_labels",
|
||||
"default_ordinary_off_is_role",
|
||||
"default_and_numeric_can_share_target",
|
||||
"unsafe64_target_preserved_unknown",
|
||||
"magnitude_mismatch_target_preserved_unknown",
|
||||
"conflicting_value_retracted",
|
||||
"conflicting_destinations_preserved_unknown",
|
||||
"api_first_dispatch_is_insufficient",
|
||||
"multiple_dispatches_rejected",
|
||||
"multiple_dispatch_target_preserved_unknown",
|
||||
"multiple_dispatch_rejected_for_other_table",
|
||||
];
|
||||
|
||||
/** Exercise actual bridge methods on detached Ghidra objects with owned process cleanup. */
|
||||
export async function verifySwitchEvidenceControls({
|
||||
installation,
|
||||
entrypoint,
|
||||
target,
|
||||
workspace,
|
||||
runId,
|
||||
}) {
|
||||
const { spawnOwnedProviderProcess, ProviderProcessSupervisor } = await import(
|
||||
"../dist/process/ProviderProcess.js"
|
||||
);
|
||||
const { cleanupOwnedProcessGroup } = await import(
|
||||
"../dist/process/ProcessOwnership.js"
|
||||
);
|
||||
const bridge = await realpath(
|
||||
join(dirname(entrypoint), "../bridge/ghidra/ReaGhidraBridge.java"),
|
||||
);
|
||||
const fixtures = fileURLToPath(
|
||||
new URL("../tests/conformance/ghidra", import.meta.url),
|
||||
);
|
||||
const project = join(workspace, "guard-project");
|
||||
await mkdir(project);
|
||||
const sourceDigest = digest(await readFile(bridge));
|
||||
const targetDigest = digest(await readFile(target));
|
||||
const launch = await spawnOwnedProviderProcess({
|
||||
command: installation.analyzeHeadlessPath,
|
||||
arguments: [
|
||||
project,
|
||||
"SwitchEvidence",
|
||||
"-import",
|
||||
target,
|
||||
"-noanalysis",
|
||||
"-readOnly",
|
||||
"-scriptPath",
|
||||
`${fixtures};${dirname(bridge)}`,
|
||||
"-postScript",
|
||||
"ReaSwitchEvidenceProbe.java",
|
||||
bridge,
|
||||
"-deleteProject",
|
||||
],
|
||||
runId,
|
||||
expectedCommand: null,
|
||||
});
|
||||
const supervisor = new ProviderProcessSupervisor({
|
||||
...launch,
|
||||
ownsProcessLifetime: true,
|
||||
cleanup: () => cleanupOwnedProcessGroup(launch.ownership),
|
||||
});
|
||||
try {
|
||||
assert.ok(
|
||||
await supervisor.waitForExit(120000),
|
||||
"Production switch guard lane exceeded its 120-second headless deadline",
|
||||
);
|
||||
const snapshot = supervisor.snapshot();
|
||||
const output = `${snapshot.stdout.text}\n${snapshot.stderr.text}`;
|
||||
assert.equal(snapshot.exitCode, 0, output);
|
||||
const reports = [
|
||||
...output.matchAll(/REA_SWITCH_EVIDENCE_PROBE_JSON (\{[^\r\n]*\})/gu),
|
||||
];
|
||||
assert.equal(
|
||||
reports.length,
|
||||
1,
|
||||
`Expected one production guard report: ${output}`,
|
||||
);
|
||||
assert.ok(output.includes("REA_SWITCH_EVIDENCE_PROBE_COMPLETE"), output);
|
||||
const report = JSON.parse(reports[0][1]);
|
||||
assertControlReport(
|
||||
report,
|
||||
bridge,
|
||||
sourceDigest,
|
||||
installation.providerVersion,
|
||||
);
|
||||
assert.equal(
|
||||
digest(await readFile(bridge)),
|
||||
sourceDigest,
|
||||
"Guard modified bridge source",
|
||||
);
|
||||
assert.equal(
|
||||
digest(await readFile(target)),
|
||||
targetDigest,
|
||||
"Guard modified imported fixture bytes",
|
||||
);
|
||||
return report;
|
||||
} finally {
|
||||
const stopped = await supervisor.stop();
|
||||
supervisor.dispose();
|
||||
assert.notEqual(stopped.status, "incomplete", JSON.stringify(stopped));
|
||||
}
|
||||
}
|
||||
|
||||
function digest(bytes) {
|
||||
return createHash("sha256").update(bytes).digest("hex");
|
||||
}
|
||||
|
||||
function assertControlReport(report, bridge, sourceDigest, version) {
|
||||
assert.ok(
|
||||
typeof report === "object" && report !== null && !Array.isArray(report),
|
||||
);
|
||||
assert.equal(report.schema_version, 1);
|
||||
assert.equal(report.status, "passed");
|
||||
assert.equal(report.ghidra_version, version);
|
||||
assert.equal(report.bridge_source_path, bridge);
|
||||
assert.equal(report.bridge_source_sha256, sourceDigest);
|
||||
assert.ok(Array.isArray(report.checks));
|
||||
assert.deepEqual(
|
||||
[...report.checks].sort(),
|
||||
[...EXPECTED_CHECKS].sort(),
|
||||
"Production guard did not execute every required case",
|
||||
);
|
||||
assert.equal(report.check_count, EXPECTED_CHECKS.length);
|
||||
assert.ok(
|
||||
typeof report.scope === "string" &&
|
||||
report.scope.includes("detached Ghidra model objects"),
|
||||
);
|
||||
}
|
||||
@@ -0,0 +1,348 @@
|
||||
#!/usr/bin/env node
|
||||
import assert from "node:assert/strict";
|
||||
import { execFile } from "node:child_process";
|
||||
import { createHash } from "node:crypto";
|
||||
import {
|
||||
copyFile,
|
||||
mkdir,
|
||||
mkdtemp,
|
||||
readFile,
|
||||
readdir,
|
||||
rm,
|
||||
writeFile,
|
||||
} from "node:fs/promises";
|
||||
import { tmpdir } from "node:os";
|
||||
import { join, resolve } from "node:path";
|
||||
import { fileURLToPath } from "node:url";
|
||||
import { parseArgs, promisify } from "node:util";
|
||||
import { Client } from "@modelcontextprotocol/client";
|
||||
import { StdioClientTransport } from "@modelcontextprotocol/client/stdio";
|
||||
import {
|
||||
buildSwitchSource,
|
||||
switchSymbolOracle,
|
||||
assertCompiledSwitchOracle,
|
||||
} from "../tests/conformance/ghidra/switch-fixture.mjs";
|
||||
import {
|
||||
assertSwitchBoundary,
|
||||
assertSwitchOracleControls,
|
||||
} from "./verify-real-ghidra-switch-assertions.mjs";
|
||||
import { createVerifierRun, completeVerifierRun } from "./lib/verifier-run.mjs";
|
||||
import { verifySwitchEvidenceControls } from "./verify-real-ghidra-switch-controls.mjs";
|
||||
|
||||
// Narrow compiler-shape lane; no cross compiler or game artifact prerequisites.
|
||||
const { values } = parseArgs({
|
||||
options: {
|
||||
"compiler-oracle-only": { type: "boolean", default: false },
|
||||
entrypoint: { type: "string" },
|
||||
},
|
||||
});
|
||||
const compilerOnly = values["compiler-oracle-only"];
|
||||
const entrypoint =
|
||||
values.entrypoint === undefined
|
||||
? fileURLToPath(new URL("./rea.mjs", import.meta.url))
|
||||
: resolve(values.entrypoint);
|
||||
assert.ok(
|
||||
process.platform === "linux" && process.arch === "x64",
|
||||
"Ghidra switch compiler lane requires Linux x64; macOS/Windows and cross targets use their separate provider lanes.",
|
||||
);
|
||||
const exec = promisify(execFile);
|
||||
const commands = {
|
||||
gcc: process.env.REA_GCC ?? "gcc",
|
||||
clang: process.env.REA_CLANG ?? "clang",
|
||||
nm: process.env.REA_NM ?? "nm",
|
||||
objdump: process.env.REA_OBJDUMP ?? "objdump",
|
||||
strip: process.env.REA_STRIP ?? "strip",
|
||||
};
|
||||
const versions = {};
|
||||
for (const [role, command] of Object.entries(commands)) {
|
||||
try {
|
||||
const { stdout } = await exec(command, ["--version"]);
|
||||
versions[role] = stdout.split("\n")[0];
|
||||
} catch (cause) {
|
||||
throw new Error(
|
||||
`Ghidra switch compiler lane prerequisite missing: ${role} '${command}'`,
|
||||
{ cause },
|
||||
);
|
||||
}
|
||||
}
|
||||
let installation;
|
||||
if (!compilerOnly) {
|
||||
const { inspectGhidraInstallation } = await import(
|
||||
"../dist/ghidra/GhidraInstallation.js"
|
||||
);
|
||||
assert.ok(
|
||||
process.env.GHIDRA_INSTALL_DIR,
|
||||
"Ghidra switch lane prerequisite missing: GHIDRA_INSTALL_DIR (bring your own)",
|
||||
);
|
||||
installation = inspectGhidraInstallation({
|
||||
installDir: process.env.GHIDRA_INSTALL_DIR,
|
||||
...(process.env.JAVA_HOME === undefined
|
||||
? {}
|
||||
: { javaHome: process.env.JAVA_HOME }),
|
||||
});
|
||||
assert.equal(installation.status, "available", JSON.stringify(installation));
|
||||
}
|
||||
const run = createVerifierRun();
|
||||
const workspace = await mkdtemp(join(tmpdir(), "rea-switch-proof-"));
|
||||
const runtime = join(workspace, "runtime");
|
||||
await mkdir(runtime);
|
||||
const source = join(workspace, "switch.c");
|
||||
await writeFile(source, buildSwitchSource());
|
||||
const flags = ["-O2", "-g", "-fno-pie", "-no-pie"];
|
||||
const results = [];
|
||||
let productionControls = null;
|
||||
try {
|
||||
for (const compiler of ["gcc", "clang"]) {
|
||||
const original = join(workspace, `${compiler}-optimized`);
|
||||
await exec(commands[compiler], [...flags, source, "-o", original]);
|
||||
const bytes = await readFile(original);
|
||||
const { stdout: symbols } = await exec(commands.nm, ["-n", original]);
|
||||
const { stdout: disassembly } = await exec(commands.objdump, [
|
||||
"-d",
|
||||
original,
|
||||
]);
|
||||
const fixtures = assertCompiledSwitchOracle(
|
||||
bytes,
|
||||
switchSymbolOracle(symbols),
|
||||
disassembly,
|
||||
);
|
||||
const oracleFaultControls = assertSwitchOracleControls(fixtures);
|
||||
if (!compilerOnly && productionControls === null) {
|
||||
productionControls = await verifySwitchEvidenceControls({
|
||||
installation,
|
||||
entrypoint,
|
||||
target: original,
|
||||
workspace,
|
||||
runId: run.run_id,
|
||||
});
|
||||
assert.equal(
|
||||
digest(await readFile(original)),
|
||||
digest(bytes),
|
||||
"Guard changed compiler-oracled input",
|
||||
);
|
||||
}
|
||||
const stripped = join(workspace, `${compiler}-stripped`);
|
||||
await copyFile(original, stripped);
|
||||
await exec(commands.strip, ["--strip-all", stripped]);
|
||||
// Byte/physical target oracle survives removal of the names that REA could use.
|
||||
assertCompiledSwitchOracle(await readFile(stripped), fixtures, disassembly);
|
||||
for (const [variant, path] of [
|
||||
["optimized", original],
|
||||
["stripped", stripped],
|
||||
]) {
|
||||
const sha256 = digest(await readFile(path));
|
||||
const observation = compilerOnly
|
||||
? null
|
||||
: await verifyTarget(path, sha256, fixtures, variant);
|
||||
assert.equal(
|
||||
digest(await readFile(path)),
|
||||
sha256,
|
||||
"REA analysis changed original compiled fixture",
|
||||
);
|
||||
results.push({
|
||||
compiler,
|
||||
variant,
|
||||
oracle_fault_controls: oracleFaultControls,
|
||||
sha256,
|
||||
compiler_oracle: fixtures.map(
|
||||
({
|
||||
name,
|
||||
address,
|
||||
dispatch_address,
|
||||
table_address,
|
||||
slots,
|
||||
default_address,
|
||||
}) => ({
|
||||
name,
|
||||
address,
|
||||
dispatch_address,
|
||||
table_address,
|
||||
slots,
|
||||
default_address,
|
||||
}),
|
||||
),
|
||||
observation,
|
||||
});
|
||||
}
|
||||
}
|
||||
} finally {
|
||||
try {
|
||||
assert.deepEqual(
|
||||
(await readdir(runtime)).filter((name) => name.startsWith("rea-ghidra-")),
|
||||
[],
|
||||
"Owned Ghidra runtime survived close",
|
||||
);
|
||||
} finally {
|
||||
await rm(workspace, { recursive: true, force: true });
|
||||
}
|
||||
}
|
||||
const lifecycle = await completeVerifierRun(run);
|
||||
if (lifecycle.process_lineage.status === "verified")
|
||||
assert.deepEqual(lifecycle.process_lineage.descendants, []);
|
||||
process.stdout.write(
|
||||
`${JSON.stringify({ lane: "linux-x64-compiler-switch", compiler_only: compilerOnly, entrypoint, versions, compiler_flags: flags, verifier_run: lifecycle, production_controls: productionControls, results, limitations: ["Exact compiler oracle admits absolute 8-byte native x86-64 ELF tables and fails explicitly when a compiler changes lowering.", "Compiled binaries are analyzed read-only; target programs are never executed.", "Comparison-only control proves absence of a fabricated table and preservation of provider limitations, not recovery of C source.", "Detached Ghidra object controls exercise actual bridge methods through reflection; they do not claim naturally compiled ambiguous dispatches.", "CLI/MCP comparison covers switch observations, excluding process-specific Evidence IDs."], cleanup: "complete" })}\n`,
|
||||
);
|
||||
|
||||
function digest(bytes) {
|
||||
return createHash("sha256").update(bytes).digest("hex");
|
||||
}
|
||||
async function verifyTarget(path, sha256, fixtures, variant) {
|
||||
const env = {
|
||||
PATH: process.env.PATH ?? "/usr/bin:/bin",
|
||||
TMPDIR: runtime,
|
||||
REA_LOG_LEVEL: "silent",
|
||||
REA_ANALYSIS_PROVIDER: "ghidra",
|
||||
REA_PROCESS_RUN_ID: run.run_id,
|
||||
GHIDRA_INSTALL_DIR: process.env.GHIDRA_INSTALL_DIR,
|
||||
...(process.env.JAVA_HOME === undefined
|
||||
? {}
|
||||
: { JAVA_HOME: process.env.JAVA_HOME }),
|
||||
};
|
||||
const transport = new StdioClientTransport({
|
||||
command: process.execPath,
|
||||
args: [entrypoint, "mcp"],
|
||||
env,
|
||||
stderr: "pipe",
|
||||
});
|
||||
const client = new Client({ name: "rea-real-switch-proof", version: "1" });
|
||||
let opened = false;
|
||||
let stderr = "";
|
||||
const observations = [];
|
||||
try {
|
||||
await client.connect(transport);
|
||||
transport.stderr?.on("data", (chunk) => {
|
||||
stderr = (stderr + chunk.toString()).slice(-65536);
|
||||
});
|
||||
const target = await call(client, "open_binary", {
|
||||
path,
|
||||
provider: "ghidra",
|
||||
});
|
||||
opened = true;
|
||||
assert.equal(target.sha256, sha256);
|
||||
assert.equal(target.architecture, "x86_64");
|
||||
assert.equal(target.format, "elf");
|
||||
const procedures = await call(client, "list_procedures");
|
||||
for (const fixture of fixtures) {
|
||||
const observationFixture = {
|
||||
...fixture,
|
||||
allow_unsigned_32_labels:
|
||||
variant === "stripped" && fixture.name === "negative",
|
||||
};
|
||||
const procedure = procedures.find(
|
||||
({ address }) => address === fixture.address,
|
||||
);
|
||||
assert.ok(
|
||||
procedure,
|
||||
`Source-owned function at ${fixture.address} not discovered in optimized/stripped fixture`,
|
||||
);
|
||||
const observed = await toolResult(client, "inspect_native_api", {
|
||||
procedure: procedure.address,
|
||||
});
|
||||
assertWorkflowIdentity(observed.evidence, sha256);
|
||||
assert.equal(observed.result.procedure.address, procedure.address);
|
||||
const summary = assertSwitchBoundary(
|
||||
observed.result.boundary,
|
||||
observationFixture,
|
||||
);
|
||||
assert.deepEqual(
|
||||
[...observed.result.residual_unknowns].sort(),
|
||||
expectedResidualUnknowns(observed.result.boundary, fixture).sort(),
|
||||
"Residual unknowns must preserve unresolved ABI types and exactly the expected switch uncertainty",
|
||||
);
|
||||
const cli = await cliSwitchEvidence(
|
||||
entrypoint,
|
||||
path,
|
||||
procedure.address,
|
||||
env,
|
||||
);
|
||||
assertWorkflowIdentity(cli, sha256);
|
||||
assert.equal(cli.normalized_result.procedure.address, procedure.address);
|
||||
assertSwitchBoundary(cli.normalized_result.boundary, observationFixture);
|
||||
assert.deepEqual(
|
||||
cli.normalized_result.boundary.jump_tables,
|
||||
observed.result.boundary.jump_tables,
|
||||
"CLI/MCP switch mappings/defaults/data-source evidence differ",
|
||||
);
|
||||
assert.deepEqual(
|
||||
cli.normalized_result.residual_unknowns,
|
||||
observed.result.residual_unknowns,
|
||||
);
|
||||
observations.push({
|
||||
name: fixture.name,
|
||||
...summary,
|
||||
cli_mcp_equal: true,
|
||||
limitations: observed.result.boundary.limitations,
|
||||
residual_unknowns: observed.result.residual_unknowns,
|
||||
jump_tables: observed.result.boundary.jump_tables,
|
||||
});
|
||||
}
|
||||
return { observations, stderr };
|
||||
} finally {
|
||||
try {
|
||||
if (opened) await call(client, "close_binary");
|
||||
} finally {
|
||||
try {
|
||||
await client.close();
|
||||
} finally {
|
||||
await transport.close();
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
function assertWorkflowIdentity(evidence, sha256) {
|
||||
assert.equal(evidence.subject.digest.sha256, sha256);
|
||||
assert.equal(evidence.operation, "inspect_native_api");
|
||||
assert.equal(evidence.provider.id, "rea-workflow");
|
||||
assert.equal(evidence.analysis_profile.provider.id, "rea-workflow");
|
||||
assert.equal(
|
||||
evidence.analysis_profile.parameters.upstream_analysis_profile.parameters
|
||||
.language_id,
|
||||
"auto-from-header",
|
||||
);
|
||||
}
|
||||
|
||||
function expectedResidualUnknowns(boundary, fixture) {
|
||||
const unknowns = [boundary.return_type, ...boundary.parameters]
|
||||
.filter(({ confidence }) => confidence === "low")
|
||||
.map(
|
||||
({ role, data_type: type }) =>
|
||||
`Can the inferred ${role} type ${type} be confirmed with imported metadata or an ABI probe?`,
|
||||
);
|
||||
if (fixture.unsafe_integer)
|
||||
unknowns.push(
|
||||
`Which source-level case values correspond to every target dispatched at ${boundary.jump_tables[0].dispatch_address}?`,
|
||||
);
|
||||
return [...new Set(unknowns)];
|
||||
}
|
||||
async function toolResult(client, name, arguments_ = {}) {
|
||||
const result = await client.callTool(
|
||||
{ name, arguments: arguments_ },
|
||||
{ timeout: 240000 },
|
||||
);
|
||||
assert.notEqual(result.isError, true, JSON.stringify(result));
|
||||
assert.ok(
|
||||
result.structuredContent && "result" in result.structuredContent,
|
||||
`${name} omitted structured result`,
|
||||
);
|
||||
return result.structuredContent;
|
||||
}
|
||||
async function call(client, name, arguments_ = {}) {
|
||||
return (await toolResult(client, name, arguments_)).result;
|
||||
}
|
||||
|
||||
async function cliSwitchEvidence(entrypoint, path, procedure, env) {
|
||||
const { stdout } = await exec(
|
||||
process.execPath,
|
||||
[
|
||||
entrypoint,
|
||||
"inspect-native-api",
|
||||
path,
|
||||
procedure,
|
||||
"--provider",
|
||||
"ghidra",
|
||||
"--json",
|
||||
],
|
||||
{ env, timeout: 240000, maxBuffer: 16 * 1024 * 1024 },
|
||||
);
|
||||
return JSON.parse(stdout);
|
||||
}
|
||||
@@ -33,8 +33,10 @@ import {
|
||||
verifyInventoryOperations,
|
||||
} from "./verify-real-ghidra-inventory.mjs";
|
||||
import { completeVerifierRun, createVerifierRun } from "./lib/verifier-run.mjs";
|
||||
import { hasTypedSwitchEvidence } from "./verify-real-ghidra-switch-assertions.mjs";
|
||||
|
||||
import {
|
||||
verifyDenseDefaultReturn,
|
||||
verifyNativeTypeLayout,
|
||||
verifyRelativeSwitch,
|
||||
verifyNativeValueTrace,
|
||||
@@ -308,8 +310,7 @@ function nativeFixtureTarget(platform, architecture) {
|
||||
async function verifyNativeApiCli(
|
||||
targetPath,
|
||||
procedures,
|
||||
requireDenseJumpTable,
|
||||
denseSwitchSymbol = "rea_ghidra_inventory_dense_switch",
|
||||
{ requireDenseJumpTable, denseSwitchSymbol, client },
|
||||
) {
|
||||
const denseSwitch = procedures.find(({ value }) =>
|
||||
value.endsWith(denseSwitchSymbol),
|
||||
@@ -349,11 +350,25 @@ async function verifyNativeApiCli(
|
||||
(mapping) =>
|
||||
mapping.case_value === caseValue &&
|
||||
mapping.confidence === "high" &&
|
||||
mapping.evidence.some(
|
||||
({ detail }) =>
|
||||
detail.includes(`case value ${caseValue} with target`) ||
|
||||
detail.startsWith(`Case value ${caseValue} indexes byte `),
|
||||
),
|
||||
(hasTypedSwitchEvidence(
|
||||
mapping.evidence,
|
||||
`Typed case value ${caseValue}`,
|
||||
mapping.target_address,
|
||||
denseTable.dispatch_address,
|
||||
) ||
|
||||
mapping.evidence.some(
|
||||
({ kind, source, detail }) =>
|
||||
kind === "jump-table" &&
|
||||
typeof detail === "string" &&
|
||||
detail.trim().length > 0 &&
|
||||
((source === "ghidra-high-function" &&
|
||||
detail.includes(
|
||||
`case value ${caseValue} with target ${mapping.target_address}`,
|
||||
)) ||
|
||||
(source === "ghidra-instruction-and-memory" &&
|
||||
detail.startsWith(`Case value ${caseValue} indexes byte `) &&
|
||||
detail.includes(`reaching ${mapping.target_address}.`))),
|
||||
)),
|
||||
),
|
||||
);
|
||||
if (
|
||||
@@ -368,7 +383,20 @@ async function verifyNativeApiCli(
|
||||
if (
|
||||
requireDenseJumpTable &&
|
||||
(denseTable === undefined ||
|
||||
denseCases.size !== denseTable.mappings.length ||
|
||||
denseCases.size !== expectedCases.length ||
|
||||
denseTable.mappings.length !== expectedCases.length ||
|
||||
denseTable.default_targets.length !== 1 ||
|
||||
denseTable.default_targets[0].confidence !== "high" ||
|
||||
!hasTypedSwitchEvidence(
|
||||
denseTable.default_targets[0].evidence,
|
||||
"Typed default label",
|
||||
denseTable.default_targets[0].target_address,
|
||||
denseTable.dispatch_address,
|
||||
) ||
|
||||
denseTable.mappings.some(
|
||||
({ target_address }) =>
|
||||
target_address === denseTable.default_targets[0].target_address,
|
||||
) ||
|
||||
expectedCases.some((caseValue) => !denseCases.has(caseValue)) ||
|
||||
!mappingsAreExact ||
|
||||
evidence.normalized_result?.residual_unknowns?.length !== 0)
|
||||
@@ -376,10 +404,17 @@ async function verifyNativeApiCli(
|
||||
throw new Error(
|
||||
`The shipped inspect-native-api CLI did not preserve complete dense jump-table output: ${stdout}`,
|
||||
);
|
||||
const defaultOracle = requireDenseJumpTable
|
||||
? await verifyDenseDefaultReturn(
|
||||
client,
|
||||
denseTable.default_targets[0].target_address,
|
||||
)
|
||||
: null;
|
||||
return {
|
||||
operation: evidence.operation,
|
||||
provider: evidence.provider,
|
||||
mappings_returned: denseTable?.mappings.length ?? null,
|
||||
default_oracle: defaultOracle,
|
||||
residual_unknowns: evidence.normalized_result.residual_unknowns.length,
|
||||
};
|
||||
}
|
||||
@@ -456,16 +491,16 @@ async function verifyTarget(targetPath, variant, expectedTarget = null) {
|
||||
variant === "cross-arm64-elf" || variant === "aarch64-jump-table";
|
||||
const nativeApiCli =
|
||||
variant === "debug" || crossArm64Elf
|
||||
? await verifyNativeApiCli(
|
||||
parsedTarget.value.path,
|
||||
procedures,
|
||||
crossArm64Elf ||
|
||||
? await verifyNativeApiCli(parsedTarget.value.path, procedures, {
|
||||
requireDenseJumpTable:
|
||||
crossArm64Elf ||
|
||||
(expectedNativeTarget.format === "elf" &&
|
||||
expectedNativeTarget.architecture === "x86_64"),
|
||||
crossArm64Elf
|
||||
denseSwitchSymbol: crossArm64Elf
|
||||
? "rea_cross_dense_switch"
|
||||
: "rea_ghidra_inventory_dense_switch",
|
||||
)
|
||||
client,
|
||||
})
|
||||
: null;
|
||||
const probes = variant.startsWith("relative-")
|
||||
? await verifyRelativeSwitch(
|
||||
|
||||
@@ -4,7 +4,7 @@ description: Reverse engineer native, managed, Electron/JavaScript, packaged, an
|
||||
metadata:
|
||||
version: "23"
|
||||
tool_count: 116
|
||||
catalog_digest: "73a4cdf4fc83b1728426931ff89e2113f1c8beb1b3bf337c179f2c349ce3c0f2"
|
||||
catalog_digest: "93e02e0675739b3049b010eabe96745957e29267759a7028a66057677d1f4d92"
|
||||
---
|
||||
|
||||
# REA
|
||||
|
||||
@@ -5,6 +5,71 @@ import { ghidraFunctionDossier } from "../domain/hopperValues.fixture.js";
|
||||
import { nativeApiBoundarySchema } from "../domain/nativeApiBoundary.js";
|
||||
import { projectNativeApiInspection } from "./NativeApiInspection.js";
|
||||
|
||||
describe("native API switch uncertainty", () => {
|
||||
it("reports an unevidenced default path independently of known numeric cases", () => {
|
||||
const dossier = functionDossierSchema.parse(ghidraFunctionDossier());
|
||||
const boundary = dossier.native_api;
|
||||
if (boundary?.available !== true)
|
||||
throw new TypeError("Ghidra native API fixture is unavailable");
|
||||
const table = boundary.jump_tables[0];
|
||||
if (table === undefined)
|
||||
throw new TypeError("Ghidra jump-table fixture is unavailable");
|
||||
const incomplete = functionDossierSchema.parse({
|
||||
...dossier,
|
||||
native_api: {
|
||||
...boundary,
|
||||
jump_tables: [{ ...table, default_targets: [] }],
|
||||
},
|
||||
});
|
||||
expect(projectNativeApiInspection(incomplete).residual_unknowns).toContain(
|
||||
"Which default or out-of-range path, if any, belongs to the dispatch at 0x401010?",
|
||||
);
|
||||
});
|
||||
|
||||
it("does not report evidenced defaults as unknown cases and retains genuinely unresolved mappings", () => {
|
||||
const dossier = functionDossierSchema.parse(ghidraFunctionDossier());
|
||||
const boundary = dossier.native_api;
|
||||
if (boundary?.available !== true)
|
||||
throw new TypeError("Ghidra native API fixture is unavailable");
|
||||
const table = boundary.jump_tables[0];
|
||||
const mapping = table?.mappings[0];
|
||||
if (table === undefined || mapping === undefined)
|
||||
throw new TypeError("Ghidra jump-table fixture is unavailable");
|
||||
const defaultTarget = {
|
||||
target_address: mapping.target_address,
|
||||
confidence: "high",
|
||||
evidence: mapping.evidence,
|
||||
};
|
||||
const complete = functionDossierSchema.parse({
|
||||
...dossier,
|
||||
native_api: {
|
||||
...boundary,
|
||||
jump_tables: [{ ...table, default_targets: [defaultTarget] }],
|
||||
},
|
||||
});
|
||||
expect(projectNativeApiInspection(complete).residual_unknowns).toEqual([]);
|
||||
const unresolved = functionDossierSchema.parse({
|
||||
...complete,
|
||||
native_api: {
|
||||
...boundary,
|
||||
jump_tables: [
|
||||
{
|
||||
...table,
|
||||
default_targets: [defaultTarget],
|
||||
mappings: [
|
||||
mapping,
|
||||
{ ...mapping, case_value: null, target_address: "0x401030" },
|
||||
],
|
||||
},
|
||||
],
|
||||
},
|
||||
});
|
||||
expect(projectNativeApiInspection(unresolved).residual_unknowns).toContain(
|
||||
"Which source-level case values correspond to every target dispatched at 0x401010?",
|
||||
);
|
||||
});
|
||||
});
|
||||
|
||||
describe("native API inspection", () => {
|
||||
it("preserves structured type and jump-table boundary evidence", () => {
|
||||
const dossier = functionDossierSchema.parse(ghidraFunctionDossier());
|
||||
|
||||
@@ -72,6 +72,10 @@ const availableResidualUnknowns = (
|
||||
): readonly string[] => {
|
||||
const unknowns: string[] = [];
|
||||
for (const table of boundary.jump_tables) {
|
||||
if (table.default_targets.length === 0)
|
||||
unknowns.push(
|
||||
`Which default or out-of-range path, if any, belongs to the dispatch at ${table.dispatch_address}?`,
|
||||
);
|
||||
if (table.mappings.length === 0)
|
||||
unknowns.push(
|
||||
`Which case values and targets belong to the dispatch at ${table.dispatch_address}?`,
|
||||
|
||||
@@ -40,6 +40,6 @@ export const FUNCTION_WORKFLOW_TOOL_CONTRACTS = [
|
||||
),
|
||||
functionWorkflow(
|
||||
"inspect_native_api",
|
||||
"Analyze a native API boundary in one function identified by symbol or provider-returned address. Returns confidence, evidence, jump-table dispatch/data/target mappings, unsupported branches, and residual unknowns.",
|
||||
"Analyze a native API boundary in one function identified by symbol or provider-returned address. Returns confidence, evidence, jump-table dispatch/data/case mappings, separately evidenced default targets, unsupported branches, and residual unknowns. Null case values mean unresolved cases, never a known default.",
|
||||
),
|
||||
] as const satisfies readonly ToolContract[];
|
||||
|
||||
@@ -114,6 +114,20 @@ export const ghidraNativeApiBoundary = () => ({
|
||||
],
|
||||
},
|
||||
],
|
||||
default_targets: [
|
||||
{
|
||||
target_address: "0x401030",
|
||||
confidence: "high" as const,
|
||||
evidence: [
|
||||
{
|
||||
kind: "jump-table" as const,
|
||||
source: "ghidra-clang-case-token",
|
||||
detail:
|
||||
"Typed default label belongs to the block at 0x401030 with unique indirect dispatch predecessor 0x401010.",
|
||||
},
|
||||
],
|
||||
},
|
||||
],
|
||||
limitations: [],
|
||||
},
|
||||
],
|
||||
|
||||
@@ -71,11 +71,18 @@ const jumpTableMappingSchema = z
|
||||
})
|
||||
.strict();
|
||||
|
||||
const jumpTableDefaultTargetSchema = z.strictObject({
|
||||
target_address: z.string().min(1),
|
||||
confidence: inferenceConfidenceSchema,
|
||||
evidence: z.array(inferenceEvidenceSchema).min(1),
|
||||
});
|
||||
|
||||
const inferredJumpTableSchema = z
|
||||
.object({
|
||||
dispatch_address: z.string().min(1),
|
||||
data_sources: z.array(jumpTableDataSourceSchema),
|
||||
mappings: z.array(jumpTableMappingSchema),
|
||||
default_targets: z.array(jumpTableDefaultTargetSchema).default([]),
|
||||
limitations: z.array(z.string()),
|
||||
})
|
||||
.strict();
|
||||
|
||||
File diff suppressed because one or more lines are too long
@@ -40,6 +40,8 @@ export const resolveGhidraAnalysisProfile = (
|
||||
].sort(),
|
||||
import_mode: "ephemeral-read-only",
|
||||
function_body_evidence: "complete-inclusive-ranges-v1",
|
||||
jump_table_evidence: "typed-case-default-blocks-v1",
|
||||
decompiler_jump_loads: true,
|
||||
loader: dosMz ? "MzLoader" : "auto-from-header",
|
||||
language_id: dosMz ? "x86:LE:16:Real Mode" : "auto-from-header",
|
||||
compiler_spec_id: dosMz ? "default" : "auto-default",
|
||||
|
||||
@@ -193,6 +193,113 @@ describe("Ghidra function-analysis result values", () => {
|
||||
});
|
||||
|
||||
describe("Ghidra jump-table mapping contract", () => {
|
||||
it("preserves evidenced defaults separately from cases and unresolved targets", () => {
|
||||
const dossier = functionDossierSchema.parse(ghidraFunctionDossier());
|
||||
const boundary = dossier.native_api;
|
||||
if (boundary?.available !== true)
|
||||
throw new TypeError("Ghidra native API fixture is unavailable");
|
||||
const table = boundary.jump_tables[0];
|
||||
const mapping = table?.mappings[0];
|
||||
if (table === undefined || mapping === undefined)
|
||||
throw new TypeError("Ghidra jump-table fixture is unavailable");
|
||||
const defaults = [
|
||||
{
|
||||
target_address: mapping.target_address,
|
||||
confidence: "high",
|
||||
evidence: [
|
||||
{
|
||||
kind: "jump-table",
|
||||
source: "ghidra-clang-case-token",
|
||||
detail: "Default label reaches this recovered destination.",
|
||||
},
|
||||
],
|
||||
},
|
||||
];
|
||||
const parsed = parseGhidraFunctionResult("analyze_function", {
|
||||
...dossier,
|
||||
native_api: {
|
||||
...boundary,
|
||||
jump_tables: [
|
||||
{
|
||||
...table,
|
||||
default_targets: defaults,
|
||||
mappings: [
|
||||
mapping,
|
||||
{ ...mapping, case_value: null, target_address: "0x401030" },
|
||||
],
|
||||
},
|
||||
],
|
||||
},
|
||||
});
|
||||
expect(parsed.ok).toBe(true);
|
||||
if (!parsed.ok) throw parsed.error;
|
||||
const output = functionDossierSchema.parse(parsed.value).native_api;
|
||||
if (output?.available !== true)
|
||||
throw new TypeError("Ghidra native API fixture is unavailable");
|
||||
expect(output.jump_tables[0]).toMatchObject({
|
||||
default_targets: defaults,
|
||||
mappings: [
|
||||
{ case_value: 0, target_address: "0x401020" },
|
||||
{ case_value: null, target_address: "0x401030" },
|
||||
],
|
||||
});
|
||||
});
|
||||
|
||||
it("normalizes legacy missing defaults without promoting unknown cases", () => {
|
||||
const dossier = functionDossierSchema.parse(ghidraFunctionDossier());
|
||||
const boundary = dossier.native_api;
|
||||
if (boundary?.available !== true)
|
||||
throw new TypeError("Ghidra native API fixture is unavailable");
|
||||
const table = boundary.jump_tables[0];
|
||||
const mapping = table?.mappings[0];
|
||||
if (table === undefined || mapping === undefined)
|
||||
throw new TypeError("Ghidra jump-table fixture is unavailable");
|
||||
const { default_targets: _legacyDefaults, ...legacy } = table;
|
||||
const parsed = parseGhidraFunctionResult("analyze_function", {
|
||||
...dossier,
|
||||
native_api: {
|
||||
...boundary,
|
||||
jump_tables: [
|
||||
{ ...legacy, mappings: [{ ...mapping, case_value: null }] },
|
||||
],
|
||||
},
|
||||
});
|
||||
expect(parsed.ok).toBe(true);
|
||||
if (!parsed.ok) throw parsed.error;
|
||||
expect(functionDossierSchema.parse(parsed.value).native_api).toMatchObject({
|
||||
jump_tables: [{ default_targets: [], mappings: [{ case_value: null }] }],
|
||||
});
|
||||
});
|
||||
|
||||
it("rejects non-canonical default destinations and defaults without evidence", () => {
|
||||
const dossier = functionDossierSchema.parse(ghidraFunctionDossier());
|
||||
const boundary = dossier.native_api;
|
||||
if (boundary?.available !== true)
|
||||
throw new TypeError("Ghidra native API fixture is unavailable");
|
||||
const table = boundary.jump_tables[0];
|
||||
const mapping = table?.mappings[0];
|
||||
if (table === undefined || mapping === undefined)
|
||||
throw new TypeError("Ghidra jump-table fixture is unavailable");
|
||||
for (const destination of [
|
||||
{
|
||||
target_address: "0X401020",
|
||||
confidence: "high",
|
||||
evidence: mapping.evidence,
|
||||
},
|
||||
{ target_address: "0x401020", confidence: "high", evidence: [] },
|
||||
]) {
|
||||
expect(
|
||||
parseGhidraFunctionResult("analyze_function", {
|
||||
...dossier,
|
||||
native_api: {
|
||||
...boundary,
|
||||
jump_tables: [{ ...table, default_targets: [destination] }],
|
||||
},
|
||||
}),
|
||||
).toMatchObject({ ok: false, error: { _tag: "AnalysisOutputError" } });
|
||||
}
|
||||
});
|
||||
|
||||
it("keeps jump-table sources separate from case-to-target mappings", () => {
|
||||
const parsed = parseGhidraFunctionResult(
|
||||
"analyze_function",
|
||||
|
||||
@@ -197,6 +197,7 @@ const ghidraNativeApiBoundary = nativeApiBoundarySchema.superRefine(
|
||||
table.dispatch_address,
|
||||
...table.data_sources.map(({ address }) => address),
|
||||
...table.mappings.map(({ target_address }) => target_address),
|
||||
...table.default_targets.map(({ target_address }) => target_address),
|
||||
]);
|
||||
if (
|
||||
addresses.some(
|
||||
|
||||
@@ -39,6 +39,31 @@ const provider = (
|
||||
return new GhidraProvider(config.value, silentLogger, host, clientFactory);
|
||||
};
|
||||
|
||||
describe("Ghidra jump-table profile", () => {
|
||||
it("separates typed case/default evidence and jump-load metadata from legacy cache profiles", async () => {
|
||||
const resolved = await provider().resolveAnalysisProfile(
|
||||
executableTarget("elf", "x86_64"),
|
||||
);
|
||||
if (!resolved.ok || resolved.value.profile === null)
|
||||
throw new Error("expected a committed Ghidra profile");
|
||||
const profile = resolved.value.profile;
|
||||
const legacy = createAnalysisProfile(
|
||||
profile.provider,
|
||||
Object.fromEntries(
|
||||
Object.entries(profile.parameters).filter(
|
||||
([key]) =>
|
||||
key !== "jump_table_evidence" && key !== "decompiler_jump_loads",
|
||||
),
|
||||
),
|
||||
);
|
||||
expect(profile.digest).not.toBe(legacy.digest);
|
||||
expect(profile.parameters.jump_table_evidence).toBe(
|
||||
"typed-case-default-blocks-v1",
|
||||
);
|
||||
expect(profile.parameters.decompiler_jump_loads).toBe(true);
|
||||
});
|
||||
});
|
||||
|
||||
describe("Ghidra provider", () => {
|
||||
it("separates complete body evidence from legacy length-only cache profiles", async () => {
|
||||
const resolved = await provider().resolveAnalysisProfile(
|
||||
|
||||
@@ -18,7 +18,14 @@ describe("Ghidra MCP native API evidence", () => {
|
||||
expect(inspection.normalized_result).toMatchObject({
|
||||
boundary: {
|
||||
available: true,
|
||||
jump_tables: [{ mappings: [{ target_address: "0x401020" }] }],
|
||||
jump_tables: [
|
||||
{
|
||||
mappings: [{ case_value: 0, target_address: "0x401020" }],
|
||||
default_targets: [
|
||||
{ target_address: "0x401030", confidence: "high" },
|
||||
],
|
||||
},
|
||||
],
|
||||
},
|
||||
residual_unknowns: [],
|
||||
});
|
||||
|
||||
@@ -0,0 +1,242 @@
|
||||
//@category REA Verification
|
||||
|
||||
import com.google.gson.JsonArray;
|
||||
import com.google.gson.JsonObject;
|
||||
import generic.jar.ResourceFile;
|
||||
import ghidra.app.decompiler.ClangCaseToken;
|
||||
import ghidra.app.decompiler.ClangNode;
|
||||
import ghidra.app.decompiler.ClangToken;
|
||||
import ghidra.app.script.GhidraScript;
|
||||
import ghidra.app.script.GhidraScriptProvider;
|
||||
import ghidra.app.script.GhidraScriptUtil;
|
||||
import ghidra.framework.Application;
|
||||
import ghidra.program.model.address.Address;
|
||||
import ghidra.program.model.address.AddressSet;
|
||||
import ghidra.program.model.pcode.JumpTable;
|
||||
import ghidra.program.model.pcode.PcodeBlock;
|
||||
import ghidra.program.model.pcode.PcodeBlockBasic;
|
||||
import ghidra.program.model.pcode.PcodeOp;
|
||||
import ghidra.program.model.pcode.PcodeOpAST;
|
||||
import java.io.File;
|
||||
import java.lang.reflect.Constructor;
|
||||
import java.lang.reflect.Field;
|
||||
import java.lang.reflect.InvocationTargetException;
|
||||
import java.lang.reflect.Method;
|
||||
import java.nio.file.Files;
|
||||
import java.security.MessageDigest;
|
||||
import java.util.ArrayList;
|
||||
import java.util.HexFormat;
|
||||
import java.util.List;
|
||||
import java.util.Map;
|
||||
import java.util.Objects;
|
||||
import java.util.Set;
|
||||
|
||||
/**
|
||||
* Executes the production bridge's typed switch evidence methods on detached Ghidra objects.
|
||||
* This is a pinned-model reflection fixture, not a natural compiler ambiguity reproduction.
|
||||
* It never executes the bridge run method or modifies the imported program/database.
|
||||
* Pass the exact bridge source path as the single script argument; source resolution fails closed.
|
||||
*/
|
||||
public class ReaSwitchEvidenceProbe extends GhidraScript {
|
||||
private GhidraScript bridge;
|
||||
private Method typedCases;
|
||||
private Method exactValue;
|
||||
private final JsonArray checks = new JsonArray();
|
||||
|
||||
private static void setField(Class<?> owner, Object object, String name, Object value)
|
||||
throws Exception {
|
||||
Field field = owner.getDeclaredField(name);
|
||||
field.setAccessible(true);
|
||||
field.set(object, value);
|
||||
}
|
||||
|
||||
private static Object field(Object result, String name) throws Exception {
|
||||
Field field = result.getClass().getDeclaredField(name);
|
||||
field.setAccessible(true);
|
||||
return field.get(result);
|
||||
}
|
||||
|
||||
private static Map<?, ?> cases(Object result) throws Exception {
|
||||
Object value = field(result, "cases");
|
||||
if (!(value instanceof Map<?, ?> map)) throw new IllegalStateException("cases is not Map");
|
||||
return map;
|
||||
}
|
||||
|
||||
private static Set<?> set(Object result, String name) throws Exception {
|
||||
Object value = field(result, name);
|
||||
if (!(value instanceof Set<?> values)) throw new IllegalStateException(name + " is not Set");
|
||||
return values;
|
||||
}
|
||||
|
||||
private static Object invoke(Method method, Object target, Object... args) throws Exception {
|
||||
try {
|
||||
return method.invoke(target, args);
|
||||
} catch (InvocationTargetException exception) {
|
||||
throw new IllegalStateException("Production method failed: " + method.getName(), exception.getCause());
|
||||
}
|
||||
}
|
||||
|
||||
private void require(String name, boolean condition) {
|
||||
if (!condition) throw new IllegalStateException("Switch evidence assertion failed: " + name);
|
||||
checks.add(name);
|
||||
}
|
||||
|
||||
private PcodeBlockBasic block(Address start) throws Exception {
|
||||
Constructor<PcodeBlockBasic> constructor = PcodeBlockBasic.class.getDeclaredConstructor();
|
||||
constructor.setAccessible(true);
|
||||
PcodeBlockBasic block = constructor.newInstance();
|
||||
setField(PcodeBlockBasic.class, block, "cover", new AddressSet(start, start.add(15)));
|
||||
return block;
|
||||
}
|
||||
|
||||
private static PcodeOpAST append(PcodeBlockBasic block, Address address, int opcode)
|
||||
throws Exception {
|
||||
PcodeOpAST operation = new PcodeOpAST(address, 0, opcode, 0);
|
||||
Method append = PcodeBlockBasic.class.getDeclaredMethod("insertEnd", PcodeOp.class);
|
||||
append.setAccessible(true);
|
||||
append.invoke(block, operation);
|
||||
return operation;
|
||||
}
|
||||
|
||||
private static void incoming(PcodeBlockBasic destination, PcodeBlockBasic source)
|
||||
throws Exception {
|
||||
Method add = PcodeBlock.class.getDeclaredMethod("addInEdge", PcodeBlock.class, int.class);
|
||||
add.setAccessible(true);
|
||||
add.invoke(destination, source, 0);
|
||||
}
|
||||
|
||||
private static ClangCaseToken token(String text, long magnitude, PcodeOp operation)
|
||||
throws Exception {
|
||||
ClangCaseToken token = new ClangCaseToken(null);
|
||||
setField(ClangToken.class, token, "text", text);
|
||||
setField(ClangCaseToken.class, token, "value", magnitude);
|
||||
setField(ClangCaseToken.class, token, "op", operation);
|
||||
return token;
|
||||
}
|
||||
|
||||
private Object value(String text, long magnitude) throws Exception {
|
||||
return invoke(exactValue, null, token(text, magnitude, null));
|
||||
}
|
||||
|
||||
private static boolean hasUnknownLabelDetail(
|
||||
Object result, String label, long magnitude, Address target, Address dispatch
|
||||
) throws Exception {
|
||||
for (Object item : set(result, "limitations")) {
|
||||
if (item instanceof String detail &&
|
||||
detail.contains(label) &&
|
||||
detail.contains(Long.toUnsignedString(magnitude)) &&
|
||||
detail.contains("0x" + Long.toUnsignedString(target.getOffset(), 16)) &&
|
||||
detail.contains("0x" + Long.toUnsignedString(dispatch.getOffset(), 16))) return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
private Object evidence(Address dispatch, List<Address> destinations, ClangNode... tokens)
|
||||
throws Exception {
|
||||
JumpTable table = new JumpTable(dispatch, new ArrayList<>(destinations), false, 0);
|
||||
return invoke(typedCases, bridge, table, List.of(tokens));
|
||||
}
|
||||
|
||||
private void numericChecks() throws Exception {
|
||||
require("positive_decimal", Objects.equals(value("3", 3), 3L));
|
||||
require("unsigned32_literal_not_rewritten", Objects.equals(value("0xfffffff9", 4294967289L), 4294967289L));
|
||||
require("negative_embedded_token_sign", Objects.equals(value("-3", 3), -3L));
|
||||
require("negative_hex", Objects.equals(value("-0x3", 3), -3L));
|
||||
require("zero", Objects.equals(value("0", 0), 0L));
|
||||
require("magnitude_mismatch_unknown", value("-3", 2) == null);
|
||||
require("signed_encoding_is_not_magnitude", value("-3", -3) == null);
|
||||
require("symbol_label_unknown", value("NAMED_CASE", 3) == null);
|
||||
require("compound_label_unknown", value("1 + 2", 3) == null);
|
||||
require("safe_positive_boundary", Objects.equals(value("9007199254740991", 9007199254740991L), 9007199254740991L));
|
||||
require("safe_negative_boundary", Objects.equals(value("-9007199254740991", 9007199254740991L), -9007199254740991L));
|
||||
require("safe_hex_boundary", Objects.equals(value("0x1fffffffffffff", 9007199254740991L), 9007199254740991L));
|
||||
require("unsafe_positive_unknown", value("9007199254740992", 9007199254740992L) == null);
|
||||
require("unsafe_negative_unknown", value("-9007199254740992", 9007199254740992L) == null);
|
||||
require("unsigned64_unknown", value("0xffffffffffffffff", -1L) == null);
|
||||
}
|
||||
|
||||
private void graphChecks() throws Exception {
|
||||
Address dispatch = toAddr(0x1000);
|
||||
Address otherDispatch = toAddr(0x2000);
|
||||
Address target = toAddr(0x3000);
|
||||
Address otherTarget = toAddr(0x4000);
|
||||
PcodeBlockBasic first = block(dispatch);
|
||||
PcodeBlockBasic second = block(otherDispatch);
|
||||
append(first, dispatch, PcodeOp.BRANCHIND);
|
||||
append(second, otherDispatch, PcodeOp.BRANCHIND);
|
||||
PcodeBlockBasic destination = block(target);
|
||||
PcodeOp body = append(destination, target.add(5), PcodeOp.COPY);
|
||||
ClangCaseToken label = token("3", 3, body);
|
||||
Object none = evidence(dispatch, List.of(target), label);
|
||||
require("no_dispatch_not_attributed", cases(none).isEmpty() && set(none, "defaults").isEmpty());
|
||||
incoming(destination, first);
|
||||
Object one = evidence(dispatch, List.of(target), label);
|
||||
require("unique_dispatch_block_start", Objects.equals(cases(one).get(3L), target));
|
||||
require("instruction_offset_is_not_destination", !body.getSeqnum().getTarget().equals(target));
|
||||
Object wrong = evidence(otherDispatch, List.of(target), label);
|
||||
require("wrong_dispatch_not_attributed", cases(wrong).isEmpty() && set(wrong, "defaults").isEmpty());
|
||||
Object absent = evidence(dispatch, List.of(otherTarget), label);
|
||||
require("target_not_in_table_not_attributed", cases(absent).isEmpty());
|
||||
|
||||
Object signed = evidence(dispatch, List.of(target), token("-3", 3, body), label);
|
||||
require("signed_and_positive_distinct", cases(signed).size() == 2 && Objects.equals(cases(signed).get(-3L), target) && Objects.equals(cases(signed).get(3L), target));
|
||||
Object shared = evidence(dispatch, List.of(target), token("1", 1, body), token("2", 2, body));
|
||||
require("shared_destination_keeps_all_labels", cases(shared).size() == 2 && Objects.equals(cases(shared).get(1L), target) && Objects.equals(cases(shared).get(2L), target));
|
||||
Object defaultRole = evidence(dispatch, List.of(target), token("default", 1, body));
|
||||
require("default_ordinary_off_is_role", cases(defaultRole).isEmpty() && set(defaultRole, "defaults").contains(target));
|
||||
Object defaultShared = evidence(dispatch, List.of(target), token("default", 1, body), token("1", 1, body));
|
||||
require("default_and_numeric_can_share_target", Objects.equals(cases(defaultShared).get(1L), target) && set(defaultShared, "defaults").contains(target));
|
||||
Object unsafe = evidence(dispatch, List.of(target), token("9007199254740992", 9007199254740992L, body));
|
||||
require("unsafe64_target_preserved_unknown", cases(unsafe).isEmpty() && set(unsafe, "unknownTargets").contains(target) && hasUnknownLabelDetail(unsafe, "9007199254740992", 9007199254740992L, target, dispatch));
|
||||
Object mismatch = evidence(dispatch, List.of(target), token("-3", 2, body));
|
||||
require("magnitude_mismatch_target_preserved_unknown", cases(mismatch).isEmpty() && set(mismatch, "unknownTargets").contains(target) && hasUnknownLabelDetail(mismatch, "-3", 2, target, dispatch));
|
||||
|
||||
PcodeBlockBasic conflictBlock = block(otherTarget);
|
||||
incoming(conflictBlock, first);
|
||||
PcodeOp conflictBody = append(conflictBlock, otherTarget.add(5), PcodeOp.COPY);
|
||||
Object conflict = evidence(dispatch, List.of(target, otherTarget), label, token("3", 3, conflictBody), label);
|
||||
require("conflicting_value_retracted", cases(conflict).isEmpty() && set(conflict, "ambiguousValues").contains(3L));
|
||||
require("conflicting_destinations_preserved_unknown", set(conflict, "unknownTargets").contains(target) && set(conflict, "unknownTargets").contains(otherTarget) && !set(conflict, "limitations").isEmpty());
|
||||
|
||||
incoming(destination, second);
|
||||
require("api_first_dispatch_is_insufficient", label.getSwitchOp().getSeqnum().getTarget().equals(dispatch));
|
||||
Object multiple = evidence(dispatch, List.of(target), label, token("default", 1, body));
|
||||
require("multiple_dispatches_rejected", cases(multiple).isEmpty() && set(multiple, "defaults").isEmpty());
|
||||
require("multiple_dispatch_target_preserved_unknown", set(multiple, "unknownTargets").contains(target) && !set(multiple, "limitations").isEmpty());
|
||||
Object multipleOther = evidence(otherDispatch, List.of(target), label);
|
||||
require("multiple_dispatch_rejected_for_other_table", cases(multipleOther).isEmpty() && set(multipleOther, "unknownTargets").contains(target));
|
||||
}
|
||||
|
||||
@Override
|
||||
public void run() throws Exception {
|
||||
String[] args = getScriptArgs();
|
||||
if (args.length != 1) throw new IllegalArgumentException("Expected exact ReaGhidraBridge.java source path");
|
||||
File expected = new File(args[0]).getCanonicalFile();
|
||||
ResourceFile source = GhidraScriptUtil.findScriptByName("ReaGhidraBridge.java");
|
||||
if (source == null) throw new IllegalStateException("ReaGhidraBridge.java is absent from scriptPath");
|
||||
File actual = new File(source.getAbsolutePath()).getCanonicalFile();
|
||||
if (!expected.equals(actual)) throw new IllegalStateException("Bridge source mismatch: expected " + expected + ", resolved " + actual);
|
||||
GhidraScriptProvider provider = GhidraScriptUtil.getProvider(source);
|
||||
if (provider == null) throw new IllegalStateException("No official script provider for " + source);
|
||||
bridge = provider.getScriptInstance(source, errorWriter);
|
||||
if (bridge == null) throw new IllegalStateException("Official provider returned no bridge instance");
|
||||
bridge.set(getState(), getControls());
|
||||
typedCases = bridge.getClass().getDeclaredMethod("typedJumpTableCases", JumpTable.class, List.class);
|
||||
typedCases.setAccessible(true);
|
||||
exactValue = bridge.getClass().getDeclaredMethod("exactTypedCaseValue", ClangCaseToken.class);
|
||||
exactValue.setAccessible(true);
|
||||
numericChecks();
|
||||
graphChecks();
|
||||
JsonObject report = new JsonObject();
|
||||
report.addProperty("schema_version", 1);
|
||||
report.addProperty("status", "passed");
|
||||
report.addProperty("ghidra_version", Application.getApplicationVersion());
|
||||
report.addProperty("bridge_source_path", actual.toString());
|
||||
report.addProperty("bridge_source_sha256", HexFormat.of().formatHex(MessageDigest.getInstance("SHA-256").digest(Files.readAllBytes(actual.toPath()))));
|
||||
report.addProperty("check_count", checks.size());
|
||||
report.add("checks", checks);
|
||||
report.addProperty("scope", "production private methods on detached Ghidra model objects; no bridge run or imported-program mutation; reflection depends on pinned model internals");
|
||||
println("REA_SWITCH_EVIDENCE_PROBE_JSON " + report);
|
||||
println("REA_SWITCH_EVIDENCE_PROBE_COMPLETE");
|
||||
}
|
||||
}
|
||||
@@ -0,0 +1,235 @@
|
||||
import assert from "node:assert/strict";
|
||||
|
||||
/** Source-owned case/target labels; no REA or Ghidra result defines this oracle. */
|
||||
export const SWITCH_FIXTURES = [
|
||||
{
|
||||
name: "dense",
|
||||
groups: [[0], [1], [2], [3], [4], [5], [6], [7]],
|
||||
table: true,
|
||||
},
|
||||
{
|
||||
name: "holes_shared",
|
||||
groups: [[0], [2, 3], [5], [6, 7], [9]],
|
||||
table: true,
|
||||
},
|
||||
{
|
||||
name: "nonzero",
|
||||
groups: [[11], [12], [13], [14], [15], [16], [17], [18]],
|
||||
table: true,
|
||||
},
|
||||
{
|
||||
name: "negative",
|
||||
groups: [[-7], [-6], [-5], [-4], [-3], [-2], [-1], [0]],
|
||||
table: true,
|
||||
},
|
||||
{ name: "comparison", groups: [[-1000], [17], [100000]], table: false },
|
||||
{
|
||||
name: "unsafe_integer",
|
||||
groups: Array.from({ length: 8 }, (_, index) => [
|
||||
(9007199254740993n + BigInt(index)).toString(),
|
||||
]),
|
||||
table: true,
|
||||
unsafe_integer: true,
|
||||
selector_type: "unsigned long long",
|
||||
},
|
||||
];
|
||||
|
||||
/** Emit native GCC/Clang C switches whose first case instruction has a public label. */
|
||||
export function buildSwitchSource() {
|
||||
const functions = SWITCH_FIXTURES.map((fixture, fixtureIndex) => {
|
||||
const blocks = fixture.groups.map((cases, groupIndex) => {
|
||||
const marker = 0x3100 + fixtureIndex * 0x100 + groupIndex;
|
||||
return `${cases.map((value) => `case ${value}${fixture.unsafe_integer ? "ULL" : ""}:`).join("\n")}\n${block(fixture.name, `case_${groupIndex}`, marker)}`;
|
||||
});
|
||||
blocks.push(
|
||||
`default:\n${block(fixture.name, "default", 0x3900 + fixtureIndex)}`,
|
||||
);
|
||||
return `__attribute__((noinline, used)) int rea_switch_${fixture.name}(${fixture.selector_type ?? "int"} selector) {\nswitch (selector) {\n${blocks.join("\n")}\n}\n}`;
|
||||
});
|
||||
// Constant calls preserve every function without executing imported targets in REA.
|
||||
return `${functions.join("\n\n")}\nint main(int argc, char **argv) { (void)argv; return ${SWITCH_FIXTURES.map(({ name }) => `rea_switch_${name}(argc)`).join(" ^ ")}; }\n`;
|
||||
}
|
||||
|
||||
function block(name, suffix, marker) {
|
||||
return `{ int result; __asm__ volatile (".globl rea_oracle_${name}_${suffix}\\nrea_oracle_${name}_${suffix}:\\nmovl $${marker}, %%eax" : "=a"(result)); return result; }`;
|
||||
}
|
||||
|
||||
/** Match nm's independent pre-strip symbols to public source labels. */
|
||||
export function switchSymbolOracle(nmOutput) {
|
||||
const symbols = new Map();
|
||||
for (const line of nmOutput.split("\n")) {
|
||||
const match = /^([0-9a-fA-F]+) [A-Za-z] (\S+)$/u.exec(line.trim());
|
||||
if (match)
|
||||
symbols.set(match[2], `0x${BigInt(`0x${match[1]}`).toString(16)}`);
|
||||
}
|
||||
return SWITCH_FIXTURES.map((fixture, fixtureIndex) => {
|
||||
const get = (symbol) => {
|
||||
const address = symbols.get(symbol);
|
||||
assert.ok(
|
||||
address,
|
||||
`Compiler omitted independent oracle symbol ${symbol}`,
|
||||
);
|
||||
return address;
|
||||
};
|
||||
const blocks = fixture.groups.map((values, groupIndex) => ({
|
||||
values,
|
||||
address: get(`rea_oracle_${fixture.name}_case_${groupIndex}`),
|
||||
marker: 0x3100 + fixtureIndex * 0x100 + groupIndex,
|
||||
}));
|
||||
return {
|
||||
...fixture,
|
||||
address: get(`rea_switch_${fixture.name}`),
|
||||
blocks,
|
||||
default_address: get(`rea_oracle_${fixture.name}_default`),
|
||||
default_marker: 0x3900 + fixtureIndex,
|
||||
};
|
||||
});
|
||||
}
|
||||
|
||||
/** Translate a public virtual address through ELF64 little-endian section headers. */
|
||||
export function elfBytesAt(bytes, address, length) {
|
||||
assert.equal(bytes.subarray(0, 6).toString("hex"), "7f454c460201");
|
||||
const table = Number(bytes.readBigUInt64LE(40));
|
||||
const entrySize = bytes.readUInt16LE(58);
|
||||
const count = bytes.readUInt16LE(60);
|
||||
const offset = BigInt(address);
|
||||
for (let index = 0; index < count; index++) {
|
||||
const entry = table + index * entrySize;
|
||||
if (bytes.readUInt32LE(entry + 4) === 8) continue; // NOBITS has no file bytes.
|
||||
const base = bytes.readBigUInt64LE(entry + 16);
|
||||
const size = bytes.readBigUInt64LE(entry + 32);
|
||||
if (offset < base || offset + BigInt(length) > base + size) continue;
|
||||
const fileOffset = Number(
|
||||
bytes.readBigUInt64LE(entry + 24) + offset - base,
|
||||
);
|
||||
assert.ok(fileOffset + length <= bytes.length);
|
||||
return bytes.subarray(fileOffset, fileOffset + length);
|
||||
}
|
||||
throw new Error(`Oracle address ${address} has no file-backed ELF section`);
|
||||
}
|
||||
|
||||
/** First-block instruction identity, independent of decompiler labels or table order. */
|
||||
export function markerBytes(marker) {
|
||||
const bytes = Buffer.alloc(5);
|
||||
bytes[0] = 0xb8; // mov imm32,%eax
|
||||
bytes.writeUInt32LE(marker, 1);
|
||||
return bytes;
|
||||
}
|
||||
|
||||
/** Verify each case/default label begins at the expected machine instruction. */
|
||||
export function assertSwitchMarkerBytes(bytes, fixtures) {
|
||||
for (const fixture of fixtures) {
|
||||
for (const block of fixture.blocks)
|
||||
assert.deepEqual(
|
||||
elfBytesAt(bytes, block.address, 5),
|
||||
markerBytes(block.marker),
|
||||
);
|
||||
assert.deepEqual(
|
||||
elfBytesAt(bytes, fixture.default_address, 5),
|
||||
markerBytes(fixture.default_marker),
|
||||
);
|
||||
}
|
||||
}
|
||||
|
||||
/** Check actual compiler jump-table slots/default guard against the source labels. */
|
||||
export function assertCompiledSwitchOracle(bytes, fixtures, disassembly) {
|
||||
assertSwitchMarkerBytes(bytes, fixtures);
|
||||
return fixtures.map((fixture) => {
|
||||
const start = disassembly.indexOf(`<rea_switch_${fixture.name}>:`);
|
||||
assert.ok(start >= 0, `objdump omitted ${fixture.name}`);
|
||||
const nextFunction = disassembly
|
||||
.slice(start + 1)
|
||||
.search(/<rea_switch_[a-z_]+>:/u);
|
||||
const code =
|
||||
nextFunction < 0
|
||||
? disassembly.slice(start)
|
||||
: disassembly.slice(start, start + 1 + nextFunction);
|
||||
const jumps = [
|
||||
...code.matchAll(
|
||||
/^\s*([0-9a-f]+):\s*((?:[0-9a-f]{2}\s+)+)jmp\s+\*0x([0-9a-f]+)\(,%r[a-z0-9]+,8\)/gmu,
|
||||
),
|
||||
];
|
||||
if (!fixture.table) {
|
||||
assert.equal(
|
||||
jumps.length,
|
||||
0,
|
||||
"Comparison control unexpectedly became a table",
|
||||
);
|
||||
assert.ok(
|
||||
!/jmp\s+\*/u.test(code),
|
||||
"Comparison control gained another indirect jump",
|
||||
);
|
||||
return {
|
||||
...fixture,
|
||||
dispatch_address: null,
|
||||
table_address: null,
|
||||
slots: [],
|
||||
};
|
||||
}
|
||||
assert.equal(
|
||||
jumps.length,
|
||||
1,
|
||||
`Compiler no longer emits one absolute 8-byte table for ${fixture.name}`,
|
||||
);
|
||||
const dispatchAddress = `0x${jumps[0][1]}`;
|
||||
const instructionBytes = Buffer.from(
|
||||
jumps[0][2].replace(/\s/gu, ""),
|
||||
"hex",
|
||||
);
|
||||
assert.deepEqual(
|
||||
elfBytesAt(bytes, dispatchAddress, instructionBytes.length),
|
||||
instructionBytes,
|
||||
"Compiler dispatch instruction bytes changed",
|
||||
);
|
||||
const tableAddress = `0x${jumps[0][3]}`;
|
||||
if (fixture.name === "negative")
|
||||
assert.equal(
|
||||
elfBytesAt(bytes, fixture.address, 6).toString("hex"),
|
||||
"83c70783ff07",
|
||||
"Negative fixture no longer uses 32-bit ADD EDI,7 / CMP EDI,7",
|
||||
);
|
||||
const values = fixture.groups.flat().map((value) => BigInt(value));
|
||||
const first = values.reduce((a, b) => (a < b ? a : b));
|
||||
const last = values.reduce((a, b) => (a > b ? a : b));
|
||||
const table = elfBytesAt(
|
||||
bytes,
|
||||
tableAddress,
|
||||
Number(last - first + 1n) * 8,
|
||||
);
|
||||
const slots = [];
|
||||
for (let value = first; value <= last; value += 1n) {
|
||||
const target = `0x${table.readBigUInt64LE(Number(value - first) * 8).toString(16)}`;
|
||||
const block = fixture.blocks.find((candidate) =>
|
||||
candidate.values.some(
|
||||
(candidateValue) => BigInt(candidateValue) === value,
|
||||
),
|
||||
);
|
||||
assert.equal(
|
||||
target,
|
||||
block?.address ?? fixture.default_address,
|
||||
`Compiler table slot ${fixture.name}:${value} does not enter the exact source block label`,
|
||||
);
|
||||
slots.push({
|
||||
value: fixture.unsafe_integer ? value.toString() : Number(value),
|
||||
target_address: target,
|
||||
explicit_case: block !== undefined,
|
||||
});
|
||||
}
|
||||
const defaultGuard = [...code.matchAll(/\bja\s+([0-9a-f]+)\s/gu)];
|
||||
assert.ok(
|
||||
defaultGuard.some(
|
||||
(match) =>
|
||||
`0x${BigInt(`0x${match[1]}`).toString(16)}` ===
|
||||
fixture.default_address,
|
||||
),
|
||||
`No independent bounds branch enters exact default block ${fixture.name}`,
|
||||
);
|
||||
return {
|
||||
...fixture,
|
||||
dispatch_address: dispatchAddress,
|
||||
discriminator_size_bytes: fixture.name === "negative" ? 4 : null,
|
||||
table_address: tableAddress,
|
||||
slots,
|
||||
};
|
||||
});
|
||||
}
|
||||
Reference in New Issue
Block a user