Runtime enforcement ensures that a running system complies with a property by observing and modifying the system’s actions. In practice, the property is often defined in terms of high-level, abstract events, while the system’s behavior consists of low-level, concrete actions. The relationship between actions and events is established in the instrumentation process, where developers must ensure that (i) system actions report the right events, and (ii) the necessary modifications to the system’s behavior are correctly enforced. However, the abstraction gap between a high-level property and low-level actions makes this process error-prone.

In this paper, we refine an existing formal model of runtime enforcement, which leaves instrumentation implicit, into a more precise model that explicitly accounts for instrumentation. We propose a correctness criterion for instrumentation and present a novel library, called InstrLib{}, that instruments Python applications for runtime enforcement.