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

TL;DR

RampoNN tackles the challenge of cyber-kinetic vulnerability detection in CPS by addressing the $k^H$ combinatorial explosion of possible cyber trajectories with an abstraction-based, reachability-guided approach. It combines DynamicsNN (modeling the physical dynamics) and STL2NN (encoding the STL specification) as DeepBern-Nets, enabling tight, global bounds on robustness via Bernstein-based operators to prune safely. The framework then focuses expensive falsification on the UNCERTAIN trajectories to efficiently uncover concrete vulnerabilities, demonstrated on a PLC water-tank and a switched-PID automotive engine, with acceleration up to 98.27% and superior scalability. This work provides a practical, scalable pipeline for safety-critical CPS analysis that integrates formal reachability with learning-enabled components and supports iterative vulnerability remediation.

Abstract

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.

Figures (4)

• Figure 1: An example of cyber-kinetic vulnerability that shows both the physical trajectory (right) violating some safety constraint $\varphi$ and the corresponding cyber trajectory (left). The cyber trajectory tree (left) illustrates the $k^H$ combinatorial explosion. Each branch represents a different control decision, causing the number of possible cyber trajectories to analyze to grow exponentially.
• Figure 2: RampoNN Framework Overview.
• Figure 3: Execution Time and number of identified vulnerabilities for different time horizons (Top) Water Tank model (Bottom) Automotive Engine model.
• Figure :

Theorems & Definitions (1)

• Definition 3.1: Cyber Trajectories