論文の概要: Verifying Device Drivers with Pancake

• arxiv url: http://arxiv.org/abs/2501.08249v1
• Date: Tue, 14 Jan 2025 16:40:05 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-01-15 13:27:59.184969
• Title: Verifying Device Drivers with Pancake
• Title（参考訳）: パンケーキによるデバイスドライバの検証
• Authors: Junming Zhao, Alessandro Legnani, Tiana Tsang Ung, H. Truong, Tsun Wang Sau, Miki Tanaka, Johannes Åman Pohjola, Thomas Sewell, Rob Sison, Hira Syeda, Magnus Myreen, Michael Norrish, Gernot Heiser,
• Abstract要約: Pancakeはシステムプログラミングのための命令型言語で、よく定義され、検証しやすいセマンティクスを備えている。 我々は、バイナリがソースコードのセマンティクスを保持することを保証するPancake用のコンパイラを開発する。 そこで我々は,PancakeのVier SMTフロントエンドへの自動翻訳を行い,Ethernet NICの性能検証を行った。
• 参考スコア（独自算出の注目度）: 31.430399514484368
• License:
• Abstract: Device driver bugs are the leading cause of OS compromises, and their formal verification is therefore highly desirable. To the best of our knowledge, no realistic and performant driver has been verified for a non-trivial device. We propose Pancake, an imperative language for systems programming that features a well-defined and verification-friendly semantics. Leveraging the verified compiler backend of the CakeML functional language, we develop a compiler for Pancake that guarantees that the binary retains the semantics of the source code. Usng automatic translation of Pancake to the Viper SMT front-end, we verify a performant driver for an Ethernet NIC.
• Abstract（参考訳）: デバイスドライバのバグはOSの妥協の主な原因であり、正式な検証は非常に望ましい。 我々の知る限りでは、非自明なデバイスに対して、現実的でパフォーマンスの高いドライバーは確認されていない。 本稿では,システムプログラミングのための命令型言語であるPancakeを提案する。 CakeML関数言語の検証済みコンパイラバックエンドを活用することで、バイナリがソースコードのセマンティクスを保持することを保証するPancake用のコンパイラを開発する。 そこで我々は,PancakeのVier SMTフロントエンドへの自動翻訳を行い,Ethernet NICの性能検証を行った。

関連論文リスト

• Assured Automatic Programming via Large Language Models [8.006578501857447]
  我々は,その意図に適合するコードを生成しつつ,プログラマの意図を発見することを目的としている。 本研究の目的は,ユーザ意図の理解を深めることによって,プログラム,仕様,テスト間の一貫性を実現することである。 提案手法によって発見された曖昧な意図が,検証可能な自動生成プログラムの割合をいかに高めるかを示す。
  論文  参考訳（メタデータ） (2024-10-24T07:29:15Z)
• Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
  本稿では,検証対応言語における仕様の質を評価するための指標を提案する。 MBPPコード生成ベンチマークのDafny仕様の人間ラベル付きデータセットに,我々の測定値が密接に一致することを示す。 また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。
  論文  参考訳（メタデータ） (2024-06-14T06:52:08Z)
• MambaByte: Token-free Selective State Space Model [71.90159903595514]
  マンババイト(英: MambaByte)は、マンバSSMがバイト配列で自己回帰的に訓練したトークンレス適応である。 MambaByteは、言語モデリングタスクにおいて、最先端のサブワードトランスフォーマーよりも優れています。
  論文  参考訳（メタデータ） (2024-01-24T18:53:53Z)
• OpenBSD formal driver verification with SeL4 [1.747820331822631]
  ソフトウェアコンポーネントの適切な検証は、ハードウェアの故障がない限り、デバイスが適切に動作することを保証する。 本稿では,デバイスドライバの動作をモデル化し,コード実装が期待する動作と一致することを示す。 証明はIsabelle/HOLで書かれており、CからIsabelleへのコード変換はC-to-IsabelleとAutoCorresツールを使用して自動的に行われる。
  論文  参考訳（メタデータ） (2023-11-06T22:35:53Z)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。 コントローラと証明書を形式的に合成する自動化手法を提案する。 我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
  論文  参考訳（メタデータ） (2023-09-12T09:37:26Z)
• (Security) Assertions by Large Language Models [25.270188328436618]
  セキュリティのためのハードウェアアサーション生成において,コード生成に新たな大規模言語モデル(LLM)を用いることを検討する。 我々は、人気のあるLCMに注目し、プロンプトの様々なレベルの詳細を考慮し、アサーションを箱から書き出す能力を特徴付ける。
  論文  参考訳（メタデータ） (2023-06-24T17:44:36Z)
• Code-Switching without Switching: Language Agnostic End-to-End Speech Translation [68.8204255655161]
  我々は音声認識と翻訳を一貫したエンドツーエンドの音声翻訳問題として扱う。 LASTを両方の入力言語で訓練することにより、入力言語に関係なく、音声を1つのターゲット言語にデコードする。
  論文  参考訳（メタデータ） (2022-10-04T10:34:25Z)
• Faith: An Efficient Framework for Transformer Verification on GPUs [27.363093119720723]
  本稿では,GPU上でのトランスフォーマー検証のための効率的なフレームワークであるFaithを提案する。 我々はセマンティック情報を利用して,計算グラフレベルでの効率的なカーネル融合を実現する。 Faithは最先端のフレームワークよりも2.1times$から3.4times$(2.6times$)のスピードアップを達成した。
  論文  参考訳（メタデータ） (2022-09-23T15:07:22Z)
• Auditing AI models for Verified Deployment under Semantic Specifications [65.12401653917838]
  AuditAIは、解釈可能な形式検証とスケーラビリティのギャップを埋める。 AuditAIは、画素空間の摂動のみを用いた検証の限界に対処しながら、検証と認定トレーニングのための制御されたバリエーションを得られるかを示す。
  論文  参考訳（メタデータ） (2021-09-25T22:53:24Z)
• Worse WER, but Better BLEU? Leveraging Word Embedding as Intermediate in Multitask End-to-End Speech Translation [127.54315184545796]
  音声翻訳(ST)は、ソース言語の音声からターゲット言語のテキストへの変換を学習することを目的としている。 単語埋め込みを中間語として活用することでマルチタスクSTモデルを改善することを提案する。
  論文  参考訳（メタデータ） (2020-05-21T14:22:35Z)

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

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