論文の概要: 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マイクロカーネルの検証により、その効率が既に示されていたため、イザベルの定理証明器を選択する。
関連論文リスト
- Selene: Pioneering Automated Proof in Software Verification [69.7891799471749]
我々は,seL4オペレーティングシステムマイクロカーネルの実際の産業レベルのプロジェクトに基づいて構築された,最初のプロジェクトレベルの自動証明ベンチマークであるSeleneを紹介する。
GPT-3.5-turbo や GPT-4 のような先進的な LLM による実験結果は,自動証明生成領域における大規模言語モデル (LLM) の機能を強調した。
論文 参考訳(メタデータ) (2024-01-15T13:08:38Z) - KernelGPT: Enhanced Kernel Fuzzing via Large Language Models [9.860752730040709]
本稿では,Syzkaller仕様をLarge Language Modelsを介して自動推論する最初のアプローチであるKernelGPTを提案する。
予備的な結果から、KernelGPTは、Syzkallerがより高いカバレッジを達成し、これまで知られていなかった複数のバグを見つけるのに役立ちます。
論文 参考訳(メタデータ) (2023-12-31T18:47:33Z) - Chain of Code: Reasoning with a Language Model-Augmented Code Emulator [119.0018170558366]
言語モデル(LM)はコード記述を活用して思考の連鎖推論を改善する。
我々は、LMコード駆動推論を改善するシンプルな、そして驚くほど効果的な拡張であるChain of Code (CoC)を提案する。
CoCは、大小のモデルと同様の規模でスケールし、LMが「コードを考える」ことで正しく答えられるような推論の問題の範囲を広げる。
論文 参考訳(メタデータ) (2023-12-07T17:51:43Z) - Abusing Processor Exception for General Binary Instrumentation on Bare-metal Embedded Devices [11.520387655426521]
PIFER (Practical Instrumenting Framework for Embedded fiRmware) は、組み込みベアメタルファームウェアに対して、汎用的できめ細かな静的バイナリーインスツルメンテーションを可能にする。
本稿では,修正後のファームウェアの正しい実行を保証するための命令翻訳方式を提案する。
論文 参考訳(メタデータ) (2023-11-28T05:32:20Z) - Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [102.00359477458029]
本稿では,ニューラル・シンボリック統合法について述べる。
LLMフリーのシンボリック・ソルバを用いて、知識を用いた熟考的推論を行う。
論文 参考訳(メタデータ) (2023-11-16T11:26:21Z) - 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) - An Extendable Python Implementation of Robust Optimisation Monte Carlo [0.0]
本稿では,PythonパッケージELFIにおけるロバスト最適化モンテカルロ(ROMC)の実装について述べる。
ROMCは、後方から正確な重み付けされたサンプルを提供する、新しくて効率的な(高い並列化が可能な)LFIフレームワークである。
論文 参考訳(メタデータ) (2023-09-19T13:37:47Z) - LLM-assisted Generation of Hardware Assertions [0.0]
セキュリティのためのハードウェアアサーション生成において,コード生成に新たな大規模言語モデル(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) - Level 2 Autonomous Driving on a Single Device: Diving into the Devils of
Openpilot [112.21008828205409]
Comma.aiは、1台のカメラとボードを内蔵した999ドルのアフターマーケットデバイスがL2シナリオを処理する能力を持っていると主張している。
Comma.aiがリリースした全システムのオープンソースソフトウェアとともに、プロジェクトはOpenpilotと名付けられた。
このレポートでは、最新の知見を公開し、産業製品レベルでのエンドツーエンドの自動運転という、新たな視点について光を当てたいと思います。
論文 参考訳(メタデータ) (2022-06-16T13:43:52Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。