論文の概要: Misquoted No More: Securely Extracting F* Programs with IO

• arxiv url: http://arxiv.org/abs/2602.19973v1
• Date: Mon, 23 Feb 2026 15:37:18 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-02-24 17:42:02.885344
• Title: Misquoted No More: Securely Extracting F* Programs with IO
• Title（参考訳）: Misquoted No More: IOでF*プログラムを安全に抽出する
• Authors: Cezar-Constantin Andrici, Abigail Pribisova, Danel Ahman, Catalin Hritcu, Exequiel Rivas, Théo Winterhalter,
• Abstract要約: 効果を表すモナドを使用する浅層埋め込みは、証明指向言語で人気がある。 浅い組込みプログラムが検証されると、しばしばOCamlやCのような主流言語に抽出される。 私たちはこのアイデアに基づいていますが、翻訳バリデーションの使用を最初の抽出ステップに制限します。
• 参考スコア（独自算出の注目度）: 0.3848364262836075
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Shallow embeddings that use monads to represent effects are popular in proof-oriented languages because they are convenient for formal verification. Once shallowly embedded programs are verified, they are often extracted to mainstream languages like OCaml or C and linked into larger codebases. The extraction process is not fully verified because it often involves quotation -- turning the shallowly embedded program into a deeply embedded one -- and verifying quotation remains a major open challenge. Instead, some prior work obtains formal correctness guarantees using translation validation to certify individual extraction results. We build on this idea, but limit the use of translation validation to a first extraction step that we call relational quotation and that uses a metaprogram to construct a typing derivation for the given shallowly embedded program. This metaprogram is simple, since the typing derivation follows the structure of the original program. Once we validate, syntactically, that the typing derivation is valid for the original program, we pass it to a verified syntax-generation function that produces code guaranteed to be semantically related to the original program. We apply this general idea to build SEIO*, a framework for extracting shallowly embedded F* programs with IO to a deeply embedded lambda-calculus while providing formal secure compilation guarantees. Using two cross-language logical relations, we devise a machine-checked proof in F* that SEIO* guarantees Robust Relational Hyperproperty Preservation (RrHP), a very strong secure compilation criterion that implies full abstraction as well as preservation of trace properties and hyperproperties against arbitrary adversarial contexts. This goes beyond the state of the art in verified and certifying extraction, which so far has focused on correctness rather than security.
• Abstract（参考訳）: 効果を表すモナドを用いた浅層埋め込みは、形式的検証に便利なため、証明指向言語で人気がある。 浅い組込みプログラムが検証されると、しばしばOCamlやCのような主流言語に抽出され、より大きなコードベースにリンクされる。 抽出プロセスが完全には検証されていないのは、しばしば引用(浅く埋め込まれたプログラムを深く埋め込まれたプログラムに変える)が伴うためであり、引用を検証することが大きな課題である。 代わりに、いくつかの先行研究は、個々の抽出結果を認証するために翻訳バリデーションを使用して正式な正当性を保証する。 このアイデアに基づいて構築するが、翻訳バリデーションの使用をリレーショナルクォーテーションと呼ばれる最初の抽出ステップに制限し、メタプログラムを使用して、与えられた浅層プログラムのタイピング導出を構築する。 このメタプログラミングは、タイピングの派生が元のプログラムの構造に従うため、単純である。 構文的に、入力導出が元のプログラムに有効であることを検証したら、元のプログラムに意味論的に関連があることが保証されたコードを生成する検証された構文生成関数に渡す。 この一般的な考え方を応用してSEIO*を構築する。これは、IOで浅い埋め込みF*プログラムを、正式なセキュアなコンパイル保証を提供しながら、深く埋め込まれたラムダ計算に抽出するフレームワークである。 2つの言語間の論理的関係を用いて、SEIO*がRobost Relational Hyperproperty Preservation (RrHP)を保証しているというF*のマシンチェック証明を考案した。 これは、これまでセキュリティよりも正確性に重点を置いてきた、認証と認証の抽出における最先端以上のものだ。

関連論文リスト

• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。 提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
  論文  参考訳（メタデータ） (2025-11-26T06:39:19Z)
• zkStruDul: Programming zkSNARKs with Structural Duality [0.2449909275410287]
  zkStruDulは、入力変換を統一し、定義を単一の複合抽象化に述語する言語である。 我々は、ソースレベルのセマンティクスを提供し、その振る舞いが予測されたセマンティクスと同一であることを証明する。
  論文  参考訳（メタデータ） (2025-11-13T18:06:21Z)
• Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
  本稿では,検証対応言語における仕様の質を評価するための指標を提案する。 MBPPコード生成ベンチマークのDafny仕様の人間ラベル付きデータセットに,我々の測定値が密接に一致することを示す。 また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。
  論文  参考訳（メタデータ） (2024-06-14T06:52:08Z)
• FoC: Figure out the Cryptographic Functions in Stripped Binaries with LLMs [51.898805184427545]
  削除されたバイナリの暗号関数を抽出するFoCと呼ばれる新しいフレームワークを提案する。 まず、自然言語における暗号関数のセマンティクスを要約するために、バイナリ大言語モデル(FoC-BinLLM)を構築した。 次に、FoC-BinLLM上にバイナリコード類似モデル(FoC-Sim)を構築し、変更に敏感な表現を作成し、データベース内の未知の暗号関数の類似実装を検索する。
  論文  参考訳（メタデータ） (2024-03-27T09:45:33Z)
• SECOMP: Formally Secure Compilation of Compartmentalized C Programs [2.5553752304478574]
  C言語の未定義の動作は、しばしば破壊的なセキュリティ脆弱性を引き起こす。 本稿では,機械チェックによるC言語のコンパイラSECOMPを紹介する。 このような強い基準が主流のプログラミング言語で証明されたのは、これが初めてです。
  論文  参考訳（メタデータ） (2024-01-29T16:32:36Z)
• 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)

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

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