We propose a symbolic execution method for analyzing the safety of software under fault attacks both accurately and efficiently. Fault attacks leverage physically injected hardware faults in an embedded system to break the safety of a software program. While there are existing methods for analyzing the impact of maliciously injected hardware faults on the embedded software, they suffer from inaccurate fault modeling and inefficient fault analysis. To overcome these limitations, we propose two novel techniques. First, we propose a new fault modeling technique that leverages automated program transformation to add symbolic variables to the original program, to accurately model the new program behavior induced by the injected faults. This new fault modeling approach has two advantages over existing techniques: (a) the fault-induced program behavior is closely related to what attackers exploit in practice and (b) the automatically transformed program may be analyzed by any downstream fault analysis algorithm. Second, we propose an efficient symbolic execution algorithm that is designed specifically for conducting fault analysis on the transformed program. It leverages two pruning techniques to mitigate path explosion. We have implemented the proposed method and evaluated it on a variety of benchmark programs. The experimental results show that our method significantly outperforms the state-of-the-art techniques. Compared to the current state-of-the-art, it is able to detect previously-missed safety violations and at the same time avoid bogus violations. Furthermore, compared to the baseline algorithm, our optimized symbolic execution algorithm can be orders-of-magnitude faster.

翻译：我们提出一种符号执行方法，用于准确且高效地分析故障攻击下软件的安全性。故障攻击利用嵌入式系统中物理注入的硬件故障破坏软件程序的安全性。现有方法虽能分析恶意注入硬件故障对嵌入式软件的影响，但存在故障建模不准确与故障分析效率低下的问题。为克服这些局限，我们提出两项创新技术。首先，提出一种新型故障建模技术，通过自动程序变换向原始程序添加符号变量，精确模拟注入故障引发的新程序行为。该技术较现有方法具备两大优势：(a) 故障引发的程序行为紧密贴合攻击者在实际场景中的利用模式；(b) 经自动变换后的程序可被任意下游故障分析算法处理。其次，针对变换后程序的故障分析需求，专门设计了一种高效符号执行算法，通过两种剪枝技术缓解路径爆炸问题。我们实现了所提方法并在多种基准程序上展开评估。实验结果表明，该方法显著优于现有最先进技术：相较于当前最优方案，既能检测出先前遗漏的安全违规，又能避免误报违规。此外，与基础算法相比，优化后的符号执行算法可实现数个数量级的加速。