論文の概要: Accurate and Extensible Symbolic Execution of Binary Code based on Formal ISA Semantics

• arxiv url: http://arxiv.org/abs/2404.04132v2
• Date: Mon, 20 Jan 2025 11:56:45 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-01-22 19:37:18.779225
• Title: Accurate and Extensible Symbolic Execution of Binary Code based on Formal ISA Semantics
• Title（参考訳）: 形式的ISAセマンティックスに基づくバイナリコードの高精度で拡張可能な記号実行
• Authors: Sören Tempel, Tobias Brandt, Christoph Lüth, Christian Dietrich, Rolf Drechsler,
• Abstract要約: RISC-V ISA のプロトタイプを提示し、ケーススタディを行い、追加命令に容易に拡張できることを実証する。 従来の研究と実験的な比較を行った結果,IR ベースのシンボル executor angr の ISA 実装において,これまで知られていなかった5つのバグが発見された。
• 参考スコア（独自算出の注目度）: 2.3589687550723335
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Symbolic execution is an SMT-based software verification and testing technique. Symbolic execution requires tracking performed computations during software simulation to reason about branches in the software under test. The prevailing approach on symbolic execution of binary code tracks computations by transforming the code to be tested to an architecture-independent IR and then symbolically executes this IR. However, the resulting IR must be semantically equivalent to the binary code, making this process complex and error-prone. The semantics of the binary code are specified by the targeted ISA, commonly given in natural language and requiring a manual implementation of the transformation to an IR. In recent years, the use of formal languages to describe ISA semantics in a machine-readable way has gained increased popularity. We investigate the utilization of such formal semantics for symbolic execution of binary code, achieving an accurate representation of instruction semantics. We present a prototype for the RISC-V ISA and conduct a case study to demonstrate that it can be easily extended to additional instructions. Furthermore, we perform an experimental comparison with prior work which resulted in the discovery of five previously unknown bugs in the ISA implementation of the popular IR-based symbolic executor angr.
• Abstract（参考訳）: シンボリック実行は、SMTベースのソフトウェア検証とテスト技術である。 シンボリック実行では、テスト中のソフトウェアの分岐を推論するために、ソフトウェアシミュレーション中に実行された計算を追跡する必要がある。 バイナリコードのシンボリックな実行に対する一般的なアプローチは、テスト対象のコードをアーキテクチャに依存しないIRに変換し、象徴的にこのIRを実行することによって、計算を追跡する。 しかし、結果のIRはバイナリコードと意味的に等価でなければならないため、このプロセスは複雑でエラーを起こしやすい。 バイナリコードのセマンティクスは、ターゲットISAによって指定され、一般的に自然言語で与えられ、IRへの変換を手動で実装する必要がある。 近年,ISAセマンティクスを機械で読める形で記述する形式言語が普及している。 このような形式的意味論をバイナリコードの記号的実行に利用し、命令意味論の正確な表現を実現する。 RISC-V ISAのプロトタイプを提示し、ケーススタディを行い、追加命令に容易に拡張できることを実証する。 さらに,従来の研究と実験的な比較を行い,IR ベースのシンボル executor angr の ISA 実装における5つの既知のバグを発見した。

関連論文リスト

• An Empirical Study on the Effectiveness of Large Language Models for Binary Code Understanding [50.17907898478795]
  本研究では,現実のリバースエンジニアリングシナリオにおけるLarge Language Models(LLM)の有効性を評価するためのベンチマークを提案する。 評価の結果、既存のLLMはバイナリコードをある程度理解でき、それによってバイナリコード解析の効率が向上することが明らかとなった。
  論文  参考訳（メタデータ） (2025-04-30T17:02:06Z)
• StrTune: Data Dependence-based Code Slicing for Binary Similarity Detection with Fine-tuned Representation [5.41477941455399]
  BCSDは、悪意のあるコードスニペットの識別や、コードパターンの比較によるバイナリパッチ解析といったバイナリタスクに対処することができる。 バイナリは異なるコンパイル構成でコンパイルされるため、既存のアプローチはバイナリの類似性を比較する際にも注目すべき制限に直面している。 データ依存に基づいてバイナリコードをスライスし,スライスレベルの微調整を行うStrTuneを提案する。
  論文  参考訳（メタデータ） (2024-11-19T12:20:08Z)
• Training Neural Networks as Recognizers of Formal Languages [87.06906286950438]
  ニューラルネットワークを文字列のバイナリ分類器として直接訓練し評価する。 3つのニューラルアーキテクチャに対して、チョムスキー階層の様々な言語について結果を提供する。 我々の貢献は、将来の研究において、言語認識の主張を理論的に健全に検証するのに役立つだろう。
  論文  参考訳（メタデータ） (2024-11-11T16:33:25Z)
• Unsupervised Binary Code Translation with Application to Code Similarity Detection and Vulnerability Discovery [2.022692275087205]
  クロスアーキテクチャのバイナリコード解析が新たな問題となっている。 ディープラーニングベースのバイナリ分析は、有望な成功を収めている。 低リソースのISAでは、十分な量のデータを見つけることは困難である。
  論文  参考訳（メタデータ） (2024-04-29T18:09:28Z)
• Symbol-LLM: Leverage Language Models for Symbolic System in Visual Human Activity Reasoning [58.5857133154749]
  本稿では,広い範囲のシンボルと合理的なルールを持つ新しい記号体系を提案する。 我々は,LLMの最近の進歩を2つの理想的な性質の近似として活用する。 本手法は,広範囲な活動理解タスクにおいて優位性を示す。
  論文  参考訳（メタデータ） (2023-11-29T05:27:14Z)
• CP-BCS: Binary Code Summarization Guided by Control Flow Graph and Pseudo Code [79.87518649544405]
  本稿ではCP-BCSと呼ばれる制御フローグラフと擬似コード案内バイナリコード要約フレームワークを提案する。 CP-BCSは双方向の命令レベル制御フローグラフと擬似コードを利用して、専門家の知識を取り入れ、包括的なバイナリ関数の実行動作と論理意味論を学ぶ。
  論文  参考訳（メタデータ） (2023-10-24T14:20:39Z)
• Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
  学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。 確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。 Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
  論文  参考訳（メタデータ） (2023-09-25T15:42:18Z)
• Code Representation Pre-training with Complements from Program Executions [29.148208436656216]
  テストケースで明らかになったプログラムの動的情報を調べ,それを補体としてコードの特徴表現に埋め込むために,FuzzPretrainを提案する。 FuzzyPretrainは、ソースコードやASTのみをトレーニングしたコード検索に対して、6%/9%のmAP改善を実現した。
  論文  参考訳（メタデータ） (2023-09-04T01:57:22Z)
• Code Prompting: a Neural Symbolic Method for Complex Reasoning in Large Language Models [74.95486528482327]
  コードプロンプト(code prompting)は、ゼロショットバージョンと少数ショットバージョンの両方を持ち、中間ステップとしてコードをトリガーするニューラルシンボルプロンプトである。 我々は,記号的推論と算術的推論を含む7つの広く使用されているベンチマーク実験を行った。
  論文  参考訳（メタデータ） (2023-05-29T15:14:09Z)
• ProgSG: Cross-Modality Representation Learning for Programs in Electronic Design Automation [38.023395256208055]
  高レベル合成(HLS)により、開発者はCとC++のソフトウェアコード形式で高レベルな記述をコンパイルできる。 HLSツールは相変わらず、プラグマで表されるマイクロアーキテクチャの決定を必要とする。 本稿では,ソースコードシーケンスのモダリティとグラフのモダリティを深く,きめ細かな方法で相互に相互作用させることができるProgSGを提案する。
  論文  参考訳（メタデータ） (2023-05-18T09:44:18Z)
• Soft-Labeled Contrastive Pre-training for Function-level Code Representation [127.71430696347174]
  textbfSoft-labeled contrastive pre-training framework with two positive sample construction method。 大規模コードコーパスにおけるコード間の関連性を考慮すると、ソフトラベル付きコントラスト付き事前学習は、きめ細かいソフトラベルを得ることができる。 SCodeRは、7つのデータセットで4つのコード関連タスクに対して、最先端のパフォーマンスを新たに達成する。
  論文  参考訳（メタデータ） (2022-10-18T05:17:37Z)
• Pre-Training Representations of Binary Code Using Contrastive Learning [13.570375923483452]
  本稿では、表現学習中にソースコードとコメント情報をバイナリコードに組み込む、バイナリcOde分析のためのContrastive Learning Model(COMBO)を提案する。 COMBOは、ソースコード、バイナリコード、コメントをコントラストコード表現学習に組み込んだ最初の言語表現モデルである。
  論文  参考訳（メタデータ） (2022-10-11T02:39:06Z)
• BinBert: Binary Code Understanding with a Fine-tunable and Execution-aware Transformer [2.8523943706562638]
  本稿では,新しいアセンブリコードモデルであるBinBertを紹介する。 BinBertは、アセンブリ命令シーケンスとシンボル実行情報の巨大なデータセットに基づいて事前トレーニングされたトランスフォーマー上に構築されている。 微調整を通じて、BinBertは特定のタスクに事前学習で得られた一般的な知識をどう適用するかを学ぶ。
  論文  参考訳（メタデータ） (2022-08-13T17:48:52Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)
• A Natural Language Processing Approach for Instruction Set Architecture Identification [6.495883501989546]
  符号化されたバイナリの文字レベルの特徴を導入し、各ISA固有のきめ細かいビットパターンを識別する。 提案手法は,バイト・ヒストグラムとバイト・パターン・シグネチャに基づく最先端特徴よりも8%高い精度が得られる。
  論文  参考訳（メタデータ） (2022-04-13T19:45:06Z)
• Semantic-aware Binary Code Representation with BERT [27.908093567605484]
  バグ発見、マルウェア分析、コードクローン検出など、幅広いバイナリ分析アプリケーションでは、バイナリコード上でのコンテキスト意味の回復が必要である。 近年,バイナリのコード表現を自動再構築するために,機械学習に基づくバイナリ解析手法が提案されている。 本稿では,バイナリコードのセマンティックなコード表現を生成するためにBERTを利用するDeepSemanticを提案する。
  論文  参考訳（メタデータ） (2021-06-10T03:31:29Z)
• How could Neural Networks understand Programs? [67.4217527949013]
  ソースコードにnlpプリトレーニング技術を直接適用するか、あるいはtheshelfによってモデルに機能を追加するかで、プログラムをより理解するためのモデルを構築するのは難しい。 本研究では,(1)操作セマンティクスの基本操作とよく一致する表現と(2)環境遷移の情報からなる情報から,モデルが学ぶべき新しいプログラムセマンティクス学習パラダイムを提案する。
  論文  参考訳（メタデータ） (2021-05-10T12:21:42Z)
• High-performance symbolic-numerics via multiple dispatch [52.77024349608834]
  Symbolics.jlは拡張可能なシンボルシステムで、動的多重ディスパッチを使用してドメインのニーズに応じて振る舞いを変更する。 実装に依存しないアクションでジェネリックapiを形式化することで、システムに最適化されたデータ構造を遡及的に追加できることを示します。 従来の用語書き換えシンプリファイアと電子グラフベースの用語書き換えシンプリファイアをスワップする機能を実証する。
  論文  参考訳（メタデータ） (2021-05-09T14:22:43Z)
• Representing Partial Programs with Blended Abstract Semantics [62.20775388513027]
  プログラム合成エンジンにおける部分的なプログラム表現手法について紹介する。 モジュラーニューラルネットワークとして実装された近似実行モデルを学ぶ。 これらのハイブリッドニューロシンボリック表現は、実行誘導型シンセサイザーがより強力な言語構成を使うことができることを示す。
  論文  参考訳（メタデータ） (2020-12-23T20:40:18Z)

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

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