STORM: State Transition Online Runtime Monitor

Introduction

This repository contains a proof-of-concept for monitoring correct execution order of an arbirary C program using a transition matrix.

First, the program is abstracted as a state transition system. This transition system is then modeled as a state transition matrix. A state transition matrix determines the allowed state depending on the last state. States here are synonmous with program checkpoints. The advantage of modeling the expected program flow as a matrix is that branching behaviour can be described.

Using this matrix, by storing the last state and given a current state, the runtime monitor can check if program execution is valid.