Monitoring C Programs by Finite State Machines


Monitoring programs at runtime for security property violations is a
common and widely used concept that has its roots in the area of 
access control enforcement. In runtime verification, monitors are 
generated from formal properties and integrated into programs. These 
monitors observe security critical actions at runtime and permit or 
prohibit an action depending on the evaluation of the property in the 
current program state.

The monitoring approach poses two major questions: 
1) Is it sound and complete? That is, will the monitor permit all and 
only those actions that are valid with regard to the property? 
2) Will the monitor have to prohibit actions at runtime? That is, is 
the program insecure?

The first question is answered by so called hybrid approaches that
statically verify the monitor and its integration into the source 
program. An approach to answer the second question is presented with 
CFSMon in this thesis. We implement a monitor generation and 
instrumentation tool for parametric temporal safety properties in such 
a way that the monitored programs can be statically verified by a 
model checker or dynamically veried by runtime monitoring both with 
regard to the second question.

We rigorously derive formalizations of selected guidelines from the
CERT C Secure Coding Standard and show that CFSMon monitors decide
compliant and non-compliant code examples correctly at runtime as well
as in a static analysis with the model checker CPAchecker.