Enforcing information flow by combining staticand dynamic analysis
Andrew Bedford, Josée Desharnais,Théophane G. Godonou, and Nadia Tawbi
Université Laval, Qubec, Canada{andrew.bedford.1,theophane-gloria.godonou.1}@ulaval.ca{josee.desharnais,nadia.tawbi}@ift.ulaval.ca

Abstract. This paper presents an approach to enforce information flow
policies using a multi-valued type-based analysis followed by an instrumentation when needed. The target is a core imperative language. Our
approach aims at reducing false positives generated by static analysis,
and at reducing execution overhead by instrumenting only when needed.
False positives arise in the analysis of real computing systems when some
information is missing at compile time, for example the name of a file,and consequently, its security level. The key idea of our approach is todistinguish between negative and may responses. Instead of rejecting thepossibly faulty commands, they are identified and annotated for the second step of the analysis; the positive and negative responses are treatedas is usually done. This work is a hybrid security enforcement mechanism: the maybe-secure points of the program detected by our type based
analysis are instrumented with dynamic tests. The basic type based analysis has been reported in [6], this paper presents the modification of thetype system and the newly presented instrumentation step. The noveltyof our approach is the handling of four security types, but we also treat
variables and channels in a special way. Programs interact via communication channels. Secrecy levels are associated to channels rather than tovariables whose security levels change according to the information they
store. Thus the analysis is flow-sensitive.

1

Introduction

In today’s world, we depend on information systems in many aspects of our lives.
Those systems are interconnected, rely on mobile components and are more andmore complex. Security issues in this context are a major concern, especiallywhen it comes to securing information flow. How can we be sure that a programusing a credit card number will not leak this information to an unauthorized
person? Or that one that verifies a secret password to authenticate a user will
not write it in a file with public access? Those are examples of information flow
breaches in a program that should be controlled. Secure information flow analysis
is a technique used to prevent misuse of data. This is done by restricting how
data are transmitted among variables or other entities in a program, according
to their security classes.

2

Our objective is to take advantage of the combination of static and dynamic analysis. We design a multi-valued type system to statically check noninterference for a simple imperative programming language. To the usual two
main security levels, public (or Low ) and private (or High), we add two values, Unknown and Blocked. The former was introduced in [6] and captures thepossibility that we may not know, before execution, whether some information
is public or private. Standard two-valued analysis has no choice but to be pessimistic with uncertainty and hence generate false positive alarms. If uncertainty
arises during the analysis, we tag the instruction in cause: in a second step, instrumentation at every such point together with dynamic analysis will allow us
to head to a more precise result than purely static approaches. We get reduced
false alarms, while introducing a light runtime overhead by instrumenting only
when there is a need for it. In this paper, we add a fourth security type, Blocked,
which is used to tag a public channel variable that must not receive any information, even public, because its value (the name of the channel) depends on
private information. As long as no information is sent over such a channel, theprogram is considered secure.
The program on the left of Figure 1 shows how the blocking type results in
fewer false positive alarms. The figure also exhibit our analysis of the program(which we will explain later) as well as the output given by our implementation.
The identifiers privateChannel, publicChannel, highValue and lowValue in all theexamples are predefined constants. The security types L, H, U, B represent Low,
High, Unknown and Blocked , respectively, pc is the security type of the context,
and instr = L to tell that there is no need for instrumentation. The first fourlines of the program would be rejected by other analyses, including [6], because
channel c is assigned a Low channel in the then branch, which depends on a
private condition, highValue. In our work, c is just marked as blocked (“c 7→Bchan”) when it is assigned a public channel in a private context. However,in the last line, an information of low content is sent to c, which cannot beallowed, as it would reveal information on our confidential condition highValue.
It is because of this last line that the program is rejected by our analysis: withoutit, c is just typed as B.

Input to analyzer

Inference analysis
Environmentpc
pcif = Hif highValuethen c := publicChannel
G(2) = [ instr 7→ L, c 7→ B chan]Helse c := privateChannel
G(3) = [ instr 7→ L, c 7→ H chan]H
end;
G(1) = [ instr 7→ L, c 7→ B chan]H
send lowValue to c
fail since c 7→ B chan
Output : Error (Send) : Cannot send lowValue to channel c because it is blocked.

i
2
3
4
4

Fig. 1. Analysis of a program where an implicit flow may lead to a leak of information

The goal of our security analysis is to ensure non-interference, that is, toprevent inadvertent information leaks from private channels to public channels.
More precisely, in our case, the goal is to ensure that 1) a well-typed programsatisfies non-interference, 2) a program not satisfying non-interference is rejectedEnforcing information flow by combining static and dynamic analysis

33) a program that may satisfy non-interference is detected and sent to the instrumentation step. Furthermore, we consider that programs interact with an external environment through communication channels, i.e., objects through whicha program can exchange information with users (printing screen, file, network,etc.). In contrast with the work of Volpano et al. [21], variables are not necessarily channels, they are local and hence their security type is allowed to change
throughout the program. This is similar to flow-sensitive typing approaches likethe one of Hunt and Sands, or Russo and Sabelfeld [10, 17]. Our approach distinguishes clearly communication channels, through which the program interacts
and which have a priori security levels, from variables, used locally. Therefore,
our definition of non-interference applies to communication channels: someone
observing the final information contained in communication channels cannot deduce anything about the initial content of the channels of higher security level.
We aim at protecting against two types of flows, as explained in [4]: explicit
flow occurs when the content of a variable is directly transferred to anothervariable, whereas implicit flow happens when the content assigned to a variable
depends on another variable, i.e., the guard of a conditional structure. Thus, thesecurity requirements are:– explicit flows from a variable to a channel of lower security are forbidden;– implicit flows where the guard contains a variable of higher security thanthe variables assigned are forbidden.
Our static analysis is based on the typing system of [6]; our contributions
are an improvement of the type system to allow fewer false positive, by the
introduction of the blocked type, and the instrumentation algorithm that wehave developed and implemented [3].
The rest of this paper is organized as follows. After describing in Section 2
the programming language used, we present the type system ensuring that information will not be leaked improperly in Section 3. The inference algorithm ispresented in Section 4. The instrumentation algorithm is presented in Section 5.
Section 6 is dedicated to related work. We conclude in Section 7.

2

Programming language

We illustrate our approach on a simple imperative programming language, introduced in [6], a variant of the one in [19], which was adapted to deal with thecommunication via channels.
2.1

SyntaxLet Var be a set of identifiers for variables, and C a set of communication channel
names. Throughout the paper, we use generically the following notation: variables are x ∈ Var, and there are two types of constants: n ∈ N and nch ∈ C. The
syntax is as follows:4(phrases)p ::= e | c(expressions) e ::= x | n | nch | e1 op e2(commands) c ::= skip | x := e | c1 ; c2
if e then c1 else c2 end | while e do c end |receivec x1 from x2 |receiven x1 from x2 |send x1 to x2
Values are integers (we use zero for false and nonzero for true), or channel names.
The symbol op stands for arithmetic or logic binary operators on integers andcomparison operators on channel names. Commands are mostly the standard
instructions of imperative programs.
We suppose that two programs can only communicate through channels(which can be, for example, files, network channels, keyboards, computer screens,etc.). We assume that the program has access to a pointer indicating the next
element to be read in a channel and that the send to a channel would append
an information in order for it to be read in a first-in-first-out order. When an
information is read in a channel it does not disappear, only the read pointeris updated, the observable content of a channel remains as it was before. Our
programming language is sequential; we do not claim to treat concurrency andcommunicating processes as it is treated in [15, 12]. We consider that external
processes can only read and write to public channels. The instructions related
to accessing channels deserve further explanations.
The instruction receivec x1 from x2 stands for “receive content”. It represents an instruction that reads a value from a channel with name x2 and assigns
its content to x1 . The instruction receiven x1 from x2 stands for “receivename”. Instead of getting data from the channel, we receive another channel
name, which might be used further in the program. This variable has to betreated like a channel. The instruction send x1 to x2 is used to output on achannel with name x2 the content of the variable x1 . The need for two different
receive commands is a direct consequence of our choice to distinguish variablesfrom channels. It will be clearer when we explain the typing of commands, but observe that this allows, for example, to receive a private name of channel througha public channel1 : the information can have a security level different from its
origin’s. This is not possible when variables are observable.
2.2 Semantics
The behavior of programs follows a commonly used operational semantics [6];we present a few rules in Table 1. An instruction p is executed under a memory
map µ : Var → N ∪ C. Hence the semantics specifies how configurations hp, µi
evolve, either to a value, another configuration, or a memory. Evaluation of
expressions under a memory involves no “side effects” that would change thestate of memory. In contrast, the role of commands is to be executed and change
the state. Thus we have two evaluation rules: he, µi leads to a value resulting
from the evaluation of expression e on memory µ; this transition is designated1

but not the converse, to avoid implicit flow leaks

Enforcing information flow by combining static and dynamic analysis

5he, µ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)(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

Table 1. A few rules of the structural operational semantics

by →e . Finally, hc, µi leads to a memory produced by the execution of commandc on memory µ; this transition is designated by →.
We explain the rules that manipulate channels. The instructions receivec x1
from x2 and receiven x1 from x2 are semantically evaluated similarly. Information from the channel x2 is read and assigned to the variable x1 . The distinctive
feature of the rule RECEIVE-CONTENT is that the result of evaluation is an
integer variable, while for the rule RECEIVE-NAME, the result is a channel
name. Here, we introduce a generic function read(channel) that represents theaction of getting information from a channel (eg. get a line from a file, input
from the keyboard, etc.). The content of a channel remains the same after bothkinds of receive.
The instruction send x1 to x2 updates the channel x2 with the value of thevariable x1 . This is done by the generic function update(channel, information),
which represents the action of updating the channel with some information. Notethat the content of the variable x2 , that is, the name of the channel, does notchange; hence µ stays the same. The content of the channel is updated after a
send.

3

Security type system

We now present the security type system that we use to check whether a programof the language described above, either satisfies non-interference, may satisfy it
or does not satisfy it. It is an improvement of the one introduced in [6]: we add
a security level, B, to tag a channel that should be blocked.
The security types are defined as follows:(data types) τ ::= L | U | H | B(phrase types) ρ ::= τ val | τ chan | τ cmd

6

We consider a set of four security levels SL = {L, U, H, B}. This set is extended
to a lattice (SL, v) using the following order: L v U v H v B (we use freely
the usual symbols w and A). It is with respect to this order that the supremumt and infimum u over security types are defined. We lift this order to phrase
types in the trivial way, and assume this returns ⊥ when applied to phrases ofdifferent types, e.g., H chan t H val = ⊥.
When typing a program, security types are assigned to variables, channels
and commands, hence phrase types – and to the context of execution. The meaning of types is as follows. A variable of type τ val has a content of security type
τ ; a channel of type τ chan can store information of type τ or lower (indeed, aprivate channel must have the possibility to contain or receive both private andpublic information). The security typing of commands is standard, but has aslightly different meaning: a command of type τ cmd is guaranteed to only allow
flows into channels whose security types are τ or higher. Hence, if a commandis of type L cmd then it may contain a flow to a channel of type L chan. TypeB will only be assigned to channels, to indicate that they were of type L chanbut must be blocked, to avoid an implicit flow. The context type pc represents
the type of the surrounding conditionals and helps in indicating implicit flows.
Our type system satisfies two natural properties: simple security, applying to
expressions and confinement, applying to commands [19]. Simple security saysthat an expression e of type τ val or τ chan contains only variables of level τ orlower. Simple security ensures that the type of a variable is consistent with theprinciple stated in the precedent paragraph. Confinement says that a commandc of type τ cmd executed under a context of type pc allows flows only to channelsof level τ t pc or higher, in order to avoid a flow from a channel to another oflower security (H to L for example). Those two properties are used to prove
non-interference. The complete soundness proof of this algorithm is similar tothe one presented in [7].
Our typing rules are shown in Table 2. They are the same as in [6] except
for the three rules that deal with channels. A typing judgment has the form
Γ, pc ` p : ρ, Γ 0 , where Γ and Γ 0 are typing environments, mapping variables
to a type of the form τ val or τ chan that represents their security level; pc is
the security type of the context. The program is typed with a context of typeL; according to the security types of conditions, some blocks of instructions are
typed with a higher context, as will be explained later. The typing judgment
can be read as: within an initial typing environment Γ and a security typecontext pc, the command p has type ρ, yielding a final environment Γ 0 . When thetyping environment stays unchanged, Γ 0 is omitted. Since the type of channels isconstant, there is a particular typing environment for channel constants, named
TypeOf Channel that is given before the analysis. In the rules, α stands for either
the label val or chan, depending on the context.
We use, as in [6], a special variable instr, whose type (maintained in thetyping environment map according to the typing rules) tells whether or not the
program needs instrumentation. The initial value of instr is L; if the inference
algorithm detects a need for instrumentation, its value is changed to U , H or

Enforcing information flow by combining static and dynamic analysis(CHAN S)(OP S)(SKIP S)

TypeOf Channel(nch) = τ(INT S) Γ, pc ` n : L val
Γ, pc ` nch : τ chanΓ, pc ` e1 : τ1 α,
Γ, pc ` e2 : τ2 α
Γ (x) = τ α(VAR S)Γ, pc ` e1 op e2 : (τ1 t τ2 )val
Γ, pc ` x : τ αΓ, pc ` skip : H cmd
Γ, pc ` e : τ val
Γ, pc ` x := e : (τ t pc) cmd, Γ † [x 7→ (τ t pc)val]
Γ, pc ` e : τ chan

(ASSIGN-VAL S)(ASSIGN-CHAN S)

7B
Γ, pc ` x := e : τ cmd, Γ t [ instr 7→ HLL
L (pc, τ )] † [x 7→ HLτ (pc, τ )chan]Γ (x2 ) = τ chan
(RECEIVECONTENT S) Γ, pc ` receivec x1 from x2 : (τ t pc) cmd, Γ † [x1 7→ (τ t pc)val]
Γ (x2 ) = τ chan
(RECEIVEΓ,pc`
receiven x1 from x2 : τ cmd,
NAME S)B
Γ t [ instr 7→ HLL
τ (pc, τ )] † [x1 7→ HLU tτ (pc, τ )chan]Γ (x1 ) = τ1 α
(SEND S)Γ (x2 ) = τ chan¬((τ1 t pc) = H ∧ τ = L)

τ 6= BΓ, pc ` send x1 to x2 : τ cmd, Γ t [ instr 7→ HLU
L (τ1 t pc, τ )](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 2. Typing rules

B, depending on the rule applied, most of the time depending on the type of achannel. When it is updated, the supremum operator is always involved to makesure that the need for instrumentation is recorded until the end.
We need to define three operators, two of which on typing environments:Γ †[x 7→ρ] and Γ t Γ 0 . The former is a standard update, where the image of x
is set to ρ, no matter if x is in the original domain of Γ or not. For the conditional
rule in particular, we need a union of environments where common value variables must be given, as security type, the supremum of the two types, and wherechannel variables are given type U if they differ and none of them is blocked.

8Definition 1. The supremum of two environments is given as dom(Γ t Γ 0 ) =dom(Γ ) ∪ dom(Γ 0 ), andΓ (x)if x ∈ dom(Γ ) \ dom(Γ 0 )



0
Γ (x)
if x ∈ dom(Γ 0 ) \ dom(Γ )Γ tΓ 0 (x) =U chan if Bchan 6= Γ (x) = τ chan 6= τ 0 chan = Γ 0 (x) 6= BchanΓ (x) t Γ 0 (x) otherwise.
Note that Γ t Γ 0 (x) can return ⊥ if Γ and Γ 0 are incompatible on variablex, for example if Γ (x) is a value, and Γ 0 (x) is a channel (this can only happen
if Γ and Γ 0 come from different branches of an if command).
In the three rules that modify a channel, ASSIGN-CHAN S, RECEIVENAME S et SEND S, the following operator is also used.
Definition 2. The function HL computes the security level of instr and channel
variables in thethree typing rules where a channel is modified.
 ψ if (pc, τ ) = (H, L)
U if (pc, τ ) ∈ {(U, L), (U, U ), (H, U )} where ψ, ν, pc, τ ∈ SL.
HLψ
ν (pc, τ ) =ν otherwise.
The notation HL refers to a downward flow “H to L” because this (handy andmaybe tricky) function encodes (with ψ and ν), in particular, how such a flowfrom pc to τ should be handled. When it is clear that there is a downward flow,from H to L, then HL returns type ψ. When we are considering the security typeof a channel variable, ψ is either U or B. Such a flow may not lead to a rejectionof the program, nor to an instrumentation: when a variable is blocked, there
is no need to instrument. For other flows, the analysis distinguishes between
safe flows and uncertain ones. For example, flows from U to H are secure, nomatter what the types of uncertain variables actually are at runtime (L or H).
In these cases, HLψν (pc, τ ) returns ν. However, depending on the actual type of
the U variable at runtime, a flow U to L, from U to U or from H to U may besecure or not. A conservative analysis would reject a program with such flows
but ours will tag the program as needing instrumentation and will carry on thetype analysis. Hence, in these cases, HL will return U .
In related work, there are subtyping judgements of the form ρ1 ⊆ ρ2 orρ1 ≤ ρ2 [19, 21]. For instance, given two security types τ and τ 0 , if τ ⊆ τ 0 thenany data of type τ can be treated as data of type τ 0 . Similarly, if a commandassigns contents only to variables of level H or higher then, a fortiori, it assigns
only to variables L or higher; thus we would have H cmd ⊆ L cmd. In ourwork, we integrated those requirements directly in the typing rules. Instead ofusing type coercions, we assign a fixed type to the instruction according to themore general type. For two expressions e1 and e2 of type τ1 and τ2 respectively,
e1 op e2 is typed with τ1 t τ2 . For two commands c and c0 typed τ and τ 0 , thecomposition through sequencing or conditionals is typed with τ u τ 0 .
We now comment the typing rules that are modified with respect to [6].
ASSIGN-CHAN S and RECEIVE-NAME S both modify a channel variable andthey make use of the function HLψν . The usual condition for the modification of a

Enforcing information flow by combining static and dynamic analysis

9channel would be to avoid downward flow by imposing pc v τ or, as in [6], pc  τ ;the latter is a weakening of the former, that returns false only if pc = H andτ = L. In this paper, we chose to only reject a program if an unauthorized sendis performed. If we detect an implicit flow in ASSIGN-CHAN S or RECEIVENAME S, that is, pc = H and τ = L, we rather block the assigned channel (byψ = B in HLB− ), as in the program of Figure 1; if the channel is never used, afalse positive has been avoided. If the channel is blocked, there is no need for
instrumentation, hence ψ = L in HLL− for both rules. In RECEIVE-NAME S,
we must call instrumentation when τ is U or H to prevent a downward flow fromx2 to x1 . In that case, the channel variable obtains security type U t τ because
its type is unknown: we could receive the name of a private channel on a public
one (but could not read on in). In ASSIGN-CHAN S, this type is τ , the type of
the assigned expression.
The rule for SEND S states that the typing fails in two situations where theleak of information is clear: either the channel to which x1 is sent is blocked(τ = B), or it is of type L and either the context or the variable sent has type
H ((τ1 t pc) = H). An example where τ = B was just discussed above. If thetyping does not fail, the instrumentation will be called in each case where there
is a possibility, at runtime, that τ1 t pc be H while the channel has type L;
those are the cases (τ1 t pc, τ ) ∈ {((U, L), (U, U ), (H, U )}. The “ψ branch” in thedefinition of HLψ
− is useless, as it is a case where the typing rejects the program.
The rule CONDITIONAL S requires to type the branches c1 and c2 under thetype context pc t τ0 , to prevent downward flows from the guard to the branches.
We now explain why t is defined differently on channel variables and value
variables. If Γ and Γ 0 , the environments associated to the two branches of the ifcommand, differ on a value variable, we choose to be pessimistic, and assign thesupremum of the two security types. A user who prefers to obtain fewer false positive could assign type U to this variable, and leave the final decision to dynamic
analysis. In the case of channel variables, we do not have the choice: different
unblocked channels must obtain the type U chan. The program on the left of Figure 3 illustrates why. The last line of the program would require that c be typed
as Lchan so that the program be rejected. However, since the else branch makesc a private information, a command like send c to publicChannel should also
be rejected, and hence in this case we would like that c had been typed Hchan.
Hence we must type c as U chan, justifying the definition of t. Interestingly, thisalso shows that in our setting, the uncertain typing is necessary.
We conclude this section by discussing occurrences of false positive alarms.
A rejection can only happen from the application of the rule SEND S: either thechannel to which x1 is sent is blocked, or it is of type L and the context, or thevariable sent, is of type H. According to our rules, type L can only be assigned if
it is the true type of the variable, but H can be the result of a supremum taken inrule CONDITIONAL S or LOOP S. False positive can consequently occur fromtyping an if or while command whose guard always prevent a “bad” branch tobe taken. This is unavoidable in static analysis, unless we want to instrument any
uncertainty arising from the values of guards. Nevertheless, our inference typing

10

rules prevent more false positives than previous work through the blocking ofchannels and the unknown types U .

4Inference Algorithm

The inference algorithm implements the specification given by the type system together with some refinements we adopted in order to prepare for the
instrumentation step. The refinements consist in keeping track of the commandline number and of the generated environment for this command. Although it
may seem overloading, this strategy lightens the dynamic step since it avoids
type inference computation whenever it is already done. The algorithm is implemented as the function Infer which is applied to the current typing environment,ge : Var → {L, H, U, B}, a number identifying the current command to be analyzed, the command line i, the security level of the current context, pc, andthe actual command to be analyzed, c . Along the way, Infer returns a typing
environment representing the environment valid after the execution of the command c and an integer representing the number identifying the next command
to be analyzed. Infer updates G : int → (Var → {L, H, U, B}) as a side effect;
G associates to each command number a typing environment valid after its execution. Recall that the environment associates to a specific variable instr a
security level. After the application of the inference algorithm, if the program is
not rejected and the resulting environment associates U , H or B to instr thenthe program needs instrumentation, otherwise it is safe w.r.t. non-interference.
To analyze a program P , Infer is invoked with ge = [ instr 7→ L] , i = 0,
pc = L and c = P . The inference algorithm uses a set of utility functions that
implement some operators, functions and definitions appearing in the typing system. Their meaning and their implementation are straightforward. Here is thelist of these functions. The set SecType stands for {τ v : τ ∈ {L, U, H, B}, v ∈{val, chan}}, t and ti ranges over SecType, and gi ranges over Env, lessOrEqual
implements v, inf and sup implement respectively the infimum and the supremum of two security levels. supEnv implements the supremum of two environments, as in Definition 1. infV : SecType × SecType → SecType ∪ {⊥T } returns⊥T if the two security types do not have the same nature. If the nature is
the same, then it returns a security type where the security level is the infimum of the two security types given as argument, supV : SecType × SecType →SecType ∪ {⊥T } behaves the same way as infV except that it returns a security
type where the security level is the supremum of the two security types given
as argument, incBottomEnv : Env → bool returns true if at least one variable
is associated to ⊥T in its parameter, updateEnv : Env × Var × SecType → Env
implements Γ † [x 7→ ρ], eqEnv : Env × Env → bool checks if two environments are equal. It returns true if the two environments have the same domain
and all their variables have the same security type. It returns false otherwise,
evalN : SecType → {val, chan}, extracts the nature of a security type (val orchan), evalT : SecType → {L, U, H, B}, extracts the level of a security type,
inferE : Env × Exp → SecType returns the highest security type of the variables present in the expression to which it is applied, and HL : {L, U, H, B}4 →{L, U, H, B} implements the function HL as in Definition 2.

Enforcing information flow by combining static and dynamic analysis

11

Infer: Env × int × Sec × cmd → Env × int
Infer(ge , i, pc, c) =case c ofskip : G(i) = ge
return (G(i), i + 1)
x := e :τ = evalT(inferE(ge , e))case evalN(inferE(ge , e) ) of
val: G(i) = updateEnv(ge , x, sup(pc, τ ) val)
return (G(i), i + 1)
chan: instrt = HL(L, L, pc, τ )xt = HL(B, τ, pc, τ )instrt2 = ge ( instr)
G(i) = updateEnv(updateEnv(ge , instr, sup( instrt , instrt2 )), x, xt chan)return (G(i), i + 1)
receivec x1 from x2 :
τ = evalT(ge (x2 ))G(i) = updateEnv(ge , x1 , sup(pc, τ ) val)
return (G(i), i + 1)
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)
c1 ; c2 :(g1 , j) = Infer(ge , i, pc, c1 )(g2 , k) = Infer(g1 , j, pc, c2 )return (g2 , k)if e then c1 else c2 end:t = evalT(inferE(ge , e))pcif = sup(pc, t)(g1 , j) = Infer(ge , i + 1, pcif , c1 )(g2 , k) = Infer(ge , j, pcif , c2 )if(¬incBottomEnv(supEnv(g1 , g2 ))) then G(i) = supEnv(g1 , g2 )else failreturn (G(i), k)
while e do c end:t = evalT( inferE(ge , e))pcwhile = sup(pc, t)(ge0 , j) = Infer(ge , i + 1, pcwhile , c)if (eqEnv(ge , supEnv(ge , ge0 )) and (¬incBottomEnv(supEnv(ge , ge0 ))))
then gres = supEnv(ge , ge0 )
else if (¬eqEnv(ge , supEnv(ge , ge0 )) and (¬incBottomEnv(supEnv(ge , ge0 ))))
then (gres , j) = Infer(supEnv(ge , ge0 ), i, pcwhile , while e do c end)
else failG(i) = supEnv(G(i), gres)return (gres , j)

Table 3. Inference Algorithm

The inference algorithm Infer is presented in Table 3. Some examples of its
output are presented in the following section.

12

Correctness proof To guarantee the correction of the algorithm we have to prove
its soundness and its completeness w.r.t. the type system.
Theorem 1. (Correctness of Infer algorithm) Let P be a program in our target
language, G a typing environment, and pc a security level, Infer(G, 0, pc, P ) =(G0 , j) ⇐⇒ G, pc ` P : rho, G0 , and Infer rejects P if and only if the typing
system leads to a similar conclusion.

5

Instrumentation

Our instrumentation is based on the inference algorithm. It is a new contribution w.r.t. [6]. It inserts commands in the program so that, during execution,
the program will update the security level of variables which were unknown (U )statically. Each instruction is treated with its corresponding line number and its
context security level.Instructions may be inserted to prevent unsecure executions. The instrumentation algorithm is shown in Table 4; it is given a command
cmd to instrument and the number of this command. The algorithm updates
IC : String as a side effect, which is the instrumented program; it uses thematrix of typing environments G produced by the inference algorithm, which
is a global variable. G(i) refers to the typing environment of instruction i, andhence G(i)(x) is the security type of variable x at instruction i.
Commands are inserted so that the instrumented program will keep a tableg M of the security levels of variables, picking the already known types in G.
This table is also a global variable. g M offers two advantages, it keeps track of
the most recent values of the variables. No further analysis is necessary to findwhich instruction was the last to modify the variables. It is also easier to readthe value from a table than from the matrix G. The usefulness of g M can beshown with the following example.
receiven c from publicChannel ;receivec a from publicChannel ;if (a mod 2 6= 0) thenreceivec a from c
end;
send a to publicChannel
The inference algorithm determines after the first instruction that the typeof c is U chan. Variable a, before the if command, has the type L val. The static
analysis will conclude that the type of a after executing the if command is U val.
If the instrumented program updates the variables immediately in G, the type ofa would be H val. The following send would be considered unsecure no matter
what the dynamic value of a is. Our instrumentation will insert instructions thatput in g M the last type of a when it was read. So depending on whether the
execution of the instrumented program enters the then branch or not, a will takeeither the security level of c, or it will keep the security level of publicChannel .
This will allow the instrumented program to be rejected during execution only
if it is actually unsecure.
A set of utility functions are predefined in the target language and used by
the instrumented programs. Function TypeOf Channel serves as a register for theEnforcing information flow by combining static and dynamic analysis

13

Instrument: cmd * int → int
Instrument(c, i) =case c ofskip : IC ∧ “ skip; ”
return (i + 1)
x := e :τ = evalT(inferE(G(i), e))case evalN(inferE(G(i), e)) ofval: IC = IC∧ “x := e ; ”
if (τ = U ) thenIC = IC∧“updateEnv(G(i), x, sup(evalT(TypeOf Expression(e)), top(pc))val); ”
end ;IC = IC∧ “ updateEnv(g M, x, G(i)(x)) ; ”
return (i + 1)
chan: IC = IC∧ “x := e ; ”
if (τ = U ) thenIC = IC∧“ updateEnv(G(i), x, TypeOf Channel(e)); ”
end
IC = IC∧ “ updateEnv(g M, x, G(i)(x)); ”
return (i + 1)
receivec x1 from x2 :IC = IC ∧ “receivec x1 from x2 ; ”
if (G(i)(x1 ) = U val) thenIC = IC∧ “ updateEnv(G(i), x1 , sup(evalT(TypeOf Expression(x2 )), top(pc))val) ; ”
end
IC = IC∧ “updateEnv(g M, x1 , G(i)(x1 )) ; ”
return (i + 1)
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)
c1 ; c2 :j = Instrument(c1 , i); k = Instrument(c2 , j)return ksend 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)
if e then c1 else c2 end :IC = IC∧ “push(sup(top(pc), evalT(TypeOf Expression(e))), pc) ;if e then ”
j = Instrument(c1 , i + 1)
IC = IC∧ “else ”
k = Instrument(c2 , j)
IC = IC∧ “end;pop (pc); ”
return k
while e to c end:
IC = IC∧“push(sup(top(pc), evalT(TypeOf Expression(e))), pc);
while e do ”
j = Instrument(c, i + 1)
IC = IC∧ “end ;pop (pc) ; ”
return j

Table 4. Instrumentation algorithm.

14constant channels defined prior to the execution. Function TypeOf Expression
returns the actual type of an expression: it uses the information of g M forvariables, TypeOf Channel for actual channels and takes the supV of these values when the expression is e1 op e2 . TypeOf Expression and TypeOf Channel arecommands executed by the instrumented program. To prevent implicit flows,commands are inserted so that the instrumented program will keep a stack ofcontexts pc. Each time the execution branches on an expression, whether it is in
an if or a while command, the context is pushed onto the stack. The context
is the supremum of the type of expression e and the context in which the actual command is executed. The last context is popped from the stack everytime
the execution of a branching command finishes. The stack pc is initially empty
and the result of reading an empty stack is always L. The functions push andpop are used to manipulate the stack of contexts during the execution of the
instrumented program. The remaining functions are an implementation of theircounter part in the algorithm Infer.
The analysis and the instrumentation has been implemented. The interested
reader can find a link to the implemented code in [3]. The implementation isdivided into two parts : an analyzer and an interface. The analyzer is written
in OCaml. It uses OCamllex and OCamlyacc to generate the lexer and parser.
In order to maximize the portability of our application, we use OCaml-Java tocompile our OCaml code into bytecode so that it may run on a Java Virtual
Machine. As for the interface, it is written in Java and uses the standard Swinglibrary. If an error is detected while analyzing, whether it is a lexical, syntactic,
semantic or flow error, the analyzer stops and displays a message explaining thecause of the error. If the analyzer infers that the code needs to be instrumented,
it automatically generates and displays the instrumented code. If no error occurs and there is no need for instrumentation, then a message of correctness is
displayed.
Examples A few examples of the whole approach are presented in the following
figures. The figures show the returned environment G, the returned command
number i as well as the input pc, the security level of the context. Recall thatthe identifiers privateChannel, publicChannel, highValue and lowValue are predefined constants. The result of the analysis, including instrumentation whennecessary, is shown in the lower part of the figures.
The program of Figure 2 is rejected. The security level of the value variable
x is H because its value is assigned inside the context of highValue, which isof type H. There is an attempt to send x on a public channel, which make theprogram be rejected.
Input to analyzer

Inference analysis
Environmentpc
pcif = Hif highValue
G(2) = [ instr 7→ L, x 7→ H val]Hthen x := lowValueelse skip
G(3) = [ instr 7→ L]H
end;
G(1) = [ instr 7→ L, x 7→ H val]H
send x to publicChannel
fail since H 6v L
Output : Error (Send) : Cannot send x (H) to publicChannel (L).

Fig. 2. Implicit flow

i
2
3
4
4

Enforcing information flow by combining static and dynamic analysis

15

The program in Figure 3 is similar to the one in Figure 1 except that thecontext in which c is defined is now L instead of H. For this reason, it is notnecessary to block channel c. Since c can either be a public or private channel(depending on the value of lowValue), it is marked as unknown. A call for instrumentation results from the first send, to ensure that highValue is only sent
to a private channel.
Input to analyzer

Inference analysis
Environmentpc
i
if lowValue
G(1) = [ instr 7→ L]
pcif = L 2
then c := publicChannel
G(2) = [ instr 7→ L, c 7→ L chan]L3else c := privateChannel
G(3) = [ instr 7→ L, c 7→ H chan]L4end;
G(1) = [ instr 7→ L, c 7→ U chan]L
4send highValue to cG(4) = [ instr 7→ U, c 7→ U chan]L
5
Output : push(sup(top(pc), evalT(TypeOf Expression(lowValue))), pc);
if lowValue thenc := publicChannel;
updateEnv(g M, c, G(2)(c));
else
c := privateChannel;
updateEnv(g M, c, G(3)(c));
end;pop(pc);tau = TypeOf Expression(c);tau1 = TypeOf Expression(highValue);if (((tau = Lchan) and (sup(evalT(tau1 ), top(pc)) = H)) or (tau = B chan))then fail;else send highValue to c;

Fig. 3. The send of a high value on an unknown channel calls for instrumentation

The example presented in Figure 4 shows how the instrumentation algorithm
works. The inference algorithm determines that the program needs instrumentation. The program is shown on the upper left corner of the figure. The instrumentation result is shown in the lower part of the figure. The third instruction
receives a channel name on another one. The instrumentation is necessary toobtain the real type of this channel. In the sixth instruction of the instrumented
program, the update of G(3) is due to the fact that the inference algorithm
marks the channel c as unknown on that line. The fourth instruction is a sendcommand. A check is inserted in the instrumented code to ensure that a secret
information is neither sent on a public channel (the type of c being unknown
statically) nor on a blocked one (B).
A more “realistic” example is described in [22]: one may want to “prohibit apersonal finance program from transmitting credit card information over the Internet even though the program needs Internet access to download stock market
reports. To prevent the finance program from illicitly transmitting the private
information (perhaps cleverly encoded), the compiler checks that the information flows in the program are admissible.” This could be translated into the codeof Figure 5 where all the channels, except internet, are private.

6

Related work

Securing flow information has been the focus of active research since the seventies. Dynamic techniques were the first methods as in [8]. Some of those tech-

16
Input to analyzer

pc
L
pcif = LG(3) = [ instr 7→ L, v 7→ H val, c 7→ U chan]L
G(4) = [ instr 7→ U, v 7→ H val, c 7→ U chan]L
G(5) = [ instr 7→ L, v 7→ H val]L
G(2) = [ instr 7→ U, v 7→ H val, c 7→ U chan]L
receivec v from privateChannel;
updateEnv(g M, v, G(1)(v));
push(sup(top(pc), evalT(TypeOf Expression(lowValue))), pc);
if lowValue thenreceiven c from publicChannel;
updateEnv(G(3), c, TypeOf Channel(c));
updateEnv(g M, c, G(3)(c));
tau = TypeOf Expression(c);tau1 = TypeOf Expression(v);if (((tau = L chan) and (sup(evalT(tau1 ), top(pc)) = H))or (tau = B chan))then fail;else send v to c;else skip;
end;
pop(pc);receivec v from privateChannel;
if lowV alue thenreceiven c from publicChannel;
send v to celse skipend
Output :Inference analysis
Environment
G(1) = [ instr 7→ L, v 7→ H val]

i
2
3
4
5
6
6

Fig. 4. The send of a high value on an unknown channel calls for instrumentation

Input

Outputreceivec stockMarketReports from internet;
send stockMarketReports to screen;
receivec creditCardNumber from settings;
send creditCardNumber to secureLinkToBank;
receivec latestTransactions from secureLinkToBank;
send latestTransactions to screen;
cleverlyEncodedCreditCardNumber := creditCardNumber ∗ 3 + 2121311611218191;
send cleverlyEncodedCreditCardNumber to internet
Error (Send) : Cannot send cleverlyEncodedCreditCardNumber (H) to internet (L).

Fig. 5. Example from [22]niques try to prevent explicit flows as well as implicit flows in program runs.
Those techniques are given with no soundness proof. Denning and Denning [5]introduce for the first time, secure information-flow by static analysis, based oncontrol and data flow analysis. Subsequently, many approaches have been devised using type systems. They vary in the type of language, its expressivness
and the property being enforced. Volpano and Smith in [21] introduce a typebased analysis for an imperative language. Pottier and Simonet in [16] analyse the functional language ML, with references, exceptions and polymorphism.
Banerjee and Naumann devise a type based analysis for a Java-like language.
Their analysis however has some trade-offs like low security guards for conditionals that involve recursive calls. In [14], Myers statically enforces information
policies in JFlow, an extension of Java that adds security levels annotations tovariables. Barthe et al. in [2], investigate logical-formulation of non-interference,
enabling the use of theorem proving or model-checking techniques. Nevertheless,purely static approaches are too conservative and suffer from a large numberof false positive. In fact some information need to take an accurate decision
are often only available during execution. This has cause a revival of interest

Enforcing information flow by combining static and dynamic analysis

17

for dynamic analysis. Russo and Sabelfeld in [18], prove that dynamic analyses could enforce the same security policy enforced by most static analyses,
termination-insensitive non-interference and even be more permissive ( with lessfalse-positive). This is true for flow insensitive analyses but not for flow sensitive
ones. In [17], Russo and Sabelfeld show the impossibility for a sound purely dynamic monitor to accept the same set of programs accepted by the classic flow
sensitive analysis [11] of Hunt and Sands. Russo and Sabelfeld in [17] present amonitor that uses static analysis during execution. In [9], the authors present aninteresting approach to non-interference based on abstract interpretation.
Our approach is flow sensitive, similarly to [11]. However, it distinguishes
between variables in live memory and channels. We argue that our approachlead to less false positive and to lighter executions than existing approaches.

7

Conclusion

Ensuring secure information flow within sensitive systems has been studied extensively. In general, the key idea in type-based approaches is that if a programis well typed, then it is secure according to the given security properties.
We define a sound type system that captures lack of information in a programat compile-time. Our type system is flow sensitive, variables are assigned the
security levels of their stored values. We clearly distinguish between variables
and channels through which the program communicates, which is more realistic.
Our main contribution is the handling of a multi-valued security typing. The
program is considered well typed, ill typed or uncertain. In the first case, theprogram can safely be executed, in the second case the program is rejected andneed modifications, while in the third case instrumentation is to be used in order to guarantee the satisfaction of non-interference. This approach allows toeliminate false positives due to conservative static analysis approximations andto introduce run-time overhead only when it is necessary. We obtain fewer false
positives than purely static approaches because we send some usually rejected
programs to instrumentation. Future work includes extensions to take into account concurrency, declassification and information leakage due to termination[20, 1, 13]. We would like to scale up the approach to deal with real world languages and to test it on elaborate programs. The use of abstract interpretation
to prove the correctness is also to be considered in a future work.

References
1. A. Askarov and S. Chong. Learning is change in knowledge: Knowledge-based
security for dynamic policies. In Proceedings of the 25th IEEE Computer Security
Foundations Symposium, pages 308–322, Piscataway, NJ, USA, June 2012. IEEE
Press.
2. G. Barthe, P. R. D’Argenio, and T. Rezk. Secure information flow by selfcomposition. In Proceedings of the IEEE workshop on Computer Security Foundations, 2004.
3. A. Bedford, J. Desharnais, T. G. Godonou, and N. Tawbi. Hybrid flow analysis implementation. http://lsfm.ift.ulaval.ca/Recherche/Hybrid_analysis,
2013.

18
4. D. E. Denning. A lattice model of secure information flow. Communications of theACM, 19:236–243, May 1976.
5. D. E. Denning and P. J. Denning. Certification of programs for secure information
flow. Communications of the ACM, 20:504–513, July 1977.
6. J. Desharnais, E. P. Kanyabwero, and N. Tawbi. Enforcing information flow policies
by a three-valued analysis. In Proceedings of the 6th international conference onMathematical Methods, Models and Architectures for Computer Network Security:
computer network security, MMM-ACNS’12, pages 114–129, Berlin, Heidelberg,
2012. Springer-Verlag.
7. J. Desharnais, E. P. Kanyabwero, and N. Tawbi. Enforcing information flow
policies by a three-valued analysis, long version. http://www.ift.ulaval.ca/
departement/professeurs/tawbi_nadia/, 2012.
8. J. S. Fenton. Memoryless subsystems. Comput. J., 17(2):143–147, 1974.
9. R. Giacobazzi and I. Mastroeni. Abstract non-interference: parameterizing noninterference by abstract interpretation. SIGPLAN Not., 39(1):186–197, January
2004.
10. S. Hunt and D. Sands. On flow-sensitive security types. In Conference recordof the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming
languages, POPL ’06, pages 79–90, New York, NY, USA, 2006. ACM.
11. S. Hunt and D. Sands. On flow-sensitive security types. SIGPLAN Not., 41(1):79–
90, January 2006.
12. N. Kobayashi. Type-based information flow analysis for the pi-calculus. Acta
Informatica, 42(4-5):291–347, 2005.
13. S. Moore, A. Askarov, and S. Chong. Precise enforcement of progress-sensitive
security. In Proceedings of the 19th ACM Conference on Computer and Communications Security, pages 881–893, New York, NY, USA, October 2012. ACM Press.
14. A. C. Myers. Jflow: Practical mostly-static information flow control. In Proceedingsof the ACM Symposium on Principles of Programming Languages, 1999.
15. K. R. O’Neill, M. R. Clarkson, and S. Chong. Information-flow security for interactive programs. In Proceedings of the IEEE Computer Security Foundations
Workshop, July 2006.
16. F. Pottier and V. Simonet. Information flow inference for ML. In Proceedings of
the The ACM Symposium on Principles of Programming Languages, 2002.
17. A. Russo and A. Sabelfeld. Dynamic vs. static flow-sensitive security analysis. In
Proceedings of the IEEE Computer Security Foundations Symposium, 2010.
18. A. Sabelfeld and A. Russo. From dynamic to static and back: Riding the roller
coaster of information-flow control research, 2009.
19. G. Smith. Principles of secure information flow analysis. In Malware Detection,
volume 27, pages 291–307. Springer, 2007.
20. J. Thomas, N. Cuppens-Boulahia, and F. Cuppens. Declassification policy management in dynamic information systems. In ARES 2011: 6th International Conference
on Availability, Reliability and Security, 2011.
21. D. Volpano, C. Irvine, and G. Smith. A sound type system for secure flow analysis.
Journal of Computer Security, 4(2-3):167–187, January 1996.
22. S. Zdancewic and A. C. Myers. Secure information flow via linear continuations.
Higher Order and Symbolic Computation, 15:2002, 2002.