Compositional IoT Safety and Security in Physical Spaces

Principal Investigator: Berkay Celik

An IoT system is composed of multiple individual components, with each component containing a set of sensors and actuators governed by a control program. The inevitable integration of many individual system components programmed independently into IoT systems has brought new challenges that require urgent attention. The main challenge is to produce proofs of correctness that ensure the composite behavior of IoT devices in physical spaces—the environment in which sensors/actuators operate—adheres to desired safety and security policies.

Celik’s project integrates research activities aimed at designing and developing algorithms and tools that formally produce the composite behavior of an IoT system and a rigorous foundation for reasoning about an IoT environment's global safety and security. 

The specific goals of the project are divided into three research thrusts. The first thrust focuses on constructing a novel composite model by unifying the behavior of individual system components through a combination of static analysis and system identification techniques to represent an IoT system's global behavior. The second thrust aims to establish a rigorous foundation for identifying physical behavior-based policies and developing formal analysis techniques that ensure an IoT system adheres to safety and security policies. The last thrust seeks to establish a series of techniques to make model construction and policy validation scalable and exhaustive in diverse IoT systems. 

Keywords: compositional security, CPS, cyber physical systems, IOT