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

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

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.