A calculus for composing security policies

A runtime monitor is a program that runs in parallel with an un-trusted application and examines actions from the application's instruc-tion stream. If the sequence of program actions deviates from a specied security policy, the monitor transforms the sequence or terminates the program. We present the design and formal specication of a language for dening 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 val-ues, 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 eect system to ensure that computations do not interfere with one another when they are composed. We also present a preliminary implementation of our language.