論文の概要: Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs

• arxiv url: http://arxiv.org/abs/2503.19609v1
• Date: Tue, 25 Mar 2025 12:50:35 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-03-26 16:53:13.138047
• Title: Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs
• Title（参考訳）: 機械化セキュアコンパイル証明のためのコールリターン木のナノパスバックトランスレーション
• Authors: Jérémy Thibault, Joseph Lenormand, Catalin Hritcu,
• Abstract要約: 研究者は、ソースコンテキストがソースプログラムに対してマウントされるような攻撃がなければ、セキュアなコンパイルチェーンを構築することを目指している。 ターゲットのコンテキストをコンパイルされたプログラムにマウントするには、ソースプログラムに同じアタックをマウントしたソースコンテキストを表示する必要がある。 本稿では,より簡単な証明を証明アシスタントでより容易に行うことができる新しいバックトランスレーション手法について述べる。
• 参考スコア（独自算出の注目度）: 0.07499722271664144
• License:
• Abstract: Researchers aim to build secure compilation chains enforcing that if there is no attack a source context can mount against a source program then there is also no attack an adversarial target context can mount against the compiled program. Proving that these compilation chains are secure is, however, challenging, and involves a non-trivial back-translation step: for any attack a target context mounts against the compiled program one has to exhibit a source context mounting the same attack against the source program. We describe a novel back-translation technique, which results in simpler proofs that can be more easily mechanized in a proof assistant. Given a finite set of finite trace prefixes, capturing the interaction recorded during an attack between a target context and the compiled program, we build a call-return tree that we back-translate into a source context producing the same trace prefixes. We use state in the generated source context to record the current location in the call-return tree. The back-translation is done in several small steps, each adding to the tree new information describing how the location should change depending on how the context regains control. To prove this back-translation correct we give semantics to every intermediate call-return tree language, using ghost state to store information and explicitly enforce execution invariants. We prove several small forward simulations, basically seeing the back-translation as a verified nanopass compiler. Thanks to this modular structure, we are able to mechanize this complex back-translation and its correctness proof in the Rocq prover without too much effort.
• Abstract（参考訳）: 研究者は、ソース・コンテクストがソース・プログラムに対してマウントされない場合、敵のターゲット・コンテクストがコンパイルされたプログラムに対してマウントできるアタックが存在しないことを強制して、セキュアなコンパイル・チェーンを構築することを目指している。 しかし、これらのコンパイルチェーンがセキュアであることを証明することは困難であり、非自明なバックトランスレーションステップを伴う: コンパイルされたプログラムに対してターゲットコンテキストがマウントされた場合、ソースプログラムに対して同じアタックを組み込んだソースコンテキストを表示する必要がある。 本稿では,より簡単な証明を証明アシスタントでより容易に行うことができる新しいバックトランスレーション手法について述べる。 有限個のトレースプレフィックスが与えられた場合、ターゲットコンテキストとコンパイルされたプログラム間の攻撃中に記録されたインタラクションをキャプチャし、同じトレースプレフィックスを生成するソースコンテキストにバック翻訳するコール-リターンツリーを構築する。 生成されたソースコンテキストの状態を使用して、コール・リターンツリーの現在の位置を記録します。 バックトランスレーションはいくつかの小さなステップで行われ、それぞれが、コンテキストが制御を回復する方法に応じて、どのように場所を変更するべきかを記述する新しい情報を追加する。 このバックトランスレーションの正当性を証明するために、ゴーストステートを使用して情報を格納し、実行不変性を明示的に強制する、すべての中間的なコール・リターンツリー言語にセマンティクスを与える。 我々は、バックトランスレーションを検証されたナノパスコンパイラと見なして、いくつかの小さなフォワードシミュレーションを証明した。 このモジュラ構造のおかげで、この複雑なバックトランスレーションと、Rocq証明器におけるその正当性証明を、あまり努力することなく機械化することができる。

関連論文リスト

• ReF Decompile: Relabeling and Function Call Enhanced Decompile [50.86228893636785]
  逆コンパイルの目標は、コンパイルされた低レベルコード(アセンブリコードなど)を高レベルプログラミング言語に変換することである。 このタスクは、脆弱性識別、マルウェア分析、レガシーソフトウェアマイグレーションなど、さまざまなリバースエンジニアリングアプリケーションをサポートする。
  論文  参考訳（メタデータ） (2025-02-17T12:38:57Z)
• Syzygy: Dual Code-Test C to (safe) Rust Translation using LLMs and Dynamic Analysis [8.361424157571468]
  Syzygyは、C言語を安全なRustに変換する自動化アプローチである。 これは、Rustのコード翻訳を安全にする上で、これまでで最大の自動化およびテスト検証済みのCである。
  論文  参考訳（メタデータ） (2024-12-18T18:55:46Z)
• SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations [0.15800607910450126]
  投機的意味論に基づくコンパイラ変換における非干渉保存の問題に対処する。 我々は,すべてのソースプログラムに対して一様に保存を保証できる検証方法を開発した。
  論文  参考訳（メタデータ） (2024-07-21T07:30:30Z)
• Unsupervised Sign Language Translation and Generation [72.01216288379072]
  教師なし手話翻訳・生成ネットワーク(USLNet)を導入する。 USLNetは、並列手話データなしで、豊富な単一モダリティ(テキストとビデオ)データから学習する。 可変長テキストとビデオシーケンスの整合性の問題に対処するスライディングウインドウ手法を提案する。
  論文  参考訳（メタデータ） (2024-02-12T15:39:05Z)
• CRIL: A Concurrent Reversible Intermediate Language [0.0]
  本稿では,高レベル並列言語を他の低レベル並列言語に翻訳するための構成の可逆中間言語を提案し,可逆性を維持する。 機能的可逆言語としてMogensen が用いた RIL の拡張として CRIL を提案し,P-V 演算に基づくマルチスレッドプロセス呼び出しと同期プリミティブを組み込んだ。
  論文  参考訳（メタデータ） (2023-09-13T20:52:54Z)
• Outline, Then Details: Syntactically Guided Coarse-To-Fine Code Generation [61.50286000143233]
  ChainCoderは、Pythonコードを段階的に生成するプログラム合成言語モデルである。 自然言語記述と構文的に整合したI/Oデータサンプルを共同で符号化するために、カスタマイズされたトランスフォーマーアーキテクチャを利用する。
  論文  参考訳（メタデータ） (2023-04-28T01:47:09Z)
• Summarize and Generate to Back-translate: Unsupervised Translation of Programming Languages [86.08359401867577]
  バックトランスレーションは、並列データがほとんど、あるいは全く利用できない場合のニューラルマシン翻訳の有効性で広く知られている。 コード要約と生成による逆翻訳を提案する。 提案手法は最先端の手法と競合することを示す。
  論文  参考訳（メタデータ） (2022-05-23T08:20:41Z)
• Reflective Decoding: Beyond Unidirectional Generation with Off-the-Shelf Language Models [63.808843089941405]
  大規模な事前訓練された言語モデル(LM)は、顕著な品質のテキストを生成するが、左から右へ連続的にしか生成しない。 非順序タスクへの一方向LMの直接適用を可能にする新しい教師なしアルゴリズムであるReflective Decodingを提案する。 2段階のアプローチでは、監視もパラレルコーパスも必要ありません。
  論文  参考訳（メタデータ） (2020-10-16T18:02:07Z)
• Contrastive Code Representation Learning [95.86686147053958]
  一般的な再構成に基づくBERTモデルは,ソースコードの編集に敏感であることを示す。 コントラコード(ContraCode)は、コード機能を学ぶのにフォームではなく、コントラスト的な事前学習タスクである。
  論文  参考訳（メタデータ） (2020-07-09T17:59:06Z)

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

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