論文の概要: CertiFlash: A Formal Verification Framework for Flash Translation Layers in Computational Solid State Drives

• arxiv url: http://arxiv.org/abs/2609.10347v1
• Date: Wed, 09 Sep 2026 15:44:46 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-10 19:44:09.086468
• Title: CertiFlash: A Formal Verification Framework for Flash Translation Layers in Computational Solid State Drives
• Title（参考訳）: CertiFlash: 計算ソリッドステートドライブにおけるFlash翻訳レイヤの形式検証フレームワーク
• Abstract要約: ストレージ中心コンピューティングは、ソリッドステートドライブ(SSD)の周辺または内部で計算を移動させることにより、データの移動オーバーヘッドを低減する 不良なフラッシュ変換層(FTL)がSSD内の5面のデバイス状態を破壊可能であることを示す。 本稿では,FTLの正式な検証フレームワークであるCertiFlashを提案する。
• 参考スコア（独自算出の注目度）: 7.464182791512048
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Data-intensive applications move large amounts of data from storage to the compute unit, incurring significant data movement overhead. Storage-centric computing reduces this overhead by moving computation near or inside solid-state drives (SSDs). Enabling it requires modifying SSD policies, e.g., address translation and garbage collection, which are part of the Flash Translation Layer (FTL), the SSD's firmware. Modifying the FTL is error-prone. Because FTL logic has direct access to security-critical device components, even a functionally correct FTL can leak data between tenants, drop integrity tags, or assign a flash block to the wrong tenant. We show that a faulty FTL can corrupt the device state at five surfaces inside the SSD, and demonstrate them on a DaisyPlus OpenSSD. Prior work verifies individual FTL designs, but has two limitations. (1) It establishes only functional correctness, so a modified FTL can violate isolation, integrity, and ownership and still pass verification. (2) It is tied to a single FTL design, so every modification requires redoing every proof. We propose CertiFlash, a formal verification framework for FTLs, mechanized in the Rocq proof assistant, that gives designers a machine-checked proof of security and correctness. CertiFlash models an FTL as a deterministic state machine with a single global invariant over mapping, isolation, integrity, ownership, and allocation. We prove once, over a general FTL model, that (i) every FTL operation preserves the invariant and (ii) the model refines an idealized block device. For a new design, a designer discharges five hypotheses about its own operations instead of redoing either proof. Across four case studies, a designer adds 27 to 3,231 lines against a 16,489-line framework, significantly reducing the verification effort. CertiFlash is open source.
• Abstract（参考訳）: データ集約型アプリケーションは、大量のデータをストレージから計算ユニットに移動させ、大きなデータ移動オーバーヘッドを発生させる。 ストレージ中心のコンピューティングは、ソリッドステートドライブ(SSD)の周辺または内側で計算を移動させることによって、このオーバーヘッドを低減する。 これを実現するには、SSDのファームウェアであるFlash Translation Layer(FTL)の一部であるアドレス変換やガベージコレクションなどのSSDポリシーを変更する必要がある。 FTLの修正はエラーを起こしやすい。 FTLロジックはセキュリティクリティカルなデバイスコンポーネントに直接アクセスできるため、機能的に正しいFTLでさえテナント間でデータをリークしたり、整合性タグをドロップしたり、間違ったテナントにフラッシュブロックを割り当てたりすることができる。 故障したFTLは、SSD内の5面のデバイス状態を破損させ、DaisyPlus OpenSSD上でそれらを実証できることを示す。 以前の作業では、個々のFTL設計を検証するが、2つの制限がある。 1) 機能的正当性のみを確立するため,修正されたFTLは分離,完全性,所有権を侵害し,検証をパスすることができる。 2) 1 つの FTL 設計に結びついているので、すべての修正はすべての証明を再設計する必要がある。 本稿では,FTLの正式な検証フレームワークであるCertiFlashを提案する。 CertiFlashは、マッピング、アイソレーション、完全性、オーナシップ、アロケーションに対して単一のグローバル不変量を持つ決定論的ステートマシンとしてFTLをモデル化する。 一般的なFTLモデルよりも、一度だけ、それを証明します。 (i)すべてのFTL操作は不変性と保存する (ii)モデルが理想的なブロックデバイスを洗練する。 新しい設計では、デザイナは、どちらかの証明を再設計する代わりに、独自の操作に関する5つの仮説を放出する。 4つのケーススタディで、デザイナは16,489行のフレームワークに対して27から3,231行を追加し、検証作業を大幅に削減した。 CertiFlashはオープンソースである。

関連論文リスト

• LLM Inference in a Flash! [66.43896490006965]
  大規模言語モデル(LLM)は、さまざまな自然言語処理タスクで印象的な機能を示している。 我々は、高価な浮動小数点演算をなくすために、エンドツーエンドの整数のみの量子化手法を提案する。
  論文  参考訳（メタデータ） (2026-09-14T18:04:30Z)
• Faster Than Flash: Exploiting Attention Sparsity for Efficient Long-Context Decoding [51.48425605758328]
  我々は,Faster Flash Decoding (FFD) という,長文デコーディングにおいてメモリ壁を壊すように設計されたハードウェア・アルゴリズムの共同設計フレームワークを提示する。 FFDはセレクタとコンピュータを完全に融合したカーネルに統合し、外部メタデータのインデックスをコンテンツ認識スキャンに置き換える。 最大11.6倍のカーネルレベルのスピードアップと256Kコンテキスト長のスケーリングを実現し、2.37倍のスループット向上を実現している。
  論文  参考訳（メタデータ） (2026-08-31T15:13:20Z)
• FLINT: Efficiently Leveraging High Bandwidth Flash for Capacity-Scalable LLM Inference Acceleration [15.418081666515919]
  LLM推論は、計算スループットよりも加速メモリ容量によってますます制限される。 HBFは、マルチテラバイト近加速器容量を提供する3DスタックのNANDフラッシュ技術である。 本稿では,作業負荷駆動型HBF基板FLINTを提案する。
  論文  参考訳（メタデータ） (2026-08-25T18:58:14Z)
• SxSSD: A Secure and Extensible Software-defined Solid State Drive [5.756407892709073]
  ソリッドステートドライブ(SSD)はNANDフラッシュメモリ上に構築され、ブロックベースのストレージインターフェースを介してオペレーティングシステムに公開される。 本研究では,セキュアだがソフトウェア定義のSSD設計であるSxSSDを紹介した。
  論文  参考訳（メタデータ） (2026-08-24T15:14:18Z)
• FlashDrive: Flash Vision-Language-Action Inference for Autonomous Driving [13.217418785964973]
  Vision-Language-Action(VLA)モデルは、エンドツーエンドの推論を自動運転にもたらすことを約束している。 計算コストは、リアルタイム制御には高すぎる。 我々は,4つのステージを同時にターゲットとする,アルゴリズムとシステムの共同設計フレームワークであるFlashDriveを提案する。
  論文  参考訳（メタデータ） (2026-08-13T08:10:54Z)
• Speculative Correction: Draft-then-Refine Decoding for Diffusion Language Models [50.758327861505784]
  まず、まず完全なドラフトを生成し、次に双方向拡散を用いて完全な応答を洗練する。 LLaDA2.1-FlashとLLaDA2.1-Miniの2つの構成を評価する。 Flash-FlashはGSM8K-384の精度を0.848から0.899に改善し、選択したFlashブロック自動回帰ベースラインの1.20倍高速に動作した。 Mini-Flashは2.17倍高速に動作しながら、0.294対0.300のMATH-384性能を含む、有用な品質とレイテンシのトレードオフを提供する。
  論文  参考訳（メタデータ） (2026-07-21T17:58:10Z)
• Fast-dDrive: Efficient Block-Diffusion VLM for Autonomous Driving [54.31800246594724]
  本稿では,ブロック拡散型VLAであるFast-dDriveについて述べる。 我々は、Fast-dDriveが運転エージェントの速度精度フロンティアを再定義することを示す。
  論文  参考訳（メタデータ） (2026-05-22T02:31:32Z)
• One Model, Many Budgets: Elastic Latent Interfaces for Diffusion Transformers [80.19461768457622]
  Elastic Latent Interface Transformer (ELIT) は、入力画像サイズを計算から切り離すための、ドロップインでDiT互換のメカニズムである。 読み取りと書き込み クロスアテンション・レイヤは空間トークンとラテントの間で情報を移動し、重要な入力領域を優先する。 ImageNet-1K 512pxでは、ELITの平均利得は35.3%、FIDおよびFDDスコアは39.6%である。
  論文  参考訳（メタデータ） (2026-03-12T17:57:04Z)
• TorchFL: A Performant Library for Bootstrapping Federated Learning Experiments [4.075095403704456]
  本稿では,フェデレート学習実験をブートストラップするパフォーマンスライブラリTorchFLを紹介する。 TorchFLはPyTorchとLightningを使ってボトムアップで設計されている。 PyTorchとLightningを使用したボトムアップ設計に基づいて構築されたTorchFLは、モデル、データセット、FLアルゴリズムのための準備の整った抽象化を提供する。
  論文  参考訳（メタデータ） (2022-11-01T20:31:55Z)
• Decepticons: Corrupted Transformers Breach Privacy in Federated Learning for Language Models [58.631918656336005]
  悪意のあるパラメータベクトルを配置することで、プライベートなユーザテキストを明らかにする新たな攻撃を提案する。 FLに対する以前の攻撃とは異なり、攻撃はTransformerアーキテクチャとトークンの埋め込みの両方の特徴を利用する。
  論文  参考訳（メタデータ） (2022-01-29T22:38:21Z)

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

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