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.
