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.
