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

合作研究：FMitF：第一轨：嵌入式软件硬件故障攻击建模和分析的原则方法

• 批准号: 2220345
• 负责人: Chao Wang
• 金额: $ 37.5万
• 依托单位: University of Southern California
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-07-15 至 2026-06-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2220345&HistoricalAwards=false
• 关键词: Collaborative; Research; FMitF; Track; Principled

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.

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

项目成果

Systematic Testing of the Data-Poisoning Robustness of KNN

• DOI: 10.1145/3597926.3598129
• 发表时间: 2023-07
• 期刊: Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis
• 作者: Yannan Li;Jingbo Wang;Chao Wang

Certifying the Fairness of KNN in the Presence of Dataset Bias

• DOI: 10.1007/978-3-031-37703-7_16
• 发表时间: 2023-07
• 期刊: ArXiv
• 作者: Yann-Liang Li;Jingbo Wang;Chao Wang

Synthesizing MILP Constraints for Efficient and Robust Optimization

• DOI: 10.1145/3591298
• 发表时间: 2023-06
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Jingbo Wang;Aarti Gupta;Chao Wang

Constraint Based Compiler Optimization for Energy Harvesting Applications

针对能量收集应用的基于约束的编译器优化

• 发表时间: 2023
• 期刊: Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik
• 作者: Li, Yannan;Wang, Chao
• 通讯作者: Wang, Chao