Building a Modular Platform for Model Checking Glitch Attacks in RISC-V Programs
摘要
Glitch attacks may change the behaviour of applications by inducing bit-flips in the underlying hardware. Through this, the attacker can bypass security measures of an application. Though most prevalent in systems where an attacker has physical access, recent research has shown that attacks may be performed through software alone [1, 10]. It is difficult to understand the impact of glitch attacks on a given application due to an explosion of potential execution paths. In this paper, we present a modular platform for model-checking various types of glitch attacks in RISC-V code. Developers can load a RISC-V program into a configurable virtual machine modelled in Uppaal with several attacker models available to analyse the impact of glitch attacks. The model is designed to support Uppaal Classic, SMC, and timed games with TIGA, enabling both symbolic, statistical, and game theoretical analysis. This can provide developers a valuable insight into the impact of glitch attacks on their code. Using FISSC [6], we show how all three methods complement each other.