CRII: SHF: Model-Based Repair of Cyber-Physical Systems for Improving Resiliency

基于模型的设计为帮助开发人员以系统的方式构建可靠和安全的网络物理系统(CP)提供了一种有前途的方法。然而，在设计时构建行为模型来为所有类型的攻击和故障提供弹性是出了名的困难。目前缺乏能够有效修复初始设计的廉价、自动化的软件，基于模型的系统开发人员经常需要从头开始重新设计和重新实现系统。该项目正在开发一种方法，以及一个相关的框架，以帮助设计师修复原始的CPS模型，以便它继续满足修改后的假设下的正确性要求。该项目的新颖性如下。(1)它通过端到端的软件设计和实施提供了一种全新的方法，以促进基于模型的修复，从而提高CP对意外攻击和故障的恢复能力。(2)它使设计人员能够指定弹性模式；研究人员正在为CPS模型设计一个可扩展的模型转换语言。(3)该方法针对信号时态逻辑超属性(HyperSTL)中形式化的正确性需求在多个阶段进行了形式化分析。(4)正在将软件工具应用于概念验证案例研究，在这些案例研究中，可以修复CPS模型以减少实际攻击。该项目的影响在于：(1)开发新技术和最先进的软件工具来加强CPS的安全性、可靠性、安全性和弹性，以及(2)在西南部俄亥俄州地区和全国范围内加强CPS工程的指导、技能建设和劳动力准备。建议的框架涉及两个主要工具的设计、实施、评估和集成：模型转换和模型分析器。模型转换工具一致地结合了基于状态机的原始模型、弹性模式(或潜在编辑)的集合以及来自分析器的反馈，以生成更新的弹性行为模型。该工具自动搜索可扩展的弹性模式库，编写为模型转换脚本，以解决模型修复问题。Model Analyzer工具在设计时和运行时操作期间在多个阶段分析系统正确性需求。模型转换生成的完整模型使用静态证伪器进行篡改，而相应的实现则使用运行时监视工具监视违规。为了确保一套丰富的规范，研究人员利用了通过HyperSTL指定的目标和安全约束。另一个功能是反例分析器，它向设计人员提供反馈，以开发新的弹性模式。工具链的设计和实现需要在严格的形式化、计算引擎和可伸缩性启发式方面的理论进步。在这个项目中开发的模型修复、弹性模式和形式分析的算法是研究社区在设计和分析CP方面的重要贡献。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Model-based design offers a promising approach for assisting developers to build reliable and secure cyber-physical systems (CPS) in a systematic manner. However, constructing a behavioral model at design time that offers resiliency for all kinds of attacks and failures is notoriously difficult. There is currently a shortage of inexpensive, automated software that can effectively repair an initial design, and a model-based system developer regularly needs to redesign and reimplement a system from scratch. The project is developing a methodology, along with an associated framework, to assist a designer in repairing an original CPS model so that it continues to satisfy the correctness requirements under modified assumptions. The project’s novelties are as follows. (1) It provides a fresh approach with an end-to-end design and implementation of a software to facilitate model-based repair for improving the resiliency of CPS against unanticipated attacks and failures. (2) It enables a designer to specify resiliency patterns; the investigator is designing an extensible model transformation language for CPS models. (3) The methodology utilizes formal analysis with respect to correctness requirements formalized in signal temporal logic hyper-properties (HyperSTL) at multiple stages. (4) Software tools are being applied on proof-of-concept case studies where the CPS models can be repaired to mitigate practical attacks. The project’s impacts are in (1) developing new technologies and state-of-the-art software tools to enforce the safety, reliability, security, and resiliency of CPS and (2) strengthening mentorship, skill-building, and workforce readiness for CPS engineering in the Southwest Ohio region and nationally.The proposed framework involves the design, implementation, evaluation, and integration of two main tools: a Model Transformation and a Model Analyzer. A Model Transformation tool consistently incorporates an original state-machine-based model, a collection of resiliency patterns (or potential edits), and feedback from analyzers to produce an updated resilient behavioral model. The tool automatically searches through the extensible library of resiliency patterns, written as model transformation scripts, to solve the model repair problem. A Model Analyzer tool analyzes the system correctness requirements at multiple stages, both at design time and during runtime operation. The complete model generated by the Model Transformation is falsified using a static falsifier, while the corresponding implementation is monitored for violations using a runtime monitor tool. To ensure a rich set of specifications, the investigator is utilizing objectives and safety constraints specified via HyperSTL. An additional feature is a counter-example analyzer that produces feedback to a designer for developing new resiliency patterns. Design and implementation of the tool-chain requires theoretical advances in terms of rigorous formalization, computational engines, and heuristics for scalability. The algorithms for model repair, resiliency patterns, and formal analysis developed in this project are contributions of significant interest to the research community in design and analysis of CPS.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.