Formal Methods in Security

IFC Sheet 2 - Solutions and Grade

Written on 02.12.2020 12:24 by Marco Vassena

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

A few general comments about this assignment:

• Also the second assignment went pretty well: 71% of the submissions were scored > 17 points.
• A program leaks secret data if the *public* output of the program is influenced by secret inputs. Therefore, when you claim that a program is leaky you need to argue that (1) it is well-typed and the output is labeled public (e.g., bool^L) and (2) explain how different secret inputs produce different public outputs.
• The purpose of the program counter label (pc) is to prevent implicit leaks through the value store (e.g., if secret then low := true else ()). Therefore, only constructs that write to the store (i.e., e₁ := e₂, new(e)) include security checks that involve the pc. In particular, when a program writes some data labeled "l" to the store, the data must be at least as sensitive as the "pc" label, i.e., pc ⊑ l.
  Reading from the store (i.e., !e) does not need checks that involve the pc label because the type of the result is labeled with the label of the data.
• Expressions that "create" values (e.g., (), true, false, \x.e, new(e)) can be labeled with any label. All the security checks appear in the typing rules that "use" these values (e.g., if e then e₁ else e₂, e₁ e₂, !e, write(e)). This makes the type system more permissive (it accepts more secure programs). For example, in λ^SFG rule [New-T] allows "new(true)" to be typed both (Ref Bool^L)^H  (in a public context) and (Ref Bool^H)^L. Although rule [Read-T] prevents programs from reading from a reference typed (Ref Bool^H)^L,  we can still accept all programs that create such a reference but never read from it. (There are extensions to λ^SFG that would also allow to read from such references as well).
• Even if we modify rule [New-T] to require that the label of the reference is at least as sensitive as the label of the content, e.g., l₁ ⊑ l₂, we are not entitled to omit this constraint in the other rules (e.g., [Read-T]): the inputs of the program can be arbitrarily typed, so we could still have references where l₁ ⊑ l₂ does not hold.
• When you extend λ^SFG with a new type, remember that there are two categories of types: simple types and labeled types. New types (e.g., array \tau) typically belong to the category "simple type".
• The label of unit can be chosen freely in rule [Write-T] because a value () does not contain any real information (this is the only possible value of type unit).