SE547: Lecture 2 (Information Flow)

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

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 x_H=y_L (write up) OK? Is y_L=x_H (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?

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.

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. x_H=y_L;
2. y_L=x_H;
3. x_H=0; if(even(y_L)) { x_H=1; }
4. y_L=0; if(even(x_H)) { y_L=1; }

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.

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)]

Model of commands (c₁, μ₁) (c₂, μ₂):

1. If (c₁, μ₁) μ₂ then (c₁d, μ₁) (d, μ₂)

2. If (c₁, μ₁) (c₂, μ₂) then (c₁d, μ₁) (c₂d, μ₂)

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 (c₁, μ₁) μ₂:

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

7. What about while?

Example:

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

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

1. { x_H = 37, y_L = 5 } ~ { x_H = 0, y_L = 5 }?
2. { x_H = 37, y_L = 5 } ~ { x_H = 37, y_L = 0 }?

A command c satisfies sequential noninterference when:

If μ₁ ~ ρ₁ and (c, μ₁) ^* μ₂ and (c, ρ₁) ^* ρ₂ then μ₂ ~ ρ₂.

Which of these satisfy sequential noninterference?

1. x_H=y_L;
2. y_L=x_H;
3. x_H=0; if(even(y_L)) { x_H=1; }
4. y_L=0; if(even(x_H)) { y_L=1; }

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. x_H=y_L;
2. y_L=x_H;
3. x_H=0; if(even(y_L)) { x_H=1; }
4. y_L=0; if(even(x_H)) { y_L=1; }

Secure Types:

• Data Types (denoted by τ) --- a set of security classes partially ordered by <=
• Phrase Types
  • Data types for expressions
  • Variable types (τ var) --- variable that stores information at level τ or lower
  • Command types (τ cmd) --- every assignment in the command assigns to level τ or higher

Subtyping:

• τ <: τ' means τ' is a higher security class than τ (e.g. L <: H)
• τ var <: τ' var if τ <: τ' (covariant)
• τ' cmd <: τ cmd if τ <: τ' (contravariant)
• Subtyping is reflexive (and transitive). All types are subtypes of themselves (τ <: τ)

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

Payoff from static analysis:

If c passes static analysis then c satisfies sequential noninterference.

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

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

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.

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

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

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

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

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

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

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.

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

These notes are from Alan Jeffrey

Revised: 2006/04/06 17:04