Lecture notes by Lynette I. Millett
There are three issues that we discuss today. The first is that of rights propagation. Can a given subject ever get access to a particular object? The second is enforcement: How can we ensure that any attempt to, for example, read an object is mediated by the protection matrix? Finally, we explore representations of access control matrices.
It would certainly be useful to have an analyzer that could answer the question: Is it possible for right r to be an element of [S, O] after some execution? Such an analyzer would provide a way to understand the ramifications of a given set of commands.
We now outline a proof of the undecidability result. In the proof, we show that a Turing Machine (TM) can be represented as a protection system. If we could build an analyzer as described above, then the analyzer could be used to determine whether a TM could halt. We know that the "Halting Problem" is undecidable, so have arrived at a contradiction. Thus, the analyzer cannot be built.
Briefly, a TM consists of an infinite tape and a control device with a read/write head and a finite-state control. The read/write head can move one square to the right or left and can read and write symbols onto the current tape square. We must show how to think of a TM as a protection problem. In other words, we encode a TM as a protection system where a particular right (r being an element of [S, O]) is equivalent to the TM halting. Once a TM is represented this way, then if a rights-propagation analyzer for a protection system exists, we would have a way to determine whether a TM halts.
The first step for the encoding is to create the protection matrix from the TM's tape. We encode the contents of the TM's tape on the diagonal of the protection matrix; element [S, S] will contain the Sth tape square. Recall also that subjects and objects aren't ordered, and thus any permutation of rows or columns is an equivalent protection system. We need some way to encode the fact that tape square S1 comes before tape square S2. This is down by making "own" a member of the element [Si, Si+1]. So, the matrix now looks something like: