論文の概要: Symbolon: Symbolic Execution by Learning Code Transformation
- arxiv url: http://arxiv.org/abs/2606.29108v1
- Date: Sat, 27 Jun 2026 23:16:50 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-30 18:07:15.790751
- Title: Symbolon: Symbolic Execution by Learning Code Transformation
- Title（参考訳）: シンボロン: コード変換学習によるシンボリックな実行
- Abstract要約: 多様なコード変換を学習し、それらを文脈に敏感に適用し、シンボル実行を改善するためのフレームワークであるSybolonを紹介します。
評価の結果,シンボロンは実世界の32のプログラムにおいて,16の検索戦略に対して,シンボル的実行エンジンKLEEを大幅に改善することがわかった。
- 参考スコア（独自算出の注目度）: 20.89743100548855
- License: http://creativecommons.org/licenses/by-sa/4.0/
- Abstract: Symbolic execution is a powerful program analysis technique with broad applications, such as vulnerability detection, security testing, and malware analysis. However, this technique is known to suffer from scalability issues, e.g., path explosion, complex constraints, due to certain structural and semantic patterns commonly presented in real-world programs. Existing approaches attempt to escape these patterns by transforming programs into new representations to reduce the execution cost. Unfortunately, these transformations are often too rigid to exploit diverse local program semantics and sometimes rely on compiler optimizations designed for concrete execution that may misalign with the goals of symbolic execution. We present Symbolon, a framework that automatically learns diverse code transformations and applies them context-sensitively to improve symbolic execution. Our key insight is to formulate transformation discovery as a search problem over program representations. To make the search practical, Symbolon learns transformations cheaply offline on small programs, distills them into a reusable library of agent skills, and uses an agent to instantiate these skills on repo-level targets. Our evaluation shows that Symbolon substantially improves the symbolic execution engine KLEE across 16 search strategies on 32 real-world programs, increasing line coverage by 3.69x on average while reducing peak memory and per-query solver time by 29.2x and 123x, respectively. When applied to the latest Linux kernel, Symbolon uncovers 21 previously unknown bugs, all of which have been reported to the kernel maintainers.
- Abstract（参考訳）: シンボリック実行は、脆弱性検出、セキュリティテスト、マルウェア分析といった幅広いアプリケーションを持つ強力なプログラム解析技術である。
しかし、この手法は、例えばパスの爆発、複雑な制約といったスケーラビリティの問題に悩まされていることが知られている。
既存のアプローチでは、プログラムを新しい表現に変換して実行コストを削減することで、これらのパターンを回避しようとする。
残念なことに、これらの変換は、様々なローカルプログラムセマンティクスを利用するには厳格すぎることが多く、時には、象徴的な実行の目標に反する具体的な実行のために設計されたコンパイラの最適化に依存している。
多様なコード変換を自動的に学習し、それらを文脈に敏感に適用してシンボル実行を改善するためのフレームワークであるSymbolonを提案する。
我々の重要な洞察は、プログラム表現に対する探索問題として変換発見を定式化することである。
検索を実用的なものにするために、Symbolonは、小さなプログラムで安価にオフラインで変換を学び、それらを再利用可能なエージェントスキルのライブラリに蒸留し、エージェントを使用してレポレベルのターゲットでこれらのスキルをインスタンス化する。
評価の結果、シンボロンは実世界の32のプログラムにおいて16の検索戦略でシンボル実行エンジンKLEEを大幅に改善し、平均3.69倍のラインカバレッジを向上し、ピークメモリとクエリ毎のソルバ時間を29.2倍、123倍に短縮した。
最新のLinuxカーネルに適用されると、Symbolonは21の既知のバグを明らかにし、これらはすべてカーネルメンテナに報告されている。
関連論文リスト
- Overcoming the Weakest-Link Effect in LLM-Driven Program Optimization via Heterogeneous Edit Recombination [59.679182823718556]
HEROは、多様で重複しない原子編集を生成し、それから体系的に選択し、評価器スコアを用いてコヒーレントなプログラム改善に構成するプログラムである。
我々は,アルゴリズム問題,戦略ゲーム,LSMに基づくエージェントシステムの設計,ロボット経路計画などにわたるHEROを評価する。
論文 参考訳（メタデータ） (2026-07-31T02:05:45Z) - Can LLMs Recover Program Semantics? A Systematic Evaluation with Symbolic Execution [1.5377279217726239]
難読化は、プログラムの理解、メンテナンス、テスト、脆弱性検出といったソフトウェアエンジニアリングタスクに永続的な課題をもたらす。
微調整言語モデルがプログラムを効果的に難読化し、分析可能性を取り戻すことができるかどうかを検討する。
論文 参考訳（メタデータ） (2025-11-24T13:55:20Z) - Symbolic Execution in Practice: A Survey of Applications in Vulnerability, Malware, Firmware, and Protocol Analysis [3.1844358655583846]
記号実行は、すべてのプログラムパスの体系的な探索を可能にする強力なプログラム解析技術である。
本稿では,複雑なソフトウェアシステム上でのシンボリックな実行を可能にする戦略の体系的な分類法を提案する。
脆弱性分析,マルウェア解析,ファームウェア再ホスト,ネットワークプロトコル解析など,いくつかの領域におけるシンボル実行の応用を調査した。
論文 参考訳（メタデータ） (2025-08-08T18:43:45Z) - LIFT: Automating Symbolic Execution Optimization with Large Language Models for AI Networks [31.69036961288122]
LIFT(Large- Language-model Integrated Functional-equivalent-IR Transformation)は、シンボル実行における中間表現(IR)の最適化を自動化する新しいフレームワークである。
実世界のバイナリの実験では、パフォーマンスが大幅に向上した。
論文 参考訳（メタデータ） (2025-07-07T12:26:56Z) - Exposing Go's Hidden Bugs: A Novel Concolic Framework [2.676686591720132]
本稿では,Goプログラムを包括的に評価する新しい方法論であるZoryaを紹介する。
従来のテスト以上の脆弱性を明らかにするために、システミックに実行パスを探索することで、象徴的な実行には明確なメリットがある。
我々の解は、GhidraのP-Codeを中間表現(IR)として採用する。
論文 参考訳（メタデータ） (2025-05-26T16:26:20Z) - ReF Decompile: Relabeling and Function Call Enhanced Decompile [50.86228893636785]
逆コンパイルの目標は、コンパイルされた低レベルコード(アセンブリコードなど)を高レベルプログラミング言語に変換することである。
このタスクは、脆弱性識別、マルウェア分析、レガシーソフトウェアマイグレーションなど、さまざまなリバースエンジニアリングアプリケーションをサポートする。
論文 参考訳（メタデータ） (2025-02-17T12:38:57Z) - ReGAL: Refactoring Programs to Discover Generalizable Abstractions [59.05769810380928]
Generalizable Abstraction Learning (ReGAL)は、再利用可能な関数のライブラリをコード化して学習する手法である。
ReGALによって発見された共有関数ライブラリは、プログラムが様々な領域で容易に予測できることを示している。
CodeLlama-13Bでは、ReGALはLOGOで11.5%、日付理解で26.1%、TextCraftで8.1%という絶対精度が向上し、3つのドメインのうち2つでGPT-3.5を上回った。
論文 参考訳（メタデータ） (2024-01-29T18:45:30Z) - Divide, Conquer and Verify: Improving Symbolic Execution Performance [0.0]
シンボル実行(英: Symbolic Execution)は、コンピュータプログラムの動作を確認し、ソフトウェア脆弱性を検出するための形式的な方法である。
近年のパフォーマンス向上にもかかわらず、Symbolic Executionは現実のソフトウェアに適用するには遅すぎる。
個別のスライスを実行し,その後に副作用を組み合わせることで,シンボル実行のための分割・コンカレント手法を提案する。
論文 参考訳（メタデータ） (2023-10-05T15:21:10Z) - Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。
確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。
Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
論文 参考訳（メタデータ） (2023-09-25T15:42:18Z) - Symbolic Visual Reinforcement Learning: A Scalable Framework with
Object-Level Abstraction and Differentiable Expression Search [63.3745291252038]
DiffSESは、離散的なシンボルポリシーを発見する新しいシンボリック学習手法である。
生のピクセルレベルの入力の代わりにオブジェクトレベルの抽象化を使用することで、DiffSESはシンボリック表現の単純さとスケーラビリティの利点を活用することができる。
我々の実験は、DiffSESが最先端のシンボルRL法よりもシンプルでスケーラブルなシンボリックポリシーを生成することができることを示した。
論文 参考訳（メタデータ） (2022-12-30T17:50:54Z) - High-performance symbolic-numerics via multiple dispatch [52.77024349608834]
Symbolics.jlは拡張可能なシンボルシステムで、動的多重ディスパッチを使用してドメインのニーズに応じて振る舞いを変更する。
実装に依存しないアクションでジェネリックapiを形式化することで、システムに最適化されたデータ構造を遡及的に追加できることを示します。
従来の用語書き換えシンプリファイアと電子グラフベースの用語書き換えシンプリファイアをスワップする機能を実証する。
論文 参考訳（メタデータ） (2021-05-09T14:22:43Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。