针对指令跳过攻击的软件对策的形式化验证
密码学与安全
2014-02-27 v1
摘要
针对嵌入式电路的故障攻击使得定义针对安全电路的许多新攻击路径成为可能。每条攻击路径都依赖于特定的故障模型，该模型定义了攻击者可以执行的故障类型。在嵌入式处理器上，由汇编指令跳过组成的故障模型对攻击者非常有用，且已通过多种故障注入手段实现。为避免此威胁，已提出了一些依赖时间冗余的对策方案。然而，在足够长的时间间隔内进行双重故障注入是可行的，并且可以绕过这些对策方案。针对特定指令也提出了一些细粒度的对策方案。然而，据我们所知，尚未有任何方法能够形式化地证明可使通用汇编程序安全以抵御指令跳过攻击的容错性。在本文中，我们为 Thumb-2 指令集的几乎所有指令提供了容错替换序列，并为这种容错性提供了形式化验证。这种简单的变换能够为嵌入式程序添加相当好的安全级别，并使实际的故障注入攻击更难实现。
引用
@article{arxiv.1402.6461,
title = {Formal verification of a software countermeasure against instruction skip attacks},
author = {Nicolas Moro and Karine Heydemann and Emmanuelle Encrenaz and Bruno Robisson},
journal= {arXiv preprint arXiv:1402.6461},
year = {2014}
}