Computer Security: Art and Science

16.9 Exercises

1:
Revisit the example for x := y + z in Section 16.1.1. Assume that x does not exist in state s. Confirm that information flows from y and z to x by computing H(y_s | x_t), H(y_s), H(z_s | x_t), and H(z_s) and showing that H(y_s | x_t) < H(y_s) and H(z_s | x_t) < H(z_s).
2:
Let L = (S_L, _L) be a lattice. Prove that the structure IL = (S_IL, _IL), where each of the following is a lattice.

S_IL = { [a, b] | a, b S_L a _L b }
_IL = { ([a₁, b₁], [a₂, b₂]) | a₁ _L a₂ b₁ _L b₂ }
lub_IL([a₁, b₁], [a₂, b₂]) = (lub_L(a₁, a₂), lub_L(b₁, b₂))
glb_IL([a₁, b₁], [a₂, b₂]) = (glb_L(a₁, a₂), glb_L(b₁, b₂))
3:
Prove or disprove that the set P formed by the dual mapping of a reflexive information flow policy (as discussed in Definition 16�5) is a lattice.
4:
Extend the semantics of the information flow security mechanism in Section 16.3.1 for records (structures).
5:
Why can we omit the requirement lub{ i, b[i] } a[i] from the requirements for secure information flow in the example for iterative statements (see Section 16.3.2.4)?
6:
In the flow certification requirement for the goto statement in Section 16.3.2.5, the set of blocks along an execution path from b_i to IFD(b_i) excludes these endpoints. Why are they excluded?
7:
Prove that Fenton's Data Mark Machine described in Section 16.4.1 would detect the violation of policy in the execution time certification of the copy procedure.
8:
Discuss how the Security Pipeline Interface in Section 16.5.1 can prevent information flows that violate a confidentiality model. (Hint: Think of scanning messages for confidential data and sanitizing or blocking that data.)

Top

1:	Revisit the example for x := y + z in Section 16.1.1. Assume that x does not exist in state s. Confirm that information flows from y and z to x by computing H(y_s \| x_t), H(y_s), H(z_s \| x_t), and H(z_s) and showing that H(y_s \| x_t) < H(y_s) and H(z_s \| x_t) < H(z_s).
2:	Let L = (S_L, _L) be a lattice. Prove that the structure IL = (S_IL, _IL), where each of the following is a lattice. S_IL = { [a, b] \| a, b S_L a _L b } _IL = { ([a₁, b₁], [a₂, b₂]) \| a₁ _L a₂ b₁ _L b₂ } lub_IL([a₁, b₁], [a₂, b₂]) = (lub_L(a₁, a₂), lub_L(b₁, b₂)) glb_IL([a₁, b₁], [a₂, b₂]) = (glb_L(a₁, a₂), glb_L(b₁, b₂))
3:	Prove or disprove that the set P formed by the dual mapping of a reflexive information flow policy (as discussed in Definition 16�5) is a lattice.
4:	Extend the semantics of the information flow security mechanism in Section 16.3.1 for records (structures).
5:	Why can we omit the requirement lub{ i, b[i] } a[i] from the requirements for secure information flow in the example for iterative statements (see Section 16.3.2.4)?
6:	In the flow certification requirement for the goto statement in Section 16.3.2.5, the set of blocks along an execution path from b_i to IFD(b_i) excludes these endpoints. Why are they excluded?
7:	Prove that Fenton's Data Mark Machine described in Section 16.4.1 would detect the violation of policy in the execution time certification of the copy procedure.
8:	Discuss how the Security Pipeline Interface in Section 16.5.1 can prevent information flows that violate a confidentiality model. (Hint: Think of scanning messages for confidential data and sanitizing or blocking that data.)