Modeling runtime enforcement with mandatory results automata

This paper presents a theory of runtime enforcement based on mechanism models called mandatory results automata (MRAs). MRAs can monitor and transform security-relevant actions and their results. The operational semantics of MRAs is simple and enables straightforward definitions of concrete MRAs. Moreover, the definitions of policies and enforcement with MRAs are simple and expressive. Putting all of these features together, we argue that MRAs make good general models of runtime mechanisms, upon which a theory of runtime enforcement can be based. We develop some enforceability theory by characterizing the policies deterministic and non-deterministic MRAs can and cannot enforce.