論文の概要: SecRef*: Securely Sharing Mutable References Between Verified and Unverified Code in F*

• arxiv url: http://arxiv.org/abs/2503.00404v1
• Date: Sat, 01 Mar 2025 08:48:39 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-03-05 19:12:33.047098
• Title: SecRef*: Securely Sharing Mutable References Between Verified and Unverified Code in F*
• Title（参考訳）: SecRef*: F*の検証コードと未検証コードの間で、セキュアにミュータブルな参照を共有する
• Authors: Cezar-Constantin Andrici, Danel Ahman, Catalin Hritcu, Ruxandra Icleanu, Guido Martínez, Exequiel Rivas, Théo Winterhalter,
• Abstract要約: SecRef*は、F*で検証されたステートフルなプログラムを、リンクされた未検証コードから保護するフレームワークである。 SecRef*は、未検証のコードとの健全かつセキュアな相互運用性を保証する。
• 参考スコア（独自算出の注目度）: 0.16060719742433224
• License:
• Abstract: We introduce SecRef*, a secure compilation framework protecting stateful programs verified in F* against linked unverified code, with which the program dynamically shares ML-style mutable references. To ease program verification in this setting, we propose a way of tracking which references are shareable with the unverified code, and which ones are not shareable and whose contents are thus guaranteed to be unchanged after calling into unverified code. This universal property of non-shareable references is exposed in the interface on which the verified program can rely when calling into unverified code. The remaining refinement types and pre- and post-conditions that the verified code expects from the unverified code are converted into dynamic checks about the shared references by using higher-order contracts. We prove formally in F* that this strategy ensures sound and secure interoperability with unverified code. Since SecRef* is built on top of the Monotonic State effect of F*, these proofs rely on the first monadic representation for this effect, which is a contribution of our work that can be of independent interest. Finally, we use SecRef* to build a simple cooperative multi-threading scheduler that is verified and that securely interacts with unverified threads.
• Abstract（参考訳）: SecRef*は、F*で検証されたステートフルなプログラムを、リンクされた未検証コードに対して保護し、プログラムがMLスタイルの可変参照を動的に共有するセキュアなコンパイルフレームワークである。 この環境でのプログラム検証を容易にするため、未検証のコードと共有可能な参照と共有できない参照と、未検証のコードに呼び出した後に変更が保証されるコンテンツを追跡する方法を提案する。 この共有不能な参照の普遍性は、検証済みのプログラムが未検証のコードを呼び出す際に依存するインターフェースに露呈する。 検証済みコードが未検証コードから期待する残りの改善タイプと事前条件は、高次のコントラクトを使用して共有参照に関する動的チェックに変換される。 我々は、この戦略が未検証のコードとの健全かつセキュアな相互運用性を保証することを、F*で正式に証明しています。 SecRef* は F* のモノトニック状態効果の上に構築されているので、これらの証明はこの効果に対する最初のモナディック表現に依存している。 最後に、SecRef*を使って単純な協調型マルチスレッドスケジューラを構築します。

関連論文リスト

• METAMON: Finding Inconsistencies between Program Documentation and Behavior using Metamorphic LLM Queries [10.9334354663311]
  本稿では,既存の検索ベーステスト生成技術を用いて,現在のプログラム動作をテストケース形式でキャプチャするMETAMONを提案する。 MeTAMONはこのタスクでメタモルフィックテストと自己整合性によってサポートされている。 Defects4J v2.0.1の5つのオープンソースプロジェクトを使って生成された9,482対のコードドキュメンテーションとコードスニペットに対する実証的な評価は、METAMONがコードとドキュメントの不整合を精度0.72、リコール0.48で分類できることを示している。
  論文  参考訳（メタデータ） (2025-02-05T00:42:50Z)
• AutoDeduct: A Tool for Automated Deductive Verification of C Code [0.3518504468878697]
  私たちはFrama-Cフレームワーク上に構築されたAutoDeductツールチェーンを紹介します。 Cプログラムの関数のコントラクトを自動的に推論するテクニックの組み合わせを実装している。 AutoDeductの現在のリリースは、最初のパブリックプロトタイプである。
  論文  参考訳（メタデータ） (2025-01-18T22:00:43Z)
• SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations [0.15800607910450126]
  投機的意味論に基づくコンパイラ変換における非干渉保存の問題に対処する。 我々は,すべてのソースプログラムに対して一様に保存を保証できる検証方法を開発した。
  論文  参考訳（メタデータ） (2024-07-21T07:30:30Z)
• Smart Casual Verification of the Confidential Consortium Framework [2.160395257762205]
  Confidential Consortium Framework(CCF)は、信頼できる信頼性のあるクラウドアプリケーションを開発するためのオープンソースプラットフォームである。 CCFはMicrosoftのAzure Confidential Ledgerサービスを動かしている。 本稿では、CCFの新しい分散プロトコルの正当性を検証するために、スマートカジュアル検証を適用した経験を報告する。
  論文  参考訳（メタデータ） (2024-06-25T10:49:54Z)
• SECOMP: Formally Secure Compilation of Compartmentalized C Programs [2.5553752304478574]
  C言語の未定義の動作は、しばしば破壊的なセキュリティ脆弱性を引き起こす。 本稿では,機械チェックによるC言語のコンパイラSECOMPを紹介する。 このような強い基準が主流のプログラミング言語で証明されたのは、これが初めてです。
  論文  参考訳（メタデータ） (2024-01-29T16:32:36Z)
• Fake Alignment: Are LLMs Really Aligned Well? [91.26543768665778]
  本研究では,複数質問とオープンエンド質問の相違点について検討した。 ジェイルブレイク攻撃パターンの研究にインスパイアされた我々は、これが不一致の一般化によって引き起こされたと論じている。
  論文  参考訳（メタデータ） (2023-11-10T08:01:23Z)
• Not All Metrics Are Guilty: Improving NLG Evaluation by Diversifying References [123.39034752499076]
  Div-Refは、参照数を増やして評価ベンチマークを強化する方法である。 本研究では,参照表現の多様化が自動評価と人的評価の相関性を大幅に向上させることを示す実験を行った。
  論文  参考訳（メタデータ） (2023-05-24T11:53:29Z)
• RepoCoder: Repository-Level Code Completion Through Iterative Retrieval and Generation [96.75695811963242]
  RepoCoderはリポジトリレベルのコード補完プロセスを合理化するフレームワークである。 類似性ベースのレトリバーと、事前訓練されたコード言語モデルが組み込まれている。 バニラ検索で拡張されたコード補完アプローチよりも一貫して優れています。
  論文  参考訳（メタデータ） (2023-03-22T13:54:46Z)
• CoCoMIC: Code Completion By Jointly Modeling In-file and Cross-file Context [82.88371379927112]
  予め訓練されたコード LM 上で,ファイル内コンテキストとファイル内コンテキストを協調的に学習するための,クロスファイルコンテキストを組み込んだフレームワークを提案する。 CoCoMICは既存のコードLMを33.94%の精度で改善し、クロスファイルコンテキストが提供されるとコード補完のための識別子マッチングが28.69%増加した。
  論文  参考訳（メタデータ） (2022-12-20T05:48:09Z)
• Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
  完全同型暗号方式として, 完全同型暗号方式を初めて構築する。 我々の主要な技術要素は、量子証明器が古典的検証器に量子状態の形でのLearning with Errors分布からのサンプルが削除されたことを納得させる対話的プロトコルである。
  論文  参考訳（メタデータ） (2022-03-03T10:07:32Z)
• Deep Just-In-Time Inconsistency Detection Between Comments and Source Code [51.00904399653609]
  本稿では,コード本体の変更によりコメントが矛盾するかどうかを検出することを目的とする。 私たちは、コメントとコードの変更を関連付けるディープラーニングアプローチを開発しています。 より包括的な自動コメント更新システムを構築するために,コメント更新モデルと組み合わせて提案手法の有用性を示す。
  論文  参考訳（メタデータ） (2020-10-04T16:49:28Z)

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

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