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) 它提供了一种新的方法，包括端到端的设计和软件实现，以促进基于模型的工作。 (2) 它使设计者能够指定弹性模式；研究者正在为 CPS 模型设计可扩展的模型转换语言。 (3) 该方法利用了形式分析。信号时序逻辑超属性 (HyperSTL) 在多个阶段中形式化的正确性要求 (4) 软件工具正在应用于概念验证案例研究，其中可以修复 CPS 模型以减轻该项目的影响。 (1) 新技术和最先进的软件工具，以增强 CPS 的安全性、可靠性、安保性和弹性，以及 (2) 加强 CPS 工程开发的指导、技能建设和劳动力准备工作所提出的框架始终涉及两个主要工具的设计、实现、评估和集成：模型转换和模型分析器。模型转换工具包含一个原始的基于状态机的模型，一个集合。该工具会自动搜索可扩展的弹性模式库（编写为模型转换脚本），以解决模型修复问题。分析器工具在设计时和运行时操作期间将系统正确性要求置于多个阶段，使用静态伪造器来伪造模型转换生成的完整模型，同时使用运行时监视工具监视相应的实现是否存在违规。为了确保丰富的规范，研究人员正在利用通过 HyperSTL 指定的目标和安全约束，另一个功能是反例分析器，它可以向设计人员提供反馈，以开发新的弹性模式和工具链的实现。需要在严格的形式化、计算引擎和可扩展性启发方面取得理论进展。该项目中开发的模型修复、弹性模式和形式分析算法对 CPS 设计和分析的研究社区具有重大意义。授予 NSF 的法定使命，并通过评估反映使用基金会的智力优点和更广泛的影响审查标准，被认为值得支持。

项目成果

期刊论文数量（5）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

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
通讯作者：
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
影响因子：
0
作者：
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)
影响因子：
0
作者：
M. Ivashchenko;Sung-Woo Choi;L. V. Nguyen;Hoang-Dung Tran
通讯作者：
M. Ivashchenko;Sung-Woo Choi;L. V. Nguyen;Hoang-Dung Tran

Motion Planning Using Hyperproperties for Time Window Temporal Logic