論文の概要: Automated Formal Verification of a Software Fault Isolation System
- arxiv url: http://arxiv.org/abs/2508.15898v1
- Date: Thu, 21 Aug 2025 18:00:19 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-08-25 16:42:36.153744
- Title: Automated Formal Verification of a Software Fault Isolation System
- Title（参考訳）: ソフトウェア故障分離システムの自動形式検証
- Authors: Matthew Sotoudeh, Zachary Yedidia,
- Abstract要約: ソフトウェア障害分離(SFI)は、信頼できないソフトウェアをサンドボックス化する一般的な方法である。
SFI の重要なコンポーネントは、信頼できないコードがマシン言語のサブセットで書かれていることをチェックする検証器である。
SFI検証器の健全性バグは、SFIセキュリティモデルを破り、サンドボックス化されたと思われるコードが保護されたメモリを読み取ることを可能にする。
- 参考スコア（独自算出の注目度）: 1.2836119608837133
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Software fault isolation (SFI) is a popular way to sandbox untrusted software. A key component of SFI is the verifier that checks the untrusted code is written in a subset of the machine language that guarantees it never reads or writes outside of a region of memory dedicated to the sandbox. Soundness bugs in the SFI verifier would break the SFI security model and allow the supposedly sandboxed code to read protected memory. In this paper, we address the concern of SFI verifier bugs by performing an automated formal verification of a recent SFI system called Lightweight Fault Isolation (LFI). In particular, we formally verify that programs accepted by the LFI verifier never read or write to memory outside of a designated sandbox region.
- Abstract（参考訳）: ソフトウェア障害分離(SFI)は、信頼できないソフトウェアをサンドボックス化する一般的な方法である。
SFIの重要なコンポーネントは、信頼できないコードがサンドボックス専用のメモリ領域の外で決して読み書きしないことを保証するマシン言語のサブセットで書かれていることをチェックする検証器である。
SFI検証器の健全性バグは、SFIセキュリティモデルを破り、サンドボックス化されたと思われるコードが保護されたメモリを読み取ることを可能にする。
本稿では,最近のSFIシステムである軽量故障分離(LFI)の自動検証を行うことにより,SFI検証バグの懸念に対処する。
特に,指定されたサンドボックス領域外において,LFI検証器が受信したプログラムがメモリに読み書きされないことを正式に検証する。
関連論文リスト
- TrustMee: Self-Verifying Remote Attestation Evidence [0.7491482431654224]
本稿では,遠隔検定の自己検証という概念を紹介する。
Trusteeフレームワークのプラットフォームに依存しない検証ドライバであるTrustMeeとして、この概念を実装します。
論文 参考訳（メタデータ） (2026-02-13T17:56:08Z) - 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) - InFi-Check: Interpretable and Fine-Grained Fact-Checking of LLMs [48.98720183285795]
InFi-Checkは、大規模な言語モデルの解釈ときめ細かい事実チェックのためのフレームワークである。
InFi-Checkerは、サポートエビデンスを提供し、きめ細かいエラータイプを分類し、修正と共に正当化を生成する。
実験の結果,InFi-CheckerはInFi-Check-FGの最先端性能を実現することがわかった。
論文 参考訳（メタデータ） (2026-01-10T20:00:17Z) - Propose, Solve, Verify: Self-Play Through Formal Verification [75.44204610186587]
形式的検証が信頼性の高い正当性信号を提供する検証コード生成設定における自己再生について検討する。
本稿では,PSV(Propose, Solve, Verify)という,難易度の高い合成問題を生成可能なプロジェクタと,専門家の反復によって訓練された解決器を作成するための,形式的検証信号を用いた簡単なセルフプレイフレームワークを紹介する。
そこで本研究では,生成した質問数とトレーニングの繰り返し数によるパフォーマンスの尺度を示し,形式的検証と難易度を考慮した提案を,自己再生を成功させる上で不可欠な要素として同定する。
論文 参考訳（メタデータ） (2025-12-20T00:56:35Z) - InfCode: Adversarial Iterative Refinement of Tests and Patches for Reliable Software Issue Resolution [31.874379525390967]
InfCodeは、リポジトリレベルの自動イシュー解決のための、対向的なマルチエージェントフレームワークである。
InfCodeは、テストパッチジェネレータとコードパッチジェネレータの間の逆インタラクションを通じて、テストとパッチの両方を反復的に洗練する。
DeepSeek-V3やClaude 4.5 Sonnetといったモデルを用いたSWE-bench LiteとSWE-benchの検証実験は、InfCodeが一貫して強力なベースラインを上回っていることを示している。
論文 参考訳（メタデータ） (2025-11-20T03:04:21Z) - Empirical Security Analysis of Software-based Fault Isolation through Controlled Fault Injection [21.57370108666908]
GoogleのV8ヒープサンドボックスは、ChromiumベースのすべてのブラウザとNode$.jsとElectron上に構築された数え切れないほど多くのユーザを保護する。
広く使われているにもかかわらず、そのようなSFI機構はセキュリティテストはほとんど行われていない。
本稿では,現代のSFI実装のセキュリティ境界をモデル化する新しいテスト手法を提案する。
論文 参考訳（メタデータ） (2025-09-09T13:56:17Z) - 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) - CAIBA: Multicast Source Authentication for CAN Through Reactive Bit Flipping [5.997426999817119]
コントローラエリアネットワーク(Controller Area Networks、CAN)は、車内通信のバックボーンである。
近年のサイバー攻撃はCANの弱点を露呈し、1980年代にはセキュリティ上の考慮なしに設計された。
我々は,CANのような通信バス向けに設計された,新しいマルチキャストソース認証方式であるCAIBAを提案する。
論文 参考訳（メタデータ） (2025-04-23T13:27:30Z) - On the Verification of Control Flow Attestation Evidence [9.30850875158975]
我々は、Vrfが受信した証拠を効果的に分析できれば、実行時の検証と監査は本当に役に立つと論じる。
Vrfによる実行時のエビデンスを実際に活用するためのケーススタディとして,SABRE: A Security Analysis and Binary repair Engineを提案する。
論文 参考訳（メタデータ） (2024-11-16T18:24:11Z) - Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。
SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。
我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
論文 参考訳（メタデータ） (2024-10-21T08:15:45Z) - Physical Layer Deception with Non-Orthogonal Multiplexing [52.11755709248891]
本稿では,ワイヤタッピングの試みに積極的に対処する物理層騙し(PLD)の枠組みを提案する。
PLDはPLSと偽装技術を組み合わせることで、積極的に盗聴の試みに対処する。
本研究では,PLDフレームワークの有効性を詳細な分析で証明し,従来のPLS手法よりも優れていることを示す。
論文 参考訳（メタデータ） (2024-06-30T16:17:39Z) - JustSTART: How to Find an RSA Authentication Bypass on Xilinx UltraScale(+) with Fuzzing [12.338137154105034]
7シリーズとUltraScale(+)FPGA構成エンジンのファジングについて検討する。
我々の目標は、FPGA構成エンジンの内部動作を分析し文書化するためのファジングの有効性を検討することである。
論文 参考訳（メタデータ） (2024-02-15T10:03:35Z) - Tamper-Evident Pairing [55.2480439325792]
Tamper-Evident Pairing (TEP)はPush-ButtonConfiguration (PBC)標準の改良である。
TEP は Tamper-Evident Announcement (TEA) に依存しており、相手が送信されたメッセージを検出せずに改ざんしたり、メッセージが送信された事実を隠蔽したりすることを保証している。
本稿では,その動作を理解するために必要なすべての情報を含む,TEPプロトコルの概要について概説する。
論文 参考訳（メタデータ） (2023-11-24T18:54:00Z) - (Security) Assertions by Large Language Models [25.270188328436618]
セキュリティのためのハードウェアアサーション生成において,コード生成に新たな大規模言語モデル(LLM)を用いることを検討する。
我々は、人気のあるLCMに注目し、プロンプトの様々なレベルの詳細を考慮し、アサーションを箱から書き出す能力を特徴付ける。
論文 参考訳（メタデータ） (2023-06-24T17:44:36Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。