Compositional runtime enforcement revisited

Runtime enforcement is a methodology used to enforce that the output of a running system satisfies a desired property. Given a property, an enforcement monitor modifies an (untrusted) sequence of events into a sequence that complies to that property. In practice, we may have not one, but many properties to enforce. Moreover, new properties may arise as new capabilities are added to the system. It is thus important to construct not a single, i.e., monolithic monitor, but rather several monitors, one for each property. The question is to what extent such monitors can be composed, and how. In this paper, we study two enforcement monitor composition schemes, serial and parallel composition. We show that, runtime enforcement is compositional for general regular properties with respect to one of the parallel composition schemes defined. We also show that runtime enforcement is not compositional with respect to serial composition for general regular properties, but it is for certain subclasses of regular properties. The proposed compositional runtime enforcement framework is formalized and implemented. Our experimental results demonstrate the pros and cons of using the compositional approach versus the monolithic with respect to performance.