# Detecting Fault Injection Attacks with Runtime Verification

## TL;DR

This paper introduces formal runtime verification monitors designed to detect fault injection attacks, including test inversion and control flow jumps, providing a lightweight and deployable security solution validated on a PIN verification program.

## Contribution

It presents formal models of runtime monitors for fault injection detection, with proofs of effectiveness and flexible deployment options, advancing security measures against fault injection attacks.

## Key findings

- Monitors effectively detect simulated fault injection attacks.
- Monitors are small, formal, and can be deployed flexibly.
- Validation on a PIN verification program confirms effectiveness.

## Abstract

Fault injections are increasingly used to attack/test secure applications. In this paper, we define formal models of runtime monitors that can detect fault injections that result in test inversion attacks and arbitrary jumps in the control flow. Runtime verification monitors offer several advantages. The code implementing a monitor is small compared to the entire application code. Monitors have a formal semantics; and we prove that they effectively detect attacks. Each monitor is a module dedicated to detecting an attack and can be deployed as needed to secure the application. A monitor can run separately from the application or it can be ``weaved'' inside the application. Our monitors have been validated by detecting simulated attacks on a program that verifies a user PIN.