Fugu-MT 論文翻訳(概要): Verifying Device Drivers with Pancake

論文の概要: 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 17:02:04.553967
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: http://creativecommons.org/licenses/by-sa/4.0/
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の性能検証を行った。

関連論文リスト

C*: Unifying Programming and Verification in C [15.531046191957529]
C* は C プログラミングのための言語設計の証明である。プログラマが実装コードと並行して証明コードブロックを埋め込むことで、リアルタイムの検証を可能にする。 C* は C を共通言語として使用することで実装と証明コード開発を統合する。
論文参考訳（メタデータ） (2025-04-03T03:22:22Z)
AutoDeduct: A Tool for Automated Deductive Verification of C Code [0.3518504468878697]
私たちはFrama-Cフレームワーク上に構築されたAutoDeductツールチェーンを紹介します。 Cプログラムの関数のコントラクトを自動的に推論するテクニックの組み合わせを実装している。 AutoDeductの現在のリリースは、最初のパブリックプロトタイプである。
論文参考訳（メタデータ） (2025-01-18T22:00:43Z)
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)
Improving Instruction-Following in Language Models through Activation Steering [58.876600545898675]
命令固有ベクトル表現を言語モデルから導出し,それに従ってモデルをステアリングする。提案手法は,出力形式や長さ,単語の包摂といった制約に対するモデル適合性をいかに向上させるかを示す。本研究は,アクティベーションステアリングが言語生成におけるきめ細かい制御に実用的でスケーラブルなアプローチを提供することを示す。
論文参考訳（メタデータ） (2024-10-15T08:38:20Z)
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)
(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)
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)

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