論文の概要: aLEAKator: HDL Mixed-Domain Simulation for Masked Hardware \& Software Formal Verification

• arxiv url: http://arxiv.org/abs/2512.07520v1
• Date: Mon, 08 Dec 2025 12:58:35 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-09 22:03:54.893806
• Title: aLEAKator: HDL Mixed-Domain Simulation for Masked Hardware \& Software Formal Verification
• Title（参考訳）: ALEAKator: Masked Hardware \& Software Formal VerificationのためのHDL混合ドメインシミュレーション
• Authors: Noé Amiot, Quentin L. Meunier, Karine Heydemann, Emmanuelle Encrenaz,
• Abstract要約: ALEAKatorは、CPU上で動作する暗号アクセラレータとソフトウェアの自動検証のためのオープンソースのフレームワークである。 提案手法は混合領域シミュレーションを導入し, 各種(頑健でゆるやかな)1成分リークモデルに基づく高精度なモデリングと検証を可能にする。 提案手法は既存のツールや実世界の計測値に対して検証され,CPU上での完全な一階マスキングAESの検証など,革新的な結果が得られた。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Verifying the security of masked hardware and software implementations, under advanced leakage models, remains a significant challenge, especially then accounting for glitches, transitions and CPU micro-architectural specifics. Existing verification approaches are either restricted to small hardware gadgets, small programs on CPUs such as Sboxes, limited leakage models, or require hardware-specific prior knowledge. In this work, we present aLEAKator, an open-source framework for the automated formal verification of masked cryptographic accelerators and software running on CPUs from their HDL descriptions. Our method introduces mixed-domain simulation, enabling precise modeling and verification under various (including robust and relaxed) 1-probing leakage models, and supports variable signal granularity without being restricted to 1-bit wires. aLEAKator also supports verification in the presence of lookup tables, and does not require prior knowledge of the target CPU architecture. Our approach is validated against existing tools and real-world measurements while providing innovative results such as the verification of a full, first-order masked AES on various CPUs
• Abstract（参考訳）: 高度なリークモデルの下で、マスクされたハードウェアとソフトウェア実装のセキュリティを検証することは、特にグリッチ、トランジッション、CPUマイクロアーキテクチャの特定を考慮に入れれば、依然として大きな課題である。 既存の検証アプローチは、小さなハードウェアガジェット、SboxなどのCPU上の小さなプログラム、限られたリークモデル、ハードウェア固有の事前知識に制限されている。 本稿では,ALEAKatorについて紹介する。ALEAKatorは,HDL記述からCPU上で動作する暗黙の暗号アクセラレータとソフトウェアの自動検証を行うオープンソースフレームワークである。 提案手法は混合領域シミュレーションを導入し, 各種(頑健でゆるやかな)1ビットリークモデル下での高精度なモデリングと検証を可能にし, 1ビット線に制限されることなく, 可変信号の粒度をサポートした。 ALEAKatorはルックアップテーブルの存在下での検証もサポートしており、ターゲットのCPUアーキテクチャに関する事前の知識を必要としない。 提案手法は既存のツールや実世界の計測値に対して検証され,CPU上での完全な一階マスキングAESの検証などの革新的な結果が得られた。

関連論文リスト

• UnicEdit-10M: A Dataset and Benchmark Breaking the Scale-Quality Barrier via Unified Verification for Reasoning-Enriched Edits [43.59555184340113]
  マルチツールチェーンをエンド・ツー・エンドのモデルと統一された検証後のステージで置き換える軽量なデータパイプラインを導入する。 スケーラブルな品質管理のために、7Bのデュアルタスクエキスパートモデル textbfQwen-Verify をトレーニングし、効率的な故障検出と命令再カプセル化を行う。 このパイプラインは、さまざまな基本的な複雑な編集タスクにまたがる10Mスケールのデータセットである textbfUnicEdit-10M を生成する。
  論文  参考訳（メタデータ） (2025-12-01T17:45:44Z)
• AI Bill of Materials and Beyond: Systematizing Security Assurance through the AI Risk Scanning (AIRS) Framework [31.261980405052938]
  人工知能(AI)システムの保証は、ソフトウェアサプライチェーンセキュリティ、敵機械学習、ガバナンスドキュメントに分散している。 本稿では,AI保証の運用を目的とした脅威モデルに基づくエビデンス発生フレームワークであるAI Risk Scanning(AIRS)フレームワークを紹介する。
  論文  参考訳（メタデータ） (2025-11-16T16:10:38Z)
• Quant-dLLM: Post-Training Extreme Low-Bit Quantization for Diffusion Large Language Models [47.41616630151171]
  拡散大言語モデル (dLLMs) は双方向のコンテキストと柔軟なマスマスキングデノジング生成を提供する。 我々は,dLLMに適した超低ビットPTQフレームワークであるQuant-dLLMを提案する。 Quant-dLLMは、dLLM上での最先端(SOTA)AR-transfer PTQ法よりも高い精度を達成する。
  論文  参考訳（メタデータ） (2025-09-27T13:50:42Z)
• Detecting Hardware Trojans in Microprocessors via Hardware Error Correction Code-based Modules [49.1574468325115]
  ハードウェアトロイの木馬(HT)は、攻撃者が無許可のソフトウェアを実行したり、特権操作に不正にアクセスしたりすることができる。 RISC-Vマイクロプロセッサ上のエラー訂正符号(ECC)を用いて,ランタイムHTアクティベーションを検出するハードウェアベースの手法を紹介する。
  論文  参考訳（メタデータ） (2025-06-18T12:37:14Z)
• CRAFT: Characterizing and Root-Causing Fault Injection Threats at Pre-Silicon [3.6158033114580674]
  フォールトインジェクション攻撃は組み込みシステムに重大なセキュリティ脅威をもたらす。 物理的欠陥がシステムレベルの行動にどのように伝播するかの早期発見と理解は、サイバーインフラ構造を保護するために不可欠である。 この研究は、プレシリコン分析とポストシリコンバリデーションを組み合わせたフレームワークであるCRAFTを導入し、障害インジェクションの脆弱性を体系的に発見し分析する。
  論文  参考訳（メタデータ） (2025-03-05T20:17:46Z)
• A Lean Transformer Model for Dynamic Malware Analysis and Detection [0.0]
  マルウェアは現代のコンピューティングの世界にとって急速に成長する脅威であり、既存の防衛線はこの問題に対処するのに十分な効率性を持っていない。 これまでの研究では、実行レポートから抽出したニューラルネットワークとAPI呼び出しシーケンスを活用することに成功した。 本稿では,悪意のあるファイルを検出するために,Transformersアーキテクチャに基づくエミュレーションオンリーモデルを設計する。
  論文  参考訳（メタデータ） (2024-08-05T08:46:46Z)
• HIVE: Scalable Hardware-Firmware Co-Verification using Scenario-based Decomposition and Automated Hint Extraction [2.977255700811213]
  ハードウェア確認ソフトの共検証は、信頼できるシステムの設計に不可欠である。 ハードウェアを手動で抽象化したり、ヒントを手動で生成することで、ファームウェア検証中の状態空間を削減できる有望な方法がある。 本稿では,シミュレーションに基づく検証のスケーラビリティと形式検証の完全性とを効果的に組み合わせる。
  論文  参考訳（メタデータ） (2023-09-14T19:24:57Z)
• AWQ: Activation-aware Weight Quantization for LLM Compression and Acceleration [54.692405042065815]
  LLM低ビット量のみの量子化のためのハードウェアフレンドリーなアプローチであるActivation-Aware Weight Quantization (AWQ)を提案する。 AWQ は 1% の正重みしか保護せず,命令調整型 LM とマルチモーダル LM の量子化性能に優れる。 また,4ビットオンデバイスLLM/VLMに適した,効率的なフレキシブルな推論フレームワークであるTinyChatを実装した。
  論文  参考訳（メタデータ） (2023-06-01T17:59:10Z)
• DeepGEMM: Accelerated Ultra Low-Precision Inference on CPU Architectures using Lookup Tables [49.965024476651706]
  DeepGEMMはSIMDハードウェア上で超高精度畳み込みニューラルネットワークを実行するためのルックアップテーブルベースのアプローチである。 実装は、x86プラットフォーム上で、対応する8ビット整数カーネルを最大1.74倍の性能で上回る。
  論文  参考訳（メタデータ） (2023-04-18T15:13:10Z)

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

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