scientific-method-engine

Bounded instruction-derived x86 evidence reports for segmented 16-bit MZ/FBOV code and PE32/i386 code. The engine decodes instructions with Capstone, takes their values, flags and branch conditions from Ghidra's SLEIGH specification through pypcode, follows bounded paths and emits bounded-x86-v1 JSON. It never runs the original program. It needs Python 3.12 or later.

uv add --group research scientific-method-engine     # or: pip install scientific-method-engine

For original MZ/FBOV executables, run reports through @scientific-method/executable-reader. The reader derives relocation, fixup and trampoline data from the hash-checked source and pipes a prepared config to this engine. Running the engine directly trusts whatever relocation data the config supplies, so use it directly only for synthetic inputs, PE32 sources and checked mappings. A config file is read as the reader reads it: UTF-8, with or without one leading byte order mark, and a file starting with a UTF-16 or UTF-32 byte order mark or with more than one UTF-8 mark, or bytes that are not UTF-8, are refused with the cause named.

scientific-method-engine trace analysis/query.json
python -m scientific_method_engine trace analysis/query.json

The package also carries the shared Ghidra headless scripts. scientific-method-engine ghidra-scripts prints their directory, for Ghidra's -scriptPath:

& "$env:GHIDRA_HOME/support/analyzeHeadless.bat" $project $name -process GAME.EXE -noanalysis `
  -scriptPath (scientific-method-engine ghidra-scripts) -postScript ReportReferences.java 0x1234

Addresses are Ghidra addresses (0x00401000, or 1028:d820 for segmented programs). Report scripts print to the analyzer log and cap their output. ReportScalarConstants, ReportCallsToRange, ReportConstantFirstArgumentCalls and ReportCallSitesWithScalars say when a cap stopped their scan, and ReportRangeBoundaries says when it stopped printing, with counts that still cover every range it read; for the other report scripts, a result count equal to the cap means the same. analyzeHeadless can exit with code 0 after a script failed to load, so check the log for the script's own result lines (the Ghidra workflow says what a run must show). The scripts compile against Ghidra 12.1. ReportConstantFirstArgumentCalls, ReportFirstArgumentCallSummary, ReportCallSitesWithScalars, ReportScalarConstants, ReportFunctionScalarConstants, ReportInstructionWindow, ExportBoundedFlow and ExportFunctionInventory load shared helpers from the scientificmethod/ directory beside them, so pass the directory the command prints as -scriptPath, or copy that subdirectory along with the scripts.

Reading code and data:

Finding references and calls:

Exporting for comparison (each writes one file and refuses to overwrite where noted):

Repairing the analysis (these change the Ghidra program, so run them before reports and keep the argument lists with the evidence that justifies them):

Restoration tools that build report configs can import the parsers directly, for example to derive a PE32 source's executable sections:

from scientific_method_engine.x86.pe import pe32

sections = [s for s in pe32(data)["sections"] if s["executable"]]

scientific_method_engine.x86.pe.pe32 and scientific_method_engine.x86.image.read_source are supported imports and change only in a major release. Other modules are internal.

Commands, inputs, limits and acceptance rules are in the bounded evidence reporter guide. The reader and engine check that they speak the same prepared-config protocol and refuse to run otherwise.

The effects command additionally emits path-local effectOrdering timelines, pre-call write prefixes and bounded local restoration witnesses. Unknown modeled or nested service effects stay separate; no return code establishes rollback or transactionality. See the full contract.

Each traced path carries a loops record: the restart edges the path took and, between consecutive arrivals at a loop head, which registers, flags and written bytes changed, the signedness and operands of each gate, and whether the state repeats an earlier arrival. It never reports that a loop terminates or that a retry succeeded. loopIterationLimit caps the records. See loop progress.

Evidenced segmented16 indirectJumps declarations also expose separate declaredContinuationPaths. Ordinary paths retain their unresolved transfer; conditional routes preserve prefix/child effects with target-choice, live-table and selector assumptions. Effects summaries never mark those routes complete. Concrete values/field addresses reject inconsistent rows. Continuations run after every ordinary path on their own continuationBudget (paths, total and per-path steps, visits, string iterations), so ordinary paths are the same with or without them. Overlap, boundary and continuation limits remain explicit gaps or stops. Partial-table splits are partial evidence, never complete dispatch or native-reachability claims. See the table contract.

A far call or jump through an m16:16 pointer is followed when the path stored both words and the address names declared code through one region's exact mapping, or names a source FBOV trampoline whose overlay entry is declared. The event keeps the pointer read, each word's producers and writers, and how the target was admitted. An unknown or partly unknown word, an address outside declared code, a segment alias of resident code, an overlay's analysis segment and an m16:32 pointer stop the path with a named reason. See indirect far transfers.

A call model may also sit at an INT n instruction in the real-mode model. The interrupt is still reported as a hardware boundary with its vector, the handler is not executed, and each case returns to the next instruction with SP and CS as before the interrupt. Registers, flags and memory the model does not preserve or set are unknown. leavesFlags: true describes a service that returns with a far return and leaves the interrupt's FLAGS word on the stack. Without a model, and at INT1, INT3 (in either encoding), INTO or any PE32 interrupt, the path stops at the interrupt as before. See ADR 0017.

A call model may declare preservesMemory: up to 32 scopes (4,096 bytes in total), each naming a segment register, an address-width base register, an optional displacement, a byte count and the evidence for assuming the service leaves those bytes alone. Scopes resolve against the pre-call registers. The base may be symbolic, such as BP in an entryFrame query, and then keeps the bytes at those offsets from its value. An unknown segment, a concrete interval that crosses the end of the address space, or two scopes that may share a byte stop the path. Only the scoped bytes survive the model's memory invalidation, and each scope is reported with the model, the modeled return and the effect summary. Everything else the service may do stays unknown. This input needs prepared protocol 3, so upgrade the reader and the engine together. See the call model contract.

The trace-family commands (trace, arguments, effects, returns, guards, memory, allocation) check relationalControls: assertions over reported values (reach, order, last writer, containment, value relation and value origin) evaluated on every bounded path. A violated control fails the report. A control left undecided by a stop, a limit or an unread call is reported as undecided and never counts as held. Access reports also give each byte's writeOrder, or why it has no modeled value. A last-writer control with an address asks the same of memory the program never reads back, at a checkpoint. See the controls contract.

Two reads of a byte the model holds no value for read one term until a write that may store it or a modeled call, which assumes nothing else changes memory. A query whose program polls memory that hardware, DMA or an interrupt handler updates lists those addresses in volatileMemory: up to 64 rows of segment (a real-mode paragraph, or 0 in the PE32 flat model), offset, bytes and evidence. Each read of a byte inside a declared range reads its own term, ignoring any value the path stored, and its byteProducers row gives cause declared volatile with the read's order and the declared row's index in volatileMemory. A read whose address is not concrete but may name a declared byte keeps its term and carries mayBeVolatile: true. See the memory model.

A trace-family query whose entry lies inside a function body names the function's entry in entryFrame: { "from": <site> }. The engine traces from there to the query's entry and, when SP sits at one offset from the function's entry SP at every arrival, starts the query in that frame, so the function's return balances and its paths can be read to the end. The report's entryFrame gives the offsets, or the reasons the frame is not established, in which case the query runs as it would without the input. See the narrower entry contract.

Each return event carries returnCheck: the frame's and the instruction's return widths, SP's offset from the frame's entry SP, and whether the return words were read and compared with the call. A width mismatch and an unbalanced stack stop the path with separate reasons. A root return never reads its return words, so returned: true on a root path says nothing about them. See the command overview.

A traced callee that rebuilds its return frame at the other width (pop ax; push cs; push ax; retf over a near call, or a near return over a far frame it shortened) returns to its caller when the return's words end where the call's frame ended (returnCheck.endsAtFrameEnd), the offset word is the call's return IP, and the segment, popped or kept in CS, is the call's CS. Any other conversion stops with the reason of the check it failed. See converted call frames.