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

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

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.