CAREER: A Model-Guided and Holistic Approach for Peripheral Security

USB键盘和驱动器、蓝牙扬声器和耳机等现代外围设备为用户的计算机系统提供了丰富的功能，并已成为日常生活中不可或缺的一部分。虽然外围设备提供“即插即用”解决方案以简化它们在不同场景中的使用，但由于它们的“默认信任”处理以及与目标机器的低级部分（例如，操作系统）。例如，在停车场找到的USB驱动器一旦插入就可以完全控制工业控制系统，而蓝牙扬声器一旦连接就可以拦截用户笔记本电脑的所有网络流量。该项目旨在通过提前发现和减少可能导致外围设备攻击的漏洞，检测连接后外围设备中的恶意篡改，并及时可靠地响应外围设备攻击，从而系统地提高外围设备的安全性。该项目旨在解决实现可信赖和正式验证的外围设备生态系统以及设计下一代安全外围设备和操作系统的广泛研究挑战。该项目不是针对特定的外围设备攻击，而是专注于为一般的外围设备安全（包括USB和蓝牙）开发一种模型指导和整体方法，利用从外围设备规范和堆栈实现中提取的“模型”作为关键先验知识，并涵盖外围设备安全的整个生命周期，包括攻击前，运行时和攻击后阶段。因此，模型引导的模糊化、去浮动化和形式化验证减少了暴露于外围设备的攻击面;基于模型的固件分析、指纹识别和身份验证实现了外围设备的运行时完整性;模型引导的起源、修补和形式化实现允许针对外围设备攻击的即时且有保证的响应动作。该项目将在实际应用的组合中评估所有这些考虑因素（例如，Android USB安全性）和规范增强（例如，该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Modern peripherals devices such as USB keyboards and drives, Bluetooth speakers and headsets, complement users' computer systems with rich functionality and have become an integral part of daily life. While peripheral devices offer a "Plug'n'Play" solution to ease their usage in different scenarios, attacks from these devices are increasing due to their "Trust-by-default" treatment and direct interactions with the low-level parts of the target machines (e.g., operating systems). For instance, a USB drive found in the parking lot could take complete control of an industrial control system once plugged, while a Bluetooth speaker could intercept all the network traffic of a user's laptop once connected. This work aims to systematically improve peripheral security by discovering and reducing vulnerabilities that could enable peripheral attacks ahead of time, detecting malicious tampering within peripheral devices once connected, and responding to peripheral attacks timely with assurance.This project seeks to address the broad research challenge of enabling a trustworthy and formally-verified peripheral ecosystem and designing next-gen secure peripheral devices and operating systems. Rather than targeting a specific peripheral attack, this project focuses on developing a model-guided and holistic approach for peripheral security in general, including both USB and Bluetooth, leveraging “models” extracted from peripheral specifications and stack implementations as key prior knowledge, and covering the whole life cycle of peripheral security, including pre-attack, runtime, and post-attack stages. As such, model-guided fuzzing, debloating, and formal verification reduces the attack surface exposed to peripheral devices; model-based firmware analysis, fingerprinting, and authentication enables runtime integrity of peripheral devices; model-guided provenance, patching, and formal implementation allows for immediate and assured responding actions against peripheral attacks. This project will assess all these considerations within a combination of real-world applications (e.g., Android USB security) and specification enhancements (e.g., Bluetooth security and privacy), and generalize the knowledge for securing both peripheral devices and host machines across hardware, firmware, and software stacks.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.