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

CRII：SHF：基于模型的网络物理系统修复以提高弹性

• 批准号: 2245853
• 负责人: Luan Nguyen
• 金额: $ 17.5万
• 依托单位: University of Dayton
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-05-01 至 2025-04-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2245853&HistoricalAwards=false
• 关键词: CRII; SHF; Model; Based; Repair

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.

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

项目成果

Reachability Analysis of Sigmoidal Neural Networks

• DOI: 10.1145/3627991
• 发表时间: 2023-10
• 期刊: ACM Transactions on Embedded Computing Systems
• 影响因子: 2
• 作者: Sung-Woo Choi;Michael Ivashchenko;Luan V. Nguyen;Hoang-Dung Tran

Model Checking Time Window Temporal Logic for Hyperproperties

超属性的模型检查时间窗口时态逻辑

• DOI: 10.1145/3610579.3611077
• 发表时间: 2023
• 期刊: ACM
• 作者: Bonnah, Ernest;Nguyen, Luan;Hoque, Khaza Anuarul
• 通讯作者: Hoque, Khaza Anuarul

Verifying Binary Neural Networks on Continuous Input Space using Star Reachability

• DOI: 10.1109/formalise58978.2023.00009
• 发表时间: 2023-05
• 期刊: 2023 IEEE/ACM 11th International Conference on Formal Methods in Software Engineering (FormaliSE)
• 作者: M. Ivashchenko;Sung-Woo Choi;L. V. Nguyen;Hoang-Dung Tran

Decentralized Safe Control for Distributed Cyber-Physical Systems using Real-time Reachability Analysis

使用实时可达性分析的分布式信息物理系统的去中心化安全控制

• DOI: 10.1109/tcns.2023.3239562
• 发表时间: 2023
• 期刊: IEEE Transactions on Control of Network Systems
• 影响因子: 4.2
• 作者: Nguyen, Luan Viet;Tran, Hoang-Dung;Johnson, Taylor;Gupta, Vijay
• 通讯作者: Gupta, Vijay

Motion Planning Using Hyperproperties for Time Window Temporal Logic

• DOI: 10.1109/lra.2023.3280830
• 发表时间: 2023-08
• 期刊: IEEE Robotics and Automation Letters
• 影响因子: 5.2
• 作者: Ernest Bonnah;L. Nguyen;Khaza Anuarul Hoque