CNS Core: Medium: Automated IoT Safety and Security Analysis and Synthesis

该项目专注于推进一门科学，使从业者能够验证已使用传感器、智能设备和自动基础设施等数字设备增强的家庭、工作场所和公共场所的安全性。具体地说，这项研究的目标是创建软件分析和验证技术，以评估物联网(IoT)程序和环境在一系列领域中的安全性和安全性。该项目将研究如何为物联网编程平台建模，以验证大规模的安全、安全和功能属性，以及如何创建物联网特定语言，用于按设计确保物联网实施。该项目将开发从物联网源代码中提取模型(称为过渡系统)的系统，并应用可扩展的软件验证技术，以提供具有所需属性的正确性证明。同时，该项目进一步创建物联网专用语言，以自动生成在运行时保留功能、安全和安全属性的物联网程序。该项目将开发工具和数据集，并评估验证和生成技术在不同物联网领域的有效性。该项目的预期结果是一套在线物联网分析和综合工具，以及面向公众和技术社区的物联网软件安全和安全分析课程。这些工具将以更安全和更有保障的方式实现向智能环境的持续过渡。该项目还将通过开展研讨会、外联和教程活动，帮助促进科学和工业社区参与物联网安全和安保工作。所有软件、数据、论文和教程将在整个项目网站上维护，之后随着未来工作的进展进行维护。对于公开分发，该项目的所有开发和实验文物将链接到项目网站(https://github.com/IoTBench/))，并在整个项目期间进行维护。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

This project focuses on advancing a science that enables practitioners to validate the safety of homes, workplaces, and public spaces that have been augmented with digital devices such as sensors, smart-devices, and autonomous infrastructure. Specifically, the objective of this research is the creation of software analysis and verification techniques to evaluate the safety and security of Internet of Things (IoT) programs and environments in a range of domains. This project will study how to model IoT programming platforms to validate safety, security and functional properties at scale as well as how to create IoT-specific languages for secure-by-design IoT implementations.This project will develop systems that extract models (called transition systems) from IoT source code and apply scalable software verification techniques to provide proofs of correctness with the desired properties. At the same time, this project furthers the creation of IoT-specific languages to automatically generate IoT programs that preserve functional, safety and security properties at run-time. This project will develop tools and datasets, as well as evaluate the efficacy of verification and generation techniques in diverse IoT domains.The expected results of this project are a set of online IoT analysis and synthesis tools and a curriculum for IoT software safety and security analysis for the public and technical communities. Such tools will enable the ongoing transition to smart environments in ways that will be safer and more secure. This project will also help foster the engagement of scientific and industrial communities in IoT safety and security through the development of workshop, outreach and tutorial events.All software, data, papers, and tutorials will be maintained on project website for the entirety of the project and maintained thereafter as future work progresses. For public distribution, all development and experimental artifacts for this project will be linked to the project website (https://github.com/IoTBench/) and maintained over the project duration.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.