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

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

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.