Certification through auditing allows to ensure that critical embedded systems are secure. This entails reviewing their critical components and checking for dangerous execution paths. This latter task requires the use of specialized tools which allow to explore and replay executions but are also difficult to use effectively within the context of the audit, where time and knowledge of the code are limited. Fault analysis is especially tricky as the attacker may actively influence execution, rendering some common methods unusable and increasing the number of possible execution paths exponentially. In this work, we present a new method which mitigates these issues by reducing the number of fault injection points considered to only the most relevant ones relatively to some security properties. We use fast and robust static analysis to detect injection points and assert their impactfulness. A more precise dynamic/symbolic method is then employed to validate attack paths. This way the insight required to find attacks is reduced and dynamic methods can better scale to realistically sized programs. Our method is implemented into a toolchain based on Frama-C and KLEE and validated on WooKey, a case-study proposed by the National Cybersecurity Agency of France.

翻译：认证审计可确保关键嵌入式系统的安全性，这要求审查其关键组件并检查危险执行路径。后者需使用专用工具来探索和重放执行过程，但在审计场景中，由于时间和代码知识有限，这些工具难以高效应用。故障分析尤为复杂，因为攻击者可能主动影响执行过程，导致某些常用方法失效，并使可能的执行路径呈指数级增长。本文提出一种新方法，通过将故障注入点缩减至仅与特定安全属性最相关的节点来缓解上述问题。我们采用快速稳健的静态分析检测注入点并评估其影响性，随后利用更精确的动态/符号执行方法验证攻击路径。通过这种方式，寻找攻击所需的洞察力得以降低，动态方法也能更好地扩展至实际规模的程序。该方法已基于Frama-C和KLEE工具链实现，并在法国国家网络安全局提出的WooKey案例研究中得到验证。