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

在对嵌入式软件的硬件故障攻击中，攻击者可以暂时改变嵌入式软件中指令的含义或其数据的值。未减轻的故障攻击的后果是显著的。它们可能导致攻击者的代码相对于受害者代码的权限升级，或者从受害者进程向攻击者泄漏信息。然而，软件社区还没有对故障攻击有深入的了解。故障注入对数字系统的影响只能在硬件层面上理解。差距是由于缺乏能够充分捕捉故障注入对复杂分层系统的影响的模型，导致缺乏关于软件不可利用性的明确保证。该项目的新颖之处在于对这些硬件攻击有了原则性的理解，并为安全的嵌入式软件验证创建了新颖的正式分析工具和方法。该项目的影响是帮助软件社区了解硬件故障攻击的重要性和相关性，并帮助减轻安全风险。预期的成果是正式的工具和技术，以改善故障检测和故障对策，将解决恶意的硬件故障攻击和故障相关的快速增长的问题的硅reliability.The项目研究了一个统一的框架，能够建模和分析的影响，硬件故障嵌入式软件的原则和系统的方式。该框架结合了开源模拟和编译技术，以显示可利用性，或证明不可利用性，在存在硬件故障攻击。三个研究任务导致框架的发展。首先，故障模型的设计捕获硬件故障在故障集架构（伊萨）级别的影响。第二，软硬件协同仿真表征故障模型。第三，形式化分析和验证工具集成了故障模型，以有效和准确地调查故障对软件代码的影响。最后，研究人员创建和扩展研究生水平的教育内容，在嵌入式软件领域的正式技术的使用。该奖项反映了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.