The Model Behind the Disassembly
The subject of this series is the correctness of SLEIGH processor specifications, especially the open-source specifications used by Ghidra and related analysis tools. The focus is a dependency that is easy to overlook: before a reverse engineer can interpret a disassembly, some specification has already decided what the bytes mean and how the instruction behaves. This chapter establishes why that hidden model matters and introduces the question that governs the rest of the discussion: what evidence is strong enough to trust a processor specification?
A useful answer cannot stop at “the tool produced readable assembly.” It must connect three things: whether the specification recognizes the right instruction forms, whether its semantic model matches execution, and which parts of the processor remain outside the test. InSPECtor, the study at the center of this series, makes that connection by exploring SLEIGH’s own decoding structure and comparing a SLEIGH-derived emulator with hardware. Before examining how that works, it is necessary to see what SLEIGH sits between.
The layer we usually do not see
A processor executes bytes, not assembly language. A reverse-engineering tool starts with those bytes and must infer an instruction boundary, an operation, its operands, and the state changes that should follow. SLEIGH is the language Ghidra uses to describe that relationship for a processor. Its specifications are not simply glossaries that map an opcode to a mnemonic. They describe instruction encodings closely enough to produce structured disassembly, and they describe instruction behavior closely enough to support translation into p-code.
That second output is especially important. P-code is a machine-independent register-transfer language. It gives Ghidra a common representation for operations that originate in different instruction sets, so the same broad family of data-flow and decompilation machinery can work across processors. In a simplified view, SLEIGH supplies two linked answers to every recognized instruction: “What should an analyst read?” and “What does this instruction do to registers, memory, flags, and control flow?”
Those answers feed more than one user interface. Disassembly uses the first answer to name operations and operands. Decompilation uses the p-code answer to reason about values and reconstruct higher-level structure. A SLEIGH-based emulator can also execute the p-code representation. The specification therefore occupies a boundary between physical machine behavior and several software interpretations of that behavior. If the boundary is wrong, the outputs can remain polished while disagreeing with the processor they purport to describe.
The arrangement explains why the specification is a trust boundary rather than an implementation detail. The bytes enter at one side, but the analyst usually encounters an interpretation several steps later. A wrong instruction length may alter control-flow recovery. A wrong operand width may make a register value appear to have been preserved when the processor changed it. A missing side effect may cause a data-flow analysis to treat a value as stable when it is not. The errors are not necessarily visible in the surface form of the disassembly.
SLEIGH’s p-code model makes this dependency explicit. P-code operations name their inputs and, when they write data, their output. Address spaces can model memory and registers; varnodes identify contiguous data in those spaces; operations express arithmetic, comparisons, loads, stores, branches, and other effects. This explicitness is valuable because an analysis engine can inspect the modeled data flow. It is not a guarantee that the model is faithful. The specification author still has to encode the processor’s widths, flags, ordering rules, aliases, exceptions, and special cases correctly.
Why a small modeling error can become a security error
The danger is not limited to a spectacularly invalid instruction. Many failures are locally plausible. A constructor can recognize a byte pattern and produce a familiar mnemonic while selecting the wrong variant. A semantic section can implement the main arithmetic result but omit a flag or apply an update in the wrong order. An operation can use the right registers but the wrong width. Each mistake may look minor in isolation; downstream tools combine the result into larger judgments.
Consider the difference between decoding and semantics. A decoding error changes which instruction the tool believes it has encountered, or where the next instruction begins. That can affect disassembly and control-flow analysis directly. A semantic error is subtler: the displayed instruction may look right, yet the p-code says that the instruction reads or writes the wrong location, produces the wrong flag, or has a side effect that hardware does not have. Decompilation and emulation can then diverge even though a human scanning the mnemonic sees nothing unusual.
The InSPECtor paper places these risks in concrete security workflows: vulnerability discovery, malware analysis, fuzzing, firmware auditing, and program understanding. Those workflows often use a model indirectly. A practitioner may trust a recovered control-flow graph, a decompiler’s expression, or an emulator’s state transition without reopening every processor manual. That is a reasonable division of labor only if the model underneath has earned some assurance. Otherwise, a defect can obscure a vulnerability or produce an unsound conclusion without announcing itself as a failure.
The challenge is structural as well as human. Processor specifications are large, painstaking artifacts, and modern instruction sets keep changing. The paper notes that the ARM manual runs to roughly 12,000 pages and the 2025 Intel Software Developer’s Manual exceeds 5,000 pages. Those figures do not mean every specification author copies every page by hand, but they do convey the scale and variety of the source material being represented. Operand-dependent behavior, mode changes, prefixes, legacy compatibility, and new extensions create interactions that are difficult to validate by inspection alone.
SLEIGH’s compactness increases both its usefulness and its hidden coupling. A concise constructor can be reused across several decoding paths. A context bit can carry information from one stage of decoding into another. A p-code sequence can stand in for a hardware operation whose architectural effects depend on aliasing or a special register. These mechanisms reduce repetition and make a broad architecture describable, but an error in one shared rule can affect many generated instructions and many consumers of the specification.
This is why “the specification compiles” or “the disassembler works on ordinary binaries” is weak evidence. Compilation establishes that the description satisfies the language’s syntactic and internal consistency requirements. Ordinary binaries establish that some common paths work. Neither result compares the model with the processor across the unusual encodings and states where an incorrect assumption is most likely to surface. Correctness has to be tested at the boundary where the model makes claims about execution.
From trust to testability
InSPECtor’s contribution is to turn that broad concern into a specific validation arrangement. It does not begin by throwing arbitrary byte strings at an emulator and counting how many execute. It treats the SLEIGH specification as structured evidence about which instruction forms are intended to be decodable. The study’s generator, GenSYS, follows constructor paths and derives satisfying encodings from their constraints. It also examines the p-code semantics to produce initial states that can expose edge cases. The specification supplies the map; the solver helps choose meaningful points on that map.
The second part, JuxtaPlayer, compares execution of those cases in two settings. One side is an emulator derived from the SLEIGH specification. The other is a hardware-based reference, using controlled execution and state access appropriate to the tested architecture. The comparison records observable outcomes such as registers, memory, the program counter, and exceptions. This is the sense in which the emulator is an oracle “by proxy”: the emulator is the object whose specification is being assessed, while hardware provides the independent behavioral reference.
That arrangement also explains why the study has two distinct kinds of evidence. Reaching a constructor path says that the generator found an encoding the specification recognizes. Agreement with hardware says that, for the tested initial state and environment, the modeled execution matched the reference. Neither statement alone is enough. Structural coverage without behavioral comparison can repeatedly exercise a wrong model. Behavioral comparisons without systematic generation can miss rarely reachable constructors, prefixes, aliases, or boundary values.
The distinction matters on the other side of a mismatch too. A difference between emulator and hardware is an observation, not automatically a confirmed bug. It may come from incorrect decoding or semantics, but it may also reflect unimplemented behavior, architectural unpredictability, an unavailable ISA feature, or a limitation in what SLEIGH can express. The paper’s detailed analysis therefore separates raw discrepancies from grouped behaviors and from unique root causes. That restraint is part of the method, not a qualification added after the headline result.
The central lesson is consequently narrower and stronger than “reverse engineering tools can contain bugs.” SLEIGH processor specifications are executable claims about how machine code should be read and what it should do. Because those claims sit beneath multiple analysis paths, their correctness deserves direct evidence. InSPECtor provides one way to obtain that evidence by joining the specification’s structural reach with targeted execution against hardware. The next step is to examine the language model itself—constructors, context, tables, and p-code—because those are the mechanisms that determine what the specification is actually claiming.