論文の概要: Formally Verified Binary-level Pointer Analysis
- arxiv url: http://arxiv.org/abs/2501.17766v1
- Date: Wed, 29 Jan 2025 16:57:15 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-01-30 15:52:12.125209
- Title: Formally Verified Binary-level Pointer Analysis
- Title（参考訳）: 形式的検証されたバイナリレベルポインタ解析
- Authors: Freek Verbeek, Ali Shokri, Daniel Engel, Binoy Ravindran,
- Abstract要約: 本稿では,正式に証明された2値レベルのポインタ解析へのアプローチを提案する。
我々のアプローチの健全な性質は、ポインタ解析の一般的な抽象領域が満たすべき証明の義務を、まず一般に考慮することである。
- 参考スコア（独自算出の注目度）: 1.9561775591923982
- License:
- Abstract: Binary-level pointer analysis can be of use in symbolic execution, testing, verification, and decompilation of software binaries. In various such contexts, it is crucial that the result is trustworthy, i.e., it can be formally established that the pointer designations are overapproximative. This paper presents an approach to formally proven correct binary-level pointer analysis. A salient property of our approach is that it first generically considers what proof obligations a generic abstract domain for pointer analysis must satisfy. This allows easy instantiation of different domains, varying in precision, while preserving the correctness of the analysis. In the trade-off between scalability and precision, such customization allows "meaningful" precision (sufficiently precise to ensure basic sanity properties, such as that relevant parts of the stack frame are not overwritten during function execution) while also allowing coarse analysis when pointer computations have become too obfuscated during compilation for sound and accurate bounds analysis. We experiment with three different abstract domains with high, medium, and low precision. Evaluation shows that our approach is able to derive designations for memory writes soundly in COTS binaries, in a context-sensitive interprocedural fashion.
- Abstract（参考訳）: バイナリレベルのポインタ分析は、ソフトウェアバイナリのシンボリック実行、テスト、検証、および逆コンパイルで使用することができる。
様々な文脈において、結果が信頼に値すること、すなわち、ポインタの指定が過近似であることを正式に確立することは重要である。
本稿では,正式に証明された2値レベルのポインタ解析へのアプローチを提案する。
我々のアプローチの健全な性質は、ポインタ解析の一般的な抽象領域が満たすべき証明の義務を、まず一般に考慮することである。
これにより、分析の正確さを保ちながら、精度で異なる異なる領域を簡単にインスタンス化できる。
スケーラビリティと精度のトレードオフにおいて、このようなカスタマイズは「意味のある」精度(スタックフレームの関連部分が関数実行中に上書きされないような基本的な正当性を保証するのに十分正確な)を可能にし、また、音と正確な境界解析のためのコンパイル中にポインタの計算が難しすぎるとき、粗い解析を可能にする。
我々は,高,中,低の3種類の抽象領域を実験した。
提案手法は,COTSバイナリにおけるメモリ書き込みの指定を,文脈に敏感な相互処理方式で正確に導出できることを示す。
関連論文リスト
- StrTune: Data Dependence-based Code Slicing for Binary Similarity Detection with Fine-tuned Representation [5.41477941455399]
BCSDは、悪意のあるコードスニペットの識別や、コードパターンの比較によるバイナリパッチ解析といったバイナリタスクに対処することができる。
バイナリは異なるコンパイル構成でコンパイルされるため、既存のアプローチはバイナリの類似性を比較する際にも注目すべき制限に直面している。
データ依存に基づいてバイナリコードをスライスし,スライスレベルの微調整を行うStrTuneを提案する。
論文 参考訳（メタデータ） (2024-11-19T12:20:08Z) - Smart Contract Vulnerability Detection based on Static Analysis and Multi-Objective Search [3.297959314391795]
本稿では,静的解析と多目的最適化アルゴリズムを用いて,スマートコントラクトの脆弱性を検出する手法を提案する。
永続性、スタックオーバーフローの呼び出し、整数オーバーフロー、タイムスタンプの依存関係の4つのタイプの脆弱性に焦点を当てています。
我々は,6,693のスマートコントラクトを含むEtherscanから収集したオープンソースデータセットを用いて,このアプローチを検証する。
論文 参考訳（メタデータ） (2024-09-30T23:28:17Z) - Scaling Symbolic Execution to Large Software Systems [0.0]
シンボル実行は、プログラム検証とバグ検出ソフトウェアの両方で使用される一般的な静的解析手法である。
我々は、Clang Static Analyzerと呼ばれるエラー検出フレームワークと、その周辺に構築されたインフラストラクチャーであるCodeCheckerに焦点を当てた。
論文 参考訳（メタデータ） (2024-08-04T02:54:58Z) - FoC: Figure out the Cryptographic Functions in Stripped Binaries with LLMs [54.27040631527217]
削除されたバイナリの暗号関数を抽出するFoCと呼ばれる新しいフレームワークを提案する。
まず、自然言語における暗号関数のセマンティクスを要約するために、バイナリ大言語モデル(FoC-BinLLM)を構築した。
次に、FoC-BinLLM上にバイナリコード類似モデル(FoC-Sim)を構築し、変更に敏感な表現を作成し、データベース内の未知の暗号関数の類似実装を検索する。
論文 参考訳（メタデータ） (2024-03-27T09:45:33Z) - DeepSec: Deciding Equivalence Properties for Security Protocols -- Improved theory and practice [8.735998284944436]
我々はこの検証問題の理論と実践に貢献する。
静的同値、トレース同値およびラベル付き二相性のための新しい複雑性結果を確立する。
我々の手順は、多種多様な暗号プリミティブに対して、トレース同値とラベル付き二相性を決定する最初の方法である。
論文 参考訳（メタデータ） (2022-11-06T22:01:04Z) - Measuring the Interpretability of Unsupervised Representations via
Quantized Reverse Probing [97.70862116338554]
本稿では,自己教師付き表現の解釈可能性の測定問題について検討する。
我々は、後者を、表現と手動でラベル付けされた概念の空間の間の相互情報を推定するものとして定式化する。
提案手法は,多人数の自己教師付き表現の評価に利用し,解釈可能性による評価を行う。
論文 参考訳（メタデータ） (2022-09-07T16:18:50Z) - Rethinking Counting and Localization in Crowds:A Purely Point-Based
Framework [59.578339075658995]
そこで本稿では,共同クラウドカウントと個別ローカライゼーションのための純粋にポイントベースのフレームワークを提案する。
我々は、P2PNet(Point to Point Network)と呼ばれる、このフレームワークの下で直感的なソリューションを設計する。
論文 参考訳（メタデータ） (2021-07-27T11:41:50Z) - Semantic-aware Binary Code Representation with BERT [27.908093567605484]
バグ発見、マルウェア分析、コードクローン検出など、幅広いバイナリ分析アプリケーションでは、バイナリコード上でのコンテキスト意味の回復が必要である。
近年,バイナリのコード表現を自動再構築するために,機械学習に基づくバイナリ解析手法が提案されている。
本稿では,バイナリコードのセマンティックなコード表現を生成するためにBERTを利用するDeepSemanticを提案する。
論文 参考訳（メタデータ） (2021-06-10T03:31:29Z) - Target-Aware Object Discovery and Association for Unsupervised Video
Multi-Object Segmentation [79.6596425920849]
本稿では,教師なしビデオマルチオブジェクトセグメンテーションの課題について述べる。
より正確で効率的な時間区分のための新しいアプローチを紹介します。
DAVIS$_17$とYouTube-VISに対する提案手法を評価した結果,セグメント化精度と推論速度の両方において最先端の手法より優れていることが示された。
論文 参考訳（メタデータ） (2021-04-10T14:39:44Z) - Making Affine Correspondences Work in Camera Geometry Computation [62.7633180470428]
局所的な特徴は、ポイント・ツー・ポイント対応ではなく、リージョン・ツー・リージョンを提供する。
本稿では,全モデル推定パイプラインにおいて,地域間マッチングを効果的に活用するためのガイドラインを提案する。
実験により、アフィンソルバはより高速な実行時にポイントベースソルバに匹敵する精度を達成できることが示された。
論文 参考訳（メタデータ） (2020-07-20T12:07:48Z) - Deep Hough Transform for Semantic Line Detection [70.28969017874587]
自然の場面で意味のある線構造、つまり意味的な線を検知する基本的なタスクに焦点をあてる。
従来の手法は線の性質を無視し、準最適性能をもたらす。
行検出のためのワンショットエンドツーエンド学習フレームワークを提案する。
論文 参考訳（メタデータ） (2020-03-10T13:08:42Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。