The Internet of Things (IoT) is expected to transform the quality of our lives in various domains. However, the Mirai botnet and other cyber attacks that exploited vulnerabilities in IoT devices have revealed major security and privacy issues in the current deployments of IoT. These incidents indicate the importance of securing the IoT ecosystem as a precursor to achieving the transformative power of IoT. The IoT ecosystem involves a variety of components including constrained devices, edge devices, mobile devices, and the cloud. Securing an IoT deployment requires a deep understanding of the attack surface of each component and the attack surfaces that are formed as a result of the interactions between various components. However, the complexity of software that powers these components poses a big challenge. The goal of this project is to achieve a holistic view of security engineering using automated model extraction and model guided analysis. The project will yield methodologies, tools, and educational material that will empower the IoT industry in terms of secure software development and deployment practices. Additionally, the project will help broaden participation of women and other underrepresented groups in IoT security, formal methods, and software engineering research.
This project will investigate scalable analysis of system software to reason about system-level behavior. The key insight is that software is often developed according to a programming model, which imposes certain structural and semantic associations for data and code. This knowledge provides a great opportunity to deal with the complexity of code as it provides guidance on how to analyze components in isolation and how to effectively explore the state space during analysis. Specifically, the project builds on three research thrusts: 1) Formalization of programming models that are used in system software, 2) Automated model extraction and model guided analysis that leverage formally defined programming models and the integration of a variety of program analysis techniques, and 3) System-level analysis of IoT systems through integration of automatically extracted component models with run-time data. The automatically constructed system-level model will be subjected to rigorous analysis and will support effective run-time monitoring of IoT deployments for improved usability, reliability, privacy, and security. A novel, incremental, and model checking based regression analysis will enable safe and secure evolution of IoT systems.
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.
