ABSTRACT

The inevitable integration of many individual system components programmed independently into the Internet of Things (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 they operate - adheres to desired safety and security policies. Recent research in systems security introduced methods to synthesize IoT implementations that guarantee a range of safety and security policies. These approaches focus either on policy specification and verification of individual components in isolation of each other or ensure security through models solely abstracted from the source code of programs. Despite the success of past research, there is a significant gap in developing theory and practice that indicates how the behavior of each device can be unified to formally reason about the safety and security of IoT systems in practice. This 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 results of this project will ultimately enhance the current verification and validation practices of IoT systems and build trust in national infrastructure and protect citizens.

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. A common theme in all research directions is the adaptive creation and disposal of system components that allow for flexible configuration of added, removed, and updated IoT devices, programs, and environmental changes. Thus, the research activities will apply to existing software systems and guide future system designs.

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.

Please report errors in award information by writing to: awardsearch@nsf.gov.