Building a Modular Platform for Model Checking Glitch Attacks in RISC-V Programs

doi:10.1007/978-3-032-00942-5_15

2026-01-01

PRE

Brandhoj, Andreas Kjeldgaard *

Bogedal, Tobias Worm

Hansen, Rene Rydhof

Larsen, Kim G. Uldstrand

Poulsen, Danny Bogsted

DOI：10.1007/978-3-032-00942-5_15

原文链接

原文求助

摘要

En 中文

时序错误攻击可能通过在底层硬件中诱导位翻转来改变应用程序的行为。通过这种方式，攻击者可以绕过应用程序的安全措施。尽管此类攻击在攻击者拥有物理访问权限的系统中最为普遍，但近期研究表明，仅通过软件即可执行此类攻击[1, 10]。由于潜在执行路径的爆炸式增长，难以理解时序错误攻击对特定应用程序的影响。在本文中，我们提出了一种模块化平台，用于对RISC-V代码中的各种时序错误攻击进行模型检测。开发人员可以将RISC-V程序加载到Uppaal中配置的虚拟机模型中，并利用可用的多种攻击者模型来分析时序错误攻击的影响。该模型设计为支持Uppaal Classic、SMC以及带有TIGA的时间博弈，能够实现符号化、统计和博弈论分析。这可以为开发人员提供关于时序错误攻击对其代码影响的宝贵见解。我们使用FISSC[6]展示了三种方法的互补性。

Keyword:

glitch attacks

RISC-V

model checking

Uppaal

timed games