RampoNN: A Reachability-Guided System Falsification for Efficient Cyber-Kinetic Vulnerability Detection

Detecting kinetic vulnerabilities in Cyber-Physical Systems (CPS), vulnerabilities in control code that can precipitate hazardous physical consequences, is a critical challenge. This task is complicated by the need to analyze the intricate coupling between complex software behavior and the system's physical dynamics. Furthermore, the periodic execution of control code in CPS applications creates a combinatorial explosion of execution paths that must be analyzed over time, far exceeding the scope of traditional single-run code analysis. This paper introduces RampoNN, a novel framework that systematically identifies kinetic vulnerabilities given the control code, a physical system model, and a Signal Temporal Logic (STL) specification of safe behavior. RampoNN first analyzes the control code to map the control signals that can be generated under various execution branches. It then employs a neural network to abstract the physical system's behavior. To overcome the poor scaling and loose over-approximations of standard neural network reachability, RampoNN uniquely utilizes Deep Bernstein neural networks, which are equipped with customized reachability algorithms that yield orders of magnitude tighter bounds. This high-precision reachability analysis allows RampoNN to rapidly prune large sets of guaranteed-safe behaviors and rank the remaining traces by their potential to violate the specification. The results of this analysis are then used to effectively guide a falsification engine, focusing its search on the most promising system behaviors to find actual vulnerabilities. We evaluated our approach on a PLC-controlled water tank system and a switched PID controller for an automotive engine. The results demonstrate that RampoNN leads to acceleration of the process of finding kinetic vulnerabilities by up to 98.27% and superior scalability compared to other state-of-the-art methods.

• Publication year

  2025

• Venue

  arXiv.org

• Publication date

  2025-11-20

• Fields of study

  Computer Science, Engineering

• Identifiers
  DOI 10.48550/arXiv.2511.16765arXiv 2511.16765
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• A Neurosymbolic Approach to the Verification of Temporal Logic Properties of Learning-enabled Control Systems

  2023cited by this paper
• NNV 2.0: The Neural Network Verification Tool

  2023cited by this paper
• DeepBern-Nets: Taming the Complexity of Certifying Neural Networks using Bernstein Polynomial Activations and Precise Bound Propagation

  2023influential reference
• BERN-NN: Tight Bound Propagation For Neural Networks Using Bernstein Polynomial Interval Arithmetic

  2022cited by this paper
• PGFUZZ: Policy-Guided Fuzzing for Robotic Vehicles

  2021cited by this paper
• Verisig 2.0: Verification of Neural Network Controllers Using Taylor Model Preconditioning

  2021cited by this paper
• Symbolic execution formally explained

  2021cited by this paper
• ReachNN*: A Tool for Reachability Analysis of Neural-Network Controlled Systems

  2020cited by this paper
• Active fuzzing for testing and securing cyber-physical systems

  2020cited by this paper
• Reachability analysis for neural feedback systems using regressive polynomial rule inference

  2019cited by this paper
• JuliaReach: a toolbox for set-based reachability

  2019cited by this paper
• The Marabou Framework for Verification and Analysis of Deep Neural Networks

  2019cited by this paper
• VerifAI: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems

  2019cited by this paper
• AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation

  2018cited by this paper
• Verisig: verifying safety properties of hybrid systems with neural network controllers

  2018cited by this paper
• Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks

  2017cited by this paper
• HyLAA: A Tool for Computing Simulation-Equivalent Reachability for Linear Systems

  2017cited by this paper
• Compositional Falsification of Cyber-Physical Systems with Machine Learning Components

  2017cited by this paper
• Flow*: An Analyzer for Non-linear Hybrid Systems

  2013cited by this paper
• Efficient Robust Monitoring for STL

  2013cited by this paper
• SpaceEx: Scalable Verification of Hybrid Systems

  2011cited by this paper
• S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems

  2011influential reference
• Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems

  2010cited by this paper
• Z3: An Efficient SMT Solver

  2008cited by this paper
• Monitoring Temporal Properties of Continuous Signals

  2004cited by this paper

• No citing papers are available for this paper.