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.

翻译：检测信息物理系统（CPS）中的物理性漏洞——即控制代码中可能导致危险物理后果的缺陷——是一项关键挑战。该任务的复杂性在于需要分析复杂软件行为与系统物理动力学之间错综复杂的耦合关系。此外，CPS应用中控制代码的周期性执行会随时间产生需分析的执行路径组合爆炸，这远远超出了传统单次运行代码分析的范围。本文提出RampoNN，这是一个在给定控制代码、物理系统模型以及安全行为的信号时序逻辑（STL）规范下，系统性地识别物理性漏洞的新型框架。RampoNN首先分析控制代码，以映射在不同执行分支下可能生成的控制信号。随后，它采用神经网络来抽象物理系统的行为。为了克服标准神经网络可达性分析扩展性差和过度近似过于宽松的问题，RampoNN创新性地利用了深度伯恩斯坦神经网络，该网络配备了定制的可达性算法，能够产生数量级更紧的边界。这种高精度的可达性分析使得RampoNN能够快速剪除大量被保证安全的行为，并根据剩余轨迹违反规范的可能性对其进行排序。该分析的结果随后被用于有效引导一个证伪引擎，将其搜索集中在最有希望发现实际漏洞的系统行为上。我们在一个PLC控制的水箱系统和一个用于汽车发动机的切换PID控制器上评估了我们的方法。结果表明，与其他最先进的方法相比，RampoNN能将发现物理性漏洞的过程加速高达98.27%，并展现出更优的可扩展性。