Security mechanisms are omnipresent and found at all layers of the
hardware and software stack, ranging from memory management
hardware to policy decision and enforcement points used in
middleware and web services. A fundamental question is "what kinds
of security policies can such mechanisms enforce?"
We examine this question for mechanisms that work by execution
monitoring. This covers a wide class of access control mechanisms which
intercept actions and prevent unauthorized actions from occurring, based
on a security policy. We will review work in this setting, in
particular the seminal work of Fred Schneider on the relationship
between enforceable security properties and safety properties. We will
clarify limitations in existing work and give necessary and sufficient
conditions for a security policy to be enforceable. In doing so, we
build upon ideas from control theory and formal language theory.
Furthermore, for different specification languages, we provide results
on deciding whether a given policy is enforceable and synthesizing an
enforcement mechanism from an enforceable policy.
(Joint work with Vincent Juge, Felix Klaedtke and Eugen Zalinescu)