CAREER: Compositional IoT Safety and Security in Physical Spaces

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

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.