Stream-Monitoring Automata

Over the past nearly twenty years, numerous formal models of enforcement and runtime monitors have been investigated. This paper takes the lessons learned from earlier models and proffers a new general model of runtime enforcement that is more suitable for modeling security mechanisms that operate over infinite event streams. The new model, called Stream-Monitoring Automata (SMAs), enables the constraints and analyses of interest in previous models to be encoded, and overcomes several shortcomings of existing models with respect to expressiveness. SMAs capture the practical abilities of mechanisms to monitor infinite event streams, execute even in the absence of event inputs, enforce non-safety policies, and operate an enforcement model in which extraneous constraints such as transparency and uncontrollable events may be specified as meta-policies.