InSPECtor: Improving SLEIGH Processor Specification Veracity via Proxy

• URL: http://arxiv.org/abs/2608.13042v2
• Date: Mon, 17 Aug 2026 01:53:48 GMT
• Title: InSPECtor: Improving SLEIGH Processor Specification Veracity via Proxy
• Abstract summary: This study is a significant undertaking to enable the systematic validation of open-source SLEIGH language specifications.<n>We design and implement a testing framework based on an automated oracle validation strategy by proxy.<n>Applying InSPECtor across diverse, open-source specifications, we uncovered over 38,920 discrepancies that led to 125 unique bugs.
• Score: 14.535794931718229
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: 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.

Related papers

• IdeaAMBIG: Benchmarking Implementation-Critical Gaps in Research-Idea Specifications [52.570108663867046]
  A research idea may be novel, coherent, and scientifically plausible, yet its proposed method may remain insufficiently specified for faithful implementation.<n>We study the codification readiness of implementation-facing research-method specifications, defined by whether they provide sufficient methodological information for a competent implementer or coding agent to construct the intended method without unsupported assumptions.<n>We introduce IdeaAMBIG, a benchmark of 660 evidence-grounded instances: 163 real-world gaps from reports and GitHub issues, and 497 controlled synthetic gaps injected into codification-ready references.
  arXiv  Detail & Related papers  (2026-09-09T17:59:04Z)
• Specification-Driven Development as the Foundation of AI-Native Enterprise Software Engineering [0.0]
  Large language models (LLMs) and agentic AI are shifting software engineering from manual coding toward intent specification, architecture, and governance.<n>Two paradigms have emerged: vibe coding, and an intuition-driven approach accepting AI artifacts via observed behavior, and Specification-Driven Development (SDD), which uses structured specifications as the authoritative source of truth.<n>This article makes three contributions. First, it identifies failure modes of ungoverned conversational generation: the productivity-reliability paradox, architectural erosion from limited context, security exposure, and technical debt.<n>Second, it introduces the Specification Governance Reference Model (SGRM), which formalize
  arXiv  Detail & Related papers  (2026-07-18T07:27:02Z)
• Teaching Code LLMs to Reason with Intermediate Formal Specifications [9.552020178028576]
  SpecCoder is a training framework that learns from validated reference programs, behavior-changing mutants, and multi-turn specification-refinement traces.<n> SpecCoder selects specifications that hold on correct executions while rejecting faulty executions, turning specifications from passive annotations into executable evidence.
  arXiv  Detail & Related papers  (2026-07-05T11:09:30Z)
• CrypFormBench: Benchmarking Formal Analysis Capability of Large Language Models for Cryptographic Schemes [16.171581449458582]
  Large language models (LLMs) are a promising alternative, but their effectiveness in this domain remains unexplored.<n>We introduce CrypFormBench (C.F.B), a benchmark jointly covering symbolic and computational security to evaluate five core LLM capabilities.<n>It comprises 700 instances spanning 677 schemes, 7 mainstream formal verifier languages, and 160 security properties.<n>Overall, their performance remains limited, with Claude-3.5 achieving the highest score at 48.7 out of 100.
  arXiv  Detail & Related papers  (2026-06-24T08:37:38Z)
• Reversa: A Reverse Documentation Engineering Framework for Converting Legacy Software into Operational Specifications for AI Agents [0.0]
  This paper presents Reversa, a reverse documentation engineering framework for converting legacy software into traceable operational specifications for AI agents.<n> specialized agents map the project surface, analyze modules, extract implicit rules, synthesize architecture, write unit-level specifications, and review generated claims.<n>The proposal emphasizes three mechanisms: traceability between code and specification, explicit confidence marking, and preservation of gaps for human validation.
  arXiv  Detail & Related papers  (2026-05-18T17:23:13Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  Large language models (LLMs) and agents have shown promising progress, but their true capabilities and failure modes remain unclear.<n>We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs.
  arXiv  Detail & Related papers  (2026-05-02T11:31:33Z)
• Beyond Code Reasoning: Specification-Anchored Auditing of Multi-Implementation Distributed Protocols [1.5229705287183657]
  SPECA is an audit framework that derives explicit, categorized security properties from natural-language specifications and reuses them across implementations.<n>On the RepoAudit benchmark, SPECA reaches 88.9% precision at 100% recall (F1=0.94) and surfaces 12 author-validated bugs beyond ground truth.<n>On the Sherlock Fusaka Audit Contest (10 targets, 366 submissions), SPECA recovers all 15 vulnerabilities expert-augmented and surfaces 4 fix-confirmed bugs.
  arXiv  Detail & Related papers  (2026-04-29T09:57:07Z)
• Intent-aligned Formal Specification Synthesis via Traceable Refinement [43.72968325799861]
  We present VeriSpecGen, a traceable refinement framework that synthesizes intent-aligned specifications in Lean through requirement-level attribution and localized repair.<n>VeriSpecGen decomposes natural language into atomic requirements and generates requirement-targeted tests with explicit traceability maps.<n>We achieve 86.6% on VERINA SpecGen task using Claude Opus 4.5, improving over baselines by up to 31.8 points across different model families and scales.
  arXiv  Detail & Related papers  (2026-04-12T00:52:27Z)
• Statistical-Based Metric Threshold Setting Method for Software Fault Prediction in Firmware Projects: An Industrial Experience [4.339839287869652]
  Machine learning-based fault prediction models have demonstrated high accuracy, but their lack of interpretability limits their adoption in industrial settings.<n>We present a structured process for defining context-specific software metric thresholds suitable for integration into fault detection in industrial settings.<n>Our approach supports cross-project fault prediction by deriving thresholds from one set of projects and applying them to independently developed firmware.
  arXiv  Detail & Related papers  (2026-02-06T16:19:36Z)
• What Do They Fix? LLM-Aided Categorization of Security Patches for Critical Memory Bugs [46.325755802511026]
  We developLM, a dual-method pipeline that integrates two approaches based on a Large Language Model (LLM) and a fine-tuned small language model.<n>LM successfully identified 111 of 5,140 recent Linux kernel patches addressing OOB or UAF vulnerabilities, with 90 true positives confirmed by manual verification.
  arXiv  Detail & Related papers  (2025-09-26T18:06:36Z)
• Certifiably robust malware detectors by design [48.367676529300276]
  We propose a new model architecture for robust malware detection by design.<n>We show that every robust detector can be decomposed into a specific structure, which can be applied to learn empirically robust malware detectors.<n>Our framework ERDALT is based on this structure.
  arXiv  Detail & Related papers  (2025-08-10T09:19:29Z)
• Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs [79.74676890436174]
  We present an APR tool for Dafny that uses formal specifications as oracles for fault localization and repair.<n>We localize faults through a series of steps, which include using Hoare logic to determine the state of each statement within the program.<n>Our tool achieves 89.6% fault localization coverage and GPT-4o mini yields the highest repair success rate of 74.18%.
  arXiv  Detail & Related papers  (2025-07-04T15:36:12Z)
• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  Large language models (LLMs) struggle with consistent and accurate reasoning. LLMs are trained primarily on correct solutions, reducing their ability to detect and learn from errors. We propose a novel collaborative method integrating Chain-of-Thought (CoT) and Program-of-Thought (PoT) solutions for verification.
  arXiv  Detail & Related papers  (2024-10-05T05:21:48Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.