論文の概要: Finding a Crab in the C: Assured Translation via Comparative Symbolic Execution

• arxiv url: http://arxiv.org/abs/2605.12731v1
• Date: Tue, 12 May 2026 20:33:33 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-14 23:30:27.6789
• Title: Finding a Crab in the C: Assured Translation via Comparative Symbolic Execution
• Title（参考訳）: C言語のクレーブを見つける: 比較記号的実行による保証翻訳
• Authors: Caleb Helbling, Graham Leach-Krouse, Michael Crystal,
• Abstract要約: cozyは、"安全でない"ソースコードからコンパイルされたバイナリと、ソースコードのメモリセーフ言語への変換からコンパイルされたバイナリを分析する、比較バイナリ分析ツールである。 cozyは2つのバイナリの動作の差異を開発者に向かって歩き、それぞれの違いを示し、ユーザがその違いが意図的(良い)かどうかを判断するように求めます。 Cozyは自動翻訳、バグ修正、コードレビュー、オペレーション認可、自動翻訳に応用できる。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Modern high-assurance software systems development favors memory safe languages such as SPARK (ADA) or Rust. However, developers often encounter non-memory safe code (e.g., C) in legacy systems and libraries which would be prohibitively expensive or risky to re-write. In response, developers have begun turning to machine learning/AI systems and other automated code translators. Automated translation comes with its own risks, however. The original and ported code are not precisely the same, semantically - otherwise there would be no point in performing the translation. To reduce these risks, we have developed cozy, a comparative binary analysis tool that simultaneously analyzes a binary compiled from "unsafe" source code and a binary compiled from a translation of the source code to a memory safe language. cozy walks the developer through differences in the behavior of the two binaries, presenting each difference and asking the user to assess whether the difference is intentional (good) or erroneous. Outside of the flagged differences, the binaries are formally verified to be equivalent. Consequently, the review process guarantees equivalence modulo changes approved by the developer. cozy has applications to automated translation, bug correction, code reviews, operation authorization, and automatic translation.
• Abstract（参考訳）: 現代の高可用性ソフトウェアシステムは、SPARK(ADA)やRustのようなメモリセーフな言語を好む。 しかし、開発者はレガシシステムやライブラリで非メモリセーフなコード(例えばC)に遭遇することが多い。 これに反応して、開発者は機械学習/AIシステムや他の自動コードトランスレータに移行し始めた。 しかし、自動翻訳には独自のリスクがある。 オリジナルのコードと移植されたコードは、正確には同じではなく、意味的に同じではない。 ソースコードからコンパイルされたバイナリと、ソースコードからメモリセーフ言語への変換からコンパイルされたバイナリを同時に解析する比較バイナリ解析ツールであるcozyを開発した。 cozyは2つのバイナリの動作の差異を開発者に向かって歩き、それぞれの違いを示し、ユーザがその違いが意図的(良い)かどうかを判断するように求めます。 フラグ付きの違い以外では、バイナリは正式に等価であると確認されている。 これにより、レビュープロセスは、開発者が承認した同値モジュロ変更を保証する。 Cozyは自動翻訳、バグ修正、コードレビュー、オペレーション認可、自動翻訳に応用できる。

関連論文リスト

• Deterministic Fully-Static Whole-Binary Translation without Heuristics [4.112095753709181]
  Elevatorはx86-64実行ファイル全体をAArch64デバッグ情報、ソースコード、コードレイアウトに関する仮定に変換する。 我々は,SPECint 2006スイート全体を含む,現実世界のバイナリの多種多様なコーパス上でエレベータを評価する。
  論文  参考訳（メタデータ） (2026-05-08T19:25:06Z)
• Context-Guided Decompilation: A Step Towards Re-executability [50.71992919223209]
  バイナリ逆コンパイルは、ソフトウェアセキュリティ分析、リバースエンジニアリング、マルウェア理解において重要な役割を果たす。 大規模言語モデル (LLMs) の最近の進歩により、ニューラルデコンパイルが可能になったが、生成されたコードは一般的に意味論的にのみ使用可能である。 In-context Learning(ICL)を活用して,再実行可能なソースコードを生成するためのILC4Decompを提案する。
  論文  参考訳（メタデータ） (2025-11-03T17:21:39Z)
• IFEvalCode: Controlled Code Generation [69.28317223249358]
  本稿では,Code LLMの命令追従能力を改善するために,前方および後方制約生成を提案する。 IFEvalCodeは、7つのプログラミング言語の1.6Kテストサンプルからなる多言語ベンチマークである。
  論文  参考訳（メタデータ） (2025-07-30T08:08:48Z)
• 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)
• RedCode: Risky Code Execution and Generation Benchmark for Code Agents [50.81206098588923]
  RedCodeはリスクの高いコード実行と生成のためのベンチマークである。 RedCode-Execは、危険なコード実行につながる可能性のある、挑戦的なプロンプトを提供する。 RedCode-Genは160のプロンプトに関数シグネチャとドキュメントを入力として提供し、コードエージェントが命令に従うかどうかを評価する。
  論文  参考訳（メタデータ） (2024-11-12T13:30:06Z)
• Context-aware Code Segmentation for C-to-Rust Translation using Large Language Models [1.8416014644193066]
  大きな言語モデル(LLM)は、ルールベースのメソッドよりも自然で安全なコードを生成することで、この翻訳を自動化することを約束している。 大規模Cコードをコンパイル可能なRustコードに変換する際の成功率を改善するLLMベースの翻訳方式を提案する。 4キロのコードを含む20のベンチマークCプログラムの実験では、すべてのプログラムをコンパイル可能なRustコードに変換することに成功した。
  論文  参考訳（メタデータ） (2024-09-16T17:52:36Z)
• BinGo: Identifying Security Patches in Binary Code with Graph Representation Learning [19.22004583230725]
  バイナリコードに対する新しいセキュリティパッチ検出システムであるBinGoを提案する。 BinGoは、パッチデータ前処理、グラフ抽出、埋め込み生成、グラフ表現学習の4つのフェーズで構成されている。 実験の結果、BinGoは隣り合う2つのバイナリコードのセキュリティパッチを80.77%の精度で識別できることがわかった。
  論文  参考訳（メタデータ） (2023-12-13T06:35:39Z)
• Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
  学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。 確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。 Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
  論文  参考訳（メタデータ） (2023-09-25T15:42:18Z)
• Predicting Vulnerability In Large Codebases With Deep Code Representation [6.357681017646283]
  ソフトウェアエンジニアは様々なモジュールのコードを書きます。 過去に(異なるモジュールで)修正された同様の問題やバグも、本番コードで再び導入される傾向にある。 ソースコードから生成した抽象構文木(AST)の深部表現とアクティブフィードバックループを用いた,AIに基づく新しいシステムを開発した。
  論文  参考訳（メタデータ） (2020-04-24T13:18:35Z)

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

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