論文の概要: 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検証器が受信したプログラムがメモリに読み書きされないことを正式に検証する。
関連論文リスト
- 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。