Understanding Information Flow Control Mechanisms in Computer Science

Lecture 20: Information Flow Control CS 181S Spring 2024

Where we were Authentication: mechanisms that bind principals to actions Authorization: mechanisms that govern whether actions are permitted Audit: mechanisms that record and review actions

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

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

Enforcing Information Flow Goal: Enforce that only programs that satisfy NonInterference can run in our system. Goal: Design a type system such that p p satisfies NonInterference

Review: Type Inference (Expressions) int x; bool y; ? = ???; ? = ????; Type environment maps variables to type Goal: Judgement (aka proof that) e : t According to mapping , expression e has type t Constants: ? ??? ???? ???? ????? ???? Variables: x =? ? t Expressions: ?1 ???, ?2 ??? ?1 ???, ?2 ??? ?1<?2 ???? ?1+?2 ???

Review: Static type system e : t Assignment-Rule: t (x) x=e; p1 p2 Sequence-Rule: p1 p2 e : bool p1 p2 If-Rule: if(e) then{ p1 } else{ p2 } e : bool While-Rule: p while(e){ p } Skip-Rule: nop;

Label Inference (Expressions) label ? = ?; ? = ?; Type environment maps variables to type Goal: Judgement (aka proof that) e : According to mapping , expression e has label Constants: ? ? Variables: x = ? ? ??? ? Unary Operations: Binary Operations:

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, {}

Join Operator for combining labels For each 1 and 2, there exists a label 3, such that: 1 3 2 3 for all 4 such that 4 and 2 4, then 3 4. 3 is called the joinof and 2 and denoted 1 2 Operator is associative and commutative.

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, {}

Exercise: Join What are the following labels (H or L)? High ? ? ? ? ? ? ? ? 1. 2. 3. 4. Low

Label Inference (Expressions) label ? = ?; ? = ?; Type environment maps variables to type Goal: Judgement (aka proof that) e : According to mapping , expression e has label Constants: ? ? Variables: x = ? ? ??? ? Unary Operations: Binary Operations: ?1 1, ?2 2 ?1+?2 1 2

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

Exercise Let (x)= L and (y)= H. What is the type of y>x+5? Proof tree: (x) = L 5 : L x : L (y) = H x + 5 : L y : H y > x + 5 : H

Exercise: Checking an assignment x = y; (x) is L. (y) is L. Does this assignment satisfy NI? (x) is L. (y) is H. Does this assignment satisfy NI? (x) is H. (y) is L. Does this assignment satisfy NI? (x) is H. (y) is H. Does this assignment satisfy NI? To satisfy NI, need (y) (x).

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

Exercise: Checking a conditional assignment if(z > 0){ x = 1; }else{ x = 0; } Examples for confidentiality (x) is L. (z) is L. Does the assignment satisfy NI? (x) is L. (z) is H. Does the assignment satisfy NI? (x) is H. (z) is L. Does the assignment satisfy NI? (x) is H. (z) is H. Does the assignment satisfy NI?

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

Context if(z > 0){ x = 1; } else { x = 0; } They reveal information about z>0. Introduce a context label ??? Its ??? is the type of the expression z > 0

Context if(z > 0){ x = 1; } else { x = 0; } Check if ??? (e) (x). Explicit flow Implicit flow Introduce a context label ??? Its ??? is the label of the expression z > 0.

Static type system e : Assignment-Rule: ??? (x) , ??? x = e; , ??? p1 e : , ??? p2 If-Rule: , ??? if(e){ p1 } else{ p2 } e : , ??? p While-Rule: , ??? while(e){ p } , ??? p1 , ??? p2 Sequence-Rule: , ??? p1 p2 Skip-Rule: ??? nop;

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

Exercise: Type Checking Assume ? = ? and ? = ?. Prove that the program if(z>0){x = 1;} else {x = 0;} type checks (in a L context).

Exercise: Type Checking Assume ? = ? and ? = ?. Try to prove that the program if(z>0){x = 1;} else {x = 0;} type checks (in a L context).

Languages for Information Flow Control Declare variables with information flow labels int {Alice Bob} x; FlowCAML LMonad (Haskell) SPARK dependency contracts

Security type: only root may learn information in this field

Declassification: okay to leak whether password matches

Information Flow Control: fixed ? L ? 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 any flow violates noninterference

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.

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. Also have to deal with declassification