Secure-by-Construction Controller Synthesis for Cyber-Physical Systems

信息物理系统的安全构建控制器综合

• 批准号: 2015403
• 负责人: Majid Zamani
• 金额: $ 38.76万
• 依托单位: University of Colorado at Boulder
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-08-15 至 2024-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2015403&HistoricalAwards=false
• 关键词: Secure; Construction; Controller; Synthesis; Cyber

This project advocates a paradigm shift in the development of safety- and security-critical cyber-physical systems (CPS) by proposing a secure-by-construction controller synthesis framework that generalizes existing correct-by-construction synthesis methods by considering privacy and safety properties simultaneously. CPS are the technological backbone of the increasingly interconnected and smart world where design fault or security vulnerability can be catastrophic. Self-driving cars, wearable and implantable medical devices, smart infrastructure and connected communities are some of the high-profile examples that underscore privacy and safety concerns of modern CPS. In the last decade, safety concerns have received considerable attention in the design of CPS, while security analysis is left as an afterthought for the later stages. This existing paradigm results in costly and lengthy development of CPS due to the high cost of post-facto security verification and validation. The proposed research lays the foundations for safe and secure deployments of CPS applications including self-driving cars, wearable and implantable medical devices, and autonomous drones. The proposed secure-by-construction controller synthesis methodology is through a general scheme called symbolic controller synthesis. In this methodology, the safety and privacy requirements for the system are described using formal specifications expressed as linear temporal logic formulae or omega-regular languages. Then, a finite abstraction of the continuous control system is constructed in such a way that safety and privacy properties are preserved over the abstraction. Moreover, a secure-by-construction controller designed on the finite abstraction can be refined into a hybrid controller enforcing given formal specifications over the original system. This project develops algorithmic techniques and computational tools for constructing discrete controllers guaranteeing both safety and privacy properties, which are then automatically refined as hybrid controllers for the original concrete systems. To tackle the computational complexity associated with symbolic control schemes, the project proposes a divide and conquer strategy to scale secure-by-construction controller synthesis for CPS by combining compositional synthesis techniques from computer science (e.g. assume-guarantee rules) with those from control theory (e.g. small-gain theorems). The proposed theoretical results will be made available to the practicing control engineers as an end-to-end tool implementing a design flow for secure-by-construction controller synthesis for large-scale 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)开发的范式转变。CP是日益互联的智能世界的技术支柱，在这个世界中，设计缺陷或安全漏洞可能是灾难性的。自动驾驶汽车、可穿戴和植入式医疗设备、智能基础设施和互联社区都是突显现代CP隐私和安全担忧的一些高调例子。在过去的十年中，安全问题在CPS的设计中得到了相当大的关注，而安全分析则被留到了后面的阶段。由于事后安全核查和确认的高成本，这一现有模式导致了成本高昂和冗长的方案规划的开发。拟议的研究为安全可靠地部署CPS应用奠定了基础，包括自动驾驶汽车、可穿戴和植入式医疗设备以及自动无人机。所提出的按构造安全的控制器综合方法是通过一种称为符号控制器综合的一般方案来实现的。在这种方法中，系统的安全和隐私需求使用表示为线性时态逻辑公式或omega-Regular语言的形式规范来描述。然后，以这样一种方式构造连续控制系统的有限抽象，即在该抽象之上保持安全和隐私属性。此外，在有限抽象的基础上设计的按构造安全控制器可以被细化为在原始系统上强制执行给定形式规范的混合控制器。这个项目开发了算法技术和计算工具，用于构建既保证安全又保证隐私的离散控制器，然后将这些控制器自动改进为原始具体系统的混合控制器。为了解决与符号控制方案相关的计算复杂性，该项目提出了一种分而治之的策略，通过结合计算机科学的组合综合技术(例如假设-保证规则)和控制理论的组合综合技术(例如小增益定理)来扩展CPS的按构造安全控制器综合。建议的理论结果将作为端到端工具提供给实践控制工程师，作为实施大规模CP的按施工安全控制器综合的设计流程的工具。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Secure-by-Construction Synthesis of Cyber-Physical Systems

• DOI: 10.1016/j.arcontrol.2022.03.004
• 发表时间: 2022-02
• 期刊: ArXiv
• 作者: Siyuan Liu;Ashutosh Trivedi;Xiang Yin;Majid Zamani

Verification of approximate infinite-step opacity using barrier certificates

使用屏障证书验证近似无限步不透明度

• DOI: 10.23919/ecc55457.2022.9838153
• 发表时间: 2022
• 期刊: European Control Conference (ECC
• 作者: Kalat, Shadi Tasdighi;Liu, Siyuan;Zamani, Majid
• 通讯作者: Zamani, Majid

Modular Verification of Opacity for Interconnected Control Systems via Barrier Certificates

• DOI: 10.1109/lcsys.2021.3087103
• 发表时间: 2022
• 期刊: IEEE Control Systems Letters
• 影响因子: 3
• 作者: Shadi Tasdighi Kalat;Siyuan Liu;Majid Zamani

Translating Omega-Regular Specifications to Average Objectives for Model-Free Reinforcement Learning

• DOI: 10.5555/3535850.3535933
• 发表时间: 2022
• 作者: M. Kazemi;Mateo Perez;F. Somenzi;Sadegh Soudjani;Ashutosh Trivedi;Alvaro Velasquez

A Scenario Approach for Synthesizing k -Inductive Barrier Certificates

合成 k 感应势垒证书的场景方法

• DOI: 10.1109/lcsys.2022.3184661
• 发表时间: 2022
• 期刊: IEEE Control Systems Letters
• 影响因子: 3
• 作者: Murali, Vishnu;Trivedi, Ashutosh;Zamani, Majid
• 通讯作者: Zamani, Majid