CAREER: Towards a Secure and Reliable Internet of Things through Automated Model Extraction and Analysis

职业：通过自动模型提取和分析迈向安全可靠的物联网

• 批准号: 1942235
• 负责人: Tuba Yavuz
• 金额: $ 48.71万
• 依托单位: University of Florida
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-10-01 至 2025-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1942235&HistoricalAwards=false
• 关键词: CAREER; Towards; Secure; Reliable; Internet

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.

物联网 (IoT) 有望在各个领域改变我们的生活质量。然而，Mirai 僵尸网络和其他利用物联网设备漏洞的网络攻击暴露了当前物联网部署中的主要安全和隐私问题。这些事件表明，确保物联网生态系统的安全是实现物联网变革力量的先导。物联网生态系统涉及各种组件，包括受限设备、边缘设备、移动设备和云。确保物联网部署的安全需要深入了解每个组件的攻击面以及由于各个组件之间的交互而形成的攻击面。然而，为这些组件提供支持的软件的复杂性带来了巨大的挑战。该项目的目标是使用自动模型提取和模型引导分析来实现安全工程的整体视图。该项目将产生方法、工具和教育材料，为物联网行业提供安全软件开发和部署实践方面的支持。此外，该项目将有助于扩大女性和其他代表性不足的群体对物联网安全、形式化方法和软件工程研究的参与。该项目将研究系统软件的可扩展分析，以推理系统级行为。关键的见解是软件通常是根据编程模型开发的，该模型对数据和代码强加了某些结构和语义关联。这些知识为处理代码的复杂性提供了很好的机会，因为它提供了如何单独分析组件以及如何在分析过程中有效探索状态空间的指导。具体来说，该项目建立在三个研究重点之上：1）系统软件中使用的编程模型的形式化，2）利用正式定义的编程模型和各种程序分析技术的集成的自动模型提取和模型引导分析，以及3）通过将自动提取的组件模型与运行时数据集成，对物联网系统进行系统级分析。自动构建的系统级模型将接受严格的分析，并将支持物联网部署的有效运行时监控，以提高可用性、可靠性、隐私和安全性。基于新颖、增量和模型检查的回归分析将实现物联网系统的安全可靠的发展。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力优点和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Analyzing system software components using API model guided symbolic execution

使用 API 模型引导的符号执行分析系统软件组件

• DOI: 10.1007/s10515-020-00276-5
• 发表时间: 2020
• 期刊: Automated Software Engineering
• 影响因子: 3.4
• 作者: Yavuz, Tuba;Bai, Ken
• 通讯作者: Bai, Ken

SEESAW: a tool for detecting memory vulnerabilities in protocol stack implementations

SEESAW：用于检测协议栈实现中内存漏洞的工具

• DOI: 10.1145/3487212.3487345
• 发表时间: 2021
• 期刊: MEMOCODE'21
• 作者: Fowze, Farhaan;Yavuz, Tuba
• 通讯作者: Yavuz, Tuba

Verifying Absence of Hardware-Software Data Races using Counting Abstraction

使用计数抽象验证硬件软件数据争用的存在

• 发表时间: 2020
• 期刊: MEMOCODE 2020
• 作者: Yavuz, Tuba

A Study on the Testing of Android Security Patches

• DOI: 10.1109/cns56114.2022.9947240
• 发表时间: 2022-10
• 期刊: 2022 IEEE Conference on Communications and Network Security (CNS)
• 作者: Christopher Brant;Tuba Yavuz

Security Analysis of IoT Frameworks using Static Taint Analysis

• DOI: 10.1145/3508398.3511511
• 发表时间: 2022-04
• 期刊: Proceedings of the Twelfth ACM Conference on Data and Application Security and Privacy
• 作者: Tuba Yavuz;Christopher Brant