Computer Security: Art and Science

20.8 Exercises

1:
Add a SPECIAL specification to the example beginning on page 522 that describes get_access (see Section 5.2.4.1).
2:
Section 20.3.1.1 presents three properties of the SRI model as embedded in the MLS tool. Compare and contrast these properties with the simple security property and the *-property of the Bell-LaPadula Model.
3:
Why does the Boyer-Moore theorem prover perform induction only when the other five steps fail to simplify the formula? Why does it not try induction first?
4:
Contrast the goals of the Gypsy Verification Environment with those of HDM. In particular, when is using HDM appropriate, and when is using Gypsy appropriate? Can HDM and Gypsy be used interchangeably?
5:
Add rules to the rats example for PVS in Section 20.4.1.1 for exponentiation (^) and remainder (%). Remember that 0⁰ and the remainder of anything when divided by 0 are both undefined.
6:
Compare the life cycle concept that the PVS proof checker uses with the waterfall model of software engineering (see Section 18.2.2). Can the life cycle concept be expressed as a form of the waterfall model?
7:
Consider the example in Section 20.4.2.2. The proof of the nonblocking condition states that "for every computational path, every state n_i has a successor state t_i." But the path s₀s₁s₂ is a cycle in which n₂ never changes to t₂. Reconcile this observation with the statement in the proof that "Inspection of Figure 20-5 shows that this is true."

Top

1:	Add a SPECIAL specification to the example beginning on page 522 that describes get_access (see Section 5.2.4.1).
2:	Section 20.3.1.1 presents three properties of the SRI model as embedded in the MLS tool. Compare and contrast these properties with the simple security property and the *-property of the Bell-LaPadula Model.
3:	Why does the Boyer-Moore theorem prover perform induction only when the other five steps fail to simplify the formula? Why does it not try induction first?
4:	Contrast the goals of the Gypsy Verification Environment with those of HDM. In particular, when is using HDM appropriate, and when is using Gypsy appropriate? Can HDM and Gypsy be used interchangeably?
5:	Add rules to the rats example for PVS in Section 20.4.1.1 for exponentiation (^) and remainder (%). Remember that 0⁰ and the remainder of anything when divided by 0 are both undefined.
6:	Compare the life cycle concept that the PVS proof checker uses with the waterfall model of software engineering (see Section 18.2.2). Can the life cycle concept be expressed as a form of the waterfall model?
7:	Consider the example in Section 20.4.2.2. The proof of the nonblocking condition states that "for every computational path, every state n_i has a successor state t_i." But the path s₀s₁s₂ is a cycle in which n₂ never changes to t₂. Reconcile this observation with the statement in the proof that "Inspection of Figure 20-5 shows that this is true."