Fugu-MT 論文翻訳(概要): BinSym: Binary-Level Symbolic Execution using Formal Descriptions of Instruction Semantics

論文の概要: BinSym: Binary-Level Symbolic Execution using Formal Descriptions of Instruction Semantics

arxiv url: http://arxiv.org/abs/2404.04132v1
Date: Fri, 5 Apr 2024 14:29:39 GMT
ステータス: 処理完了
システム内更新日: 2024-04-08 15:45:42.564703
Title: BinSym: Binary-Level Symbolic Execution using Formal Descriptions of Instruction Semantics
Title（参考訳）: BinSym:インストラクションセマンティクスの形式記述を用いたバイナリレベルシンボリック実行
Authors: Sören Tempel, Tobias Brandt, Christoph Lüth, Rolf Drechsler,
Abstract要約: BinSymはバイナリ形式でソフトウェアを記号的に解析するフレームワークである。バイナリコード命令を直接操作し、中間表現にリフティングする必要はない。
参考スコア（独自算出の注目度）: 2.4576576560952788
License: http://creativecommons.org/licenses/by-sa/4.0/
Abstract: BinSym is a framework for symbolic program analysis of software in binary form. Contrary to prior work, it operates directly on binary code instructions and does not require lifting them to an intermediate representation (IR). This is achieved by formulating the symbolic semantics on top of a formal description of binary code instruction semantics. By building on existing formal descriptions, BinSym eliminates the manual effort required by prior work to implement transformations to an IR, thereby reducing the margin for errors. Furthermore, BinSym's symbolic semantics can be directly related to the binary code, which improves symbolic execution speed by reducing solver query complexity.
Abstract（参考訳）: BinSymはバイナリ形式でソフトウェアを記号的に解析するフレームワークである。以前の作業とは対照的に、バイナリコード命令を直接操作し、それらを中間表現(IR)に持ち上げる必要はない。これは、バイナリコード命令セマンティクスの形式記述の上にシンボルセマンティクスを定式化することで達成される。既存の公式記述に基づいて、BinSymはIRへの変換を実装する事前作業に必要な手作業を取り除き、エラーのマージンを減らす。さらに、BinSymのシンボリックセマンティクスはバイナリコードに直接関連し、ソルバクエリの複雑さを減らすことでシンボリック実行速度を改善することができる。

関連論文リスト

Training Neural Networks as Recognizers of Formal Languages [87.06906286950438]
形式言語理論は、特に認識者に関するものである。代わりに、非公式な意味でのみ類似したプロキシタスクを使用するのが一般的である。ニューラルネットワークを文字列のバイナリ分類器として直接訓練し評価することで、このミスマッチを補正する。
論文参考訳（メタデータ） (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)
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)
ProgSG: Cross-Modality Representation Learning for Programs in Electronic Design Automation [38.023395256208055]
高レベル合成(HLS)により、開発者はCとC++のソフトウェアコード形式で高レベルな記述をコンパイルできる。 HLSツールは相変わらず、プラグマで表されるマイクロアーキテクチャの決定を必要とする。本稿では,ソースコードシーケンスのモダリティとグラフのモダリティを深く,きめ細かな方法で相互に相互作用させることができるProgSGを提案する。
論文参考訳（メタデータ） (2023-05-18T09:44:18Z)
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)

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