=Paper=
{{Paper
|id=Vol-1231/long15
|storemode=property
|title=Programmable enforcement framework of information flow policies
|pdfUrl=https://ceur-ws.org/Vol-1231/long15.pdf
|volume=Vol-1231
|dblpUrl=https://dblp.org/rec/conf/ictcs/NgoM14
}}
==Programmable enforcement framework of information flow policies==
https://ceur-ws.org/Vol-1231/long15.pdf
Programmable enforcement framework of
information flow policies
Minh Ngo and Fabio Massacci
University of Trento, Italy
{surname}@disi.unitn.it
Abstract. We propose a programmable framework that can be eas-
ily instantiated to enforce a large variety of information flow proper-
ties. Our framework is based on the idea of secure multi-execution in
which multiple instances of the controlled program are executed in par-
allel. The information flow property of choice can be obtained by sim-
ply implementing programs that control parallel executions. We present
the architecture of the enforcement mechanism and its instantiations
for non-interference (NI) (from Devriese and Piessens), non-deducibility
(ND) (from Sutherland) and some properties proposed by Mantel, such
as removal of inputs (RI) and deletion of inputs (DI), and demonstrate
formally soundness and precision of enforcement for these properties.
Keywords: Non-Interference, Non-Deducibility, Possibilistic Informa-
tion Flow Properties, Programming Language, Secure Multi Execution
1 Introduction
Computing systems often process data classified as sensitive, or, secret. To ensure
security, treatment of these data has to comply with designated information flow
policies that regulate whether the publicly visible behavior of a system can be
influenced by secret data.
Non-interference (NI) [7] totally prevents leakage of secrets to public channels
by requiring that the confidential information does not interfere with all events at
the public levels. With or without the confidential information, observations at
the public levels are still the same. By weakening or strengthening the definition
of NI, security researchers have proposed different information flow properties.
For example, declassification policies accept the behaviors in which some selected
secret data can be released [14]. Sutherland defines [15] non-deducibility (ND), a
stronger property than NI [6]. It assumes that an attacker knows the design of the
observed program, and has partial access to the public program interfaces, and
tries to infer the occurrence and non-occurrence of sequences of high input events.
ND prevents the attacker from deducing which confidential event sequences have
occurred or not.
Existing mechanisms for information flow policies enforcement and secure
information release are based on several techniques: e.g., type systems [13], sym-
bolic execution [2], multi-execution [5, 11], faceted values [1], etc. Yet these all
197
M.Ngo et al. Programmable enforcement framework of information flow policies
Table 1. EMs for the selected information flow policies
Components
Policy
MAP REDUCE TM /TR
Termination (in)sensitive non-interference [5] Fig. 3a Fig. 3b Fig. 3
Termination (in)sensitive non-deducibility [15] Fig. 3a Fig. 3b Fig. 7
Removal of inputs [9] Fig. 8a Fig. 3b Fig. 8
Deletion of inputs [9] Fig. 9a Fig. 3b Fig. 9
Local Executions
Local Input Queue Local Output Queue
TM
I0 π[0] O0
TR
Input Queue Output Queue
MAP Ii π[i] Oi REDUCE
ITOP π[TOP] OTOP
Fig. 1. Architecture of enforcement mechanisms
fall short in the same aspect: these approaches work only for a single informa-
tion flow policy, typically NI or NI equipped with declassification. Modification
of these mechanisms to enforce another information flow policy (for example,
ND) is not straight-forward. Moreover, no run-time enforcement mechanism is
proposed for ND.
1.1 The contribution of this paper
We propose a programmable enforcement mechanism (EM) that can be easily
configured to enforce NI, ND and other information flow policies. Configurations
of the EMs are summarized in Tab. 1. Our proposal is the first run-time EM that
covers ND. SME by Devriese and Piessens [5] is a special case. Our EM relies on
the secure multi-execution technique (SME) [5] in which multiple instances of the
controlled program are executed in parallel and their input and output behaviors
are controlled. To this construction we add two programmable components that
map each input to the multiple instances and reduce output of the instances
to a single output. We demonstrate soundness and precision of the proposed
mechanisms using the operational semantics.
The rest of the paper is organized as follows. §2 gives an overview of the
idea behind our approach and the architecture of the enforcement framework.
Selected information flow policies and implementations of their EMs are intro-
duced respectively in §3 and §4. Semantics of controlled programs and framework
is introduced in §5. The soundness and precision of the EMs constructed are pre-
sented in §6. We discuss related work and conclude in §7.
198
M.Ngo et al. Programmable enforcement framework of information flow policies
2 Overview
Fig. 1 depicts the general archi- π ::= program instructions :
tecture of the EM for an informa- |x := e assignment
tion flow property on a program |π; π sequence
π. It is composed by the MAP |if e then π else π if
and REDUCE components, a stack |while e do π while
EX of local executions (π[0], . . . , |skip skip
π[T OP ], where T OP is the index |input x from c input
of the top of the stack), global in- |output e to c output
put and output queues, and the ta- (a) Basic instructions
bles TM and TR . Instructions used πM ::=π instructions :
to compose controlled programs, |map(e, c, P RED[ ]) map
MAP, and REDUCE programs are |wake(P RED[ ]) wake
in respectively Fig. 2a, Fig. 2b, and |clone(P RED[ ], P RIVTM , P RIVTR ) clone
Fig. 2c. (b) MAP instructions
Local executions are instances πR ::=π instructions :
of the original program, are exe- |retrieve x from (i, c) retrieve
cuted in parallel and are unaware |wake(P RED[ ]) wake
of each other. They are separated |clean(c, P RED[ ]) clean
from the environment input and (c) REDUCE instructions
π, e, x, and c are meta-variables for respectively in-
output actions by the EM. The lo- structions, expressions, variables, and input/output
cal input (resp. output) queue of a channels. A (controlled, MAP, or REDUCE) program
local execution contains the input is a sequence of instructions.
(resp. output) items that can be
Fig. 2. Language instructions
freely consumed (resp. generated)
by this local execution. MAP and
REDUCE are responsible for respectively the global input queue containing the
input items from the external environment, and the global output queue con-
taining the output items filtered by the EM to the environment. When a local
execution needs an input item that is not yet ready in its local input queue it will
request the help of MAP by emitting an interrupt signal. When a local execution
generates an output item it emits a signal to request the help of REDUCE.
MAP and REDUCE can autonomously send and, respectively, collect items
from local queues. The actions of MAP (resp. REDUCE) on an input (resp. out-
put) request from a local execution depend on the configuration information
in the table TM (resp. TR ). This configuration is based on two privileges: ask
(a) and tell (t). These components of the EM are customized depending on the
desired information flow policy.
All local executions with the tell privilege on the input channel c can get
the real value from the channel c when MAP broadcasts the input item to local
executions, otherwise they will get a default value. If a local execution has the tell
privilege on the output channel c, REDUCE can tell its value to the environment.
Otherwise, REDUCE will just replace it with a default value.
If a local execution has the ask privilege on the input channel c, then MAP
can fetch the input item from the environment upon receiving a signal from a
199
M.Ngo et al. Programmable enforcement framework of information flow policies
local execution. A local execution with the ask privilege on the output channel
c can ask REDUCE to start processing outputs from the local executions.
An execution with only the ask but not the tell privilege in TR will activate
REDUCE to retrieve output items, but REDUCE will not put the value in the
external output (i.e. will not tell it to anyone). The execution will have to wait
for somebody else with the tell privilege on the channel to produce an output.
3 Information flow policies
In this section we briefly present some policies.
Non-Interference. Let (π, I) ⇓ O denote a terminating execution of π that con-
sumes input sequence I and generates output sequence O. Given a security level
l (where l is in {L, H}), I|l (resp. O|l ) returns the projection of the sequence
I (resp. O) containing only items at level l. For NI, for two arbitrary input se-
quences I and I 0 that are low-equivalent (I 0 |L = I|L ), the generated outputs O
and O0 are also low-equivalent (O0 |L = O|L ). NI comes in termination-sensitive
(TSNI) or termination-insensitive (TINI) flavors.
Definition 1 (TINI). A program π is TINI iff
∀I, I 0 : I 0 |L = I|L ∧ (π, I) ⇓ O ∧ (π, I 0 ) ⇓ O0 =⇒ O0 |L = O|L
The formal definition of TSNI can be derived from TINI by moving (π, I 0 ) ⇓
0
O after the implication.
Non-Deducibility. Sutherland defines ND by using two views: the first view cor-
responds to secret events, and the second view corresponds to observations of
attackers at the low level [15]. There are no flows from from the former to the
latter if the two views can always be combined. In this way an attacker can-
not know whether a particular high input took place, because it can be always
replaced by another valid input and still yield a valid execution.
Termination-insensitive ND (TIND) is defined in Def. 2. TIND requires that
for any two inputs I and I ∗ , such that the program terminates with these in-
puts, there exists another input I ∗∗ , which is low-equivalent with I (I|L = I ∗∗ |L ),
high-equivalent to I ∗ (I ∗ |H = I ∗∗ |H ), and if the program terminates with I ∗∗ ,
the generated output visible to attackers at the low level (L) is not changed.
Termination-sensitive ND (TSND) assumes that attackers can observe termi-
nations of executions and the existence of the default view where we replaced
input values with default values. If the default values could not be accepted by
an execution then it would be possible to deduce that the high information is
actually different from the default value.
Definition 2 ((Input-Output) TIND). A program π is TIND iff
∀I, I ∗ : (π, I) ⇓ O ∧ (π, I ∗ ) ⇓ O∗ =⇒ (∃I ∗∗ : I|L = I ∗∗ |L ∧ I ∗ |H = I ∗∗ |H ∧
∧ ((π, I ∗∗ ) ⇓ O∗∗ =⇒ O|L = O∗∗ |L ))
200
M.Ngo et al. Programmable enforcement framework of information flow policies
The formal definition of TSND can be derived from TIND by requiring that
(π, I ∗∗ ) ⇓ O∗∗ holds and the execution where all input values have been replaced
by default values is always present and terminates.
Removal of Inputs. RI [9] requires that if a possible trace is perturbed by remov-
ing all high input items, then the result can be corrected into a possible trace. In
our notation, an input (resp output) is a queue of input (resp. output) vectors
(see §5). If all high input items in an input I are replaced by default items (df~)
or removed, the input can be modified to an input I 0 such that the program
terminates when executing on I 0 and the generated output will be equivalent at
the low level with the original output. I|c returns an input I 0 whose items are
in I and from channel c.
Definition 3 (RI). A program π satisfies RI iff
∀I, ∀ values of valdef : (π, I) ⇓ O =⇒ ∃I 0 :I 0 |L = I|L ∧ ∀c, k I 0 |c k≤k I|c k ∧
~ )∗ ∧
∧ I 0 |H = (df
∧ (π, I 0 ) ⇓ O0 ∧ O0 |L = O|L
~ contains the default value, and k Q k returns the length of Q.
where df
Deletion of Inputs. DI [9] requires that if we perturb a possible trace t = β.e.α
(there is no high input event in α) by deleting the high input event e, the result
can be corrected into a possible trace t0 (t0 = β 0 .α0 ). Parts β and β 0 and α
and α0 are equivalent on the low input events and the high input events; α
and α0 are also equivalent on low output events. In our notation, if we have an
input I = I1 .~v .I2 , where ~v contains a value from a high channel (~v [c] 6= ⊥ and
LV L[c] = H) and in I2 there are either no high items or only high items with
default values (I2 |H = (df~ )∗ ), then this input can be changed by replacing ~v by
~
a default vector (df ). The obtained input can be sanitized by removing existing
default high input items in I2 or adding other default high input items to I2 .
The sanitized queue is consumed completely by the program and the output is
still low-equivalent to the original output generated with input I (O0 |L = O|L ).
Definition 4 (DI). A program π satisfies DI iff
∀I, ∀ values of valdef : I = I1 .~v .I2 ∧ LV L[c] = H ∧ I2 |H = (df ~ )∗ ∧ (π, I) ⇓ O
~ )∗ ∧ (π, I 0 ) ⇓ O0 ∧ O0 |L = O|L
=⇒ ∃I 0 : I 0 = I1 .I 0 ∧ I 0 |L = I|L ∧ I 0 |H = (df
2 2
~ contains a default value.
where ~v [c] 6= ⊥ and df
4 Implementing the policies
201
M.Ngo et al. Programmable enforcement framework of information flow policies
1: if a ∈ TM [i][c] then 1: x := valdef
2: input x from c 2: if a ∈ TR [i][c] then
3: map(x, c, canT ell(c)) 3: retrieve x from (i, c)
4: map(valdef , c, ¬canT ell(c)) 4: if t ∈ TR [i][c] then
5: wake(isReady(c)) 5: output x to c
6: else 6: clean(c, identical(i))
7: if t 6∈ TM [i][c] then 7: wake(identical(i))
8: map(valdef , c, identical(i)) (b) REDUCE for an output to c from π[i]
9: wake(identical(i))
10: else TM π[0] π[1] TR π[0] π[1]
11: skip LV L[c] = H at − LV L[c] = H at −
LV L[c] = L t at LV L[c] = L − at
(a) MAP for an input from c from π[i]
Fig. 3. Implementation of NI
Non-Interference. Implementation of NI is in Fig. 3. The EM of NI on a pro-
gram π needs only two local executions: the high execution (π[0]) and the low
execution (π[1]). When the low execution needs a high input item, MAP sends a
fake value to it. Thus, the execution of the low is independent from high input
items consumed by the EM. In addition, only the low execution can send output
items to low output channels. Put differently, high input items do not influence
consumed low inputs and generated low outputs.
When MAP is activated on signal c from π[i] having the ask privilege on c,
MAP performs an input action, sends the real value to all local copies having the
tell privilege on c, and sends a fake value to others. When MAP is activated on a
signal c from π[i] that has no privilege on c, MAP sends a fake value to π[i] and
wakes it up. Function canT ell(c) , λx.t ∈ TM [x][c] indicates whether a local
copy π[x] has the tell privilege on c. A local copy is ready to be waken up if it has
received the required input item, isReady(c) , λx.EX[x].stt = S ∧ EX[x].prg =
input y from c; π ∧ EX[x].in = I ∧ dequeue(I, c) = (val, I 0 ) ∧ val 6= ⊥, where
dequeue(I, c) = (val, I 0 ) means there is an item from c in I. Function identical()
is defined as identical(i) , λx.x = i.
When REDUCE is activated on a signal c from π[i], it checks whether π[i] has
the ask privilege on c (a ∈ TR [i][c]). If so, REDUCE gets the output value from
the local output queue of π[i]. Otherwise a fake output value is used. REDUCE
only sends an output value to c if π[i] has the tell privilege on c (t ∈ TR [i][c]).
After that, the output queue of π[i] is cleaned and π[i] is waken.
In [10] we give a full proof that SME as identified by [5] is captured by our
mechanism. In [5] soundness and precision are proved w.r.t a specific scheduler,
our proof works for any scheduler respecting the configuration.
We illustrate the execution of the EM on a sample program presented in
Fig. 4. The execution of this program requires confidential information about
salary and bonus (at lines 2 and 5). This program does not satisfy NI since the
desired salary can be sent to public channels (evil.com at line 7).
The execution of local executions of the EM is described in Fig. 5 with the
input sequence (cL1 = T) (cH1 = M )(cH2 = m) which means that the position
chosen by the applicant is “CEO”, his desired salary is M , and the bonus is m.
The high and the low copies execute instructions from line 1 to 7. The value
202
M.Ngo et al. Programmable enforcement framework of information flow policies
1 input l1 from cL1 //Get the position selected by the applicant.
2 input h1 from cH1 //Get the desired salary entered by the applicant.
3 h2 = 0
4 if l1 then //If the selected position is CEO,
5 input h2 from cH2 //Get the bonus from https://goodCompany/getBonus.
6 output h1 + h2 to cH3 //Show the income to users.
7 output h1 + h2 to cL2 //Send the income to http://evil.com/.
The script gets the desired position chosen by a prospective applicant from a public channel; and
retrieves the desired annual salary from a confidential channel. If the chosen position is CEO, the
script fetches also the annual bonus from goodCompany/getBonus, a confidential channel. Then, it
shows the desired salary and the bonus to the applicant via cH2, and sends everything to evil.com.
Fig. 4. Running Example Program
Input to MAP:
Output by REDUCE:
0 1 2
1 input l1 from cL1 //Use T asked by π[1]. 0 1 2 3 4
cL1 T ⊥ ⊥
2 input h1 from cH1 //Get M from cH1. cH3 ⊥ ⊥ ⊥ M +m ⊥
cH1 ⊥ M ⊥
3 h2 = 0; cL2 ⊥ ⊥ ⊥ ⊥ ∗
cH2 ⊥ ⊥ m
4 if l1 then Local Executions:
5 input h2 from cH2 //Get m from cH2. High execution π[0]:
6 output h1 + h2 to cH3 //Send M + m to cH3.
Local input: Local output:
7 output h1 + h2 to cL2 //The output is ignored.
cL1 T ⊥ ⊥
cH3 ⊥ ⊥ ⊥ M +m ⊥
cH1 ⊥ M ⊥
(a) The high execution π[0] cL2 ⊥ ⊥ ⊥ ⊥ •
cH2 ⊥ ⊥ m
1 input l1 from cL1 //Get T from cL1.
Low execution π[1]:
2 input h1 from cH1 //The default value is used.
Local input: Local output:
3 h2 = 0;
4 if l1 then
cL1 T ⊥ ⊥
cH3 ⊥ ⊥ ⊥ • ⊥
input h2 from cH2 //The default value is used. cH1 ⊥ ∗ ⊥
5 cL2 ⊥ ⊥ ⊥ ⊥ ∗
6 output h1 + h2 to cH3//The output is ignored. cH2 ⊥ ⊥ ∗
7 output h1+h2 to cL2 //Send ∗ to cL3.
• is an output value that is ignored. ∗ is a default
(b) The low execution π[1] value or is calculated based on default values.
Fig. 5. Executions of local copies for NI Fig. 6. Input and output queues for NI
generated by the output instruction of the high copy (resp. the low copy) at line
7 (resp. line 6) is ignored. To facilitate the presentation we present the contents
of the global and local input and output queues in Fig. 6. The global input queue
is consumed completely by the execution of the EM. The values sent to cH3 and
cL2 are respectively M + m and ∗, where ∗ denotes values calculated based
on default values. Each column in the table corresponds to an input/output
operation. Input and output tables should be read from left to right; columns
describe the input/output to each channel at time t = 0, t = 1, etc.
Non-Deducibility. The configuration of the mechanism TM π[0] π[1] π[2]
of ND requires three local copies. The low execution LV L[c] = H t at −
LV L[c] = L t − at
(π[2]) can consume only low input items and generate
low output item. The high execution (π[0]) can consume TR π[0] π[1] π[2]
real values from all channels and can send high output LV L[c] = H at − −
LV L[c] = L − − at
items to the environment. The purpose of the shadow
execution (π[1]) is to make sure that low inputs do not
determine high inputs. Indeed the shadow execution is Fig. 7. Impl. of ND
203
M.Ngo et al. Programmable enforcement framework of information flow policies
the only one that can ask for high inputs but only receives dummy low inputs.
We used the word shadow as its output are ignored (only legitimate high output
from the high is going to see the light). In other words, the low inputs and the
high inputs consumed by the EM are independent from each other.
The programs of MAP and REDUCE are the same as the ones of NI. Privileges
of the low execution are the same as those of the low execution of NI. The only
difference is that the high execution can be told but cannot ask input values and
can output its values to high output channels. The shadow execution is the only
one that can ask for high input items. Fig. 7 shows configuration of TM and TR .
Our EM is slightly stronger as it will generate the correct low output even if the
high execution might not terminate.
Removal of Inputs. The configuration of RI 1: if a ∈ TM [i][c] then
is in Fig. 8. The EM of RI is similar to the 2: input x from c
3: map(x, c, canT ell(c))
one of NI except the way of handling signals 4: map(valdef , c, ¬canT ell(c))
on high input channels from the low execution 5: wake(isReady(c))
6: else
(π[1]). To ensure the existence of I 0 as in the 7: skip
definition, MAP is allowed to ask high input (a) MAP for an input from c from π[i]
items for the low execution. To ensure that the
TM π[0] π[1]
behaviors visible to attackers do not change, LV L[c] = H at a
the low execution receives only default high LV L[c] = L t at
input items and only it can send outputs to
Fig. 8. Implementation of RI
low output channels.
The configuration table TM is similar to the one of NI except that the low
execution has the ask privilege on high input channels. The MAP program is
also similar to the one of RI except the cases of handling signals from the low
execution on high input channels. In these cases, MAP performs an input action,
sends the read value to the high, and send a default value to the low. Functions
canT ell(c), isReady(c) and identical(i) are as in the ones in NI.
Deletion of Inputs. DI is en- 1: if LV L[c] == H and i == 0 then
forced with the idea that 2: clone(identical(i), P RIVTM , P RIVTR )
3: if a ∈ TM [i][c] then
whenever the high execution 4: if t ∈ TM [i][c] then
(π[0]) requests a high input 5: input x from c
6: map(x, c, canT ell(c))
item, this execution will be 7: map(valdef , c, ¬canT ell(c))
cloned. The clones have to 8: wake(isReady(c))
9: else
reuse low input items asked 10: map(valdef , c, identical(i))
by the low execution (π[1]), 11: wake(identical(i))
12: else
will not receive real values 13: skip
from high channels and can- (a) MAP for DI for an input from c from π[i]
not send output to the envi-
TM π[0] π[1] π[i] > 1 TR π[0] π[1] π[i] > 1
ronment. As in NI, the low LV L[c] = H at − − LV L[c] = H at − −
execution can only receive LV L[c] = L t at t LV L[c] = L − at −
fake high input values.
Implementation of EM Fig. 9. Implementation of DI
of DI is presented in Fig. 9.
204
M.Ngo et al. Programmable enforcement framework of information flow policies
0 ~ 7→ m(e)]
π = input x from c I =~v .I v [c] 6= ⊥
~ π = output e to c v = ⊥[c
~
INP OUTP
∆, prg:π, mem:m, in:I ∆, prg:π, out:O
0
_ ∆, prg:skip, mem:m[x 7→ ~ v [c]], in:I _ ∆, prg:skip, out:O.~
v
Fig. 10. Semantics of input and output instructions of programs
The program of REDUCE is identical to the one in NI. The EM of DI requires
more than two local executions. Only the high execution π[0] can ask for and get
the high input items, other local executions will use default values. Each time
the high execution asks a high input item, it is cloned. In Fig. 9 the configura-
tion of the clones for input and output is presented in respectively TM and TR
in the columns with title π[i] > 1; These columns are the privilege templates for
P RIVTM and P RIVTR in clone instruction in Fig. 9a. As in NI, only the low
execution π[1] can ask for low input items and generate low output items; other
local executions will reuse the low input items retrieved by the low execution.
Functions canT ell(c), isReady(c) and identical(i) are as in the ones in NI.
5 Semantics
Semantics of controlled programs. Our model language is close to the one used
in the SME paper [5]. Valid values in this language are boolean values (T and
F) or non-negative integers. A program π is an instruction described in Fig. 2a
where π, e, x, and c are meta-variables for respectively instructions, expres-
sions, variables, and input/output channels. Since a program is just a sequence
of instructions (i.e. a complex instruction itself), we will use program and in-
struction interchangeably when referring to complex instructions. We model an
input (output) item as a vector ~v and define input (output) of program instances
as queues I, O so that ~v .I (resp. ~v .O) adds the element ~v to the queue. We use
vectors of channel to accommodate forms in which multiple fields are submitted
simultaneously but are classified differently (e.g. credit card numbers vs. user
names). Given a vector ~v and a channel c, the value of the channel is denoted by
~v [c]. To simplify the formal presentation, in the sequel w.l.o.g. we assume that
each input and output operation only affect one channel at a time. Thus, for
each vector, there is only one channel c such that ~v [c] 6= ⊥.
To define an execution configuration, we use a set of labelled pairs. A labelled
pair is composed by a label and an object and in the form label:object. The label
is attached to the object in order to differentiate this object from others, so
each label occurs only once. An (execution) configuration of a program is a set
{prg:π, mem:m, in:I, out:O}, where π is the program to be executed, m is the
memory (a function mapping variables to values), I (resp. O) is the queue of
input (resp. output) vectors. The operational semantics of the input and output
instructions of the model language is the natural one. Fig. 10 illustrates some
examples. See also [5] for similar one and [10] for detail. The conclusion part of
each semantic rule is written as ∆, Γ ⇒ ∆, Γ 0 , where ∆ denotes the elements of
205
M.Ngo et al. Programmable enforcement framework of information flow policies
the execution configuration that are unchanged upon the transition. We abuse
the notation m(.) and use it to evaluate expressions to values. When an output
command sends a value to the channel c, an output vector ~v = ⊥[c ~ 7→ val] is
inserted into the output queue, where ~v is the vector with all undefined channels,
except c that is mapped to m(e), so ~v [c0 ] = ⊥ for all c0 6= c and ~v [c] = m(e).
Semantics of the Enforcement Mechanism. A configuration of an EM is a set
{tm :TM , tS
r :TR , top:T OP, map.prg:πM , map.mem:mM , red.prg:πR , red.mem:mR , in:
I, out:O, i LECSi }, where TM and TR are configuration tables for respectively
MAP and REDUCE, T OP is the index of the top of the stack of configurations
of local executions EX, πM and mM (resp. πR and mR ) are the program to be
executed and the memory of MAP (resp. REDUCE), I and O are respectively the
input and output queues of the EM, and LECSi is the configuration of the i-th
local execution.
For the initial configuration, all local input and output queues will be empty,
all local executions will be in the executing state, and skip is the only instruction
in MAP and REDUCE programs. The EM terminates when all local executions,
MAP and REDUCE programs terminate, and the global input queue is consumed
completely.
The semantics of EM is the interleaving of concurrent atomic instructions
of the various programs so each transition rule either by a local execution, by
MAP, or by REDUCE is a step of the EM as a whole.
Local Executions. Each local execution is identified by a unique identifier i,
which is its number on stack EX. A local copy can be in one of two states: E
(Executing) or S (Sleeping). A local copy moves from E to S when it needs an
input item that is not available in its local queue or when it generates an output
item. A local copy moves from S to E when the required input item is ready or
its output item is consumed.
A configuration of i-th local copy is LECSi , {EX[i].stt : st, EX[i].int :
s, EX[i].prg : π, EX[i].mem : m, EX[i].in : I, EX[i].out : O}, where st is its state,
s is a signal, π, m, I, and O are as in configuration of controlled programs, EX
is the global stack of local execution. The initial configuration of i-th local copy
is {EX[i].stt:E, EX[i].int:⊥, EX[i].prg:π, EX[i].mem:m0 , EX[i].in:, EX[i].out:}.
A local copy terminates if there is only a skip instruction to be executed.
The semantics of assignment, composition, if, while, skip instructions is es-
sentially identical to the one of the controlled programs. The only difference is
the explicit condition that the local state must be E. When the input instruction
of π[i] is executed and the required input item is not in the local input queue
(dequeue(I, c) = (⊥, I 0 )), π[i] emits a signal c and moves to a sleep state (rule
LINP2 in Fig. 11). Otherwise, the first available item will be consumed. A signal
c is generated when the output instruction is executed (rule LOUTP in Fig. 11).
MAP. In addition to the instructions in Fig. 2a (except the output instruction),
the program πM is also composed by instructions in Fig. 2b, where P RED[ ] ,
206
M.Ngo et al. Programmable enforcement framework of information flow policies
0
EX[i].stt = E EX[i].prg:π = input x from c dequeue(I, c) = (⊥, I )
LINP2
∆, EX[i].stt:E, EX[i].int:⊥ ⇒ ∆, EX[i].stt:S, EX[i].int:c
EX[i].stt = E π = output e to c EX[i].mem = m ~ ~ 7→ m(e)]
v = ⊥[c
LOUTP
∆, EX[i].stt:E, EX[i].int:⊥, EX[i].prg:π, EX[i].out:O
⇒ ∆, EX[i].stt:S, EX[i].int:c, EX[i].prg:skip, EX[i].out:O.~
v
Fig. 11. Semantics of input and output instructions of controlled π[i]
πM = map(e,[
c, P RED[ ]) m = map.mem S = {i ∈ {0, . .[
. , T OP } : P RED[i]}
~ 7→ m(e)] 0
LECS = {EX[i].in:I} v = ⊥[c
~ LECS = {EX[i].in:I.~
v}
i∈S i∈S
MAP 0
∆, map.prg:πM , LECS ⇒ ∆, map.prg:skip, LECS
0
πR = retrieve x from (i, c) EX[i].out = O dequeue(O, c) = (val, O ) val 6= ⊥
RETR
∆, red.prg:πR , red.mem:m ⇒ ∆, red.prg:skip, red.mem:m[x 7→ val]
Fig. 12. Semantics of map and retrieve instructions of MAP and REDUCE
λx.P red(x) is a meta-variable for predicates. The evaluation of the predicate
P RED[ ] on π[i] is denoted as P RED[i].
The execution of map, wake, or clone instruction is applied simultaneously
to all local executions π[i] such that P RED[i] is true. For map, the value of
expression e (which is considered from c) is sent to the input queues of all
π[i]. The semantics of map instruction is described in Fig. 12. For wake, all
local executions π[i] are awaken and interrupt signals in their configurations are
removed. For clone, the configuration of each π[i] is cloned. The list P RIVTM
(resp. P RIVTR ) is an input (resp. output) privilege template for clones which
varies depending on the enforced property. We give an example of such templates
in §4, where the enforced property requires cloning.
The initial configuration of MAP is {map.prg:πM , map.mem:m0 }. The execu-
tion of MAP terminates if skip is the only instruction in the MAP program. MAP
is activated when the previous execution of MAP has terminated, and there is a
local execution asking for help for an input item.
REDUCE. Except the input instruction, in addition to the instructions in Fig. 2a,
the program of REDUCE may contain instructions in Fig. 2c. The execution of
retrieve instruction reads the value from the output queue of π[i] and stores it
into x. The execution of clean instruction is applied to all π[i] such that P RED[i]
is true. This instruction removes the first output item to c from O of π[i]. The
execution of the wake instruction is similar to the one of MAP. Configuration,
activation and termination of REDUCE are similar to the ones of MAP. The
semantics of retrieve instruction is shown in Fig. 12 where dequeue(O, c) returns
a first item to c in O.
207
M.Ngo et al. Programmable enforcement framework of information flow policies
6 Formal Properties
[The full versions of the similar
proofs are available in [10].] ND NI RI DI
The soundness property states
that the EM correctly en-
forces the desired policy on Prop. 3
Prop. 1 Prop. 2 Prop. 4
an arbitrary program. Our Semantics
Input of EM(π) Output of EM(π) Clones in DI
Equivalence
notion of soundness is taken
from [5, 4] and is close to the Fig. 13. Proof Strategy for Soundness
one used in [8]. It has some
known limitations (see [11] for a different definition) but we retained it because it
is widely used and understood. Soundness does not hold for EMs of termination-
sensitive properties because one local copy might terminate but the others might
not. Thus, the whole EM does not terminate.
Theorem 1 (Soundness of Enforcement). For all programs π, each EM
executed on π in Tab. 1 satisfies the corresponding policy, except for termination-
sensitive policies.
The proof strategy of soundness is sketched in Fig. 13. Prop. 1 states that
the input handling in MAP is correct w.r.t. the specification: e.g., we prove that
for NI, MAP only asks input items from the environment for high input requests
from the high execution. Prop. 2 states that the output handling by REDUCE
is correct w.r.t. to the specification: e.g., only the high execution sends items to
high output channels. Prop. 3 states that the semantics of controlled programs
and the semantics of local executions are equivalent (for I1 and I2 , which coincide
for all channels, the execution of the original program on I1 and the execution
of a local copy on I2 yield the same output queues).
To prove the soundness theorem for NI and ND we perform case-based rea-
soning showing that outputs produced by EMs satisfies the respective definitions.
This proof strategy is also used to prove the soundness theorem for RI. For DI,
we need another proposition (Prop. 4) stating that the clones do not influence
the consumed inputs and the generated outputs of the EM.
The notion of precision for enforcement of a property is taken from [5, 4].
The intuition is that the EM does not change the visible behavior of a program
that is secure with respect to the property (and in particular the I/O behaviour
on specific channels).
Definition 5. An EM is precise w.r.t a property, if for any program π satisfying
the property, and for every input I, where (π, I) ⇓ O, the actually consumed input
I ∗ and the actual output O∗ of the EM, regardless of the order of executing local
copies, are s.t. EM terminates and I ∗ |c = I|c and O∗ |c = O|c for all channels c.
Theorem 2 (Precision of Enforcement). Each EM in Tab. 1 is precise w.r.t.
the corresponding policy except for termination-insensitive policies.
208
M.Ngo et al. Programmable enforcement framework of information flow policies
Fig. 14 shows the proof strategy for
RI
precision. We prove simple properties DI
regarding the correct handling of inter- similar
similar
rupt signals (Prop. 5 and Prop. 6). We NI ND
show that from the input of the high
Prop. 2
execution we can reconstruct the origi- Output of EM(π)
nal global input (Prop. 7). The proof of Prop. 3
Semantics of controlled
the precision theorem of the EM of NI Lem. 1
programs and local executions
Lem. 2
(resp. ND) follows directly from Lem. 1 Input Input
Consumption Consumption
(resp. Lem. 2). Lem. 1 shows that if a of NI of ND
program π satisfies TSNI, terminates,
and all local executions consume input Prop. 5 Prop. 7
Prop. 6
correctly, then the consumed input of Local Input
consumption Wake of π[i]
Relationship between Global
Queue and Local Queue
the mechanism is I ∗ where I|c = I ∗ |c
for all c. The proofs of the precision the-
Fig. 14. Proof Strategy for Precision
orem of EMs of RI and DI are similar.
Precision does not hold for mechanisms of termination-insensitive properties.
For a program satisfying a termination-insensitive property, its execution on an
input might terminate, while execution on the other inputs as in the definition of
the property might not. Thus, there is a case that the high copy might terminate
but other executions might not.
7 Related Works and Conclusions
Information flow policies can be enforced by many approaches [13, 12, 3]. Our
choice of using the multi-execution approach, despite its performance overhead,
was dictated by its advantages over the static and dynamic information flow
analysis techniques. Furthermore, the multi-execution approach is also practical
as demonstrated in [4], where SME, an instance of this approach, is implemented
in FireFox. The implementation introduces a noticeable performance overhead
but not prohibitive and the implementation works with most existing web sites.
SME [5] has inspired many researchers to push further investigation of this
technique. The influence of the order of executing local copies on timing and
termination channels is investigated in [8]. Stronger notions of precision are
investigated in [11, 16]. Our current proposal does not address timing and termi-
nation channels, and does not offer the same precision guarantees. However, our
proposal can be further extended by using the techniques proposed in [8, 11, 16].
The focus of our paper is to develop a programmable framework that is capable
of handling different information flow properties.
SME-based EMs of declassification policies are proposed in [1, 11]. Our frame-
work can be instantiated to enforce stateless declassification policies like the one
in [11] where the existence of the high input items can be released. The config-
uration of this policy is similar to the one of RI except that the low does not
have the ask privilege on high input channels. To enforce stateful declassification
policies in which the physical locations of release are specified [14], one possible
209
M.Ngo et al. Programmable enforcement framework of information flow policies
approach is to introduce declassify operators as in [1, 11]. However, by doing this
we lose one advantage of SME which treats controlled programs as black boxes.
We presented a programmable framework that can enforce multiple informa-
tion flow properties via running several copies of a program. The framework is
instantiated for enforcing non-interference (NI) [5], non-deducibility (ND) [15],
removal of inputs (RI) and deletion of inputs (DI) [9]. For these properties we
formally proved soundness and precision of enforcement.
The framework uses the MAP and REDUCE components to interact with the
environment: all input and output actions are mediated by these two compo-
nents. Local executions consume different inputs (real input values or default
ones) fed by MAP, depending on their privileges in the table TM ; for each chan-
nel the outputs are fetched by REDUCE from the dedicated execution (which
has the corresponding privilege in the table TR ).
Acknowledgements This work is partly supported by the project EU-IST-
NOE-NESSOS.
References
1. T. H. Austin and C. Flanagan. Multiple facets for dynamic information flow.
SIGPLAN Not., 47(1):165–178, Jan. 2012.
2. M. Balliu, M. Dam, and G. L. Guernic. Encover: Symbolic exploration for infor-
mation flow security. In Proc. of CSF 2012, pages 30–44, 2012.
3. G. Barthe, J. M. Crespo, D. Devriese, F. Piessens, and E. Rivas. Secure multi-
execution through static program transformation. In Proc. of FMOODS/FORTE
2012, 2012.
4. W. De Groef, D. Devriese, N. Nikiforakis, and F. Piessens. Flowfox: a web browser
with flexible and precise information flow control. In Proc. of CCS 2012, 2012.
5. D. Devriese and F. Piessens. Noninterference through secure multi-execution. In
Proc. of IEEE S&P 2010, 2010.
6. R. Focardi and R. Gorrieri. A classification of security properties for process
algebras. J. of Comp. Sec., 3:5–33, 1994.
7. J. Goguen and J. Meseguer. Security policies and security models. In Proc. of
IEEE S&P’82, 1982.
8. V. Kashyap, B. Wiedermann, and B. Hardekopf. Timing- and termination-sensitive
secure information flow: Exploring a new approach. In Proc. of IEEE S&P, 2011.
9. H. Mantel. Possibilistic definitions of security - an assembly kit. In Proc. of CSFW
2000, 2000.
10. M. Ngo, F. Massacci, and O. Gadyatskaya. MAP-REDUCE runtime enforcement
of information flow policies. Availabe as ArXiv report http://arxiv.org/abs/
1305.2136. Technical Report DISI-13-019, University of Trento, 2013.
11. W. Rafnsson and A. Sabelfeld. Secure multi-execution: fine-grained,
declassification-aware, and transparent. In Proc. of CSF 2013, 2013.
12. A. Russo and A. Sabelfeld. Dynamic vs. static flow-sensitive security analysis. In
Proc. of CSF 2010, 2010.
13. A. Sabelfeld and A. Myers. Language-based information-flow security. J. on Se-
lected Areas in Comm., 21(1):5 – 19, 2003.
210
M.Ngo et al. Programmable enforcement framework of information flow policies
14. A. Sabelfeld and D. Sands. Declassification: Dimensions and principles. J. on
Comput. Secur., 17(5):517–548, Oct. 2009.
15. D. Sutherland. A model of information. In Proc. of NCSC’86, 1986.
16. D. Zanarini, M. Jaskelioff, and A. Russo. Enforcement of confidentiality for reactive
systems. In Proc. of CSF 2013, 2013.
211