From simple logical constructs to complex deep neural network models, Artificial Intelligence (AI) agents are increasingly controlling physical/mechanical systems. Self-driving cars, drones, and smart cities are just examples of AI-controlled Cyber-Physical Systems (CPS) to name a few. However, regardless of the explosion in the use of AI within a multitude of CPS domains, the safety and reliability of these AI-controlled CPS is still an under-studied problem. It is then unsurprising the failure of these systems in several, safety-critical, situations leading to human fatalities.

Mathematically based techniques for the specification, development, and verification of software and hardware systems, also known as formal methods, hold the promise to provide appropriate rigorous analysis of the reliability and safety of engineered systems. Unfortunately, there is currently a huge disconnect within the field of CPS formal verification. On the one side, the celebrated achievements in software and hardware verification field are inadequate of generalizing to analyze the dynamics of the underlying physical components of CPS. On the other hand, the techniques developed in the control theory community have focused mainly on the formal verification of the dynamics of physical/mechanical systems while ignoring the complexity of the computational and cyber components. This project isolates the key reasons for those gaps and addresses them systematically leading to a new generation of formal methods that are capable of simultaneously analyzing the cyber components (including AI-agents, in general, and deep neural networks, in particular) and the physical components of CPS. This new generation of formal methods will be used to analyze the safety and reliability of AI-controlled CPS, characterize the environments for which the system is guaranteed to operate correctly, automatically find vulnerabilities in AI logic, and predict their failure at real-time.

State-of-the-art cyber-physical systems (CPS) are far from being fully autonomous. Regardless of how many situations they were trained (or programmed) to consider, autonomous CPS will always face new situations which the human designer failed to examine during the design phase. The problem is exacerbated in cases when malicious agents are present. In such circumstances, malicious agents could exploit the lack of CPS capability to adapt to new situations that impose safety-threatening scenarios. This opens the question of how to equip CPS with a layer of ``cognition'' that allows CPS to learn and adapt from adversarial situations and acquire a level of resilience against the unforeseen, while still satisfying strong theoretical guarantees. We refer to CPS with such capabilities as ``Resilient-by-Cognition CPS'' which is the main focus of this project.

In biological context, adversarial situations allowed biological species to evolve and thrive in their nature. Relevant and applicable insights are found in the study of nature, such as threat avoidance behavior in starling flocks, and prey-capture abilities of echolocating bats. Inspired by the current advances in the field of evolutionary games (a mathematical framework that models the evolution of biological systems), we focus, in this project, on developing a rigorous framework for reasoning about resilient-by-cognition CPS by combining ideas from game theory, formal methods, and controls.

The use of unmanned aerial vehicles (UAVs) in the context of law enforcement agencies has witnessed a rapid growth over the past few years in the United States. In 2016, at least 167 law enforcement agencies acquired drones which is more than the number of drones acquired in the previous three years combined. This rapid growth in adopting UAVs by law enforcement agencies is derived from the need for a bird's eye view of crime and disaster scenes to enhance surveillance capabilities and improve situational awareness during natural disasters and catastrophic incidents. Recent successful examples of adapting remote-controlled drones include the use of a drone equipped with a thermal imaging camera to find a man who fled an accident scene and the usage of a drone to reclaim stolen construction equipment.

However, and with this increase in criminal's technological abilities, it will not be surprising to see criminals adapting recently reported attacks against law enforcement drones. The long view of this project is multifold. First, we seek to understand and model potential new threats and system vulnerabilities in drones when used in critical and high-risk tactical missions. Second, we seek to develop principled methods to analyze the data collected from various sensors to detect these attacks while preserving the privacy of public citizens whose sensitive data may have been captured by drone sensors. Third, to be resilient against software vulnerabilities, we seek to explore the usage of hardware-assisted cyber resilient platforms like ARM TrustZone. Fourth, we seek to develop novel control algorithms triggered by detection of attacks that are resilient to these attacks and which can, formally, guarantee the satisfaction of these high-risk tactical missions regardless the existence of these attacks. To achieve this level of resilience, drones need to be able to adapt and react to different attacks in real-time. Accordingly, an overarching objective of this project is to ensure that all developed algorithms come with real-time guarantees in addition to privacy and resilience guarantees.

A recent trend in IoT security is the exploitation of the heterogeneous redundancy in data collected by several nodes to provide security checks. In other words, while sensors are collecting data from different sources, these are dependent and hence a malicious change in some of those sensory data can be discovered by fusing the data from the rest of the sensors. However, a major question is where to place those sensors in the first place in a way that maximizes the ability of detecting maliciously corrupted sensory data. A closely related question is how to design optimal transmission policies that allows those wireless sensors to maximize the utilization of the shared wireless channel. Unfortunately, there is a tradeoff between these two objectives; security and network utilization. Within this project, we focus on exploring this tradeoff with the aim to develop new algorithms and tools that allow engineers to co-design security and networking for IIoT systems.

Several formal methods have been developed over the years to perform static analysis of software logic to discover software-related vulnerabilities such as buffer overflows, string format exploits, and general memory corruption. A common thread in these tools is to parse the software code into an intermediate verification language which is then translated into a set of logical constraints, in the spirit of bounded model checking. Along with this encoding comes a set of pre- and post-conditions that capture the formal property that needs to be verified. An SMT solver is then used to localize errors and provide traces which reach the error location in the software code. Unfortunately, such software verification tools are incapable of reasoning about system-level vulnerabilities which take into consideration the safety and reliability of the physical system. This stems from the weakness of state-of-the-art SMT solvers to reason about complex nonlinear constraints that appear naturally when the continuous dynamics of the physical system is encoded. In this project, we investigate novel formal verification tools that can analyze the robotic software while taking into account the underlying the physics of the robot in order to automatically find software vulnerabilities that can hinder the safety of the robotic system.