Enforcing Information Flow Policies

Enforcing information flow by combining static anddynamic analysis
Andrew Bedford, Josée Desharnais, Théophane G. Godonou,
Nadia Tawbi
Université Laval, Québec, Canada

Université Laval 2014

Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 2014

1 / 33

Enforcing Information Flow Policies

1

Context

2

The language

3

Dynamic Semantics

4

Motivation

5

Type based analysis

6

Instrumentation

7

Conclusion

Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 2014

2 / 33

Enforcing Information Flow Policies
Context

Plan
1

Context

2

The language

3

Dynamic Semantics

4

Motivation

5

Type based analysis

6

Instrumentation

7

Conclusion

Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 2014

3 / 33

Enforcing Information Flow Policies
Context

Context

Enforcing security mechanisms must control how information flows
through the system.
No information can flow from a private source to a public destination.
Static mechanisms, usually type-based, are conservative, they rejectprograms in case of doubt.
Our approach is type-based data-flow sensitive
The program is safe: all the executions satisfy the information flow
policyThe program may be unsafe: instrumentation is needed.
The program is unsafe: rejection.

Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 2014

4 / 33

Enforcing Information Flow Policies
Context

The non-interference property

Non-interference essentially means that a variation of program input
associated with a given security level does not cause variation of
output of lower security level.
We have to forbid explicit flow and implicit flow.

Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 2014

5 / 33

Enforcing Information Flow Policies
The language

The core language(instructions)(expressions)(commands)

Nadia Tawbi (Université Laval)

p ::=
e ::=
c ::=

e |c
x | n | nch | e1 op e2
x := e |skip |
if e then c1 else c2 end |while e do c end |c1 ; c2 |receivec x1 from x2 |receiven x1 from x2 |send x1 to x2

Enforcing Information Flow Policies

Université Laval 2014

6 / 33

Enforcing Information Flow Policies
The language

The language

Programs are sequential.
Programs communicate via channels.
An external observer can see only the channels not the variables.
The channels are assigned a priori security levels, types.
The variables security levels depend on the security level of theircontent.

Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 2014

7 / 33

Enforcing Information Flow Policies
Dynamic Semantics

Plan
1

Context

2

The language

3

Dynamic Semantics

4

Motivation

5

Type based analysis

6

Instrumentation

7

Conclusion

Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 20148 / 33

Enforcing Information Flow Policies
Dynamic Semantics

Some dynamic rules I

he, µi →e v
hx := e, µi → µ[x 7→ v ](ASSIGN)(RECEIVE-CONTENT)x2 ∈ dom(µ)
read(µ(x2 )) = n
hreceivec x1 from x2 , µi → µ[x1 7→ n](RECEIVE-NAME)

x2 ∈ dom(µ)
read(µ(x2 )) = nch
hreceiven x1 from x2 , µi → µ[x1 7→ nch]x1 ∈ dom(µ)
hsend x1 to x2 , µi → µ, update(µ(x2 ), µ(x1 ))(SEND)

Table : A few rules of the structural operational semantics
Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 2014

9 / 33

Enforcing Information Flow Policies
Dynamic Semantics

Some dynamic rules II(CONDITIONAL)

he, µi →e nn 6= 0hif e then c1 else c2 end, µi → hc1 , µi
he, µi →e nn=0
hif e then c1 else c2 end, µi → hc2 , µi
he, µi →e nn=0hwhile e do c end, µi → µ(LOOP)

he, µi →e nn 6= 0hwhile e do c end, µi → hc; while e then c end, µi
hc1 , µi → µ0

(SEQUENCE)

hc1 ; c2 , µi → hc2 , µ0 i

Table : Structural operational semantics
Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 2014

10 / 33

Enforcing Information Flow Policies
Motivation examples

Explicit or implicit flow
Reject programs leading to explicit or implicit flow.
1.
2.

x := highValue;
send x to publicChannel

1.
2.
3.

if highValue thenx := 1else
x := 2end;
send x to publicChannel

4.
5.

Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 201411 / 33

Enforcing Information Flow Policies
Motivation examples

Flow sensitivity

Take into account data flows.
1.
2.
3.
4.
5.

receivec x from privateChannel;
receiven c from publicChannel;
receivec x from c;
x := 0;send x to publicChannel;

Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 201412 / 33

Enforcing Information Flow Policies
Motivation examples

Unknown flow

Do not reject programs leading to unknown flows.
1.
2.
3.

receivec x from privateChannel;
receiven c from publicChannel;
send x to c

Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 201413 / 33

Enforcing Information Flow Policies
Motivation examples

Blocked channel

Reject programs leading to more subtle implicit flow.
1.
2.
3.
4.
5.

receivec x from privateChannel;
if x > 0 thenc:= publicChannel1;else
c:= publicChannel2
end;
send lowValue to c

Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 201414 / 33

Enforcing Information Flow Policies
Type based analysis

Plan
1

Context

2

The language

3

Dynamic Semantics

4

Motivation

5

Type based analysis

6

Instrumentation

7

Conclusion

Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 201415 / 33

Enforcing Information Flow Policies
Type based analysis

The typing principles

The security types are defined as follows:(data types)
τ ::= L | U | H | B(instruction types) ρ ::= τ val | τ chan | τ cmd
L v U v H v B, B 6v H 6v U 6v L
U is assigned when the type cannot be determined statically.
B is used to block a channel without rejecting the program.
A special variable instr indicates the need of instrumentation or not.
Channels are assigned a priori security types namely H or L.
Variables security types depend on the security type of their content.

Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 201416 / 33

Enforcing Information Flow Policies
Type based analysis

The non-interference property revisited
Definition(Non-interference) A program P satisfies non-interference if, for any
memories µ and ν that are τ -equivalent and that agree on values of typeτ 0 v τ , the memories µ0 and ν 0 produced by running P on µ and ν are alsoτ -equivalent (provided that both runs terminate successfully).
Definition(τ -equivalence) Two memories µ and ν are τ -equivalent, writtenµ ∼τ ν, if ∀x ∈ dom(µ) ∩ dom(ν) : (x is a channel of type τ 0 chan ∧ τ 0 v
τ ) ⇒ µ(x) =ch ν(x).
where τ is a security level.
Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 201417 / 33

Enforcing Information Flow Policies
Type based analysis

Some typing rules(ASSIGN-CHAN S)(RECEIVECONTENT S)(RECEIVENAME S)

Γ, pc ` e : τ chanΓ, pc ` x := e : τ cmd, Γ t [ instr 7→ HLLL (pc, τ )] † [x 7→ HLBτ (pc, τ )chan]
Γ(x2 ) = τ chanΓ, pc ` receivec x1 from x2 : (τ t pc) cmd, Γ † [x1 7→ (τ t pc)val]
Γ(x2 ) = τ chanΓ, pc ` receiven x1 from x2 : τ cmd,
Γ t [ instr 7→ HLLτ (pc, τ )] † [x1 7→ HLBUtτ (pc, τ )chan]Γ(x1 ) = τ1 α

(SEND S)Γ(x2 ) = τ chan¬((τ1 t pc) = H ∧ τ = L)

τ 6= BΓ, pc ` send x1 to x2 : τ cmd, Γ t [ instr 7→ HLUL (τ1 t pc, τ )]Table : Typing rules 1
Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 201418 / 33

Enforcing Information Flow Policies
Type based analysis

Some typing rules II(CONDITIONAL S)
Γ, pc ` e : τ0 val

Γ, (pc t τ0 ) ` c1 : τ1 cmd, Γ0Γ, (pc t τ0 ) ` c2 : τ2 cmd, Γ00

Γ0 t Γ00 A ⊥Γ, pc ` if e then c1 else c2 end : (τ1 u τ2 ) cmd, Γ0 t Γ00(LOOP1 S)

Γ, pc ` e : τ0 val

Γ, (pc t τ0 ) ` c : τ cmd, Γ0

Γ, pc ` while e do c end : τ cmd, Γ t Γ0Γ, (pc t τ0 ) ` c : τ cmd, Γ0(LOOP2 S)Γ = Γ t Γ0 A ⊥Γ, pc ` e : τ0 val

Γ 6= Γ t Γ0 A ⊥Γ t Γ0 , (pc t τ0 ) ` while e do c end : τ 0 cmd, Γ00

Γ, pc ` while e do c end : τ 0 cmd, Γ00(SEQUENCE S)

Γ, pc ` c1 : τ1 cmd, Γ0Γ0 , pc ` c2 : τ2 cmd, Γ00
Γ, pc ` c1 ; c2 : (τ1 u τ2 ) cmd, Γ00

Table : Typing rules2
Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 201419 / 33

Enforcing Information Flow Policies
Type based analysis

Explicit flow

Nadia Tawbi (Université Laval)1.

x := highValue;

2.

send x to publicChannel

Enforcing Information Flow Policies

Université Laval 2014

20 / 33

Enforcing Information Flow Policies
Type based analysis

Explicit flow

1.
2.

Nadia Tawbi (Université Laval)

x := highValue;[x 7→ H val]
send x to publicChannel

Enforcing Information Flow Policies

Université Laval 2014

20 / 33

Enforcing Information Flow Policies
Type based analysis

Explicit flow

1.
2.

Nadia Tawbi (Université Laval)

x := highValue;[x 7→ H val]
send x to publicChannel
RejectEnforcing Information Flow Policies

Université Laval 2014

20 / 33

Enforcing Information Flow Policies
Type based analysis

Implicit flow4.

if highValue thenx := 1else
x := 2end;

5.

send x to publicChannel

1.
2.
3.

Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 2014

21 / 33

Enforcing Information Flow Policies
Type based analysis

Implicit flow

1.
2.
3.
4.
5.

Nadia Tawbi (Université Laval)

if highValue thenx := 1else
x := 2end;[x 7→ H val]
send x to publicChannel

Enforcing Information Flow Policies

Université Laval 2014

21 / 33

Enforcing Information Flow Policies
Type based analysis

Implicit flow

1.
2.
3.
4.
5.

Nadia Tawbi (Université Laval)

if highValue thenx := 1else
x := 2end;[x 7→ H val]
send x to publicChannel
RejectEnforcing Information Flow Policies

Université Laval 2014

21 / 33

Enforcing Information Flow Policies
Type based analysis

Flow sensitivity
1.

receivec x from privateChannel;

2.

receiven c from publicChannel;

3.

receivec x from c;4.

x := 0;5.

send x to publicChannel;

Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 201422 / 33

Enforcing Information Flow Policies
Type based analysis

Flow sensitivity

2.

receivec x from privateChannel;[x 7→ H val]
receiven c from publicChannel;

3.

receivec x from c;4.

x := 0;5.

send x to publicChannel;

1.

Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 201422 / 33

Enforcing Information Flow Policies
Type based analysis

Flow sensitivity

3.

receivec x from privateChannel;[x 7→ H val]
receiven c from publicChannel;[x 7→ H val, c 7→ U chan]receivec x from c;4.

x := 0;5.

send x to publicChannel;

1.
2.

Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 201422 / 33

Enforcing Information Flow Policies
Type based analysis

Flow sensitivity

4.

receivec x from privateChannel;[x 7→ H val]
receiven c from publicChannel;[x 7→ H val, c 7→ U chan]receivec x from c;[c 7→ U chan, x 7→ U val]
x := 0;5.

send x to publicChannel;

1.
2.
3.

Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 201422 / 33

Enforcing Information Flow Policies
Type based analysis

Flow sensitivity
1.
2.
3.
4.
5.

Nadia Tawbi (Université Laval)

receivec x from privateChannel;[x 7→ H val]
receiven c from publicChannel;[x 7→ H val, c 7→ U chan]receivec x from c;[c 7→ U chan, x 7→ U val]
x := 0;[x 7→ L val]
send x to publicChannel;

Enforcing Information Flow Policies

Université Laval 201422 / 33

Enforcing Information Flow Policies
Type based analysis

Flow sensitivity
1.
2.
3.
4.
5.

Nadia Tawbi (Université Laval)

receivec x from privateChannel;[x 7→ H val]
receiven c from publicChannel;[x 7→ H val, c 7→ U chan]receivec x from c;[c 7→ U chan, x 7→ U val]
x := 0;[x 7→ L val]
send x to publicChannel;
AcceptEnforcing Information Flow Policies

Université Laval 201422 / 33

Enforcing Information Flow Policies
Type based analysis

Flow sensitivity
receivec h from privateChannel;
e := 0;x1 := 0;x2 := 0;x3 := 0;while e < 5 do
send x3 to publicChannel;
x3 := x2;
x2 := x1;
x1 := h;e := e+1
end
Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 2014

23 / 33

Enforcing Information Flow Policies
Type based analysis

Flow sensitivity
receivec h from privateChannel;
e := 0;x1 := 0;x2 := 0;x3 := 0;while e < 5 do
[h 7→ H val, e 7→ L val, x1 7→ H val, x2 7→ H val, x3 7→ H val]
send x3 to publicChannel;
x3 := x2;
x2 := x1;
x1 := h;e := e+1
end
Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 2014

23 / 33

Enforcing Information Flow Policies
Type based analysis

Flow sensitivity
receivec h from privateChannel;
e := 0;x1 := 0;x2 := 0;x3 := 0;while e < 5 do
[h 7→ H val, e 7→ L val, x1 7→ H val, x2 7→ H val, x3 7→ H val]
send x3 to publicChannel;
x3 := x2;
x2 := x1;
x1 := h;e := e+1
end
RejectNadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 2014

23 / 33

Enforcing Information Flow Policies
Type based analysis

Unknown flow

1.

receivec x from privateChannel;

2.

receiven c from publicChannel;

3.

send x to c

Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 201424 / 33

Enforcing Information Flow Policies
Type based analysis

Unknown flow2.

receivec x from privateChannel;[x 7→ H val]
receiven c from publicChannel;

3.

send x to c

1.

Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 201424 / 33

Enforcing Information Flow Policies
Type based analysis

Unknown flow

1.
2.
3.

Nadia Tawbi (Université Laval)

receivec x from privateChannel;[x 7→ H val]
receiven c from publicChannel;[x 7→ H val, c 7→ U chan]send x to c

Enforcing Information Flow Policies

Université Laval 201424 / 33

Enforcing Information Flow Policies
Type based analysis

Unknown flow

1.
2.
3.

Nadia Tawbi (Université Laval)

receivec x from privateChannel;[x 7→ H val]
receiven c from publicChannel;[x 7→ H val, c 7→ U chan]send x to c
Tag for need of instrumentation

Enforcing Information Flow Policies

Université Laval 201424 / 33

Enforcing Information Flow Policies
Type based analysis

Blocked channel
1.

receivec x from privateChannel;

2.
3.

if x > 0 thenc:= publicChannel1;

4.

else
c:= publicChannel2
end;

5.

Nadia Tawbi (Université Laval)

send lowValue to c

Enforcing Information Flow Policies

Université Laval 2014

25 / 33

Enforcing Information Flow Policies
Type based analysis

Blocked channel

2.
3.

receivec x from privateChannel;[x 7→ H val]
if x > 0 thenc:= publicChannel1;

4.

else
c:= publicChannel2

1.

end;
5.

Nadia Tawbi (Université Laval)

send lowValue to c

Enforcing Information Flow Policies

Université Laval 2014

25 / 33

Enforcing Information Flow Policies
Type based analysis

Blocked channel
1.
2.
3.

4.

receivec x from privateChannel;[x 7→ H val]
if x > 0 thenc:= publicChannel1;
pc 7→ H, [x 7→ H val, c 7→ B chan]else
c:= publicChannel2
end;

5.

Nadia Tawbi (Université Laval)

send lowValue to c

Enforcing Information Flow Policies

Université Laval 2014

25 / 33

Enforcing Information Flow Policies
Type based analysis

Blocked channel
1.
2.
3.

4.

5.

Nadia Tawbi (Université Laval)

receivec x from privateChannel;[x 7→ H val]
if x > 0 thenc:= publicChannel1;
pc 7→ H, [x 7→ H val, c 7→ B chan]else
c:= publicChannel2
pc 7→ H, [x 7→ H val, c 7→ B chan]end;
send lowValue to c

Enforcing Information Flow Policies

Université Laval 2014

25 / 33

Enforcing Information Flow Policies
Type based analysis

Blocked channel
1.
2.
3.

4.

5.

Nadia Tawbi (Université Laval)

receivec x from privateChannel;[x 7→ H val]
if x > 0 thenc:= publicChannel1;
pc 7→ H, [x 7→ H val, c 7→ B chan]else
c:= publicChannel2
pc 7→ H, [x 7→ H val, c 7→ B chan]end;[x 7→ H val, c 7→ B chan]send lowValue to c

Enforcing Information Flow Policies

Université Laval 2014

25 / 33

Enforcing Information Flow Policies
Type based analysis

Blocked channel
1.
2.
3.

4.

5.

Nadia Tawbi (Université Laval)

receivec x from privateChannel;[x 7→ H val]
if x > 0 thenc:= publicChannel1;
pc 7→ H, [x 7→ H val, c 7→ B chan]else
c:= publicChannel2
pc 7→ H, [x 7→ H val, c 7→ B chan]end;[x 7→ H val, c 7→ B chan]send lowValue to c
RejectEnforcing Information Flow Policies

Université Laval 2014

25 / 33

Enforcing Information Flow Policies
Type based analysis

Inference algorithm refines the type system
Infer(ge , i, pc, c) =case c of..
.
receiven x1 from x2 :
τ = evalT(ge (x2 ))instrt = HL(L, τ, pc, τ )instrt2 = ge ( instr)
x1t = HL(B, sup(U, τ ), pc, τ )G (i) = updateEnv(updateEnv(ge , instr, sup( instrt , instrt2 )), x1 , x1t chan)return (G (i), i + 1)
send x1 to x2 :
τ1 = evalT(ge (x1 ))τ = evalT(ge (x2 ))instrt = HL(U, L, sup(τ1 , pc), τ )instrt2 = ge ( instr)if ((τ 6= B) and ¬(sup(τ1 , pc) = H and τ = L))then G (i) = updateEnv(ge , instr, sup( instrt , instrt2 ))else failreturn (G (i), i + 1)..
.
Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 2014

26 / 33

Enforcing Information Flow Policies
Instrumentation

Plan
1

Context

2

The language

3

Dynamic Semantics

4

Motivation

5

Type based analysis

6

Instrumentation

7

Conclusion

Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 201427 / 33

Enforcing Information Flow Policies
Instrumentation

Instrumentation algorithm
Instrument: cmd * int → int
Instrument(c, i) =case c of..
.
receiven x1 from x2 :IC = IC ∧ “receiven x1 from x2 ”;
if (G (i)(x2 ) ! = L chan)then IC = IC ∧ “ if TypeOf Channel(x1 ) = L chan and TypeOf Channel(x2 ) = H chanthen updateEnv(G (i), x1 , B chan)else updateEnv(G (i), x1 , TypeOf Channel(x1 ))end ”
else IC = IC ∧ “updateEnv(G (i), x1 , TypeOf Channel(x1 ))”end
IC = IC ∧ “ updateEnv(g M, x1 , G (i)(x1 )); ”
return (i + 1)
send x1 to x2 :IC = IC ∧ “ tau = TypeOf Expression(x2 ) ; tau1 = TypeOf Expression(x1 );if(((tau = L chan) and (sup(evalT(tau1 ), top(pc)) = H)) or (tau = B chan))then fail else send x1 to x2 end; ”
return (i + 1).
..
Nadia Tawbi (Université Laval)
Enforcing Information Flow Policies
Université Laval 201428 / 33

Enforcing Information Flow Policies
Instrumentation

Example: unknown flow

1.
2.
3.

Nadia Tawbi (Université Laval)

receivec x from privateChannel;[x 7→ H val]
receiven c from publicChannel;[x 7→ H val, c 7→ U chan]send x to c
Tag for need of instrumentation

Enforcing Information Flow Policies

Université Laval 201429 / 33

Enforcing Information Flow Policies
Instrumentation

Instrumented example
push(L, pc);

1.

receivec x from privateChannel;
updateEnv(g M, x, G(1)(x));

2.

receiven c from publicChannel;
updateEnv(G(2), c, TypeOf Channel(c));
updateEnv(g M, c, G(2)(c));
tau = TypeOf Expression(c);tau1 = TypeOf Expression(x);if ((tau = L chan) and sup(evalT(tau1), top(pc)) = H) or(tau = B chan) then fail; else5.

send x to c

Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 201430 / 33

Enforcing Information Flow Policies
Conclusion

Plan
1

Context

2

The language

3

Dynamic Semantics

4

Motivation

5

Type based analysis

6

Instrumentation

7

Conclusion

Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 201431 / 33

Enforcing Information Flow Policies
Conclusion

Conclusion
Contribution
The definition of a sound type system that captures lackof information in a program at compile-time.
A multi-valued type analysis:
The program is safe: all the executions satisfy the
information flow policy
The program may be unsafe: instrumentation is needed.
The program is unsafe: rejection

leading to fewer false positives and lighter overhead
Future Work
Dynamic code.
Non-termination and concurrency.
Leverage to a real language.
Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 201432 / 33

Enforcing Information Flow Policies
ThanksThanksQuestions?

Nadia Tawbi (Université Laval)

Enforcing Information Flow Policies

Université Laval 201433 / 33