A Calculus for Composing Security Policies
A runtime monitor is a program that runs in parallel with an untrusted
application and examines actions from the application's instruction
stream. If the sequence of program actions deviates from a specified
security policy, the monitor transforms the sequence or terminates the
program. We present the design and formal specification of a language
for defining the policies enforced by program monitors.
Our language provides a number of facilities for composing complex
policies from simpler ones. We allow policies to be parameterized by
values, or other policies. There are also operators for forming the
conjunction and disjunction of policies. Since the computations that
implement these policies modify program behavior, naive composition of
computations does not necessarily produce the conjunction (or
disjunction) of the policies that the computations implement
separately. We use a type and effect system to ensure that
computations do not interfere with one another when they are composed.
We also present a preliminary implementation of our language.