Modern Cyber-Physical Systems (CPS) are large complex systems of systems, where arguments about the behavior of the whole system rely on guarantees about the individual components. Individual components, however, may be designed using machine learning methods such as neural networks that are currently not amenable to formal analysis, or the components may simply be too large and complex for complete verification. Hence, it is increasingly difficult to ensure the safety and security of CPS.

To cope with this challenges, we explore new sandboxing mechanisms to design novel software architectures such that a cyber-physical system can use unverified controllers, but its safety does not depend on it. At the core of this technology, there are a Safety Advisor and a Supervisor (Safe-visor). On one hand, Safety Advisor only focuses on the safety of the system, which should be treated as a fallback in case the unverified controller is trying to perform some harmful actions. On the other hand, the unverified controller is designed for functionality; i.e., it is expected to realize some tasks which are much more complicated than only keeping the system safe. To ensure a specific level of safety probability for the controlled physical system, the supervisor specifies verifiable safety rules for the unverified controller to follow. The control inputs of the controller fed to the system are checked at run-time and can only be accepted when they are not disobeying the safety rules defined in the sandboxing mechanism. In general, the Safe-visor architecture can be used to sandbox any types of unverified controllers in order to guarantee the safety of the controlled physical system. In summary, we are able to use an unverified controller for realizing complex tasks while preventing the system from being threatened by its harmful behavior, if any. Compared to existing literature that focuses on similar problems, a safe-visor architecture aims to provide safety guarantee while avoiding restricting too much the capability of unverified controller. From a security stand point, Safe-visor acts like a “last line of defence” mechanism by providing integrity and assurance, but it doesn’t preserve confidentiality. That means an intruder might still be able to observe the protected CPS, however, he/she cannot damage its physical components. Moreover, the proposed Safe-visor is complementary to, and works well with, existing methods that provide confidentiality, like encryption. Finally, this research focuses on stochastic Cyber-Physical Systems modeled as controlled Markov Process, which enables us to reason about the statistical properties of CPS influenced by sensor and input noise.

As part of this research, we also want to look at more general safety specifications (e.g., those described by temporal logic) and more general system models (e.g., partial observable Markov Decision Process). Moreover, we want to develop software for CPS controllers’ synthesis and their code generation.