論文の概要: Themis: A Filesystem Model Checker That Owns the Machine
- arxiv url: http://arxiv.org/abs/2608.01135v1
- Date: Sun, 02 Aug 2026 10:29:50 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-04 15:07:25.091839
- Title: Themis: A Filesystem Model Checker That Owns the Machine
- Title（参考訳）: Themis: マシンを所有するファイルシステムモデルチェッカー
- Abstract要約: ファイルシステムモデルチェッカーは、未修正のイン・カーネルの状態空間を探索する。
Themisは、仮想ブロックデバイスと仮想クロックというマシンを所有している。
実際のext2書き込みはフォークウィンドウ内で提供され、完全にリバージョンされる。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Filesystem model checkers explore an unmodified in-kernel filesystem's state space to find bugs that escape unit tests. The state of the art, Metis, runs inside the OS: it drives syscalls, and, lacking a cheap way to snapshot in-kernel state from user space, it hand-codes a reference filesystem (RefFS) as its differential oracle and sets time aside as noise. Where a checker sits shapes what it can see. I present Themis, a filesystem model checker built beneath an unmodified in-kernel filesystem on a bare-metal Type-1 AMD-V hypervisor. Themis owns the machine: the virtual block device and the virtual clock under a stock Linux/ext2 guest. Ownership buys four things. (1) A machine-layer epsilon-copy fork whose restore cost is proportional to dirtied pages, not filesystem image size, so every unmodified filesystem becomes its own differential reference and no hand-coded reference is required. (2) Below-filesystem observation and byte-level whole-disk diffs with nuisance-field normalization. (3) Control of the clock, turning time into an explored search dimension. (4) The same fork, made re-armable, doubling as a checkpoint for bit-exact deterministic replay. Over a campaign of 40+ hardware runs on an AMD Zen5 9800X3D, the mechanism is proven end-to-end: a real ext2 write is served inside a fork window and fully reverted (DRAM, disk, and device state) in 9 microseconds for the dirtied set. The principal result is the clock: Themis drives real ext2 across a clock sweep and witnesses a real Y2038 defect, a 128-byte-inode clamp that a time-excluded fingerprint cannot register. A real ext2 workload replays whole-DRAM and whole-disk bit-exact across nine passes, and a timing-flaky outcome (nine distinct hashes raw) becomes reproducible when the clock is served (nine identical).
- Abstract（参考訳）: ファイルシステムモデルチェッカーは、未修正のカーネル内のファイルシステムの状態空間を調べて、ユニットテストから逃れるバグを見つけます。
サイスコールを駆動し、ユーザー空間からカーネル内の状態をスナップショットする安価な方法がないため、レファレンスファイルシステム(RefFS)をその微分オラクルとして手書きし、ノイズとして時間を設定する。
チェッカーが座っていると、見えるものを形作る。
ベアメタルType-1 AMD-Vハイパーバイザ上に、未修正のインカーネルファイルシステムの下に構築されたファイルシステムモデルチェッカーであるThemisを紹介します。
Themisが所有しているマシンは、仮想ブロックデバイスと、Linux/ext2の標準ゲストの仮想クロックである。
オーナーは4つのものを買う。
1)復元コストがファイルシステムのイメージサイズに比例せず、未修正のすべてのファイルシステムが独自の差分参照となり、手書きの参照が不要なマシン層エプシロンコピーフォーク。
2)Nuisance-field normalizationによる低ファイルシステム観察とバイトレベル全ディスク差分
(3) 時刻の制御, 時刻を探索次元に変換する。
(4)同じフォークが再武装可能となり、ビットエクササイズ決定論的リプレイのチェックポイントとして倍増した。
AMD Zen5 9800X3D上で40以上のハードウェアを動作させながら、このメカニズムはエンドツーエンドで証明されている。実際のext2書き込みはフォークウィンドウ内で提供され、ダートセットの9マイクロ秒で完全にリバージョン(DRAM、ディスク、デバイス状態)される。
Themisは実際のext2をクロックスイープで駆動し、本物のY2038の欠陥を目撃する。
実のext2ワークロードは、9つのパスにまたがってDRAM全体と全ディスクビットをリプレイし、クロックが提供されたとき(9つの同一)にタイミング不安定な結果(9つの異なるハッシュ)が再現可能である。
関連論文リスト
- Can Code Specify a System Precisely Enough to Formally Verify It? [0.0]
本報告では,業務用レストラン・ポイント・オブ・セールシステムの支払ワークフローを実運用ソフトウェアで評価する。
コアプロトコルは、正確に定義された障害モデルの下で手作りのラインアクティベートされたモデルに対して正しい。
生産用サンドボックスの1つのプローブは、全リカバリはしごを到達不能にする応答形状のばらつきを露呈した。
論文 参考訳（メタデータ） (2026-07-06T13:39:00Z) - Non-Uniform L2 Cache Latency Across the Streaming Multiprocessors of an NVIDIA L40 [0.2864713389096699]
NVIDIA L40は96MiB L2キャッシュを公開する。
L2-hitレイテンシは、物理ストリーミングマルチプロセッサ(SM)がどの負荷に対処するかに強く、再現的に依存します。
ターンシリアライズされた %smid-resolved プローブは、1回の打ち上げで142個のSMの全てのヒット遅延をマッピングする。
論文 参考訳（メタデータ） (2026-06-21T16:50:45Z) - Echo-Memory: A Controlled Study of Memory in Action World Models [58.77172260403133]
本研究では,行動条件付き世界モデルにおける記憶機構の制御に関する研究を行う。
既存のメモリ設計と比較するのは難しいのは、ゲインにはバックボーン、トレーニング、検索、評価の違いが絡み合っているからである。
我々はEcho-Memoryを使ってアクション・ツー・ビデオのインタフェースを修正し、生成元によって履歴が保存され読み込まれるかだけを変える。
論文 参考訳（メタデータ） (2026-06-08T17:54:10Z) - FileGram: Grounding Agent Personalization in File-System Behavioral Traces [79.65734230265521]
FileGramは、エージェントメモリとファイルシステムの挙動トレースのパーソナライズを基盤とする包括的なフレームワークである。
FileGramEngine、FileGramBench、FileGramOSで構成されている。
このフレームワークをオープンソース化することで、パーソナライズされたメモリ中心のファイルシステムエージェントに関する将来の研究を支援したいと考えています。
論文 参考訳（メタデータ） (2026-04-06T17:49:31Z) - Model2Kernel: Model-Aware Symbolic Execution For Safe CUDA Kernels [6.682299469816275]
プロダクション推論システムはコア操作を実装するためにカーネルに依存している。
メモリセーフティのバグは、モデルの重み付けを破損させたり、推論サービスをクラッシュさせたり、あるいは敵攻撃も可能になったりする。
本稿では,推論に使用されるカーネルのメモリ安全性を自動検証する最初の実用システムであるModel2 Kernelを提案する。
論文 参考訳（メタデータ） (2026-03-06T04:13:28Z) - Outrunning LLM Cutoffs: A Live Kernel Crash Resolution Benchmark for All [57.23434868678603]
Live-kBenchは、新たに発見されたカーネルバグのエージェントをスクラップし、評価するセルフ進化ベンチマークの評価フレームワークである。
kEnvは、カーネルのコンパイル、実行、フィードバックのためのエージェントに依存しないクラッシュ解決環境である。
kEnvを用いて3つの最先端エージェントをベンチマークし、最初の試行で74%のクラッシュを解決したことを示す。
論文 参考訳（メタデータ） (2026-02-02T19:06:15Z) - CrashFixer: A crash resolution agent for the Linux kernel [58.152358195983155]
この作業は、システムレベルのLinuxカーネルバグのベンチマークと、Linuxカーネルで実験を実行するプラットフォームを共有するkGymの上に構築されている。
CrashFixerはLinuxカーネルのバグに適応する最初のLCMベースのソフトウェア修復エージェントである。
論文 参考訳（メタデータ） (2025-04-29T04:18:51Z) - KGym: A Platform and Dataset to Benchmark Large Language Models on Linux Kernel Crash Resolution [59.20933707301566]
大規模言語モデル(LLM)は、ますます現実的なソフトウェア工学(SE)タスクにおいて一貫して改善されている。
現実世界のソフトウェアスタックでは、Linuxカーネルのような基本的なシステムソフトウェアの開発にSEの取り組みが費やされています。
このような大規模システムレベルのソフトウェアを開発する際にMLモデルが有用かどうかを評価するため、kGymとkBenchを紹介する。
論文 参考訳（メタデータ） (2024-07-02T21:44:22Z) - model-based script synthesis for fuzzing [10.739464605434977]
既存のアプローチは、トレースからのsyscallシーケンスやシステムコードの静的解析をモデル化することでカーネルを混乱させる。
我々は、異なるカーネル状態に到達するために、トレースされたsyscallシーケンスを学習し、変更するためのWinkFuzzを提案する。
論文 参考訳（メタデータ） (2023-08-08T08:07:50Z) - Compression for Qubit Clocks [55.38708484314286]
クォービットクロックの同じ準備状態に対して$n$の圧縮プロトコルを提案する。
このプロトコルは、状態を$(1/2)log n$ qubitsと$(1/2)log n$ classical bitsに忠実にエンコードする。
論文 参考訳（メタデータ） (2022-09-14T09:45:53Z) - Online detection of failures generated by storage simulator [2.3859858429583665]
現代のストレージインフラストラクチャの動作をシミュレートするためのGoベースの(golang)パッケージを作成します。
パッケージの柔軟な構造により、多数のコンポーネントを持つ現実世界のストレージシステムのモデルを作成することができます。
シミュレータが生成した時系列分布の故障を検出するため,オンラインモードで動作する変更点検出アルゴリズムを改良した。
論文 参考訳（メタデータ） (2021-01-18T14:56:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。