論文の概要: Rampo: A CEGAR-based Integration of Binary Code Analysis and System Falsification for Cyber-Kinetic Vulnerability Detection
- arxiv url: http://arxiv.org/abs/2402.12642v1
- Date: Tue, 20 Feb 2024 01:36:08 GMT
- ステータス: 処理完了
- システム内更新日: 2024-03-25 08:56:22.645784
- Title: Rampo: A CEGAR-based Integration of Binary Code Analysis and System Falsification for Cyber-Kinetic Vulnerability Detection
- Title（参考訳）: Rampo: サイバーキネティック脆弱性検出のためのバイナリコード解析とシステムファルシフィケーションを統合したCEGAR
- Authors: Kohei Tsujio, Mohammad Abdullah Al Faruque, Yasser Shoukry,
- Abstract要約: Rampoはバイナリコード解析を行い、CPS内のサイバーキネティックな脆弱性を識別する。
当社のツールは,同じ数の脆弱性を計算しながら,3倍から98倍のスピードアップを実現しています。
- 参考スコア（独自算出の注目度）: 14.7195342186018
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: This paper presents a novel tool, named Rampo, that can perform binary code analysis to identify cyber kinetic vulnerabilities in CPS. The tool takes as input a Signal Temporal Logic (STL) formula that describes the kinetic effect, i.e., the behavior of the physical system, that one wants to avoid. The tool then searches the possible cyber trajectories in the binary code that may lead to such physical behavior. This search integrates binary code analysis tools and hybrid systems falsification tools using a Counter-Example Guided Abstraction Refinement (CEGAR) approach. Rampo starts by analyzing the binary code to extract symbolic constraints that represent the different paths in the code. These symbolic constraints are then passed to a Satisfiability Modulo Theories (SMT) solver to extract the range of control signals that can be produced by each path in the code. The next step is to search over possible physical trajectories using a hybrid systems falsification tool that adheres to the behavior of the cyber paths and yet leads to violations of the STL formula. Since the number of cyber paths that need to be explored increases exponentially with the length of physical trajectories, we iteratively perform refinement of the cyber path constraints based on the previous falsification result and traverse the abstract path tree obtained from the control program to explore the search space of the system. To illustrate the practical utility of binary code analysis in identifying cyber kinetic vulnerabilities, we present case studies from diverse CPS domains, showcasing how they can be discovered in their control programs. Our tool could compute the same number of vulnerabilities while leading to a speedup that ranges from 3x to 98x.
- Abstract（参考訳）: 本稿では,CPSにおけるサイバーキネティックな脆弱性を識別するためのバイナリコード解析を行う,Rampoという新しいツールを提案する。
このツールは信号時間論理 (Signal Temporal Logic, STL) の式として入力され、物理系の振る舞いが避けたいという運動効果を記述する。
するとツールがバイナリコード内の可能性のあるサイバートラジェクトリを検索し、そのような物理的な振る舞いにつながる可能性がある。
この検索は、Counter-Example Guided Abstraction Refinement (CEGAR) アプローチを用いてバイナリコード解析ツールとハイブリッドシステムのファルシフィケーションツールを統合する。
Rampoはまずバイナリコードを解析して、コードの異なるパスを表すシンボリックな制約を抽出する。
これらのシンボリック制約は、コード内の各パスによって生成される制御信号の範囲を抽出するために、Satifiability Modulo Theories (SMT) ソルバに渡される。
次のステップは、サイバーパスの振る舞いに固執するが、STL公式違反につながるハイブリッドシステムファルシフィケーションツールを使用して、可能な物理的軌道を探索することである。
探索すべきサイバーパスの数は物理的軌跡の長さとともに指数関数的に増加するため、前回のファルシフィケーション結果に基づいてサイバーパス制約の洗練を反復的に行い、制御プログラムから得られた抽象パスツリーを横切り、システムの探索空間を探索する。
サイバー攻撃的脆弱性を特定するためのバイナリコード解析の実用性を説明するために,多様なCPSドメインのケーススタディを提示し,それらの制御プログラムでどのように検出できるかを示す。
当社のツールは,同じ数の脆弱性を計算しながら,3倍から98倍のスピードアップを実現しています。
関連論文リスト
- Finding Transformer Circuits with Edge Pruning [71.12127707678961]
自動回路発見の効率的かつスケーラブルなソリューションとしてエッジプルーニングを提案する。
本手法は,従来の手法に比べてエッジ数の半分未満のGPT-2の回路を探索する。
その効率のおかげで、Edge PruningをCodeLlama-13Bにスケールしました。
論文 参考訳（メタデータ） (2024-06-24T16:40:54Z) - Scalable Surrogate Verification of Image-based Neural Network Control Systems using Composition and Unrolling [9.633494094538017]
本研究では,実世界に代わって条件付き生成逆数ネットワーク(cGAN)をイメージジェネレータとして訓練し,サロゲート検証手法を提案する。
我々は、cGANとニューラルネットワークコントローラとともにシステムのダイナミクスを構成することで、一段階のエラーを克服する。
単一ステップの合成を繰り返し、制御ループの複数のステップを大規模ニューラルネットワークに展開することで、マルチステップエラーを低減する。
論文 参考訳（メタデータ） (2024-05-28T19:56:53Z) - Automatically Identifying Local and Global Circuits with Linear Computation Graphs [45.760716193942685]
Sparse Autoencoders (SAEs) と Transcoders と呼ばれる変種を用いた回路発見パイプラインを導入する。
本手法は各ノードの因果効果を計算するために線形近似を必要としない。
GPT-2 Small: Bracket, induction, Indirect Object Identification circuits の3種類の回路を解析する。
論文 参考訳（メタデータ） (2024-05-22T17:50:04Z) - Cross-domain Learning Framework for Tracking Users in RIS-aided Multi-band ISAC Systems with Sparse Labeled Data [55.70071704247794]
統合センシング・通信(ISAC)は6G通信において重要であり、再構成可能なインテリジェントサーフェス(RIS)の急速な発展によって促進される
本稿では,複数の帯域にまたがるマルチモーダルCSIインジケータを協調的に活用し,クロスドメイン方式で追跡機能をモデル化するX2Trackフレームワークを提案する。
X2Trackの下では、トランスフォーマーニューラルネットワークと逆学習技術に基づいて、トラッキングエラーを最小限に抑える効率的なディープラーニングアルゴリズムを設計する。
論文 参考訳（メタデータ） (2024-05-10T08:04:27Z) - Dynamic Neural Control Flow Execution: An Agent-Based Deep Equilibrium Approach for Binary Vulnerability Detection [4.629503670145618]
ソフトウェア脆弱性はサイバーセキュリティの課題だ。
DeepEXEはエージェントベースの暗黙のニューラルネットワークで、プログラムの実行パスを模倣する。
DeepEXEは正確かつ効率的な手法であり、最先端の脆弱性検出方法よりも優れていることを示す。
論文 参考訳（メタデータ） (2024-04-03T22:07:50Z) - 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) - Automated Static Warning Identification via Path-based Semantic
Representation [37.70518599085676]
本稿では、深層ニューラルネットワークの強力な特徴抽出と表現能力を用いて、警告識別のための制御フローグラフパスからコードセマンティクスを生成する。
事前訓練された言語モデルを微調整し、パスシーケンスを符号化し、モデル構築のための意味表現をキャプチャする。
論文 参考訳（メタデータ） (2023-06-27T15:46:45Z) - A Hierarchical Deep Neural Network for Detecting Lines of Codes with
Vulnerabilities [6.09170287691728]
ソースコードの意図しない欠陥によって引き起こされるソフトウェア脆弱性は、サイバー攻撃の根本原因である。
本稿では,自然言語処理で使用されている手法に基づいて,LLVM IR表現から脆弱性を検出するためのディープラーニング手法を提案する。
論文 参考訳（メタデータ） (2022-11-15T21:21:27Z) - Software Vulnerability Detection via Deep Learning over Disaggregated
Code Graph Representation [57.92972327649165]
この研究は、コードコーパスから安全でないパターンを自動的に学習するためのディープラーニングアプローチを探求する。
コードには解析を伴うグラフ構造が自然に認められるため,プログラムの意味的文脈と構造的規則性の両方を利用する新しいグラフニューラルネットワーク(GNN)を開発する。
論文 参考訳（メタデータ） (2021-09-07T21:24:36Z) - Risk-Averse MPC via Visual-Inertial Input and Recurrent Networks for
Online Collision Avoidance [95.86944752753564]
本稿では,モデル予測制御(MPC)の定式化を拡張したオンライン経路計画アーキテクチャを提案する。
我々のアルゴリズムは、状態推定の共分散を推論するリカレントニューラルネットワーク(RNN)とオブジェクト検出パイプラインを組み合わせる。
本手法のロバスト性は, 複雑な四足歩行ロボットの力学で検証され, ほとんどのロボットプラットフォームに適用可能である。
論文 参考訳（メタデータ） (2020-07-28T07:34:30Z) - Binary DAD-Net: Binarized Driveable Area Detection Network for
Autonomous Driving [94.40107679615618]
本稿では,二項化駆動型領域検出ネットワーク(バイナリDAD-Net)を提案する。
エンコーダ、ボトルネック、デコーダ部分の2重みとアクティベーションのみを使用する。
パブリックデータセット上で、最先端のセマンティックセグメンテーションネットワークより優れています。
論文 参考訳（メタデータ） (2020-06-15T07:09:01Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。