Collaborative: FMitF: Track I: A Principled Approach to Modeling and Analysis of Hardware Fault Attacks on Embedded Software

在针对嵌入式软件的硬件故障攻击中，攻击者可以暂时改变嵌入式软件中指令的含义或其数据的值。未减轻的故障攻击的后果是显著的。它们可能导致攻击者的代码对受害者代码的权限升级，或者从受害者进程向攻击者泄露信息。然而，软件社区还没有对错误攻击有深入的了解。故障注入对数字系统的影响只有在硬件层面才能理解。这种差距是由于缺乏能够充分捕捉故障注入对复杂分层系统的影响的模型，从而导致缺乏对软件不可利用性的明确保证。该项目的新颖之处在于对这些硬件攻击有原则性的理解，并为安全嵌入式软件验证创建新颖的形式化分析工具和方法。该项目的影响是帮助软件社区理解硬件故障攻击的重要性和相关性，并帮助减轻安全风险。预期的结果是用于改进故障检测和故障对策的正式工具和技术，这些工具和技术将解决恶意硬件故障攻击和与硅可靠性快速增长问题相关的故障。该项目研究了一个统一的框架，能够以有原则和系统的方式建模和分析硬件故障对嵌入式软件的影响。该框架结合了开源仿真和编译技术，以在存在硬件故障攻击时显示可利用性，或证明不可利用性。三个研究任务导致了该框架的发展。首先，故障模型的设计在指令集体系结构（ISA）级别捕获硬件故障的影响。其次，对故障模型进行软硬件联合仿真。第三，形式化分析和验证工具集成了故障模型，有效、准确地研究了故障对软件代码的影响。最后，研究者创建并扩展了在嵌入式软件领域使用正式技术的研究生水平的教育内容。研究人员还指导高年级论文将本科生纳入研究范围。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

In a hardware fault attack on embedded software, an attacker can temporarily change the meaning of instructions in the embedded software or the value of its data. The consequences of unmitigated fault attacks are significant. They may lead to privilege escalation of an attacker's code over victim code or information leakage from a victim process to an attacker. However, the software community does not yet have a deep understanding of fault attacks. The effects of fault injection on a digital system are only understood at the hardware level. The gap is due to the lack of models that adequately capture the effects of fault injection on complex, layered systems, leading to the lack of clear guarantees about the non-exploitability of software. The project's novelties are to develop a principled understanding of these hardware attacks and to create novel formal analysis tools and methodologies for secure embedded software verification. The project's impacts are to help the software community understand the importance and relevance of hardware fault attacks and to help mitigate the security risks. The expected outcomes are formal tools and techniques for improved fault detection and fault countermeasures that would address malicious hardware fault attacks and faults related to the rapidly growing problem of silicon reliability.The project investigates a unified framework capable of modeling and analyzing the impact of hardware faults on embedded software in a principled and systematic fashion. The framework combines open-source simulation and compilation technologies to show exploitability, or to prove non-exploitability, in the presence of hardware fault attacks. Three research tasks lead to the framework's development. First, the design of a fault model captures the impact of hardware faults at the instruction-set architecture (ISA) level. Second, hardware-software co-simulation characterizes the fault model. Third, formal analysis and verification tools integrate the fault model to efficiently and accurately investigate the faults' impact on software code. Finally, the investigators create and extend graduate-level educational content on the use of formal technologies in the field of embedded software. The investigators also direct senior theses to include undergraduate students in the research.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.