論文の概要: SecIC3: Customizing IC3 for Hardware Security Verification
- arxiv url: http://arxiv.org/abs/2601.21353v1
- Date: Thu, 29 Jan 2026 07:24:08 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-01-30 16:22:49.646455
- Title: SecIC3: Customizing IC3 for Hardware Security Verification
- Title（参考訳）: SecIC3: ハードウェアセキュリティ検証のためのIC3のカスタマイズ
- Authors: Qinhan Tan, Akash Gaonkar, Yu-Wei Fan, Aarti Gupta, Sharad Malik,
- Abstract要約: SecIC3は、IC3に基づくハードウェアモデルチェックアルゴリズムであり、この自己構成構造を利用するようにカスタマイズされている。
我々は、SecIC3を2つのオープンソースIC3実装上に実装し、10つの設計からなる非干渉チェックベンチマークで評価する。
- 参考スコア（独自算出の注目度）: 5.709679444204919
- License: http://creativecommons.org/licenses/by-sa/4.0/
- Abstract: Recent years have seen significant advances in using formal verification to check hardware security properties. Of particular practical interest are checking confidentiality and integrity of secrets, by checking that there is no information flow between the secrets and observable outputs. A standard method for checking information flow is to translate the corresponding non-interference hyperproperty into a safety property on a self-composition of the design, which has two copies of the design composed together. Although prior efforts have aimed to reduce the size of the self-composed design, there are no state-of-the-art model checkers that exploit their special structure for hardware security verification. In this paper, we propose SecIC3, a hardware model checking algorithm based on IC3 that is customized to exploit this self-composition structure. SecIC3 utilizes this structure in two complementary techniques: symmetric state exploration and adding equivalence predicates. We implement SecIC3 on top of two open-source IC3 implementations and evaluate it on a non-interference checking benchmark consisting of 10 designs. The experiment results show that SecIC3 significantly reduces the time for finding security proofs, with up to 49.3x proof speedup compared to baseline implementations.
- Abstract（参考訳）: 近年、ハードウェアのセキュリティ特性をチェックするための公式な検証が大幅に進歩している。
特に興味深いのは、シークレットと観測可能なアウトプットの間に情報フローがないことをチェックすることで、シークレットの機密性と整合性をチェックすることである。
情報フローをチェックするための標準的な方法は、対応する非干渉ハイパープロパティを、構成された設計の2つのコピーを有する設計の自己構成上の安全性特性に変換することである。
それまでの取り組みは、自己構成設計のサイズを減らすことを目的としていたが、ハードウェアセキュリティ検証のための特別な構造を利用する最先端のモデルチェッカーは存在しない。
本稿では、この自己構成構造を利用するようにカスタマイズされたIC3に基づくハードウェアモデル検査アルゴリズムSecIC3を提案する。
SecIC3はこの構造を、対称状態探索と同値述語の追加という2つの相補的な手法で利用している。
我々は、SecIC3を2つのオープンソースIC3実装上に実装し、10つの設計からなる非干渉チェックベンチマークで評価する。
実験の結果、SecIC3はセキュリティ証明の時間を大幅に短縮し、ベースライン実装と比較して49.3倍のスピードアップを実現した。
関連論文リスト
- Proving Circuit Functional Equivalence in Zero Knowledge [4.301822791698451]
ハードウェア形式検証のための最初のプライバシ保護フレームワークであるZK-CECを提案する。
正式な検証とゼロ知識証明(ZKP)を組み合わせることで、ZK-CECはIPの正当性とセキュリティを正式に検証する基盤を確立する。
ZK- CECは、AES S-Boxのような実用的な設計を実用時間内に検証することに成功した。
論文 参考訳（メタデータ） (2026-01-16T10:43:30Z) - Overcoming Joint Intractability with Lossless Hierarchical Speculative Decoding [58.92526489742584]
我々は無益な無益な提案をする。
承認されたトークンの数を大幅に増加させる検証方法。
HSDは様々なモデルファミリやベンチマークの受け入れ率に一貫した改善をもたらすことを示す。
論文 参考訳（メタデータ） (2026-01-09T11:10:29Z) - LAsset: An LLM-assisted Security Asset Identification Framework for System-on-Chip (SoC) Verification [1.7639836127386677]
LAssetは、ハードウェア設計仕様とレジスタ転送レベル(RTL)記述の両方からセキュリティ資産を識別する新しいフレームワークである。
分類精度が高く、システム・オン・チップ(SoC)設計では最大90%のリコール率、IP設計では93%のリコール率に達する。
論文 参考訳（メタデータ） (2026-01-06T00:53:23Z) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳（メタデータ） (2025-11-26T06:39:19Z) - A Zero-overhead Flow for Security Closure [1.737435659602194]
物理合成からQoR(Quality of Results)を評価する際に、セキュリティはほとんど無視されている。
本稿では,セキュリティ改善のためにQoRを劣化させることなく,セキュリティに配慮したASIC設計フローを提案する。
論文 参考訳（メタデータ） (2025-07-23T10:28:15Z) - CANTXSec: A Deterministic Intrusion Detection and Prevention System for CAN Bus Monitoring ECU Activations [53.036288487863786]
物理ECUアクティベーションに基づく最初の決定論的侵入検知・防止システムであるCANTXSecを提案する。
CANバスの古典的な攻撃を検知・防止し、文献では調査されていない高度な攻撃を検知する。
物理テストベッド上での解法の有効性を実証し,攻撃の両クラスにおいて100%検出精度を達成し,100%のFIAを防止した。
論文 参考訳（メタデータ） (2025-05-14T13:37:07Z) - Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
大規模言語モデル(LLM)は、現実のパーソナライズされたアプリケーションにますます統合されている。
RAGで使用される知識基盤の貴重かつしばしばプロプライエタリな性質は、敵による不正使用のリスクをもたらす。
これらの知識基盤を保護するための透かし技術として一般化できる既存の方法は、一般的に毒やバックドア攻撃を含む。
我々は、無害な」知識基盤の著作権保護の名称を提案する。
論文 参考訳（メタデータ） (2025-02-10T09:15:56Z) - Analogous Alignments: Digital "Formally" meets Analog [0.0]
本稿では,デジタルブロックとアナログブロックを組み合わせた混合信号知的特性(IP)の実用的形式検証に着目する。
Digital and Analog Mixed-Signal (AMS)設計は、本質的に異なるが、形式的な検証設定でシームレスに統合される。
論文 参考訳（メタデータ） (2024-09-23T13:38:31Z) - SOCI^+: An Enhanced Toolkit for Secure OutsourcedComputation on Integers [50.608828039206365]
本稿では,SOCIの性能を大幅に向上させるSOCI+を提案する。
SOCI+は、暗号プリミティブとして、高速な暗号化と復号化を備えた(2, 2)ホールドのPaillier暗号システムを採用している。
実験の結果,SOCI+は計算効率が最大5.4倍,通信オーバヘッドが40%少ないことがわかった。
論文 参考訳（メタデータ） (2023-09-27T05:19:32Z) - A Scalable Formal Verification Methodology for Data-Oblivious Hardware [3.518548208712866]
本稿では,標準プロパティチェック手法を用いて,ハードウェアにおけるデータ公開動作を正式に検証する手法を提案する。
この帰納的特性の証明は,マイクロアーキテクチャレベルでのデータ公開性を徹底的に検証するのに十分であることを示す。
あるケーススタディでは、広範囲に検証され、高度にセキュアなIBEX RISC-Vコアにおいて、データ依存のタイミング違反を発見した。
論文 参考訳（メタデータ） (2023-08-15T13:19:17Z) - Efficient Intent Detection with Dual Sentence Encoders [53.16532285820849]
本稿では,USE や ConveRT などの事前訓練された二重文エンコーダによるインテント検出手法を提案する。
提案するインテント検出器の有用性と適用性を示し,完全なBERT-Largeモデルに基づくインテント検出器よりも優れた性能を示す。
コードだけでなく、新しい挑戦的な単一ドメイン意図検出データセットもリリースしています。
論文 参考訳（メタデータ） (2020-03-10T15:33:54Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。