Trustworthy operation of next-generation complex power grid critical infrastructures requires mathematical and practical verification solutions to guarantee the correct infrastructural functionalities. This project develops the foundations of theoretical modeling, synthesis and real-world deployment of a formal and scalable controller code verifier for programmable logic controllers (PLCs) in cyber-physical settings. PLCs are widely used for control automation in industrial control systems. A PLC is typically connected to an engineering workstation where engineers develop the control logic to process the input values from sensors and issue control commands to actuators. The project focuses on protecting infrastructures against malicious control injection attacks on PLCs, such as Stuxnet, that inject malicious code on the device to drive the underlying physical platform to an unsafe state. The broader impact of this proposal is highly significant. It offers potential for real-time security for critical infrastructure systems covering sectors such as energy and manufacturing. The project's intellectual merit is in providing a mathematical and practical verification framework for cyber-physical systems through integration of offline formal methods, online monitoring solutions, and power systems analysis. Offline formal methods do not scale for large-scale platforms due to their exhaustive safety analysis of all possible system states, while online monitoring often reports findings too late for preventative action. This project takes a hybrid approach that dynamically predicts the possible next security incidents and reports to operators before an unsafe state is encountered, allowing time for response. The broader impact of this project is in providing practical mathematical analysis capabilities for general cyber-physical safety-critical infrastructure with potential direct impact on our national security. The research outcomes are integrated into education modules for graduate, undergraduate, and K-12 classrooms.

Cyber-physical systems regulating critical infrastructures, such as electrical grids and water networks, are increasingly geographically distributed, necessitating communication between remote sensors, actuators and controllers. The combination of networked computational and physical subsystems leads to new security vulnerabilities that adversaries can exploit with devastating consequences. A synchronized attack on the interdependent network components and physical plants can create complex and new security vulnerabilities that cannot be addressed by securing the constituent systems individually. This project takes a holistic view by utilizing the properties of physical systems to design new secure protocols and architectures for cyber-physical systems (CPS) through a unified conceptual framework, which uses models for the physical system and the communication/computation network to define precise attack models and vulnerabilities. These mathematical models are used to design algorithms and protocols with provable operational security guarantees, thus enabling the design of more trustworthy architectures and components. The algorithms, protocols, and architectures are validated on CPS testbeds targeting building, automobile, and smart-grid applications. Additionally, the research is being integrated into the curriculum via the creation of novel coursework combining the underlying control, information theory, cryptography, and embedded system concepts. By improving the protection of critical cyber-physical infrastructure against emerging threats, this research is expected to provide direct socio-economic benefits, ranging from individual organizations to a national scale. The inter-disciplinary team of this project will integrate teaching and curriculum development with the research, contributing to the training of a new generation of engineers well versed in the design of trustworthy cyber-physical systems.

This project is developing techniques for secured real-time services for cyber-physical systems. In particular, the research is incorporating real-time traffic modeling techniques into the security service, consequently enhancing both system security and real-time capabilities in an adverse environment. While this proposed methodology has not yet been fully tested, it is potentially transformative. To defend against traffic analysis attacks, the research is developing algorithms that can effectively mask the actual operational modes of cyber-physical applications without compromising the guaranteed quality of service. This is achieved by using the traffic modeling theory, developed by the PIs, to precisely manage the network traffic at the right time and the right place. This traffic modeling theory can also help in develop efficient attack detection and suppression methods that can identify and restrain an attack in real-time. The proposed methods are expected to be more effective, efficient, and scalable than traditional methods.

This project is developing techniques for secured real-time services for cyber-physical systems. In particular, the research is incorporating real-time traffic modeling techniques into the security service, consequently enhancing both system security and real-time capabilities in an adverse environment. While this proposed methodology has not yet been fully tested, it is potentially transformative. To defend against traffic analysis attacks, the research is developing algorithms that can effectively mask the actual operational modes of cyber-physical applications without compromising the guaranteed quality of service. This is achieved by using the traffic modeling theory, developed by the PIs, to precisely manage the network traffic at the right time and the right place. This traffic modeling theory can also help in develop efficient attack detection and suppression methods that can identify and restrain an attack in real-time. The proposed methods are expected to be more effective, efficient, and scale-able than traditional methods.