論文の概要: InSPECtor: Improving SLEIGH Processor Specification Veracity via Proxy
- arxiv url: http://arxiv.org/abs/2608.13042v2
- Date: Mon, 17 Aug 2026 01:53:48 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-18 13:30:43.589484
- Title: InSPECtor: Improving SLEIGH Processor Specification Veracity via Proxy
- Title（参考訳）: InSPECtor:プロキシによるSLEIGHプロセッサ仕様の信頼性の向上
- Abstract要約: 本研究は,オープンソースのSLEIGH言語仕様の体系的検証を可能にするための重要な取り組みである。
プロキシによる自動オラクル検証戦略に基づいて,テストフレームワークの設計と実装を行う。
InSPECtorを多種多様なオープンソース仕様に適用し、125のユニークなバグを引き起こした38,920の相違点を発見した。
- 参考スコア（独自算出の注目度）: 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.
- Abstract（参考訳）: プロセッサ仕様は、デアセンブラ、デコンパイラ、エミュレータなどの重要なセキュリティおよびプログラム分析ツールの基盤となっているが、その正確性はめったに調査されない。
仕様のエラーによってプログラムの動作が歪められ、脆弱性があいまいになり、分析回避技術が有効になる。
プロセッサ仕様の検証は簡単な作業ではありません。
我々の研究は、Ghidraが主に使用しているオープンソースのSLEIGH言語仕様の体系的検証を可能にするための重要な取り組みである。
プロキシによる自動オラクル検証戦略に基づいて,テストフレームワークの設計と実装を行う。
提案手法では、仕様自体に符号化された構造を利用して、デオード可能な命令形式を列挙し、ターゲットとする初期状態を生成する。
次に、プロセッサ仕様を実行するエミュレータとハードウェアリファレンスを比較して、これらの命令の復号化とエミュレーションを成功させる。
InSPECtorを様々なオープンソース仕様---x86-64, AArch64, ARM/Thumb, RISC-V, MSP430-に適用し、仕様スタイル、著者の好み、命令セットアーキテクチャ設計の違いを組み込んだ結果、提案された修正で125のユニークなバグ、デコードとセマンティックな欠陥、およびクロスベンダの不整合が発見された。
今後の改善を進めるため,具体的な8つの推奨事項を抽出した。
本研究は,SLEIGHプロセッサ仕様の信頼性を大幅に向上し,下流のセキュリティ・分析ツールの信頼性を高めるための実用的なツールを提供する。
関連論文リスト
- IdeaAMBIG: Benchmarking Implementation-Critical Gaps in Research-Idea Specifications [52.570108663867046]
研究のアイデアは、新しく、一貫性があり、科学的に妥当であるが、その提案された手法は、忠実な実装のために不十分に指定されている。
提案手法は,実装を対象とする研究手法仕様の体系化の可否を,有能な実装者やコーディングエージェントに十分な方法論的情報を提供して,前提条件を満たさずに目的とする手法を構築することができるかを検討する。
IdeaAMBIGは660のエビデンス基底インスタンスのベンチマークで、レポートとGitHubの問題から163の現実世界のギャップと、コーディフィケーション対応のリファレンスに注入される合成ギャップを497のコントロールで管理する。
論文 参考訳（メタデータ） (2026-09-09T17:59:04Z) - Specification-Driven Development as the Foundation of AI-Native Enterprise Software Engineering [0.0]
大規模言語モデル(LLM)とエージェントAIは、ソフトウェアエンジニアリングを手作業によるコーディングからインテント仕様、アーキテクチャ、ガバナンスへとシフトさせています。
バイブコーディング(vibe coding)と、観察された振る舞いを通じてAIアーティファクトを受け入れる直観駆動アプローチ(intuition-driven approach)と、構造化仕様を真理の信頼できる情報源として使用する仕様駆動開発(Specification-Driven Development, SDD)の2つのパラダイムが登場した。
この記事では、3つのコントリビューションを行います。まず最初に、生産性-信頼性パラドックス、限られたコンテキストからのアーキテクチャ侵食、セキュリティ露出、技術的負債といった、過度な会話生成の失敗モードを特定します。
第2に、正式な仕様ガバナンス参照モデル(SGRM)を導入する。
論文 参考訳（メタデータ） (2026-07-18T07:27:02Z) - Teaching Code LLMs to Reason with Intermediate Formal Specifications [9.552020178028576]
SpecCoderは、検証済みの参照プログラム、振る舞いを変えるミュータント、マルチターン仕様修正トレースから学ぶトレーニングフレームワークである。
SpecCoderは、欠陥のある実行を拒否しながら正しい実行を保持する仕様を選択し、受動的アノテーションから実行可能なエビデンスに変換する。
論文 参考訳（メタデータ） (2026-07-05T11:09:30Z) - CrypFormBench: Benchmarking Formal Analysis Capability of Large Language Models for Cryptographic Schemes [16.171581449458582]
大規模言語モデル(LLM)は有望な代替手段であるが、この領域におけるそれらの有効性は未解明のままである。
CrypFormBench (C.F.B) は,5つのコアLLM機能を評価するために,シンボル的および計算的セキュリティを共同でカバーするベンチマークである。
677のスキームにまたがる700のインスタンス、7つの主要な形式検証言語、160のセキュリティプロパティで構成されている。
クロード3.5は100点中48.7点で最高得点を記録した。
論文 参考訳（メタデータ） (2026-06-24T08:37:38Z) - Reversa: A Reverse Documentation Engineering Framework for Converting Legacy Software into Operational Specifications for AI Agents [0.0]
本稿では,レガシソフトウェアをAIエージェントのトレーサブルな運用仕様に変換するためのリバースドキュメンテーションエンジニアリングフレームワークであるReversaを紹介する。
特殊なエージェントは、プロジェクト表面をマッピングし、モジュールを分析し、暗黙のルールを抽出し、アーキテクチャを合成し、ユニットレベルの仕様を書き、生成されたクレームをレビューする。
提案では,コードと仕様間のトレーサビリティ,明確な信頼性マーキング,人間の検証のためのギャップの保存という,3つのメカニズムを強調している。
論文 参考訳（メタデータ） (2026-05-18T17:23:13Z) - LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。
CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
論文 参考訳（メタデータ） (2026-05-02T11:31:33Z) - Beyond Code Reasoning: Specification-Anchored Auditing of Multi-Implementation Distributed Protocols [1.5229705287183657]
SPECAは、明示的で分類されたセキュリティプロパティを自然言語仕様から導き出し、実装間で再利用する監査フレームワークである。
RepoAuditのベンチマークでは、SPECAは100%リコール(F1=0.94)で88.9%の精度に達し、著者が検証した12のバグを地上の真実を超えて表面化している。
Sherlock Fusaka Audit Contest(10のターゲット、366の応募)では、SPECAが専門家が強化した15の脆弱性をすべて回復し、4つの修正確認バグが浮上した。
論文 参考訳（メタデータ） (2026-04-29T09:57:07Z) - Intent-aligned Formal Specification Synthesis via Traceable Refinement [43.72968325799861]
VeriSpecGenは、要求レベルの属性と局所的な修復を通じて、リーンで意図に整合した仕様を合成する、トレーサブルな改善フレームワークです。
VeriSpecGenは自然言語をアトミックな要件に分解し、明示的なトレーサビリティマップで要求対象のテストを生成する。
我々は、Claude Opus 4.5を使用してVERINA SpecGenタスクの86.6%を達成し、モデルファミリとスケールで最大31.8ポイントのベースラインを改善する。
論文 参考訳（メタデータ） (2026-04-12T00:52:27Z) - Statistical-Based Metric Threshold Setting Method for Software Fault Prediction in Firmware Projects: An Industrial Experience [4.339839287869652]
マシンラーニングベースのフォールト予測モデルは高い精度を示しているが、解釈可能性の欠如により、産業環境での採用が制限されている。
本稿では,産業環境における故障検出への統合に適したコンテキスト固有のソフトウェアメトリックしきい値を定義するための構造化プロセスを提案する。
提案手法は,一組のプロジェクトからしきい値を取得し,個別に開発したファームウェアに適用することにより,プロジェクト間の障害予測を支援する。
論文 参考訳（メタデータ） (2026-02-06T16:19:36Z) - What Do They Fix? LLM-Aided Categorization of Security Patches for Critical Memory Bugs [46.325755802511026]
我々は、LLM(Large Language Model)と細調整された小言語モデルに基づく2つのアプローチを統合するデュアルメタルパイプラインであるLMを開発した。
LMは、OOBまたはUAFの脆弱性に対処する最近のLinuxカーネルのパッチ5,140のうち111つを、手作業による検証によって90の正の正が確認された。
論文 参考訳（メタデータ） (2025-09-26T18:06:36Z) - Certifiably robust malware detectors by design [48.367676529300276]
設計によるロバストなマルウェア検出のための新しいモデルアーキテクチャを提案する。
すべての堅牢な検出器を特定の構造に分解することができ、それを経験的に堅牢なマルウェア検出器の学習に適用できることを示す。
我々のフレームワークERDALTはこの構造に基づいている。
論文 参考訳（メタデータ） (2025-08-10T09:19:29Z) - Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs [79.74676890436174]
本稿では,障害の局所化と修復のためのオラクルとして形式仕様を用いたDafny用のAPRツールを提案する。
プログラム内の各ステートメントの状態を決定するために、Hoareロジックの使用を含む一連のステップを通じて、障害をローカライズします。
また, GPT-4o miniが74.18%と高い修理成功率を示した。
論文 参考訳（メタデータ） (2025-07-04T15:36:12Z) - Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。
LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。
本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
論文 参考訳（メタデータ） (2024-10-05T05:21:48Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。