論文の概要: OpenBSD formal driver verification with SeL4

• arxiv url: http://arxiv.org/abs/2311.03585v1
• Date: Mon, 6 Nov 2023 22:35:53 GMT
• ステータス: 処理完了
• システム内更新日: 2024-03-25 13:36:10.748740
• Title: OpenBSD formal driver verification with SeL4
• Title（参考訳）: SeL4によるOpenBSDの正式なドライバ検証
• Authors: Adriana Nicolae, Paul Irofti, Ioana Leustean,
• Abstract要約: ソフトウェアコンポーネントの適切な検証は、ハードウェアの故障がない限り、デバイスが適切に動作することを保証する。 本稿では,デバイスドライバの動作をモデル化し,コード実装が期待する動作と一致することを示す。 証明はIsabelle/HOLで書かれており、CからIsabelleへのコード変換はC-to-IsabelleとAutoCorresツールを使用して自動的に行われる。
• 参考スコア（独自算出の注目度）: 1.747820331822631
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The seL4 microkernel is currently the only kernel that has been fully formally verified. In general, the increased interest in ensuring the security of a kernel's code results from its important role in the entire operating system. One of the basic features of an operating system is that it abstracts the handling of devices. This abstraction is represented by device drivers - the software that manages the hardware. A proper verification of the software component could ensure that the device would work properly unless there is a hardware failure.In this paper, we choose to model the behavior of a device driver and build the proof that the code implementation matches the expected behavior. The proof was written in Isabelle/HOL, the code translation from C to Isabelle was done automatically by the use of the C-to-Isabelle Parser and AutoCorres tools. We choose Isabelle theorem prover because its efficiency was already shown through the verification of seL4 microkernel.
• Abstract（参考訳）: seL4マイクロカーネルは現在、完全に公式に認証されている唯一のカーネルである。 一般に、カーネルのコードのセキュリティを確保することへの関心は、オペレーティングシステム全体において重要な役割を担っている。 オペレーティングシステムの基本的な特徴の1つは、デバイスのハンドリングを抽象化することである。 この抽象化は、ハードウェアを管理するソフトウェアであるデバイスドライバによって表現される。 ソフトウェアコンポーネントの適切な検証により,ハードウェアの故障がない限り,デバイスが正常に動作することを保証する。この記事では,デバイスドライバの動作をモデル化し,コード実装が期待する動作と一致することを示す。 この証明はIsabelle/HOLで書かれており、CからIsabelleへのコード変換はC-to-Isabelle ParserとAutoCorresツールを使用して自動的に行われる。 我々は、seL4マイクロカーネルの検証により、その効率が既に示されていたため、イザベルの定理証明器を選択する。

関連論文リスト

• Verifying Non-friendly Formal Verification Designs: Can We Start Earlier? [2.1626093085892144]
  本稿では,2つの主要なステップからなるメタモデリング技術に基づく自動手法を提案する。 まず、C++で書かれた未使用のアルゴリズム記述を、生成されたアサーションを使用して早期に検証する。 第2に、HLECとそのメタモデルパラメータを用いて、このアルゴリズム記述をシーケンシャルな設計に対して検証する。
  論文  参考訳（メタデータ） (2024-10-24T06:09:40Z)
• LLM-DetectAIve: a Tool for Fine-Grained Machine-Generated Text Detection [87.43727192273772]
  テキストが人間の書いたものなのか、機械で作られたものなのかを判断するのは、しばしば困難である。 細粒度検出のためのLLM-DetectAIveを提案する。 i) 人書き、ii) 機械生成、(iii) 機械書、次いで機械書、(iv) 人書き、そして機械ポリッシュの4つのカテゴリをサポートする。
  論文  参考訳（メタデータ） (2024-08-08T07:43:17Z)
• SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations [0.15800607910450126]
  投機的意味論に基づくコンパイラ変換における非干渉保存の問題に対処する。 我々は,すべてのソースプログラムに対して一様に保存を保証できる検証方法を開発した。
  論文  参考訳（メタデータ） (2024-07-21T07:30:30Z)
• 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)
• Selene: Pioneering Automated Proof in Software Verification [62.09555413263788]
  実世界の産業レベルのマイクロカーネルであるseL4をベースとした,最初のプロジェクトレベルの自動証明ベンチマークであるSeleneを紹介する。 GPT-3.5-turbo や GPT-4 のような先進的な大規模言語モデル (LLM) による実験結果から, 自動証明生成領域における LLM の機能を強調した。
  論文  参考訳（メタデータ） (2024-01-15T13:08:38Z)
• KernelGPT: Enhanced Kernel Fuzzing via Large Language Models [8.77369393651381]
  我々はLarge Language Models (LLM) を通じてsyscall仕様を自動合成する最初のアプローチである KernelGPT を提案する。 以上の結果から, KernelGPTは最新の技術よりも, より新しい, 有効な仕様を作成できることを示す。
  論文  参考訳（メタデータ） (2023-12-31T18:47:33Z)
• Chain of Code: Reasoning with a Language Model-Augmented Code Emulator [115.16975276693267]
  我々は、LMコード駆動推論を改善するシンプルながら驚くほど効果的な拡張であるChain of Codeを提案する。 キーとなるアイデアは、プログラム内のセマンティックなサブタスクを、インタープリタが明示的にキャッチできるフレキシブルな擬似コードとしてフォーマットすることを、LMに促すことである。
  論文  参考訳（メタデータ） (2023-12-07T17:51:43Z)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。 本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。 我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
  論文  参考訳（メタデータ） (2023-10-23T17:58:40Z)
• (Security) Assertions by Large Language Models [25.270188328436618]
  セキュリティのためのハードウェアアサーション生成において,コード生成に新たな大規模言語モデル(LLM)を用いることを検討する。 我々は、人気のあるLCMに注目し、プロンプトの様々なレベルの詳細を考慮し、アサーションを箱から書き出す能力を特徴付ける。
  論文  参考訳（メタデータ） (2023-06-24T17:44:36Z)
• Lessons from Formally Verified Deployed Software Systems (Extended version) [65.69802414600832]
  本稿は、正式に認証されたシステムを作成し、実際に使用するためにデプロイした各種のアプリケーション分野のプロジェクトについて検討する。 使用する技術、適用の形式、得られた結果、そしてソフトウェア産業が形式的な検証技術やツールの恩恵を受ける能力について示すべき教訓を考察する。
  論文  参考訳（メタデータ） (2023-01-05T18:18:46Z)
• CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives (full version) [12.790826917588575]
  暗号は例外であり、多くのパフォーマンスクリティカルなルーチンがアセンブリで直接書かれてきた。 CryptOptは、GCCやClangが生成するものよりもはるかに高速なアセンブリコードに高レベルの暗号関数プログラムを専門とする、最初のコンパイルパイプラインである。 形式検証の面では、FiatOptフレームワーク(関数型プログラムをCライクなIRコードに変換する)に接続し、新たに公式に認証されたプログラム等価チェッカーで拡張する。
  論文  参考訳（メタデータ） (2022-11-19T11:07:39Z)

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

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