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

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.

本文提出了一种新的工具，名为Rampo，可以执行二进制代码分析，以确定CPS中的网络动力学漏洞。该工具将描述动力学效应的信号时间逻辑（STL）公式作为输入，即，物理系统的行为，人们想要避免的。然后，该工具在二进制代码中搜索可能导致这种物理行为的可能网络轨迹。该搜索集成了二进制代码分析工具和混合系统伪造工具，使用反例引导抽象细化（CEGAR）的方法。Rampo首先分析二进制代码，以提取表示代码中不同路径的符号约束。然后，这些符号约束被传递到可满足性模理论（SMT）求解器，以提取代码中每个路径可以产生的控制信号的范围。下一步是使用混合系统伪造工具搜索可能的物理轨迹，该工具遵循网络路径的行为，但会导致违反STL公式。由于需要探索的网络路径的数量随着物理轨迹的长度呈指数级增加，因此我们基于先前的伪造结果迭代地执行网络路径约束的细化，并遍历从控制程序获得的抽象路径树以探索系统的搜索空间。为了说明二进制代码分析在识别网络动力学漏洞方面的实际效用，我们提出了来自不同CPS域的案例研究，展示了如何在控制程序中发现它们。我们的工具可以计算相同数量的漏洞，同时导致从3倍到98倍的加速。