Rampo: A CEGAR-based Integration of Binary Code Analysis and System Falsification for Cyber-Kinetic Vulnerability Detection

• URL: http://arxiv.org/abs/2402.12642v1
• Date: Tue, 20 Feb 2024 01:36:08 GMT
• Title: Rampo: A CEGAR-based Integration of Binary Code Analysis and System Falsification for Cyber-Kinetic Vulnerability Detection
• Authors: Kohei Tsujio, Mohammad Abdullah Al Faruque, Yasser Shoukry,
• Abstract summary: Rampo can perform binary code analysis to identify cyber kinetic vulnerabilities in CPS. Our tool could compute the same number of vulnerabilities while leading to a speedup that ranges from 3x to 98x.
• Score: 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.

Related papers

• CyberSentinel: Efficient Anomaly Detection in Programmable Switch using Knowledge Distillation [0.0]
  CyberSentinel is a high throughput and accurate anomaly detection system deployed entirely in the programmable switch data plane. To detect unseen network attacks, CyberSentinel uses a novel knowledge distillation scheme that incorporates "learned" knowledge of deep unsupervised ML models. We implement a prototype of CyberSentinel on a testbed with an Intel Tofino switch and evaluate it on various real-world use cases.
  arXiv  Detail & Related papers  (2024-12-21T16:35:44Z)
• Can Neural Decompilation Assist Vulnerability Prediction on Binary Code? [0.0]
  This paper presents an experimental study to predict vulnerabilities in binary code without source code or complex representations of the binary. The results outperform the state-of-the-art in both neural decompilation and vulnerability prediction.
  arXiv  Detail & Related papers  (2024-12-10T14:17:14Z)
• Finding Transformer Circuits with Edge Pruning [71.12127707678961]
  We propose Edge Pruning as an effective and scalable solution to automated circuit discovery. Our method finds circuits in GPT-2 that use less than half the number of edges compared to circuits found by previous methods. Thanks to its efficiency, we scale Edge Pruning to CodeLlama-13B, a model over 100x the scale that prior methods operate on.
  arXiv  Detail & Related papers  (2024-06-24T16:40:54Z)
• Scalable Surrogate Verification of Image-based Neural Network Control Systems using Composition and Unrolling [9.633494094538017]
  We build on work that considers a surrogate verification approach, training a conditional generative adversarial network (cGAN) as an image generator in place of the real world. We overcome one-step error by composing the system's dynamics along with the cGAN and neural network controller. We reduce multi-step error by repeating the single-step composition, essentially unrolling multiple steps of the control loop into a large neural network.
  arXiv  Detail & Related papers  (2024-05-28T19:56:53Z)
• Automatically Identifying Local and Global Circuits with Linear Computation Graphs [45.760716193942685]
  We introduce our circuit discovery pipeline with Sparse Autoencoders (SAEs) and a variant called Transcoders. Our methods do not require linear approximation to compute the causal effect of each node. We analyze three kinds of circuits in GPT-2 Small: bracket, induction, and Indirect Object Identification circuits.
  arXiv  Detail & Related papers  (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]
  Integrated sensing and communications (ISAC) is pivotal for 6G communications and is boosted by the rapid development of reconfigurable intelligent surfaces (RISs) This paper proposes the X2Track framework, where we model the tracking function by a hierarchical architecture, jointly utilizing multi-modal CSI indicators across multiple bands, and optimize it in a cross-domain manner. Under X2Track, we design an efficient deep learning algorithm to minimize tracking errors, based on transformer neural networks and adversarial learning techniques.
  arXiv  Detail & Related papers  (2024-05-10T08:04:27Z)
• Dynamic Neural Control Flow Execution: An Agent-Based Deep Equilibrium Approach for Binary Vulnerability Detection [4.629503670145618]
  Software vulnerabilities are a challenge in cybersecurity. DeepEXE is an agent-based implicit neural network that mimics the execution path of a program. We show that DeepEXE is an accurate and efficient method and outperforms the state-of-the-art vulnerability detection methods.
  arXiv  Detail & Related papers  (2024-04-03T22:07:50Z)
• FoC: Figure out the Cryptographic Functions in Stripped Binaries with LLMs [54.27040631527217]
  We propose a novel framework called FoC to Figure out the Cryptographic functions in stripped binaries. We first build a binary large language model (FoC-BinLLM) to summarize the semantics of cryptographic functions in natural language. We then build a binary code similarity model (FoC-Sim) upon the FoC-BinLLM to create change-sensitive representations and use it to retrieve similar implementations of unknown cryptographic functions in a database.
  arXiv  Detail & Related papers  (2024-03-27T09:45:33Z)
• Software Vulnerability Detection via Deep Learning over Disaggregated Code Graph Representation [57.92972327649165]
  This work explores a deep learning approach to automatically learn the insecure patterns from code corpora. Because code naturally admits graph structures with parsing, we develop a novel graph neural network (GNN) to exploit both the semantic context and structural regularity of a program.
  arXiv  Detail & Related papers  (2021-09-07T21:24:36Z)
• Risk-Averse MPC via Visual-Inertial Input and Recurrent Networks for Online Collision Avoidance [95.86944752753564]
  We propose an online path planning architecture that extends the model predictive control (MPC) formulation to consider future location uncertainties. Our algorithm combines an object detection pipeline with a recurrent neural network (RNN) which infers the covariance of state estimates. The robustness of our methods is validated on complex quadruped robot dynamics and can be generally applied to most robotic platforms.
  arXiv  Detail & Related papers  (2020-07-28T07:34:30Z)
• Binary DAD-Net: Binarized Driveable Area Detection Network for Autonomous Driving [94.40107679615618]
  This paper proposes a novel binarized driveable area detection network (binary DAD-Net) It uses only binary weights and activations in the encoder, the bottleneck, and the decoder part. It outperforms state-of-the-art semantic segmentation networks on public datasets.
  arXiv  Detail & Related papers  (2020-06-15T07:09:01Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.