Service Automata is a formally specified framework for
runtime monitoring of distributed applications and the
dynamic enforcement of countermeasures before a given
security policy is violated. Originally, polices for
the Java implementation of Service Automata are specified
by extending a Java class and implementing the policy
using pure Java code. This approach suffers from the
problem that the actual "policy" is mingled with Java
internals like the initialization of data structures
or checks for null values. We extended the Java
implementation of Service Automata with support for
Datalog policies. These policies allow for a better
separation from other parts of the program and are easy
to read in a "mathematical" manner. Moreover, a formal
analysis of the applied policies is better feasible since
Datalog programs directly translate into first order
sentences with Herbrand interpretations. There always
exists a minimal finite set of semantic consequences
from a Datalog program, and efficient evaluation / proof
strategies with termination guarantees can be constructed.
We provide the foundations for the employment of Datalog
policies like a generic structure of the policies and
a notion of soundness of Datalog policies with respect
to first order security properties. Our case studies
show the applicability of our Datalog extension for the
distributed version control system Git.