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

该项目主张在安全和安全关键的网络物理系统（CPS）的发展范式转变，提出了一个安全的建设控制器综合框架，概括了现有的正确的建设综合方法，同时考虑隐私和安全属性。CPS是日益互联和智能世界的技术支柱，在这个世界中，设计错误或安全漏洞可能是灾难性的。自动驾驶汽车、可穿戴和植入式医疗设备、智能基础设施和互联社区是强调现代CPS隐私和安全问题的一些引人注目的例子。在过去的十年中，安全问题在CPS的设计中受到了相当大的关注，而安全分析则被作为后期阶段的事后考虑。由于事后安全验证和确认的高成本，这种现有的范例导致CPS的开发成本高且耗时长。拟议的研究为CPS应用的安全部署奠定了基础，包括自动驾驶汽车、可穿戴和植入式医疗设备以及自主无人机。所提出的安全的施工控制器的合成方法是通过一个一般的计划，称为符号控制器合成。在这种方法中，系统的安全性和隐私性的要求，使用线性时序逻辑公式或欧米茄正则语言表示的正式规范。然后，连续控制系统的一个有限的抽象构造在这样一种方式，安全性和隐私属性被保留的抽象。此外，一个安全的建设控制器设计的有限抽象可以细化到一个混合控制器执行给定的正式规格超过原系统。该项目开发了用于构建离散控制器的算法技术和计算工具，以保证安全和隐私属性，然后将其自动细化为原始混凝土系统的混合控制器。为了解决与符号控制方案相关的计算复杂性，该项目提出了一种分而治之的策略，通过将计算机科学（例如假设保证规则）的合成技术与控制理论（例如小增益定理）相结合，来扩展CPS的结构安全控制器合成。建议的理论结果将提供给实践控制工程师作为一个端到端的工具，实现安全的大规模CPS.This奖项的建设控制器合成的设计流程，反映了NSF的法定使命，并已被认为是值得通过使用基金会的智力价值和更广泛的影响审查标准进行评估的支持。

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.