論文の概要: Controller Datapath Aware Verification of Masked Hardware Generated via High Level Synthesis
- arxiv url: http://arxiv.org/abs/2603.18939v1
- Date: Thu, 19 Mar 2026 14:17:03 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-03-20 17:19:06.189379
- Title: Controller Datapath Aware Verification of Masked Hardware Generated via High Level Synthesis
- Title（参考訳）: 高レベル合成によるマスクハードウェアの制御器データパスによる検証
- Authors: Nilotpola Sarma, Vaishali Ghanshyam Chaudhuri, Chandan Karfa,
- Abstract要約: マスキング(Masking)は、暗号アルゴリズムにおけるパワーサイドチャネル攻撃(PSCA)に対する対策である。
最近のアプローチは、マスク付きレジスタ転送レベル(RTL)ハードウェアを自動生成する高レベル合成(HLS)ツールに依存している。
本研究は,HLS生成マスクハードウェアのハードウェアマスキング検証戦略を提案する。
- 参考スコア（独自算出の注目度）: 0.2624902795082451
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Masking is a countermeasure against Power Side Channel Attacks (PSCAs) in both software and hardware implementations of cryptographic algorithms. Compared to software masking, implementing masked hardware is time consuming and error prone. Recent approaches, therefore, rely on High Level Synthesis (HLS) tools to automatically generate masked Register Transfer Level (RTL) hardware from verified masked software, significantly reducing design effort. Since HLS was never developed for security, HLS optimizations may impact PSCA security of the generated RTL. As a result, verifying the PSCA security of HLS generated masked RTL is crucial. Existing hardware masking verification tools can verify masked hardware, but may produce false positives when applied to HLS generated designs with controller datapath architectures obtained due to resource-shared datapath obtained via HLS. This work proposes a hardware masking verification strategy for HLS generated masked hardware. Our toolflow MaskedHLSVerif, performs state-wise formal verification of controller datapath RTL obtained via HLS, thereby avoiding false positives caused by resource-shared datapaths. Our tool flow correctly verifies standard cryptographic benchmarks, consisting of cascaded masked gadgets and the PRESENT S-box masked with gadgets, where existing tools like REBECCA reports false positives. The proposed tool-flow is able to detect masking flaws induced by HLS-optimizations as well.
- Abstract（参考訳）: マスキング(Masking)は、暗号アルゴリズムのソフトウェアおよびハードウェア実装において、パワーサイドチャネルアタック(PSCA)に対する対策である。
ソフトウェアマスキングと比較すると、マスクされたハードウェアを実装するのに時間がかかり、エラーが発生しやすい。
したがって、近年のアプローチでは、認証されたマスク付きソフトウェアからマスク付きレジスタ転送レベル(RTL)ハードウェアを自動的に生成する高レベル合成(HLS)ツールに依存しており、設計の労力を大幅に削減している。
HLSはセキュリティのために開発されていないため、HLS最適化は生成されたRTLのPSCAセキュリティに影響を与える可能性がある。
その結果,HLS 生成マスク RTL の PSCA セキュリティを検証することが重要である。
既存のハードウェアマスキング検証ツールは、マスクされたハードウェアを検証できるが、HLSによって得られたリソース共有データパスによって得られたコントローラデータパスアーキテクチャを用いて、HLSが生成した設計に適用した場合、偽陽性が発生する可能性がある。
本研究は,HLS生成マスクハードウェアのハードウェアマスキング検証戦略を提案する。
我々のツールフローMaskedHLSVerifは、HLSを介して得られたコントローラデータパスRTLの状態を形式的に検証することで、リソース共有データパスによる偽陽性を回避する。
我々のツールフローは、カスケードされたマスク付ガジェットと、REBECCAのような既存のツールが偽陽性を報告しているガジェットでマスクされたPreSENT S-boxからなる標準的な暗号ベンチマークを正しく検証する。
提案したツールフローは、HLS最適化によって引き起こされるマスキング欠陥も検出できる。
関連論文リスト
- SecureRAG-RTL: A Retrieval-Augmented, Multi-Agent, Zero-Shot LLM-Driven Framework for Hardware Vulnerability Detection [1.4675092799855405]
大規模言語モデル(LLM)は自然言語処理タスクにおいて顕著な能力を示している。
本稿では, SecureRAG-RTL(Retrieval-Augmented Generation (RAG) に基づく新しいアプローチを提案する。
提案手法は,ドメイン固有検索と生成推論を統合し,ハードウェアセキュリティの専門知識に固有の制約を克服する。
論文 参考訳（メタデータ） (2026-03-05T21:25:49Z) - aLEAKator: HDL Mixed-Domain Simulation for Masked Hardware \& Software Formal Verification [0.0]
ALEAKatorは、CPU上で動作する暗号アクセラレータとソフトウェアの自動検証のためのオープンソースのフレームワークである。
提案手法は混合領域シミュレーションを導入し, 各種(頑健でゆるやかな)1成分リークモデルに基づく高精度なモデリングと検証を可能にする。
提案手法は既存のツールや実世界の計測値に対して検証され,CPU上での完全な一階マスキングAESの検証など,革新的な結果が得られた。
論文 参考訳（メタデータ） (2025-12-08T12:58:35Z) - Detecting Hardware Trojans in Microprocessors via Hardware Error Correction Code-based Modules [49.1574468325115]
ハードウェアトロイの木馬(HT)は、攻撃者が無許可のソフトウェアを実行したり、特権操作に不正にアクセスしたりすることができる。
RISC-Vマイクロプロセッサ上のエラー訂正符号(ECC)を用いて,ランタイムHTアクティベーションを検出するハードウェアベースの手法を紹介する。
論文 参考訳（メタデータ） (2025-06-18T12:37:14Z) - PRO-V: An Efficient Program Generation Multi-Agent System for Automatic RTL Verification [6.983135183126461]
Pro-Vは、堅牢なRTL検証のためのプログラム生成マルチエージェントシステムである。
生成したテストベンチの正しさを高めるため、効率的なn個の反復サンプリング戦略が組み込まれている。
Pro-Vは、黄金のRTL実装では87.17%、RTL変異では76.28%の精度で検証されている。
論文 参考訳（メタデータ） (2025-06-13T20:06:34Z) - Exploring Code Language Models for Automated HLS-based Hardware Generation: Benchmark, Infrastructure and Analysis [14.458529723566379]
LLM(Large Language Model)は、PythonやC++などのプログラミング言語に使用される。
本稿では,LLMを利用してHLS(High-Level Synthesis)ベースのハードウェア設計を行う。
論文 参考訳（メタデータ） (2025-02-19T17:53:59Z) - Place Protections at the Right Place: Targeted Hardening for Cryptographic Code against Spectre v1 [14.99532960317865]
そこで本研究では,Spectreの脆弱性を検知し,対象とするハードニングを適用するために,新しい固定点アルゴリズムを用いた分析フレームワークを提案する。
フレームワークをLightSLHとしてインスタンス化する。
論文 参考訳（メタデータ） (2024-08-29T02:31:28Z) - MaskedHLS: Domain-Specific High-Level Synthesis of Masked Cryptographic Designs [0.5737287537823071]
本稿では,PSCA保護マスクハードウェア実装に適したドメイン固有HLS手法を提案する。
レジはグリッチ・ロバスト・マスキング・ガジェットが必要とする特定の場所に配置され、セキュアなRTLとなる。
PreSENT CipherのS-boxとAES CanrightのS-boxを4つの最先端ガジェットで覆った実験の結果、MaskedHLSはレジスタが73.9%減少し、レイテンシが45.7%低下していることがわかった。
論文 参考訳（メタデータ） (2024-07-16T14:57:15Z) - When ControlNet Meets Inexplicit Masks: A Case Study of ControlNet on its Contour-following Ability [93.15085958220024]
ControlNetは、ユーザーが提供するマスクの正確な輪郭と密に一致したコンテンツを作成するのに長けている。
これらのマスクがノイズを含む場合、非専門家で頻繁に発生するため、出力には不要なアーティファクトが含まれる。
筆者らはまず, 深部分析により, 種々の劣化レベルを有する非説明マスクの影響を抑える上で重要な役割について述べる。
劣化推定器と形状優先変調ブロックからなる高度な形状認識制御ネットを考案した。
論文 参考訳（メタデータ） (2024-03-01T11:45:29Z) - An Unforgeable Publicly Verifiable Watermark for Large Language Models [84.2805275589553]
現在の透かし検出アルゴリズムは、透かし生成プロセスで使用される秘密鍵を必要としており、公開検出中にセキュリティ違反や偽造の影響を受ける。
両段階で同じキーを使用するのではなく、2つの異なるニューラルネットワークを用いて透かしの生成と検出を行う。
論文 参考訳（メタデータ） (2023-07-30T13:43:27Z) - Adaptive Shrink-Mask for Text Detection [91.34459257409104]
既存のリアルタイムテキスト検出器は、ストリップマスクによってテキストの輪郭を直接再構築する。
予測された収縮マスクへの依存は不安定な検出結果をもたらす。
スーパーピクセルウィンドウ (SPW) はネットワークを監督するように設計されている。
論文 参考訳（メタデータ） (2021-11-18T07:38:57Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。