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

TL;DR

The paper addresses the challenge of identifying cyber-kinetic vulnerabilities in CPS by bridging binary code analysis with physical-dynamics falsification. It introduces Rampo, a CEGAR-based framework that uses symbolic execution to extract path constraints, SMT to derive per-path control ranges, and a falsification engine to explore physics trajectories for STL violations, with iterative refinement to cover the exponential search space. The authors demonstrate soundness (though not completeness) of the approach and show substantial scalability and vulnerability enumeration gains (3x–98x speedups) across multiple CPS domains, including cyber-kinetic and cyber-physical-kinetic scenarios. The work has practical significance for securing critical infrastructure by enabling comprehensive, temporally-aware analysis of how software control can induce unsafe physical behavior, even under sensor-manipulation threats.

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.

Figures (9)

• Figure 1: Rampo takes as input the binary code of the control program, a black-box model that represents the physics of the system, and cyber-kinetic safety requirements captured in STL. The outputs are the cyber trajectories inside the binary code and the corresponding physical system behavior that can lead to violation of the STL requirements. Moreover, Rampo can also output attacks on the system's sensors that can also lead to kinetic vulnerabilities.
• Figure 2: An example of a code with three paths (marked with blue, green, and yellow). When considering the temporal evolution of a CPS, one needs to take into account the different combinations of these three paths across time, which leads to an exponential increase in the overall number of paths.
• Figure 3: A pictorial representation of the proposed framework. Binary-level control programs are analyzed using symbolic execution tools to extract the path constraints, path functions, and the range of the control signals associated with each path in the program. Next, a Counter-Example Guided Abstraction Refinement (CEGAR) is used to abstract all cyber trajectories for a horizon $H$, and a falsification engine is used to search for trajectories of the physical system that violate the safety requirements. The cyber trajectories are then refined around the falsifying trajectories until all concrete cyber-kinetic vulnerabilities are found.
• Figure 4: A pictorial representation of the Counter-Example Guided Abstraction Refinement process. (a) A tree of all possible cyber trajectories for a controller code with 3 paths and $H = 3$. (b) In the first iteration, Rampo will abstract all the trajectories in the search tree by considering the control signals that can be produced by all trajectories. (c) The falsification engine finds a physical-level trajectory that violates the safety requirements and Rampo extracts the corresponding trajectory. (d) The control signal ranges are refined/concretized around the trajectory found from the previous step except for the last time step. The falsification engine could not find a corresponding physical-level trajectory that violates the requirements, and hence, this sub-tree is removed from the search space. (e) Rampo backtracks one level up and abstracts the cyber trajectories around the truncated trajectory found before. (f) The falsification engine reported a physical-level vulnerability in the search tree, and the vulnerability was checked to be a concrete one.
• Figure 5: The number of cyber-kinetic vulnerabilities found and the execution time. $n\_partition$ refers to the number of partitions among each dimension of the state space in the model. In the brute-force (baseline) approach, as the number of partitions increases, the execution time increases exponentially. For both the linear- and binary-search-based abstraction refinement approaches of Rampo, the execution time is almost constant as the number of integrators in the model increases. This leads to a speedup that ranges from $3\times$ to $98\times$ while computing the same number of vulnerabilities.

Theorems & Definitions (1)

• Definition 3.1: Cyber Trajectories