SE547: Lecture 2 (Information Flow)

Contents [0/23]

Background: Operational Semantics and Type Systems [1/23]
Information flow [2/23]
Information flow [3/23]
Sequential noninterference [4/23]
Sequential noninterference [5/23]
Sequential noninterference [6/23]
Sequential noninterference [7/23]
Sequential noninterference [8/23]
Sequential noninterference [9/23]
Types [10/23]
Subtyping [11/23]
Sequential noninterference [12/23]
Timing channels [13/23]
Timing channels [14/23]
Concurrent noninterference [15/23]
Concurrent noninterference [16/23]
Declassification [17/23]
JIF [18/23]
JIF [19/23]
JIF [20/23]
Summary [21/23]
Inference Rules in Programming Languages [22/23]
Acknowledgement [23/23]

Background: Operational Semantics and Type Systems [1/23]

References

David Walker's notes on Semantics for Safe Programming Languages

Bob Harper's book on Programming Languages

Andy Pitts' course on Operational Semantics

Andy Pitts' course on Types

Information flow [2/23]

What is Mandatory Access Control?

What is a security level? Simple security levels: H and L.

Tag data and variables with security levels. Examples of information flow between security levels... Is xH=yL (write up) OK? Is yL=xH (write down) OK?

(Note: in this world, high-security programs have fewer rights than low-security programs! Spot the military funding...)

What is a covert channel? Examples? Can we completely eliminate covert channels?

Information flow [3/23]

Note that Java protection doesn't help!

  class Example {
    private int xH;
    public int yL;
    public void leak () {
      yL = xH; // Write down is OK according to Java.
    }
  }

Java doesn't stop values escaping from their static protection.

Sequential noninterference [4/23]

Informal idea behind noninterference (make this formal later):

A program P satisfies noninterference if the contents of low security variables after running P is independent of the contents of high security variables before running P

Which of the following satisfy noninterference?

  1. xH=yL;
  2. yL=xH;
  3. xH=0; if(even(yL)) { xH=1; }
  4. yL=0; if(even(xH)) { yL=1; }

Sequential noninterference [5/23]

Formal model of commands...

c, d ::=
    x = e;
    c d
    if (e) { c } else { d }
    while (e) { c }

and expressions...

e, f ::=
    x
    n
    e + f
    e == f
    ...

This is Smith and Volpano's model, dressed up in Java syntax.

Sequential noninterference [6/23]

A memory μ is a mapping from variables to integers, for example:

{ x = 37, y = 5 }

Write μ(e) for the result of evaluating expression e in memory μ. For example, in the above memory, what are:

μ(x + 1)
μ(x == y)

Write μ[x:=n] for the result of updating memory μ so x now contains n. For example, in the above memory, what are:

μ[y := μ(x + 1)]
μ[y := μ(x == y)]

Sequential noninterference [7/23]

Model of commands (c1, μ1) -> (c2, μ2):

1. If (c1, μ1) -> μ2 then (c1d, μ1) -> (d, μ2)

2. If (c1, μ1) -> (c2, μ2) then (c1d, μ1) -> (c2d, μ2)

3. If μ(e) is nonzero then (if (e) {c} else {d}, μ) -> (c, μ)

4. If μ(e) is zero then (if (e) {c} else {d}, μ) -> (d, μ)

5. What about while?

Model of commands final step (c1, μ1) -> μ2:

6. (x=e, μ) -> μ[x:=μ(e)]

7. What about while?

Example:

x:=1; while(x) { x=x-1; }

Sequential noninterference [8/23]

Write μ ~ ρ whenever μ and ρ agree on L variables:

  1. { xH = 37, yL = 5 } ~ { xH = 0, yL = 5 }?
  2. { xH = 37, yL = 5 } ~ { xH = 37, yL = 0 }?

A command c satisfies sequential noninterference when:

If μ1 ~ ρ1 and (c, μ1) ->* μ2 and (c, ρ1) ->* ρ2 then μ2 ~ ρ2.

Which of these satisfy sequential noninterference?

  1. xH=yL;
  2. yL=xH;
  3. xH=0; if(even(yL)) { xH=1; }
  4. yL=0; if(even(xH)) { yL=1; }

Sequential noninterference [9/23]

Static analysis for noninterference satisfying:

1. In x = e, if e reads from an H variable, then x is an H variable.

2. In if (e) { c } else { d }, if e reads from an H variable, then c and d only write to H variables.

3. In while (e) { c }, if e reads from an H variable, then c only writes to H variables.

Which of these pass static analysis?

  1. xH=yL;
  2. yL=xH;
  3. xH=0; if(even(yL)) { xH=1; }
  4. yL=0; if(even(xH)) { yL=1; }

Types [10/23]

Secure Types:

Subtyping [11/23]

Subtyping:

Allows for more complex set of security classes (e.g. {H,L1,L2 | L1 <: H & L2 <: H}

Sequential noninterference [12/23]

Payoff from static analysis:

If c passes static analysis then c satisfies sequential noninterference.

Timing channels [13/23]

Adding a clock to the language can break noninterference:

  finishL = System.getTimeMillis () + 1000;
  while (secretH && System.getTimeMillis () < finishL) { }
  if (System.getTimeMillis () < finishL) { resultL = 0; }
  else { resultL = 1; }

What happens in initial memory { secretH = 0, everything else = 0 }?

What happens in initial memory { secretH = 1, everything else = 0 }?

Timing channels [14/23]

State-of-the-art: make the clock high security. Not very practical!

Concurrent noninterference [15/23]

Noninterference for concurrent programs is much harder. Thread α:

  while (trigger0H == 0) {}  resultL = 1;
  trigger1H++

Thread β:

  while (trigger1H == 0) {} resultL = 0;
  trigger0H++;

Thread γ:

  if (secretH == 0) { trigger0H++; } else { trigger1H++; }

What happens in initial memory { secretH = 0, everything else = 0 }?

What happens in initial memory { secretH = 1, everything else = 0 }?

Smith and Volpano scale this up to leak an n-bit PIN, not just one bit.

Concurrent noninterference [16/23]

State-of-the-art: ban high-security while loops. Not very practical!

Also relies on a nondeterministic scheduler, otherwise timing channels are possible.

Declassification [17/23]

Mandatory Access Control is usually too restrictive in practice: we need some way to declassify data.

  booleanL checkPwd (StringL uid, StringL guess, StringH pwd) {
    return (guess == pwd); // Does not pass static analysis!
  }

Declassification requires authority, either granted directly:

  booleanL checkPwd (StringL uid, StringL guess, StringH pwd)
  where authority(H) {
    return declassify(guess == pwd, L);
  }

or granted to the calling method and delegated:

  booleanL checkPwd (StringL uid, StringL guess, StringH pwd)
  where caller(H) {
    return declassify(guess == pwd, L);
  }

JIF [18/23]

Java Information Flow http://www.cs.cornell.edu/jif/ implements static analysis for information flow.

Checks for sequential noninterference, not timing channels or concurrent noninterference.

Is this OK (file:Test1.jif):

  public int{Alice:} run (int{Alice:} x) {
    return x;
  }

Is this OK (file:Test2.jif):

  public int{Bob:} run (int{Alice:} x) {
    return x;
  }

JIF [19/23]

Is this OK (file:Test3.jif):

  public int{} run (int{Alice:} x) {
    return x;
  }

Is this OK (file:Test4.jif):

  public int{Alice:} run (int{} x) {
    return x;
  }

JIF [20/23]

Is this OK (file:Test5.jif):

  public int{Bob:} run (int{Alice:} x)
  where authority(Alice) {
    return declassify (x, {Bob:});
  }

Is this OK (file:Test6.jif):

  public int{Bob:} run (int{Alice:} x) {
    return declassify (x, {Bob:});
  }

Is this OK (file:Test7.jif):

  public int{Bob:} run (int{Alice:} x) 
  where caller(Alice) {
    return declassify (x, {Bob:});
  }

Summary [21/23]

Information flow tracks the security levels of data.

Goal of information flow is to ensure noninterference: values in low security variables cannot depend on values in high security variables.

Static analysis of sequential code without timers is possible.

Static analysis of concurrent code or code with timers is much harder.

Practical information flow systems include declassification.

Inference Rules in Programming Languages [22/23]

David Walker's notes from Oregon Summer School: http://www.cs.uoregon.edu/activities/summerschool/summer04/lectures/safelanguages.ppt

Acknowledgement [23/23]

These notes are from Alan Jeffrey


Revised: 2006/04/06 17:04