  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.
