SE547: Lecture 10

Overview

Information flow

Sequential noninterference

Timing channels

Concurrent noninterference

Declassification

JIF


Information flow

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

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

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

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

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

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

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

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; }

Sequential noninterference

Payoff from static analysis:

If c passes static analysis then c satisfies sequential noninterference.

Timing channels

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

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


Concurrent noninterference

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

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

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


Declassification

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

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 (Test1.jif):

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

Is this OK (Test2.jif):

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

JIF

Is this OK (Test3.jif):

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

Is this OK (Test4.jif):

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

JIF

Is this OK (Test5.jif):

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

Is this OK (Test6.jif):

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

Is this OK (Test7.jif):

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

Summary

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.


Next week

Final exam.