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倍的加速比。