Control of Information Flow in Computer Systems

Lecture 20: Information Flow Control CS 5430 4/11/2018

2 Information flow policies Can flow to: Alice Doc Automatic deduction of policies! computation Can flow to: Alice Can flow to: Alice Doc Doc

Labels represent policies Secret, {nuc, crypto} Secret, {nuc} Conf, {nuc,crypto} Secret, {crypto} Conf, {nuc} Secret, {} Conf, {crypto} Conf, {}

Labels represent policies High Low

5 Noninterference [Goguen and Meseguer 1982] An interpretation of noninterference for a program: Changes on H inputs should not cause changes on L outputs. H H L L Outputs Inputs Program

6 Today: Information Flow Control Goal: Enforce IF policies that tag variables in a program. There is a mapping from variables to labels, which represent desired IF policies. The enforcement mechanism should ensure that a given program and a given satisfy noninterference.

7 Information Flow Control H ? H ? L ? L Inputs Outputs ? H ? L ? L ? Label Variable Program

8 Information Flow Control: fixed ? H ? H ? L ? L ? H ? L ? L ? remains the same during the analysis of the program. The mechanism checks that satisfies noninterference. The program is rejected, if at least one red arrow appears in the program.

9 Information Flow Control: flow-sensitive ? H ? L ? L ? H ? H ? H ? L ? may change during the analysis of the program. The mechanism deduces (x), (y), (z) such that noninterference is satisfied. The program is never rejected.

10 Enforcing IF policies Static mechanism Checking and/or deduction of labels before execution. Dynamic mechanism Checking and/or deduction of labels during execution. Hybrid mechanism Combination of static and dynamic.

STATIC TYPE CHECKING fixed

A simple programming language e ::= x | n | e1+e2 | ... c ::= x := e | if e then c1 else c2 | while e do c | c1; c2

13 Checking an assignment x := y Examples for confidentiality (x) is L. (y) is L. Does this assignment satisfy NI? (x) is H. (y) is L. Does this assignment satisfy NI? (x) is L. (y) is H. Does this assignment satisfy NI?

14 Checking an assignment Assignments cause explicit information flows. x := y It satisfies NI, if (y) (x).

15 Checking an assignment x := y It satisfies NI, if (y) (x). MLS for confidentiality no read up : S may read O iff Label(O) Label (S) no write down : S may write O iff Label(S) Label (O )

16 Checking an assignment x := y It satisfies NI, if (y) (x). MLS for confidentiality no read up : C may read y iff Label(y) Label (C) no write down : C may write x iff Label(C) Label (x)

17 Checking an assignment x := y + z It satisfies NI, if (y) (x) and (z) (x). It satisfies NI, if (y+z) (x). ???

18 Operator for combining labels For each and , there should exist label , such that: , , and if and , then . is called the joinof and . Operator is associative and commutative.

19 Checking an assignment x := y + z It satisfies NI, if (y) (z) (x).

20 Lattice of labels The set of labels and relation define a lattice, with join operator . Secret, {nuc, crypto} Secret, {nuc} Conf, {nuc,crypto} Secret, {crypto} Conf, {nuc} Secret, {} Conf, {crypto} Conf, {}

21 Checking an if-statement if z > 0 then x:= 1 else x:= 0 Examples for confidentiality (x) is L. (z) is L. Does this if-statement satisfy NI? (x) is H. (z) is L. Does this if-statement satisfy NI? (x) is L. (z) is H. Does this if-statement satisfy NI?

22 Checking an if-statement if z > 0 then x:= 1 else x:= 0 Conditional commands (e.g., if-statements and while-statements) cause implicit information flows.

23 Context if z > 0 then x:= 1 else x:= 0 They reveal information about z>0. Introduce a context label ??? Its ??? is (z).

24 Context if z > 0 then x:= 1 else x:= 0 Check if ??? (e) (x). Explicit flow Implicit flow Introduce a context label ??? Its ??? is (z).

25 Typing system for IF control Static Fixed Labels as types Label (x) is the type of x. Typing rules for all possible commands. Goal: type-correctness noninterference

26 We are already familiar with typing systems! Example of typing rule from Java or OCaml: x + y : int if x : int and y : int

27 Typing rules for expressions Judgement e : According to mapping , expression ehas type (i.e., label) . Constant: n : Variable: x : (x) Expression: e+e : if e : and e :

28 Typing rules for expressions Expression: e+e : if e : and e : Inference rule: e : e : Premises e+e : Conclusion

29 Example Let (x)= L and (y)= H. What is the type of x+y+1? Proof tree: (x) = L (y) = H 1 : L x : L y : H x + y + 1 : H

30 Typing rules for commands Judgement , ??? c According to mapping , and context label ???, command c is type correct.

31 Assignment rule , ??? x:=e if e: and ??? (x) e : ??? (x) , ??? x:=e

32 If-rule e : , ??? c1 , ??? c2 , ??? if e then c1 else c2

33 If-rule (example) 0 : , (z) L (x) 1 : (z) L (x) z>0 : (z) , (z) L x:=1 , (z) L x:=0 , L if z>0 then x:=1 else x:=0

34 Static type system e : Assignment-Rule: ??? (x) , ??? x:=e , ??? c1 e : , ??? c2 If-Rule: , ??? if e then c1 else c2 e : , ??? c While-Rule: , ??? while e do c , ??? c1 , ??? c2 Sequence-Rule: , ??? c1;c2

35 Soundness of type system ,??? c c satisfies NI

36 Limitations of the type system

37 This type system does not prevent leaks through covert channels. Example of covert channel: while s != 0 do { //nothing }; p:=1 where s is a secret variable (i.e., (s)= ) and pis a public variable (i.e., (p)=L ).

38 A solution To prevent covert channels due to infinite loops, strengthen the typing rule for while-statement, to allow only low guard expression: e , ??? c , ??? while e do c : Now, type correctness implies termination sensitive NI. But, the enforcement mechanism becomes overly conservative. Another solution? Research!

39 This type system is not complete. c satisfies noninterference , ??? c There is a command c, such that noninterference is satisfied, but c is not type correct. Example 1: x = H, y = L c is if x>0 then y:=1 else y:=1 c satisfies noninterference, because xdoes not leak to y. c is not type correct, because (x) (y).

40 This type system is not complete. Example 2: x = H, y = L c is if 1=1 then y:=1 else y:=x c satisfies noninterference, because x does not leak to y. c is not type correct, because (x) (y). So, this type system is conservative. It has false negatives: There are programs that are not type correct, but that satisfy noninterference.

41 Can we build a complete mechanism? Is there an enforcement mechanism for information flow control that has no false negatives? A mechanism that rejects only programs that do not satisfy noninterference? No! [Sabelfeld and Myers, 2003] The general problem of confidentiality for programs is undecidable. The halting problem can be reduced to the information flow control problem. Example: if h>1 then c; l:=2 else skip If we could precisely decide whether this program is secure, we could decide whether c terminates!

42 Can we build a mechanism with fewer false positives? Switch from static to dynamic mechanisms!