Formal Methods in Security

[IFC] - Sheet 3 Solutions and Grade

Written on 09.12.2020 17:46 by Marco Vassena

I have graded assignment 3 and you should have received an email with your grade and a marked version of your solution.
Solutions to assignment 3 are available here.

A few general comments about this assignment:

• Also the third assignment went pretty well: 71% of the submissions were scored > 19 points.
• Most of you managed to do the proofs correctly, using the right proof technique and applying lemmas and induction appropriately): very good job!
• I noticed only two common mistakes in the proofs:

1. When reasoning about annotated references, we need to connect the label annotation from the evaluation rules with the label in the type of the reference from the typing judgment. (To do this formally, we apply type preservation, but this is less important). Importantly, an annotated label n_l1 has type (ref τ)^l2 where τ = s^l1. Notice that the label annotation l1 corresponds to the label of the content of the reference, not to the label l2 that annotates the reference type.
2. In the proof of L-equivalence preservation, we apply IH to the subterms and obtain proofs that the intermediate stores and values are L-equivalent (e.g., in case !e and e₁ e₂). Sometimes, we need to split on the L-equivalence judgment of the intermediate values (2 cases [L-Type] and [H-Type]) to complete the proof. For example, for function application e₁ e₂ we need to consider both the case where the function closures evaluated from e₁ are labeled secret (case [H-Type]) and when they are labeled public (case [L-Type]). In case [H-Type], we apply store confinement (twice) and the square lemma; in case [L-Type], we observe that the body of the function in the closures are the same and the environments are L-equivalent, and we can conclude the proof by IH.