3.2. Basic Results
The simplest case is a system in which the commands are mono-operational (each consisting of a single primitive command). In such a system, the following theorem holds.
Theorem 31.
[401] There exists an algorithm that will determine whether a given mono-operational protection system with initial state s0 is safe with respect to a generic right r. Proof Because all commands are mono-operational, we can identify each command by the type of primitive operation it invokes. Consider the minimal sequence of commands c1, ..., ck needed to leak the right r from the system with initial state s0. Because no commands can test for the absence of rights in an access control matrix entry, we can omit the delete and destroy commands from the analysis. They do not affect the ability of a right to leak. Now suppose that multiple create commands occurred during the sequence of commands, causing a leak. Subsequent commands check only for the presence of rights in an access control matrix element. They distinguish between different elements only by the presence (or lack of presence) of a particular right. Suppose that two subjects s1 and s2 are created and the rights in A[s1, o1] and A[s2, o2] are tested. The same test for A[s1, o1] and A[s1, o2] = A[s1, o2]  A[s2, o2] will produce the same result. Hence, all creates are unnecessary except possibly the first (and that only if there are no subjects initially), and any commands entering rights into the new subjects are rewritten to enter the new right into the lone created subject. Similarly, any tests for the presence of rights in the new subjects are rewritten to test for the presence of that right in an existing subject (or, if none initially, the first subject created). Let |S0| be the number of subjects and |O0| the number of objects in the initial state. Let n be the number of generic rights. Then, in the worst case, one new subject must be created (one command), and the sequence of commands will enter every right into every element of the access control matrix. After the creation, there are |S0| + 1 subjects and |O0| + 1 objects, and (|S0| + 1)(|O0| + 1) elements. Because there are n generic rights, this leads to n(|S0| + 1)(|O0| + 1) commands. Hence, k  n(|S0| + 1)(|O0| + 1) + 1.
By enumerating all possible states we can determine whether the system is safe. Clearly, this may be computationally infeasible, especially if many subjects, objects, and rights are involved, but it is computable. (See Exercise 2.) Unfortunately, this result does not generalize to all protection systems.
Before proving this, let us review the notation for a Turing machine. A Turing machine T consists of a head and an infinite tape divided into cells numbered 1, 2, ..., from left to right. The machine also has a finite set of states K and a finite set of tape symbols M. The distinguished symbol b  M is a blank and appears on all the cells of the tape at the start of all computations; also, at that time T is in the initial state q0.
The tape head occupies one square of the tape, and can read and write symbols on that cell of the tape, and can move into the cell to the left or right of the cell it currently occupies. The function d: K x M  K x M x {L, R} describes the action of T. For example, let p, q K and A, B M. Then, if d(p, A) = (q, B, R), when T is in state p and the head rests on a cell with symbol A, the tape head changes the symbol in the cell to B, moves right to the next cell (that is, if the head is in cell i, it moves to cell i + 1), and the Turing machine enters state q. If d(p, A) = (q, B, L), then the actions would be the same except the head would move to the left unless it were already in the leftmost square (because the head may never move off the tape).
Let the final state be qf, if T enters this state, it halts. The halting problem is to determine whether an arbitrary Turing machine will enter the state qf, and is known to be undecidable [299].
Given this, we can now present the following theorem.
Theorem 32.
[401] It is undecidable whether a given state of a given protection system is safe for a given generic right. Proof Proof by contradiction. We show that an arbitrary Turing machine can be reduced to the safety problem, with the Turing machine entering a final state corresponding to the leaking of a given generic right. Then, if the safety problem is decidable, we can determine when the Turing machine halts, showing that the halting problem is decidable, which (as we said above) is false. First, we construct a map from the states and symbols of T to rights in the access control matrix model. Let the set of generic rights be the symbols in M and a set of distinct symbols each representing an element in K; in other words, the set of tape symbols and states are represented by generic rights, one right for each symbol and one for each state. The cells of the Turing machine tape are sequentially ordered. We consider only the cells that the head has visited, so suppose T has scanned cells 1, 2, ..., n. To simulate this, we represent each cell as a subject and define a distinguished right called own such that si owns si+1 for 1 i < k. If cell i contains the symbol A, then subject si has A rights over itself. Furthermore, the subject sk, which corresponds to the rightmost cell visited, has end rights over itself; notice that sk+1 has not been created in this case. Finally, if the head is in cell j and T is in state p, then subject sj has p rights over itself also. (To keep the meanings of the rights unambiguous, we require the rights corresponding to the symbols for the tape to be distinct from the rights corresponding to the states.) Figure 3-1 shows an example of this mapping, when the head has visited four cells.
Next, we must translate the Turing machine function d into access control matrix commands. Suppose that d(p, A) = (q, B, L) and the head is not in the leftmost cell. Then, in terms of the access control matrix, the rights A and p must be replaced by B in the entry a[si, si] and the right q must be added to a[si1, si1]. The following access control matrix command, in which si represents the subject corresponding to the current cell, captures this.
command cp, A(si, si1)
if own in a[si1, si] and p in a[si, si] and A in a[si, si]
then
delete p from a[si, si];
delete A from a[si, si];
enter B into a[si, si];
enter q into a[si1, si1];
end
If the head is in the leftmost cell of the tape, both si and si1 are s1. Now consider motion to the right, such as d(p, A) = (q, B, R). If the head is not in the rightmost cell k, by the same reasoning as for the left motion, we have
command cp, A(si, si+1)
if own in a[si, si+1] and p in a[si, si] and A in a[si, si]
then
delete p from a[si, si];
delete A from a[si, si];
enter B into a[si, si];
enter q into a[si+1, si+1];
end
However, if the head is in the rightmost cell k, the command must create a new subject sk+1. Then, to maintain the consistency of the access control matrix, sk is given own rights over the new subject sk+1, sk+1 is given end rights over itself, and sk's end rights over itself must be removed. At that point, the problem is reduced to the problem of regular right motion. So:
command crightmostp, A(sk, sk+1)
if end in a[si, si] and p in a[si, si] and A in a[si, si]
then
delete end from a[sk, sk];
create new subject sk+1;
enter own into a[sk, sk+1];
enter end into a[sk+1, sk+1];
delete p from a[si, si];
delete A from a[si, si];
enter B into a[si, si];
enter q into a[si+1, si+1];
end
Clearly, only one right in any of the access control matrices corresponds to a state, and there will be exactly one end right in the matrix (by the nature of the commands simulating Turing machine actions). Hence, in each configuration of the Turing machine, there is at most one applicable command. Thus, the protection system exactly simulates the Turing machine, given the representation above. Now, if the Turing machine enters state qf, then the protection system has leaked the right qf; otherwise, the protection system is safe for the generic right qf. But whether the Turing machine will enter the (halting) state qf is undecidable, so whether the protection system is safe must be undecidable also.
However, we can generate a list of all unsafe systems.
Theorem 33.
[242] The set of unsafe systems is recursively enumerable. Proof See Exercise 3.
Assume that the create primitive is disallowed. Clearly, the safety question is decidable (simply enumerate all possible sequences of commands from the given state; as no new subjects or objects are created, at some point no new rights can be added to any element of the access control matrix, so if the leak has not yet occurred, it cannot occur). Hence, we have the following theorem.
Theorem 34.
[401] For protection systems without the create primitives, the question of safety is complete in P-SPACE. Proof Consider a Turing machine bounded in polynomial space. A construction similar to that of Theorem 32 reduces that Turing machine in polynomial time to an access control matrix whose size is polynomial in the length of the Turing machine input.
If deleting the create primitives makes the safety question decidable, would deleting the delete and destroy primitives but not the create primitive also make the safety question decidable? Such systems are called monotonic because they only increase in size and complexity; they cannot decrease. But:
Theorem 35.
[402] It is undecidable whether a given configuration of a given monotonic protection system is safe for a given generic right.
Restricting the number of conditions in the commands to two does not help:
Theorem 36.
[402] The safety question for biconditional monotonic protection systems is undecidable.
But if at most one condition per command is allowed:
Theorem 37.
[402] The safety question for monoconditional monotonic protection systems is decidable.
This can be made somewhat stronger:
Theorem 38.
[402] The safety question for monoconditional protection systems with create, enter, and delete primitives (but no destroy primitive) is decidable.
Thus, the safety question is undecidable for generic protection models but is decidable if the protection system is restricted in some way. Two questions arise. First, given a particular system with specific rules for transformation, can we show that the safety question is decidable? Second, what are the weakest restrictions on a protection system that will make the safety question decidable in that system?
|
