論文の概要: BASICS: Binary Analysis and Stack Integrity Checker System for Buffer Overflow Mitigation
- arxiv url: http://arxiv.org/abs/2511.19670v1
- Date: Mon, 24 Nov 2025 20:11:41 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-11-26 17:37:04.148154
- Title: BASICS: Binary Analysis and Stack Integrity Checker System for Buffer Overflow Mitigation
- Title(参考訳): BASICS:バッファオーバーフロー軽減のためのバイナリ解析とスタック統合チェッカシステム
- Authors: Luis Ferreirinha, Iberia Medeiros,
- Abstract要約: サイバー物理システムは私たちの日常生活において重要な役割を担い、電力や水などの重要なサービスを提供してきた。
従来の脆弱性発見技術は、Cプログラムのバイナリコードに直接適用する場合、スケーラビリティと精度に苦労する。
この研究は、モデルチェックとココリック実行技術を活用することによって、これらの制限を克服するために設計された新しいアプローチを導入している。
- 参考スコア(独自算出の注目度): 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Cyber-Physical Systems have played an essential role in our daily lives, providing critical services such as power and water, whose operability, availability, and reliability must be ensured. The C programming language, prevalent in CPS development, is crucial for system control where reliability is critical. However, it is also commonly susceptible to vulnerabilities, particularly buffer overflows. Traditional vulnerability discovery techniques often struggle with scalability and precision when applied directly to the binary code of C programs, which can thereby keep programs vulnerable. This work introduces a novel approach designed to overcome these limitations by leveraging model checking and concolic execution techniques to automatically verify security properties of a program's stack memory in binary code, trampoline techniques to perform automated repair of the issues, and crash-inducing inputs to verify if they were successfully removed. The approach constructs a Memory State Space - MemStaCe- from the binary program's control flow graph and simulations, provided by concolic execution, of C function calls and loop constructs. The security properties, defined in LTL, model the correct behaviour of functions associated with vulnerabilities and allow the approach to identify vulnerabilities in MemStaCe by analysing counterexample traces that are generated when a security property is violated. These vulnerabilities are then addressed with a trampoline-based binary patching method, and the effectiveness of the patches is checked with crash-inducing inputs extracted during concolic execution. We implemented the approach in the BASICS tool for BO mitigation and evaluated using the Juliet C/C++ and SARD datasets and real applications, achieving an accuracy and precision above 87%, both in detection and correction. Also, we compared it with CWE Checker, outperforming it.
- Abstract(参考訳): サイバー物理システムは私たちの日常生活において重要な役割を担い、電力や水などの重要なサービスを提供し、その運用性、可用性、信頼性を確保する必要がある。
CPS開発で広く使われているC言語は、信頼性が重要なシステム制御に不可欠である。
しかし、脆弱性、特にバッファオーバーフローの影響を受けやすいことも一般的である。
従来の脆弱性発見技術は、Cプログラムのバイナリコードに直接適用した場合、スケーラビリティと精度に苦しむことが多く、それによってプログラムの脆弱性を維持することができる。
本研究は,プログラムのスタックメモリのセキュリティ特性をバイナリコードで自動検証するモデルチェックとコンコリック実行技術,問題の自動修復を行うトランポリン技術,そして正常に除去されたかどうかを確認するためのインプットをクラッシュ誘導することで,これらの制限を克服するために設計された新しいアプローチを導入する。
このアプローチでは、バイナリプログラムの制御フローグラフからメモリ状態空間(MemStaCe)を構築し、C関数呼び出しとループ構成のココリック実行によってシミュレーションを行う。
LTLで定義されたセキュリティプロパティは、脆弱性に関連する関数の正しい振る舞いをモデル化し、セキュリティプロパティが違反したときに生成された反例トレースを分析して、MemStaCeの脆弱性を特定するアプローチを可能にする。
これらの脆弱性はトランポリンベースのバイナリパッチ方式で対処され、そのパッチの有効性は、競合実行中に抽出されたクラッシュ誘発インプットでチェックされる。
我々はBO緩和のためのBASICSツールにアプローチを実装し,Juliet C/C++およびSARDデータセットと実アプリケーションを用いて評価し,検出と修正の両方において87%以上の精度と精度を実現した。
また、私たちはそれをCWE Checkerと比較し、それよりも優れています。
関連論文リスト
- Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。
実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
論文 参考訳(メタデータ) (2025-05-28T17:57:47Z) - VulBinLLM: LLM-powered Vulnerability Detection for Stripped Binaries [4.1417640577742425]
Vul-BinLLMは、大規模言語モデルを用いたバイナリ脆弱性検出のためのフレームワークである。
Vul-BinLLMは、拡張コンテキストで逆コンパイルと脆弱性推論を微妙に最適化することで、従来のバイナリ分析を反映している。
評価の結果,Vul-BinLLMはジュリエットデータセットの脆弱性の検出に極めて有効であることがわかった。
論文 参考訳(メタデータ) (2025-05-28T06:17:56Z) - CRAFT: Characterizing and Root-Causing Fault Injection Threats at Pre-Silicon [3.6158033114580674]
フォールトインジェクション攻撃は組み込みシステムに重大なセキュリティ脅威をもたらす。
物理的欠陥がシステムレベルの行動にどのように伝播するかの早期発見と理解は、サイバーインフラ構造を保護するために不可欠である。
この研究は、プレシリコン分析とポストシリコンバリデーションを組み合わせたフレームワークであるCRAFTを導入し、障害インジェクションの脆弱性を体系的に発見し分析する。
論文 参考訳(メタデータ) (2025-03-05T20:17:46Z) - Improving Discovery of Known Software Vulnerability For Enhanced Cybersecurity [0.0]
脆弱性検出はCommon Platformion (CPE)文字列のような標準化された識別子に依存する。
ソフトウェアベンダが発行する標準化されていないCPE文字列は、大きな課題を生み出します。
一貫性のない命名規則、バージョニングプラクティスは、データベースをクエリする際のミスマッチを引き起こす。
論文 参考訳(メタデータ) (2024-12-21T12:43:52Z) - Assessing the Effectiveness of Binary-Level CFI Techniques [0.0]
フロー制御統合(CFI)は、制御フローハイジャック攻撃に対する防御を提供する。
バイナリレベルの型リカバリは本質的に投機的であり、評価フレームワークの必要性を動機付けている。
論文 参考訳(メタデータ) (2024-01-13T19:38:15Z) - Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
CBFをベースとした安全クリティカルコントローラのモデル不確実性を考慮した再構成を提案する。
次に、結果の安全制御器のポイントワイズ実現可能性条件を示す。
これらの条件を利用して、イベントトリガーによるオンラインデータ収集戦略を考案する。
論文 参考訳(メタデータ) (2022-08-23T05:02:09Z) - Learning Robust Output Control Barrier Functions from Safe Expert Demonstrations [50.37808220291108]
本稿では,専門家によるデモンストレーションの部分的な観察から,安全な出力フィードバック制御法を考察する。
まず,安全性を保証する手段として,ロバスト出力制御バリア関数(ROCBF)を提案する。
次に、安全なシステム動作を示す専門家による実証からROCBFを学習するための最適化問題を定式化する。
論文 参考訳(メタデータ) (2021-11-18T23:21:00Z) - Pointwise Feasibility of Gaussian Process-based Safety-Critical Control
under Model Uncertainty [77.18483084440182]
制御バリア関数(CBF)と制御リアプノフ関数(CLF)は、制御システムの安全性と安定性をそれぞれ強化するための一般的なツールである。
本稿では, CBF と CLF を用いた安全クリティカルコントローラにおいて, モデル不確実性に対処するためのガウスプロセス(GP)に基づくアプローチを提案する。
論文 参考訳(メタデータ) (2021-06-13T23:08:49Z) - V2W-BERT: A Framework for Effective Hierarchical Multiclass
Classification of Software Vulnerabilities [7.906207218788341]
本稿では,Transformer-based learning framework(V2W-BERT)を提案する。
自然言語処理,リンク予測,転送学習のアイデアを用いることで,従来の手法よりも優れる。
ランダムに分割されたデータの予測精度は最大97%、一時分割されたデータの予測精度は最大94%です。
論文 参考訳(メタデータ) (2021-02-23T05:16:57Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。