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

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

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.