<p>As of now I am feeling terrible because I have spent the past 10 hours trying to understand this paper titled "Protection in Operating Systems" by Harrison, Ruzzo and Ullman. At this point, any help whether it is asking me to read some other paper or some kind of an explanation is good for me. As this paper is a landmark paper, I wanted to make sure I understand it thoroughly and I did until the paper states the following theorem on Page 7:</p>

<blockquote>
  <p><strong>THEOREM 1:</strong> There is an algorithm which decides
  whether or not a given
  mono-operational protection system and
  initial configuration is unsafe for a
  given generic right r.</p>
</blockquote>

<p>I do not understand the gist of the proof. I have tried looking at lecture notes from every possible class website but apparently everyone skipped this part and just mention the theorem statement as if it were an axiom. Maybe it is obvious to everyone but somehow I am missing the big picture: What is the theorem trying to accomplish?</p>

<p>Specifically, following are the questions that I have been getting over and over again:</p>

<blockquote>
  <p>PROOF: The proof hinges on two simple observations.  First, commands can test
  for the presence of rights, but not
  for the absence of rights or objects.
  This allows delete and destroy
  commands to be removed from
  computations leading to a leak.
  Second, a command can only identify
  objects by the rights in their row and
  column of a access matrix....</p>
</blockquote>

<ul>
<li>Why are these observations important? And how does the first statement allow for the removal of delete and destroy commands? I understand that these do not lead to a leak but how is this sentence derived (or implied) by the first?</li>
</ul>

<blockquote>
  <p>Suppose </p>
  
  <p>$(*) Q_0 \vdash_{c_{1}} Q_1
&gt; \vdash_{c_{2}} ... \vdash_{c_{m}} Q_m$</p>
  
  <p>is a minimal length computation
  reaching some configuration $Q_m$ for
  which there is a command $\alpha$
  leaking $r$. Let $Q_i =
&gt; (S_i,O_i,P_i).$ Now we claim that
  $C_i$, $2 \leq i \leq m$ is an enter
  command, and $C_1$ is either an enter
  or create subject command.</p>
</blockquote>

<p>This is good until the following sentence immediately after the above sentence:</p>

<blockquote>
  <p>Suppose not, and let $C_n$ be the last non-enter command in the sequence (*). Then we could form a shorter computation as follows...</p>
</blockquote>

<p>And I am lost. Can someone please give me an intuitive explanation of this proof?</p>

CC BY-SA 2.5
2011-03-15T03:14:24.513Z
"My understanding is that to show something is decidable, we need to show there exists an algorithm that will tell me so in *polynomial time*" no, this is incorrect, check the [wikipedia article](http://en.wikipedia.org/wiki/Decidable_language) or textbooks on computability theory for the definition of decidable.
Kaveh
CC BY-SA 2.5
2011-03-15T03:24:12.307Z
@Kaveh: I made a mistake. I removed the faulty statement. I will go through the link that you pointed me to. Thank you for pointing it out.
Legend
<ds.algorithms><computability>
Understanding the HRU Model (Protection in Operating Systems)
Legend
# Understanding the HRU Model (Protection in Operating Systems)

(Asked by: username_0 on 2011-03-15)

As of now I am feeling terrible because I have spent the past 10 hours trying to understand this paper titled "Protection in Operating Systems" by Harrison, Ruzzo and Ullman. At this point, any help whether it is asking me to read some other paper or some kind of an explanation is good for me. As this paper is a landmark paper, I wanted to make sure I understand it thoroughly and I did until the paper states the following theorem on Page 7:

> **THEOREM 1:** There is an algorithm which decides
> whether or not a given
> mono-operational protection system and
> initial configuration is unsafe for a
> given generic right r.

I do not understand the gist of the proof. I have tried looking at lecture notes from every possible class website but apparently everyone skipped this part and just mention the theorem statement as if it were an axiom. Maybe it is obvious to everyone but somehow I am missing the big picture: What is the theorem trying to accomplish?

Specifically, following are the questions that I have been getting over and over again:

> PROOF: The proof hinges on two simple observations. First, commands can test
> for the presence of rights, but not
> for the absence of rights or objects.
> This allows delete and destroy
> commands to be removed from
> computations leading to a leak.
> Second, a command can only identify
> objects by the rights in their row and
> column of a access matrix....

* Why are these observations important? And how does the first statement allow for the removal of delete and destroy commands? I understand that these do not lead to a leak but how is this sentence derived (or implied) by the first?

> Suppose
>
> $(\*) Q\_0 \vdash\_{c\_{1}} Q\_1
> > \vdash\_{c\_{2}} ... \vdash\_{c\_{m}} Q\_m$
>
> is a minimal length computation
> reaching some configuration $Q\_m$ for
> which there is a command $\alpha$
> leaking $r$. Let $Q\_i =
> > (S\_i,O\_i,P\_i).$ Now we claim that
> $C\_i$, $2 \leq i \leq m$ is an enter
> command, and $C\_1$ is either an enter
> or create subject command.

This is good until the following sentence immediately after the above sentence:

> Suppose not, and let $C\_n$ be the last non-enter command in the sequence (\*). Then we could form a shorter computation as follows...

And I am lost. Can someone please give me an intuitive explanation of this proof?

**Tags:** ds.algorithms, computability

> **Comments:**
> **username_1**: "My understanding is that to show something is decidable, we need to show there exists an algorithm that will tell me so in *polynomial time*" no, this is incorrect, check the [wikipedia article](http://en.wikipedia.org/wiki/Decidable_language) or textbooks on computability theory for the definition of decidable.  
> **username_0**: @username_1: I made a mistake. I removed the faulty statement. I will go through the link that you pointed me to. Thank you for pointing it out.  

---

## 0 answers

