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模型以减轻实际攻击。 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 mentality, 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.模型转换工具一致地结合了原始的基于状态机器的模型，弹性模式的集合（或潜在的编辑）以及分析仪的反馈，以产生更新的弹性行为模型。该工具会自动通过以模型转换脚本编写的可扩展的弹性模式库进行搜索，以解决模型维修问题。模型分析仪工具在设计时间和运行时操作期间多个阶段分析系统正确性要求。模型转换生成的完整模型是使用静态伪造器的错误，而相应的实现则使用运行时监视器工具监视违规行为。为了确保丰富的规格，研究人员正在利用通过Hyperstl指定的对象和安全限制。另一个功能是反示例分析仪，该分析仪会向设计人员提供反馈，以开发新的弹性模式。该工具链的设计和实施需要理论上的进步，以严格的形式化，计算引擎和启发式方法以进行可伸缩。该项目中开发的模型维修，弹性模式和正式分析的算法是对CP的设计和分析的重要兴趣的贡献。该奖项反映了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

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

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