  The ubiquitous reliance on software systems increases the need for ensuring
that systems behave correctly and are well protected against security risks.
Runtime enforcement is a dynamic analysis technique that utilizes software
monitors to check the runtime behaviour of a software system with respect to a
correctness specification. Whenever the runtime behaviour of the monitored
system is about to deviate from the specification (either due to a programming
bug or a security hijack attack), the monitors apply enforcement techniques to
prevent this deviation.
  Current Runtime Enforcement techniques require that the correctness
specification defines the behaviour of the enforcement monitor itself. This
burdens the specifier with not only having to define property that needs to be
enforced, but also with having to specify how this should be enforced at
runtime; we thus relieve the specifier from this burden by resorting to a
highly expressive logic. Using a logic we allow the specifier to define the
correctness specification as a logic formula from which we can automatically
synthesise the appropriate enforcement monitor.
  Highly expressive logics can, however, permit for defining a wide variety of
formulae, some of which cannot actually be enforced correctly at runtime. We
thus study the enforceability of Hennessy Milner Logic with Recursion for which
we identify a subset that allows for defining enforceable formulae. This allows
us to define a synthesis function that translates enforceable formulae into
enforcement monitors. As our monitors are meant to ensure the correct behaviour
of the monitored system, it is imperative that they work correctly themselves.
We thus study formal definitions that allow us to ensure that our enforcement
monitors behave correctly.
