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倍。