CS 513 System Security -- Enforceable Security Policies

Enforceable Security Policies

Lecturer: Professor Fred B. Schneider

Lecture notes by Lynette I. Millett
Revised by Borislav Deianov

This lecture is based on:

Schneider, F.B. Enforceable Security Policies. ACM Transactions on Information and System Security 3, 1 (February 2000), 30--50.

We have been discussing various security policies (access control policies, information flow, etc.). However, we have not formally defined what we mean by "security policy." We are also, of course, interested in which of these security policies can be enforced. There is an increasing need for special-purpose policies. The mechanisms we have discussed are useful for low-level security needs, but we are also interested in abstractions related to things like funds transfer and document-use policies. These policies look nothing like the 'rwx' bits from UNIX access control. We need to find a bridge between the application level and the lower level mechanisms.

In order to understand which security policies are enforceable, we will postulate a class of enforcement mechanisms (referred to henceforth as EM-enforcement mechanisms). These mechanisms monitor execution and stop it when the security policy they enforce is about to be violated. This class of mechanisms includes virtual memory, reference monitors, capabilities, and UNIX-style access control. It's a very general notion, but it does not include mechanisms that, for example, modify programs or analyze programs prior to execution.

We define a security policy to be a predicate on sets of executions. An execution can be thought of as a sequence of states or instructions. The enforcement mechanisms described above will monitor the sequence (as it is produced). A security policy says what things are not allowed to happen in such sequences. Therefore, a system (for the purposes of this discussion) is defined by a set of executions. If we have a security policy P, and a system (set of executions) S, then the system satisfies the security policy if P(S) = true.

There are some interesting observations to make about these definitions. Suppose that T is a subset of S, and that P(S) holds. Do we want to require that P(T) hold as well? In fact, doing so would cause problems. Consider a system with two variables: s, representing an individual's salary, and x. Assume we are interested in a policy P that says that s cannot be inferred by examining x. The set of all possible executions (of any system) satisfies this policy. However, suppose that T is the set of sequences where s = x. In this case, if it is known that a sequence in T is being evaluated, s can be inferred from the value of x. T is a subset of S, but T violates the security policy P. In short, we don't want to require policies to hold for subsets. However, this means that we can write policies about information flow.

Given these very general notions, and the observations made above, what policies are EM-enforceable? In other words, what are the constraints on P that are consequences of EM-enforceability? We note three:

EM is restricted to analyzing a single execution. Thus, P(S) must have the form: (For all s in S, q(s)) for some q. This form rules out prohibiting the determination of a salary, as described above. Information flow is not EM-enforceable.
Execution must be truncated as soon as the sequence violates the security policy. More specifically, if the 'prefix' of an execution does not satisfy q, then q most be defined so that the whole execution had better fail to satisfy q. It is not possible for a sequence to violate the security policy and then recover.
Violations must be detected after a finite time. EM can only observe finite executions.

A security policy P must satisfy all three of these conditions for it to be EM-enforceable.

Almost all of the mechanisms for security that we have discussed this semester are EM mechanisms, including access control, Chinese wall, and policies such as "service is available within three seconds." However, the policy "eventually service is available" is not EM-enforceable. We noted in the last lecture that information flow is not EM-enforceable, either. The properties of security policies listed above encapsulate what are known as safety properties.

All safety properties can be characterized by automata. Here is an example of such an automaton.

We say that this automata rejects the input if it is ever required to make an undefined transition. For example, if the sequence of operations was: send, read, send. These automata are called security automata and are a form of Buchi automata. (Note that finite state automata accept inputs, these reject. Also, these automata work for infinite sequences. Moreover, the nondeterministic to deterministic FSA constructions do not apply to Buchi automata.) The security policy our example automaton specifies is: "No send after read." Our claim is that any policy satisfying the three conditions above can be specified by one of these automata.