Homework #1
Due date: April 12, 2013
Points: 100
Questions
- (20 points) Consider a very high-assurance system developed for the military. The system has a set of specifications, and both the design and implementation have been proven to satisfy the specifications. What questions should school administrators ask when deciding whether to purchase such a system for their school’s use?
- (16 points) Let c be a copy flag and let a computer system have the rights {read, write, execute, append, list, modify, own}.
- Using the syntax in Section 2.3, write a command copy_all_rights(p, q, s) that copies all rights that p has over s to q.
- Modify your command so that only those rights with an associated copy flag are copied. The new copy should not have the copy flag.
- In the previous part, what conceptually would be the effect of copying the copy flag along with the right?
- (10 points) Minsky [1, p. 256] states that “privileges should not be allowed to grow when they are transported from one place in the system to another.” Does this differ from the Principle of Attenuation of Privilege as stated in class? If not, show they are the same; if so, how do they differ?
- (30 points) Prove Theorem 3.3. (Hint: Use a diagonalization argument to test each system as the set of protection systems is enumerated. Whenever a protection system leaks a right, add it to the list of unsafe protection systems.)
- (24 points) Prove Lemma 3.2.
Extra Credit
- (20 points) Prove or give a counterexample:
The predicate can·share(α, x, y, G0) is true if and only if there is an edge from x to y in G0 labeled α, or if the following hold simultaneously.
- There is a vertex with an s-to-y edge labeled α.
- There is a subject vertex x′ such that x′ = x or x′ initially spans to x.
- There is a subject vertex s′ such that s′ = s or s′ terminally spans to s.
- There is a sequence of subjects x1, …, xn with x1 = x′, xn = s′, and xi and xi+1 (1 ≤ i < n) being connected by an edge labeled t, an edge labeled g, or a bridge.
References
- Naftaly Minsky. The principle of attenuation of privileges and its ramifications. In Richard A. DeMillo, David P. Dobkin, Anita K. Jones, and Richard J. Lipton, editors, Foundations of Secure Computing, pages 255–277. Academic Press, New York, NY, USA, 1978.