CAREER: Compositional IoT Safety and Security in Physical Spaces

许多独立编程的单个系统组件不可避免地集成到物联网（IoT）系统中，这带来了需要迫切关注的新挑战。主要的挑战是提供正确性证明，以确保物联网设备在物理空间（它们运行的环境）中的复合行为符合所需的安全和安全策略。最近的系统安全研究引入了综合物联网实现的方法，以保证一系列安全和安全策略。这些方法集中在政策规范和验证的各个组件在彼此隔离，或确保安全性，通过模型只从程序的源代码抽象。尽管过去的研究取得了成功，但在开发理论和实践方面存在着重大差距，这表明如何统一每个设备的行为，以正式推理物联网系统在实践中的安全性。该项目整合了旨在设计和开发算法和工具的研究活动，这些算法和工具正式产生物联网系统的复合行为，并为物联网环境的全球安全性和安全性推理奠定了严格的基础。该项目的成果将最终增强物联网系统当前的验证和确认实践，并建立对国家基础设施的信任和保护公民。该项目的具体目标分为三个研究重点。第一个重点是通过静态分析和系统识别技术的组合统一单个系统组件的行为来构建一个新的复合模型，以表示物联网系统的全局行为。第二个目标是建立一个严格的基础，以确定基于物理行为的策略，并开发正式的分析技术，以确保物联网系统遵守安全和安全策略。最后一个目标是建立一系列技术，使模型构建和策略验证在不同的物联网系统中具有可扩展性和详尽性。所有研究方向的一个共同主题是系统组件的自适应创建和处置，允许灵活配置添加，删除和更新的物联网设备，程序和环境变化。因此，研究活动将适用于现有的软件系统，并指导未来的系统设计。该奖项反映了NSF的法定使命，并已被认为是值得通过使用基金会的智力价值和更广泛的影响审查标准进行评估的支持。

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.