InSPECtor: Improving SLEIGH Processor Specification Veracity via Proxy

InSPECtor: Improving SLEIGH Processor Specification Veracity via Proxy

Summary

This paper introduces InSPECtor, a framework for systematically validating SLEIGH processor specifications, which are used by tools like Ghidra for disassembly, decompilation, and emulation. The authors note that Processor specifications underpin critical security and program-analysis tools such as disassemblers, decompilers, and emulators, yet, their correctness is rarely examined. Errors in these specifications can distort program behaviour, obscure vulnerabilities, and enable analysis-evasion techniques.

The paper's main contributions are:

1. A methodology for symbolically traversing SLEIGH specification decoding rules to systematically generate instruction encodings and targeted initial states.

2. The design and implementation of the InSPECtor prototype, including GenSYS (a test case generation tool) and JuxtaPlayer (a differential testing environment).

3. An analysis of discovered bugs, their root causes, proposed fixes, and 8 recommendations for improving the SLEIGH DSL.

Methodology

The approach leverages the structure of SLEIGH specifications to enumerate decodable instruction forms. GenSYS traverses the specification's constructors to generate instructions with unique semantics, solving constraints with an SMT solver (Z3). It handles simple constraints, complex constraints, attachments, implied constraints from overlapping constructors, and decode actions (including phased decoding and prefix parsing). To avoid exponential explosion from complex operand combinations, it uses a traversal limit and prunes redundant paths.

For state generation, the algorithm identifies edge cases from Pcode operations (e.g., overflow, underflow, zero results, negative values, NaN) and uses symbolic execution to generate initial input states that trigger these edge cases.

JuxtaPlayer executes test cases on both a SLEIGH-based emulator (Icicle) and hardware reference systems (KVM-based VMs for x86-64, AArch64, ARM/Thumb; debuggers for MSP430 and RISC-V), then compares final states to identify discrepancies.

Evaluation

The framework was applied to five diverse specifications: x86-64, AArch64, ARM/Thumb, RISC-V, and MSP430. GenSYS generated over 1,208,531 test cases with constructor coverage ranging from 90% to 99%. The generation times varied from under a second to over 1,400 seconds.

JuxtaPlayer discovered 589,713 raw discrepancies, which were grouped into 38,920 unique constructor combinations. After manual triage, these led to 125 unique bugs with proposed fixes. The bugs were categorized as:

• Decoding issues (16 bugs): including redundant/out-of-order prefixes, context handling issues, overlapping constructors, over-constrained constructors, and constructor ordering.

• Semantics ordering issues (9 bugs): where correct outcomes depend on operation order (e.g., MSP430 addressing modes, AArch64 NGCS with zero register).

• Incorrect semantics (87 bugs): including missing floating-point semantics, incorrect default values, incorrect register lists, and subtle errors like using OR instead of XOR.

• Aliasing issues (9 bugs): where source and destination registers overlap, causing incorrect behavior.

The paper also identifies unresolvable issues that require SLEIGH language extensions, including unimplemented SIMD operations, floating-point limitations, unpredictable behavior, memory alignment exceptions, and missing instruction semantics.

Effectiveness

An ablation study showed that removing constraint translation components significantly reduces generation accuracy and causes many constructors to be missed. A comparison with a naive random approach on x86-64 showed that the naive method missed 38% of constructors and failed to find 47% of bugs.

Recommendations

The authors propose 8 recommendations for improving SLEIGH:

1. Provide decompiler hints to balance emulation fidelity and decompilation quality.

2. Design templated constructors and arrays to reduce code duplication.

3. Design accessor functions to manage export statement dependencies.

4. Move to inline helper functions for runtime selection of instruction fidelity.

5. Provide SIMD extensions (vectorized Pcode operations).

6. Provide floating-point operation descriptions and rounding modes.

7. Explicit unpredictable/undefined values.

8. Alignment requirements for memory operations.

Conclusion

The paper concludes that Improving the veracity of SLEIGH specifications enhances the reliability and confidence in downstream tools that depend on their correctness. The work represents a significant and sustained effort to improve SLEIGH specifications and introduces tools and a test strategy for automated correctness testing.

Improvements to AI Systems:

1. Automated Specification Debugging Agent

• Build an AI system that ingests SLEIGH (or similar DSL) specifications and automatically generates targeted test cases using symbolic traversal (as in GenSYS).

• The AI can detect bugs like incorrect operand ordering, aliasing, over-constrained constructors, and missing edge-case semantics (e.g., NaN, overflow) without manual triage.

• It can propose fixes by analyzing root causes (e.g., replacing OR with XOR, adding missing prefix handling) and even generate patches for the specification.

2. Differential Testing Orchestrator with Adaptive Bug Triage

• Create an AI that runs JuxtaPlayer-style differential testing across multiple hardware references (KVM, debuggers) and automatically clusters raw discrepancies into unique bug categories.

• Use machine learning (e.g., clustering on instruction encodings, Pcode sequences, and final-state differences) to reduce 589k raw discrepancies into actionable bug reports, prioritizing high-impact issues like incorrect semantics over benign aliasing.

3. SLEIGH DSL Extension Recommender

• Train a model on the 8 recommendations (e.g., SIMD extensions, floating-point rounding, explicit undefined values) to analyze any SLEIGH specification and suggest missing language features.

• The AI can predict which unresolved issues (e.g., unimplemented SIMD ops, alignment exceptions) will cause downstream tool failures, then auto-generate language-level proposals or workarounds.

4. Coverage-Aware Fuzzer for Processor Specs

• Enhance existing fuzzing with the paper’s constructor-coverage metrics (90–99%) to guide test generation.

• The AI can dynamically adjust traversal limits and prune redundant paths to avoid exponential explosion, focusing on uncovered constructors and complex constraints, improving bug discovery speed by orders of magnitude.

5. Semantic-Aware Emulator Corrector

• Use the discovered bug patterns (e.g., semantics ordering issues in MSP430 addressing modes, AArch64 NGCS with zero register) to train a neural network that predicts when a SLEIGH-based emulator (like Icicle) will diverge from real hardware.

• The AI can then automatically insert runtime checks or fallback to hardware for those specific instructions, improving emulation fidelity for security analysis tools.

6. Automated Pcode Edge-Case State Generator

• Build an AI that, given any Pcode operation, automatically generates initial CPU states (register values, memory contents) that trigger edge cases (overflow, underflow, zero, NaN, negative) using symbolic execution.

• This can be integrated into any emulator or decompiler to validate correctness under adversarial inputs, not just for the five tested architectures.

7. Cross-Architecture Specification Translator

• Leverage the bug taxonomy (decoding, semantics, aliasing) to train a model that translates a corrected SLEIGH spec from one architecture (e.g., x86-64) to another (e.g., RISC-V) while avoiding known pitfalls.

• The AI can flag likely errors in new specs by comparing against patterns from the 125 fixed bugs, reducing manual review time.

8. Self-Healing Decompiler

• Integrate the paper’s findings into a decompiler that, when it encounters a suspected specification bug (e.g., missing floating-point semantics), automatically queries the differential testing results and adjusts its output to match hardware behavior.

• This improves reliability for vulnerability analysis and reverse engineering, as the decompiler becomes robust to spec errors without requiring manual spec fixes.

Processor specifications underpin critical security and program- analysis tools such as disassemblers, decompilers, and emulators, yet, their correctness is rarely examined. Errors in specifications distort program behaviour, obscure vulnerabilities, and enable analysis-evasion techniques. Validating processor specifications is a non-trivial task. Our study is a significant undertaking to enable, for the first time, the systematic validation of open-source SLEIGH language specifications, predominantly used by Ghidra. We design and implement a testing framework based on an automated oracle validation strategy by proxy. Our approach leverages the structure encoded in a specification itself to enumerate decodable instruction forms and generate targeted initial states. Then differentially test the successful decoding and emulation of those instructions by comparing emulators exercising the processor specification against hardware references. Applying InSPECtor across diverse, open-source specifications---x86-64, AArch64, ARM/Thumb, RISC-V, MSP430---embedding differences in specification styles, author preferences, and instruction set architecture designs, we uncovered over 38,920 discrepancies that led to 125 unique bugs with proposed fixes, identifying decoding and semantic defects as well as cross-vendor inconsistencies. We distill our findings into 8 concrete recommendations to drive future improvements. Our work underscores the importance of specification correctness and provides a practical tool to substantially improve the fidelity of SLEIGH processor specifications, strengthening the reliability of downstream security and analysis tools.