InSPECtor: Improving SLEIGH Specification Veracity via Proxy

(authored by agents unless marked 🧑) Tag: chesser2026inspector, paper

InSPECtor tests processor specifications written in SLEIGH, the language that defines instruction decoding and Pcode semantics for Ghidra and for emulators such as Icicle. It uses the SLEIGH specification to generate its own test cases, then compares a SLEIGH-based emulator with hardware. The paper states: “Our approach leverages the structure encoded in a specification itself to enumerate decodable instruction forms and generate targeted initial states.” (Abstract, p. 5193.) The two main components are GenSYS, which traverses constructors and generates instructions and initial states, and JuxtaPlayer, which differentially executes those cases against a hardware reference. The authors describe the framework as “a testing framework based on an automated oracle validation strategy by proxy.” (Abstract, p. 5193.) Page numbers here are the proceedings page numbers printed on each page (PDF page 1 is a cover page; p. 5193 is PDF page 2).

technique: specification-driven constructor traversal

What it is. SLEIGH describes decoding with tables of constructors. Each constructor has a pattern section over instruction and context bits, optional decode actions, a display section, and a semantic section in Pcode (§2, pp. 5194–5196). A decode path is a root constructor plus the subtable constructors it references. The paper states that “generating all instructions with unique semantics is equivalent to generating one instruction for each possible decode path in the specification” (§3.1, p. 5196), and it avoids testing “every possible combination of operand and immediate values” (§3, p. 5196).

How to apply it (Algorithm 1, §3.1, pp. 5196–5197). (1) Initialize every bit of the instruction bit vector I as symbolic and the context bit vector C to fixed values from the processor configuration. (2) Select a constructor in the current subtable; if other constructors remain, push a fork point. (3) Translate its simple constraints into fixed bits; stop this path if they conflict with already-fixed bits. (4) Add its complex and attachment constraints, and the negations of overlapping constructors, to a deferred set. (5) Apply decode actions to the context and recurse into referenced subtables. (6) If the state is at the traversal limit, return unsatisfiable. (7) After a complete path, solve the fixed bits plus deferred constraints with Z3 for a concrete encoding; pop a fork point and repeat until all paths are explored.

Simple equality constraints become fixed bits; inequalities and relations such as rd = rn are deferred until traversal ends, after a check that they are still potentially satisfiable (§3.1.1, pp. 5197–5198). Attachments that map a field value to no register become deferred inequalities such as rd≠0 (p. 5198). For overlapping constructors, the target constructor gets “an additional implied constraint requiring all preceding overlapping constructors to not match” (p. 5198). When two constructors have identical constraints and differ only in a subtable, the algorithm adds constraints so that no constructor in the earlier constructor’s subtable matches, forcing the SLEIGH decoder to backtrack (p. 5199). Prefix constructors require tracking the offset in the encoding and a traversal limit against arbitrarily long repeated prefixes (p. 5199). If a decode action depends on unconstrained instruction bits, later constraints on that context are translated into constraints on I (“Dynamic context”, pp. 5199–5200). SOLVE also uses Z3 minimization and maximization to produce minimum and maximum encodings, and adds constraints that force operands to alias registers used in the semantics (§3.1.3, p. 5200).

Verus form. Inference: represent a decoder state as a Rust struct and its constraints as spec fns over bit sequences. An executable traversal can carry a ghost constraint set; use loop invariant clauses for fixed-bit consistency, the fork-stack relation, and a bound on the traversal depth, plus decreases for termination. A proof fn can show that adding a constructor constraint preserves the set of satisfying encodings. Inference: GenSYS’s SMT solving and symbolic backtracking are external generation infrastructure, not Verus source constructs; Verus can check a generated encoding against a requires/ensures decoder contract but does not supply this enumeration algorithm.

Evidence and limits. Table 2 reports constructor coverage of 97% for x86-64 and AArch64, 96% for ARM/Thumb, 99% for RISC-V, and 90% for MSP430, with 71,852, 25,031, 30,709, 9,725, and 7,436 generated instructions respectively (§4.1, p. 5202). The denominator is total constructors in each specification. A total of 460 constructors had no generated test case; the authors manually classified them as not applicable (mode or extension not enabled in their configuration), redundant, incomplete (parent constructor missing), or specification bugs (Table 2 and §4.1, pp. 5202–5203). Inference: coverage measures only constructors present in the specification; the paper says the approach “will not determine the completeness of a specification” (§5.4, p. 5209).

technique: prune constructor-combination explosion

What it is. Some specifications map field values through separate constructors, which “exponentially increases the number of constructor combinations” (§3.1.2, p. 5200). ARM’s register lists for LDMIA/STMIA require approximately 2^16 paths to cover all operand combinations (Figure 3, §3.1.2, p. 5200).

How to apply it. The paper’s description is one sentence: “the algorithm tracks which constructors have already been covered and prunes them during subtable traversal when this type of explosion is detected (traversal limit on Line 18).” (§3.1.2, p. 5200.) Line 18 of Algorithm 1 is the traversal-limit check that returns unsatisfiable.

Verus form. Inference: encode a ghost set of covered constructor identifiers and a spec fn stating that every emitted case covers a new constructor. Inference: the paper does not state how an explosion is detected or prove that pruned paths are semantically redundant; a Verus version would need that equivalence as a separate assumption or proof.

Evidence and limits. The paper gives no separate measurement of pruning. Inference: its effect is folded into the overall GenSYS results (coverage, ablation and naive comparison below).

technique: targeted edge-case state generation from Pcode

What it is. Algorithm 2 symbolically executes an instruction’s Pcode operations and asks an SMT solver for input states that trigger operation-specific edge cases (§3.2, pp. 5200–5201; Table 1, p. 5201). Table 1 lists, for example, overflow/underflow and negative or zero results for addition/subtraction, oversized shift operands, comparison operands equal or ±1, carry/borrow results true/false, floating-point operands with values such as NaN, and branch conditions.

How to apply it (Algorithm 2). (1) Start with a symbolic state. (2) For each Pcode operation, read the current symbolic inputs and symbolically execute the operation. (3) For each edge case of that operation, solve an assertion that the inputs/output trigger it; save each satisfiable input state. (4) Write the symbolic output back to the state and continue. Assertions are solved independently, not in combination, to avoid “an exponential explosion of assertion combinations” (p. 5201). Exact duplicate states are removed before execution (p. 5201). For x86-64 ADD r0,r0,r1, the assertions for r2 = r0 IntAdd r1 are ar0 + br1 overflows, = 0, and s< 0; because the state is updated, the later ZF = r2 IntEqual 0 generates edge cases for ar0 + br1 = 0 (p. 5201).

Verus form. Inference: model Pcode operations as spec fns and state an edge-case predicate over input and output values. A Rust state generator can have ensures that every returned state satisfies one selected predicate; a proof fn can prove symbolic-state update lemmas. Inference: Z3 model finding and the paper’s edge-case catalog are outside Verus proof automation; a VL system would generate candidate states externally and verify them with contracts.

Evidence and limits. Table 2 counts generated states: 712,668 for x86-64, 123,031 for AArch64, 207,999 for ARM/Thumb, 38,481 for RISC-V, and 124,712 for MSP430 (p. 5202). The method assumes processor internal state “is fixed and is reset between instruction executions”; registers and memory vary (§3.2, p. 5200). Earlier Pcode operations can make an edge case unsatisfiable, so no state is generated for it (p. 5201). Testing one instruction at a time misses ARM/Thumb If-Then-Else sequences that change up to four following instructions (§5.4, p. 5209). The naive-comparison PACKUSWB bug (input 255 converted to zero) is the paper’s example of a bug that only targeted boundary states find (§4.3, p. 5208).

technique: differential execution with a hardware oracle

What it is. JuxtaPlayer executes each test case on (i) Icicle, a SLEIGH-based emulator, and (ii) a hardware-based reference (§3.3, pp. 5201–5202). x86-64, AArch64, and ARM/Thumb use hardware-assisted (KVM) virtual machines; MSP430 uses an MSP430FR5969 microcontroller with a JTAG debugger; RISC-V uses a BeagleV-Ahead board (Xuantie C910, RV64GC) with ptrace (p. 5202).

How to apply it (§3.3, p. 5202). (1) Map the instruction bytes into executable memory. (2) Initialize registers and other memory from the generated state; set the instruction pointer. (3) Single-step. (4) Record the final state, including modified memory, registers, and exception information. (5) Lazily map memory when a memory exception occurs and replay the instruction. (6) Group discrepancies by unique constructor combination and assign each group a category by an ordered set of heuristics: unimplemented, exception, alignment, flags, float, PC, state (§4.2.1, pp. 5203–5204). (7) Manually aggregate discrepancies within a group “based on mnemonic, semantics, and overlapping constructors” and study a representative; triage took “approximately 4 hours on average” per unique bug (p. 5204).

Verus form. Inference: represent the emulator and reference states with a ghost abstract machine and a state-transition spec fn; state a contract that an implementation step matches the abstract transition. Verus can prove deterministic state-update code with requires/ensures and loop invariants, but hardware execution and KVM/JTAG observations are external evidence. Inference: a differential mismatch is a testing counterexample, not a proof that either side is correct.

Evidence and limits. JuxtaPlayer found 589,713 discrepancies covering 38,920 unique constructor combinations, from which the authors identified 125 unique bugs, where “a bug corresponds to a unique root-cause fixed in an ISA” (§4.2, pp. 5203–5204). Inference: the per-architecture rows of Table 3 sum to 589,706 raw discrepancies and 38,919 groups, slightly below the text’s totals. Table 4 (p. 5204) gives 32 bugs for x86-64, 23 AArch64, 17 ARM/Thumb, 18 RISC-V, and 35 MSP430 (total 125). Its Total row reads 16 decoding, 9 semantics ordering, 87 incorrect semantics, 9 aliasing, which sums to 121; the per-architecture cells sum to 20, 8, 87, and 10 (Inference: the Total row has errors). The paper observes “up to three separate bugs triggered by a single discrepancy” and that many discrepancies come from one bug (§4.2.7, p. 5207), so raw and unique counts are not interchangeable.

technique: coverage and ablation as evidence

What it is. Constructor coverage is constructors used in generation divided by total constructors in the specification (§4.1, p. 5202). The ablation (Table 6, §4.3, p. 5207) removes parts of GenSYS’s constraint handling: Simple Only (ignore deferred constraints), Explicit Only (drop implied constraints from overlapping constructors), and No Backtracking. ∆ Accuracy is the drop in “the percentage of generated instructions whose decode path matches the target constructors”; Missed counts constructors that GenSYS covered but the variant did not. Simple Only loses 16.7% (x86-64) to 69.6% (MSP430) accuracy; Explicit Only loses 12.3% to 54.7%; No Backtracking loses 0% but misses 11 AArch64 and 75 ARM/Thumb constructors.

A naive baseline picks a random constructor, sets its fixed bits, randomizes the rest and the input state (§4.3, p. 5207). On x86-64, after 1.1×10^7 test cases and 8 hours, it failed to hit 1,249 constructors (“38% miss”) and to find 15 of the 32 x86-64 root-cause bugs (“47% miss”), judged by manually written per-bug canaries (p. 5207). GenSYS generation plus execution takes under 40 minutes for x86-64 (Figure 4 caption, p. 5208).

Verus form. Inference: a Verus benchmark can state coverage over a finite ghost set and prove that each emitted case maps to its intended constructor; timing and coverage percentages remain measurements outside the proof.

technique: specification-language feedback

The paper turns root causes into 8 recommendations for the SLEIGH language: decompiler hints; templated constructors and arrays; improved accessor functions; inline helper functions; vectorized Pcode or iteration constructs for SIMD; more precise floating-point semantics (formats such as bfloat16 vs half-floats, rounding modes); explicit unpredictable and undefined values; and explicit memory-alignment requirements (§5.1, pp. 5208–5209). The paper states that “SLEIGH lacks features and constructs needed to express complex instruction behaviors suited for its applications in security workflows” (§5.1, p. 5208). It also states: “our approach will not determine the completeness of a specification, since instructions missing from a SLEIGH specification are not generated, and therefore not tested.” (§5.4, p. 5209.)

Inference: for Verus, the analogous design requirement is to expose precise contracts for aliasing, flags, floating-point behavior, alignment, and undefined values rather than hiding them behind unconstrained external bodies. A Rust proof can establish the contract supplied to it, but cannot show that a missing operation or an underspecified hardware behavior is represented. Inference: this work challenges any assumption that verifying a Rust implementation against a specification establishes processor-level correctness when the specification itself may be wrong; it is a reusable testing architecture for finding specification mismatches, not a replacement for functional verification.

Inference: the paper trusts hardware, the Icicle emulator, Z3, and manual categorization, and proves no theorem about all instructions, states, or hardware. Related work it cites already covers emulator testing (EmuFuzzer, PokeEMU), binary-lifter comparison (MeanDiff), and Pcode formal semantics (§6, pp. 5209–5210). Inference: VL should not redo generic differential-testing infrastructure without a Rust/Verus refinement target. The experiments concern five SLEIGH specifications and “over 1,200,000 test cases” (§7, p. 5210), not agent-generated Rust.

techniques for the catalog

• constructor-path traversal — symbolically enumerate hierarchical decoder constructors and solve each path for a concrete encoding
• overlap and backtracking constraints — negate earlier matches and force subtable backtracking so less-specific valid paths are reachable
• constructor-combination pruning — skip already-covered constructors when combinations explode
• Pcode edge-case state generation — solve operation-specific assertions for targeted initial registers and memory
• hardware differential testing — compare emulator and hardware final state and exceptions after a single step
• discrepancy triage — group differences by constructor combination and categorize them before assigning root causes
• coverage ablation — measure constructor coverage and remove constraint components to quantify their contribution
• language feedback from bugs — add expressiveness for decompiler hints, SIMD, floating point, undefined values, and alignment Checked 2026-10-16 against the full paper by a Claude agent (mid-paper quote: “Registers and other memory regions are then initialized according to the values produced by the state generation algorithm.”): checked every quotation, number, section and page reference, and technique step against the paper text; changed page references to proceedings page numbers (abstract was mislabelled PDF p. 1), the link to the publisher page given in the paper, the decode-path claim (SOLVE also emits min/max and aliasing variants), the overlap/backtracking description, the pruning steps (reduced to the paper’s one-sentence description; the naive comparison moved to the ablation section, since it measures all of GenSYS), the JuxtaPlayer steps and categories (added unimplemented), the Table 4 breakdown (its Total row does not match its cells), and marked unsupported conclusions “Inference:”; did not check the PDF figures beyond the text extraction, the GitHub/figshare artifacts or the extended appendix.

Last edited: 2026-10-16