Formal Methods in Security Vassena, Nemati, K√ľnnemann


[IFC] - Sheet 3 Solutions and Grade

Written: 09.12.2020 17:46 Written 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 nl1 has type (ref τ)l2 where τ = sl1. 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 e1 e2). 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 e1 ewe need to consider both the case where the function closures evaluated from e1 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.

Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators