論文の概要: Granite: A Modular Methodology for Foundational Verification of Hardware-Software Leakage Contracts

• arxiv url: http://arxiv.org/abs/2607.27480v1
• Date: Wed, 29 Jul 2026 21:44:57 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-31 21:37:00.325873
• Title: Granite: A Modular Methodology for Foundational Verification of Hardware-Software Leakage Contracts
• Title（参考訳）: Granite: ハードウェア・ソフトウェア漏洩契約の基本的な検証のためのモジュール的方法論
• Abstract要約: Granite は ISA 契約に対する RTL プロセッサの機能的正当性と非推論の両方のモジュール検証のための方法論である。 我々は、ISAリーク契約で指定された観測可能条件のみにより、憶測、精密割り込み、I/Oを含むパイプライン化RISC設計のサイクルバイサイクルタイミングが決定されることを証明した。
• 参考スコア（独自算出の注目度）: 2.76228438275135
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Granite is a methodology for modular verification of both functional correctness and nonleakage of RTL processors against ISA contracts. We prove that the cycle-by-cycle timing of a pipelined RISC design--with speculation, precise interrupts, and I/O--is determined solely by observables specified in an ISA leakage contract. For programs that keep observables independent of secrets (i.e., following the cryptographic-constant-time discipline), this result rules out information leakage through known and unknown timing side channels. Granite's specifications only constrain functional correctness and information-flow dependencies: not how many cycles an instruction takes, at which instruction an interrupt is handled, or the exact latencies of submodules such as multipliers and memory. Granite's central technique is leakage-aware refinement via determinism, which establishes correctness and confidentiality together as trace equivalence with respect to a family of cycle-level, deterministic spec machines. Secret-independent nondeterminism is handled by existentially parameterizing specs with untrusted, deterministic functions acting only on public data. Submodules are proved against their own leakage-aware specs, and these proofs compose into the whole-design guarantee--which therefore holds over a space of secure implementations. We believe this work is the first to achieve modular and foundational connection between instruction-set-level leakage contracts and microarchitecture-specific cycle-by-cycle execution with wire-level observations. Our proofs compose with a certified static analysis that recognizes cryptographic-constant-time code to derive a single Rocq theorem about the cycle-by-cycle confidentiality of a hardware-and-software cryptographic implementation--eliminating every intermediate specification, including the ISA contract itself, from the trusted computing base.
• Abstract（参考訳）: Granite は ISA 契約に対する RTL プロセッサの機能的正当性と非推論の両方のモジュール検証のための方法論である。 我々は、ISAリーク契約で指定された観測可能条件のみにより、憶測、精密割り込み、I/Oを含むパイプライン化RISC設計のサイクルバイサイクルタイミングが決定されることを証明した。 オブザーバブルを秘密とは無関係に維持するプログラム(すなわち暗号・コンスタント・タイムの規律に従って)では、この結果は既知のタイミング側チャネルと未知のタイミング側チャネルを通じて情報漏洩を規制する。 Graniteの仕様は機能的正確さと情報フローに依存しているだけであり、命令が要するサイクル数、割り込みが処理される命令数、乗算器やメモリなどのサブモジュールの正確なレイテンシなどではない。 グラニトの中心的な技術は、決定論による漏洩認識の洗練であり、サイクルレベルの決定論的仕様機械のファミリーに対するトレース同値として、正確性と機密性を共に確立する。 シークレット非独立な非決定論は、公的なデータにのみ作用する信頼できない決定論的関数を持つ存在パラメータ化仕様によって扱われる。 サブモジュールはそれ自身のリークを意識した仕様に対して証明され、これらの証明は全体の設計保証(つまり安全な実装の空間)に構成される。 この研究は、命令セットレベルのリーク契約と、ワイヤレベル観測によるマイクロアーキテクチャ固有のサイクル・バイ・サイクル実行との間のモジュラーおよび基礎的な接続を初めて達成したと我々は信じている。 我々の証明は、ハードウェア・アンド・ソフトウェア暗号実装のサイクル・バイ・サイクルの秘密性に関する1つのRocq定理を導出するために、暗号コンスタント・タイム・コードを認識する認証された静的解析で構成され、ISA契約自身を含む全ての中間仕様を信頼されたコンピュータベースから除去する。

関連論文リスト

• TELLER: Non-intrusive Cross-Layer Root-Cause Analysis for LLM Inference [47.62941623025392]
  本稿では,非侵入的でログ対応なLLM推論フレームワークであるTELLERについて紹介する。 TELLERはモデルバイナリを変更することなく、NVTX/CUPTIトレースとサービスログを収集する。 リクエスト毎のコールチェーンツリーを再構築し、ログ行と対応する実行ステップをアライメントする。 これらの表現に加えて、TELLERは数値的候補のローカライゼーションとマルチモーダルな根起因モデルを組み合わせる。
  論文  参考訳（メタデータ） (2026-08-03T09:39:11Z)
• CLOSER-Bench: Evaluating Budgeted Cross-Stage Design Closure for Hardware Agents [5.604484678527336]
  CLOSER-Bench (CLOSER-Bench) は、予算付きクロスステージ設計クロージャのための制御された評価プロトコルである。 Spec-to-RTL、RTL-to-GDS、Spec-to-GDSタスクを組み合わせ、すべてのシミュレータ、合成、STA、プレース・アンド・ルートの呼び出しを記録する。 最終品質、任意の進捗状況、ツールコスト、ステージ間のリカバリを測定します。
  論文  参考訳（メタデータ） (2026-07-18T04:28:47Z)
• LeanDY: Type-Based and Trace-Based Symbolic Protocol Verification in Lean [9.293322518056357]
  本稿では,タイプベースの推論とトレースベースの推論を組み合わせることで,ステートフルプロトコルとアンバウンドプロトコルのモジュール検証を実現する手法を提案する。 私たちはこのフレームワークをリーン実証アシスタント用のLeanDYライブラリとして実装し、DY*の設計を構築し拡張します。 我々は、LeanDYでSegWitスタイルのブロックチェーンプリミティブを形式化し、支払いチャネルの詳細な形式化を行うことで、その表現性を実証する。
  論文  参考訳（メタデータ） (2026-07-03T15:12:30Z)
• AnchorMoE: Interpretable Time Series Classification via Anchor-Routed MoE [51.994752158953084]
  AnchorMoEは、解釈可能な構成別分類フレームワークである。 ローカルパッチのマルチビュー表現をエンコードし、専門の専門家にルーティングする。 実世界のベンチマークと合成ベンチマークの実験は、AnchorMoEが非常に競争力のある分類性能を達成することを示した。
  論文  参考訳（メタデータ） (2026-06-02T13:30:54Z)
• The Path Matters: Learning a Token-Commitment Policy for Diffusion Language Models [52.93186090124315]
  トークンのコミットメントは、再利用可能なトレースステートポリシとして学ぶことができる、と私たちは主張する。 凍結拡散言語モデルのためにこのポリシーをインスタンス化する軽量プラグインコントローラであるTraceLockを紹介する。
  論文  参考訳（メタデータ） (2026-05-23T18:23:46Z)
• Certified Circuits: Stability Guarantees for Mechanistic Circuits [80.30622018787835]
  Certified Circuitsは、回路発見のための証明可能な安定性を保証する。 ImageNetとOODデータセットでは、認定回路は91%高い精度を達成する。
  論文  参考訳（メタデータ） (2026-02-26T13:07:31Z)
• Symfrog-512: High-Capacity Sponge-Based AEAD Cipher (1024-bit State) [0.0]
  この提案には、決定論的テストベクタと再現可能なベンチマークスイートとともに、完全なリファレンス実装が含まれている。 AEADの構築は、ドメイン分離、レートとキャパシティの選択、タグ生成、参照CLIで使用される正確なファイルフォーマットなど、完全に規定されている。 報告されたパフォーマンス数値は、ドキュメンテーションされたハードウェアとコンパイラ設定の下で、組み込みのベンチマークツールによって生成される。
  論文  参考訳（メタデータ） (2026-02-19T23:39:54Z)
• Unsupervised Conformal Inference: Bootstrapping and Alignment to Control LLM Uncertainty [49.19257648205146]
  生成のための教師なし共形推論フレームワークを提案する。 我々のゲートは、分断されたUPPよりも厳密で安定した閾値を提供する。 その結果は、ラベルのない、API互換の、テスト時間フィルタリングのゲートになる。
  論文  参考訳（メタデータ） (2025-09-26T23:40:47Z)
• Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
  大規模言語モデル(LLM)は、現実のパーソナライズされたアプリケーションにますます統合されている。 RAGで使用される知識基盤の貴重かつしばしばプロプライエタリな性質は、敵による不正使用のリスクをもたらす。 これらの知識基盤を保護するための透かし技術として一般化できる既存の方法は、一般的に毒やバックドア攻撃を含む。 我々は、無害な」知識基盤の著作権保護の名称を提案する。
  論文  参考訳（メタデータ） (2025-02-10T09:15:56Z)
• HasTEE+ : Confidential Cloud Computing and Analytics with Haskell [50.994023665559496]
  信頼性コンピューティングは、Trusted Execution Environments(TEEs)と呼ばれる特別なハードウェア隔離ユニットを使用して、コテナントクラウドデプロイメントにおける機密コードとデータの保護を可能にする。 低レベルのC/C++ベースのツールチェーンを提供するTEEは、固有のメモリ安全性の脆弱性の影響を受けやすく、明示的で暗黙的な情報フローのリークを監視するための言語構造が欠如している。 私たちは、Haskellに埋め込まれたドメイン固有言語(cla)であるHasTEE+を使って、上記の問題に対処します。
  論文  参考訳（メタデータ） (2024-01-17T00:56:23Z)
• A Scalable Formal Verification Methodology for Data-Oblivious Hardware [3.518548208712866]
  本稿では,標準プロパティチェック手法を用いて,ハードウェアにおけるデータ公開動作を正式に検証する手法を提案する。 この帰納的特性の証明は,マイクロアーキテクチャレベルでのデータ公開性を徹底的に検証するのに十分であることを示す。 あるケーススタディでは、広範囲に検証され、高度にセキュアなIBEX RISC-Vコアにおいて、データ依存のタイミング違反を発見した。
  論文  参考訳（メタデータ） (2023-08-15T13:19:17Z)
• Short Blocklength Wiretap Channel Codes via Deep Learning: Design and Performance Evaluation [5.203329540700176]
  情報理論セキュリティ保証の下で,ガウス通信路の短ブロック長符号を設計する。 オートエンコーダを介して信頼性制約を処理し、ハッシュ関数による秘密制約を処理します。 ブロック長が16以下の場合、正解率の誤差の確率をシミュレーションにより評価する。
  論文  参考訳（メタデータ） (2022-06-07T17:52:46Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。