Some notions of information flow

Jérôme Feret

Description

MPRI Some notions of information flow Jérôme Feret Laboratoire d'Informatique de l'École Normale Supérieure INRIA, ÉNS, CNRS feret January 2012

• laboratoire d'informatique de l'ecole normale


• among variables


• variable v1


• v1 ?p


• ?? ? ?


• v1 ?p

Sujets

• Okane ga nai

Informations

• Publié par: pefav
• Nombre de lectures: 26
• Langue: English

Extrait

MPRI
Some notions of information flow
Jérôme Feret
Laboratoire d’Informatique de l’École Normale Supérieure
INRIA, ÉNS, CNRS

January 2012
ferethttp://www.di.ens.fr/Syntax

LetV=fV;V;V;:::g be a finite set of variables.1 2

LetZ=fz;:::g be the set of relative numbers.
Expressions are polynomial of variablesV.
E::=zjV jE+EjEE
Programs are given by the following grammar:
P :== skip
j P;P
j V :=E
j if(V0)fPg elsefPg
j while(V0)fPg
Jérôme Feret 2 January 2012Semantics
We define the semantics JPK2(V!R)!((V!R)[
) of a programP:
JskipK()=,

if JP K()=
1
JP ;P K()=1 2
JP K(JP K()) otherwise2 1

if=

JV :=EK()=
[V!(E)] otherwise
8
>
if=
<
Jif(V0)fP g elsefP gK()= JP K() if(V)01 2 1>:
JP K() otherwise2
8
>
if=
<
0 0 Jwhile(V0)fPgK()=
iff 2 Invj(V)<0g=;
>: 0 0 0 0 if =f 2 Invj(V)<0g
00 0 0 00 0where Inv= lfp(X!fg[f j9 2X; (V)0 and 2 JPK()g).
Jérôme Feret 3 January 2012
77Flow of information
Given a programP, we say that the variableV flows into the variableV if,1 2
and only if, the final value ofV depends on the initial value pfV , which is2 1
writtenV ) V .1 P 2
More formally,
0V ) V if and only if there exists2V!R,z;z 2Z such that one of the1 P 2
following three assertions is satisfied:
01. JPK([V !z])=
, JPK([V !z])=
,1 1
0and JPK([V !z])(V )= JPK([V !z])(V );1 2 1 2
02. JPK([V !z])=
and JPK([V !z])=
;1 1
03. JPK([V !z])=
and JPK([V !z])=
.1 1
Jérôme Feret 4 January 2012
7677667776677Syntactic approximation (tentative)
LetP be a program.
We define the following binary relation! among variables inV:P
V ! V if and only if there is an assignement inP of the formV :=E such1 P 2 2
thatV occurs inE.1
DoesV) V imply thatV! V ?1 P 2 1 P 2
Jérôme Feret 5 January 2012Counter-example
We consider the following progremP:
P ::= if(V 0)1
fV :=0g2
else
fV :=1g2
For any2V!R,
we have JPK([V !0])(V )=0;1 2
but, JPK([V !1])(V )=1;1 2
soV ) V ;1 P 2
ButV9 V .1 P 2
Jérôme Feret 6 January 2012
77Syntactic approximation (tentative)
For each program pointsp inP,
we denote bytest(p) the set of variables which occurs in the guard of the test
and while loop the scope of which contains the program pointp.
We define the following binary relation! among variables inV:
V ! V if and only if there is an assignement in P of the form V :=E at1 P 2 2
program pointp such that:
1. eitherV occurs inE;1
2. orV 2 test(p).1
DoesV) V imply thatV! V ?1 P 2 1 2P
Jérôme Feret 7 January 2012Counter-example
We consider the following progremP:
P ::= while(V 0)fskipg1
For any2V!R,
we have JPK([V !-1])=
;1
but, JPK([V !0])=
;1
soV ) V ;1 P 2
ButV9 V .1 2P
Jérôme Feret 8 January 2012
776Approximation of the information flow
So as to get a sound approximation of the information flow,
we have to consider that a variable that is tested in the guard of a loop may
flow in any variable.
We define the following binary relation! among variables inV:P
V !V if and only if there is an assignement in P of the form V :=E at1 2 2
program pointp such that:
1. eitherV occurs inE;1
2. orV is tested in the guard of a loop;1
3. orV 2 test(p).1
Theorem 1 IfV) V , thenV! V ?1 P 2 1 2P
Jérôme Feret 9 January 2012Limitations
The approximation is highly syntax-oriented.
It is context-insensitive;
It is very rough in the case of while loop,
=) we could show statically that some loops always terminate to avoid
fictitious dependencies;
we could detect some invariants to avoid fictitious dependencies.
Other forms of attacks could be modeled in the semantics: an atacker could
observe:
computation time;
memory assumption;
heating.
(attacks cannot be exhaustively specified).
Jérôme Feret 10 January 2012