Programmable enforcement framework of information flow policies

Abstract

We propose a programmable framework that can be easily instantiated to enforce a large variety of information flow properties. Our framework is based on the idea of secure multi-execution in which multiple instances of the controlled program are executed in parallel. The information flow property of choice can be obtained by simply 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 Information Flow Properties
• Programming Language
• Secure Multi Execution

-

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 ], symbolic execution [ 2 ], multi-execution [ 5, 11 ], faceted values [ 1 ], etc. Yet these all fall short in the same aspect: these approaches work only for a single information 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 introduced respectively in §3 and §4. Semantics of controlled programs and framework is introduced in §5. The soundness and precision of the EMs constructed are presented in §6. We discuss related work and conclude in §7. 2

Overview

πM ::=π instructions : |map(e, c, P RED[ ]) map |wake(P RED[ ]) wake |clone(P RED[ ], P RIVTM , P RIVTR ) clone (b) MAP instructions instructions : retrieve wake clean 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 consumes 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 sequences I and I0 that are low-equivalent (I0|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, I0 : I0|L = I|L ∧ (π, I) ⇓ O ∧ (π, I0) ⇓ O0 =⇒ O0|L = O|L

The formal definition of TSNI can be derived from TINI by moving (π, I0) ⇓ O0 after the implication.

Non-Deducibility. Sutherland defines ND by using two views: the first view corresponds 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 cannot 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 inputs, 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 terminations 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))

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 removing 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 (d~f ) or removed, the input can be modified to an input I0 such that the program terminates when executing on I0 and the generated output will be equivalent at the low level with the original output. I|c returns an input I0 whose items are in I and from channel c.

Definition 3 (RI). A program π satisfies RI iff

∀I, ∀ values of valdef : (π, I) ⇓ O =⇒ ∃I0 :I0|L = I|L ∧ ∀c, k I0|c k≤k I|c k ∧ ∧ I0|H = (d~f )∗ ∧ ∧ (π, I0) ⇓ O0 ∧ O0|L = O|L where d~f contains the default value, and k Q k returns the length of Q. 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 = (d~f )∗), then this input can be changed by replacing ~v by a default vector (d~f ). 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 = (d~f )∗ ∧ (π, I) ⇓ O =⇒ ∃I0 : I0 = I1.I20 ∧ I0|L = I|L ∧ I20|H = (d~f )∗ ∧ (π, I0) ⇓ O0 ∧ O0|L = O|L where ~v[c] 6= ⊥ and d~f contains a default value. 4

Implementing the policies

1: if a ∈ TM [i][c] then 2: input x from c 3: map(x, c, canT ell(c)) 4: map(valdef , c, ¬canT ell(c)) 5: wake(isReady(c)) 6: else 7: if t 6∈ TM [i][c] then 8: map(valdef , c, identical(i)) 9: wake(identical(i)) 10: else 11: skip (a) MAP for an input from c from π[i] 1: x := valdef 2: if a ∈ TR[i][c] then 3: retrieve x from (i, c) 4: if t ∈ TR[i][c] then 5: output x to c 6: clean(c, identical(i)) 7: wake(identical(i)) (b) REDUCE for an output to c from π[i]

TM π[0] π[ 1 ] TR π[0] π[ 1 ] LV L[c] = H at − LV L[c] = H at −

LV L[c] = L t at LV L[c] = L − at Non-Interference. Implementation of NI is in Fig. 3. The EM of NI on a program π 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, I0) ∧ val 6= ⊥, where dequeue(I, c) = (val, I0) 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 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. 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 of ND requires three local copies. The low execution (π[ 2 ]) can consume only low input items and generate low output item. The high execution (π[0]) can consume real values from all channels and can send high output 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

TM LV L[c] = H LV L[c] = L π[0] π[ 1 ] π[ 2 ] t at − t at

−

TR π[0] π[ 1 ] π[ 2 ] LV L[c] = H at − LV L[c] = L at − − −

Fig. 7. Impl. of ND 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 23:: imnappu(txx,cf,rcoamnTcell(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 56:: elsweake(isReady(c)) (π[ 1 ]). To ensure the existence of I0 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 behaviors visible to attackers do not change, LV LT[cM] = H πa[0t] πa[ 1 ] the low execution receives only default high LV L[c] = L t at input items and only it can send outputs to low output channels. Fig. 8. Implementation of RI

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 enforced with the idea that whenever the high execution (π[0]) requests a high input item, this execution will be cloned. The clones have to reuse low input items asked by the low execution (π[ 1 ]), will not receive real values from high channels and cannot send output to the environment. As in NI, the low execution can only receive fake high input values.

Implementation of EM of DI is presented in Fig. 9.

1: if LV L[c] == H and i == 0 then 2: clone(identical(i), P RIVTM , P RIVTR ) 3: if a ∈ TM [i][c] then 4: if t ∈ TM [i][c] then 5: input x from c 6: map(x, c, canT ell(c)) 7: map(valdef , c, ¬canT ell(c)) 8: wake(isReady(c)) 9: else 10: map(valdef , c, identical(i)) 11: wake(identical(i)) 12: else 13: skip

(a) MAP for DI for an input from c from π[i]

TM π[0] π[ 1 ] π[i]>1 LV L[c]=H at − − LV L[c]=L t at t

TR π[0] π[ 1 ] π[i]>1 LV L[c]=H at − −

LV L[c]=L − at −

Fig. 9. Implementation of DI INP π = input x from c I = ~v.I0

Δ, prg:π, mem:m, in:I _ Δ, prg:skip, mem:m[x 7→ ~v[c]], in:I0 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 configuration 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, expressions, 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 instruction 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 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 , tr:TR, top:T OP, map.prg:πM , map.mem:mM , red.prg:πR, red.mem:mR, in: I, out:O, Si 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 essentially 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) = (⊥, I0)), π[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[ ] , LOUTP EX[i].stt = E λ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 execution 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.

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 enfaonrcaersbtihtreardyespirreodgrpaomli.cyOounr InpuPtroofpE. M1(π) OutpPurtoopf.E2M(π) ESqePumrivoaapnl.et3inccse CloPnreospi.n4DI 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 terminationsensitive 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 terminationsensitive 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 reasoning 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.

Fig. 14 shows the proof strategy for precision. We prove simple properties RI DI rreugpatrdsiignngatlshe(Pcroorpre.c5t ahnadndPlirnogp.of6)in.tWere- NIsimilar similar ND show that from the input of the high execution we can reconstruct the origi- OutpPutroopf.E2M(π) nal global input (Prop. 7). The proof of Prop. 3 (t(rrheeessppp..reNLceDism)io.fno2l)tlo.hweLosermdemi.re1cotfslhytohfwerosEmtMhLaeotmfifN.1aI ConLsIoenufmpmNu.pIt1tion proSgerammasntaincsdolofccaolnetxreoclluetdions ConLsoIenufmpmNu.Dpt2tion program π satisfies TSNI, terminates, caonrdreacltll ylo,ctahleenxetchueticoonnssucomnesduminepiuntpuotf cLoonPcsrauolmpInp.p5tiuotn WaPkreoopf. 6π[i] RelQautieouneshainPpdrobLpeot.cw7aeleQnuGeuloebal 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 termination 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 framework 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 configuration 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 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 information 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 components. Local executions consume different inputs (real input values or default ones) fed by MAP, depending on their privileges in the table TM ; for each channel 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-ISTNOE-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 information 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 multiexecution 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 Selected Areas in Comm. , 21 ( 1 ): 5 - 19 , 2003 .

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 .