A Progress-Sensitive Flow-Sensitive Inlined Information-Flow Control Monitor(Extended Version)
Andrew Bedforda,, Stephen Chongc , Josée Desharnaisa , Elisavet Kozyrib , Nadia Tawbia
a Université Laval, Québec, Canadab Cornell University, New York, USA
c Harvard University, Massachusetts, USA

Abstract
We present a novel progress-sensitive, flow-sensitive hybrid information-flow control monitor for an imperative interactive
language. Progress-sensitive information-flow control is a strong information security guarantee which ensures that a
program’s progress (or lack of) does not leak information. Flow-sensitivity means that this strong security guarantee
is enforced fairly precisely: our monitor tracks information flow per variable and per program point. We illustrate ourapproach on an imperative interactive language.
Our hybrid monitor is inlined: source programs are translated, by a type-based analysis, into a target language that
supports dynamic security levels. A key benefit of this is that the resulting monitored program is amenable to standard
optimization techniques such as partial evaluation.
One of the distinguishing features of our hybrid monitor is that it uses sets of levels to track the different possible
security types of variables. This feature allows us to distinguish programs that definitely leak information from thosethat may leak information.
Keywords: information-flow control, non-interference, inline monitor, flow-sensitive, progress-sensitive

1. Introduction
We increasingly rely on computer systems to safeguard
confidential information, and maintain the integrity of critical data and operations. But in our highly interconnectedworld, these trusted systems often need to communicate
with untrusted parties. Trusted systems risk leaking confidential information to untrusted parties, or allowing input
from untrusted parties to corrupt data or the operation of
the trusted system.
Information-flow control is a promising approach to enable trusted systems to interact with untrusted parties,
providing fine-grained application-specific control of confidential and untrusted information. Static mechanisms
for information-flow control (such as security type systems [1, 2]) analyze a program before execution to determine whether the program’s execution will satisfy theappropriate information flow requirements. This has low
runtime overhead, but can generate many false positives.
Dynamic mechanisms (e.g., [3]) accept or reject individual
executions at runtime, without performing any static program analysis. Dynamic mechanisms can incur significant
runtime overheads. More important, purely dynamic approaches cannot enforce information flow policies. These
policies are not properties as defined by Schneider in [4],hence, one cannot decide whether or not the policy is satisfied by observing a single execution. Hybrid informationflow control techniques (e.g., [5]) combine static and dyPreprint submitted to Computers & Security

namic program analysis and strive to achieve the benefits of both static and dynamic approaches: precise (i.e.,
per-execution) enforcement of security, with low runtime
overhead.
In this work, we present a novel progress-sensitive [6],flow-sensitive hybrid information-flow control monitor for
an imperative interactive language. It is an extension of
the work presented at IFIP SEC 2016 [7]. The key featuresof our monitor are as follows.
Our monitor is progress-sensitive: it prevents confidential information from being leaked via progress channels.
Information leaks through a progress channel when a program’s progress (or lack of) depends on confidential information and is observable by an adversary. It is a generalization of termination-sensitive information security tointeractive systems (i.e., systems that interact with an external environment at runtime).
Our monitor is flow-sensitive: the security level associated with program variables may change during the execution. Flow sensitivity increases precision (as the monitor
is able to accept more programs) but complicates enforcement [8].
Our language has channel-valued variables: communication channels are constants that can be assigned to program variables. This language feature allows realistic communication scenarios to be modelled in our language (e.g.,where the same code may communicate with users having
arbitrary security levels), but complicates flow-sensitive
Friday 18th November, 2016

enforcement of security. Most previous work on languagebased information-flow control require that the channel
used for an input or output operation be statically known,
and allow only a single communication channel per security level.
Our monitor is inlined: source programs are translated
into a target language that supports dynamic security levels [9]. The type-based translation inserts commands totrack the security levels of program variables and contexts,
and to control information flow. A key benefit of inlining
the monitor is that the resulting monitored program in thetarget language is amenable to standard optimization techniques such as partial evaluation [10]. The instrumented
code is thereby cleaned up so that the residual code tracks
only the security levels of variables that cannot be determined statically.
Our monitor is hybrid: it uses both dynamic and static
enforcement techniques. The translation to the target language performs a static analysis. If the program is statically determined to be insecure (i.e., it definitely contains
a leak), then the program is statically rejected. Otherwise, the translation of the program dynamically tracks
the statically unknown security levels of variables, and ensures that no leak occurs at runtime.
Our main contributions are as follows.

Explicit and implicit flows. An insecure explicit information flow occurs when a confidential value is output to a
public channel. An insecure implicit information flow [11]occurs when the decision to perform output on a publicchannel depends on confidential information. This violates
security because an observer of the public channel will see
whether the output occurred, and might thus learn confidential information. Techniques for tracking and controlling implicit and explicit information flow at the language
level are well known [1, 2, 8], and are used in this work.
The following program exhibits both explicit and implicit
information flows, and our approach will reject this program statically.
(* insecure explicit flow *)send highValue to lowChannel ;i f highValue > 0 then(* insecure implicit flow *)send 42 to lowChannel
end

Unknown security levels. Our source language supports
variables whose security level could be statically unknown.
Consider the following program, where the output may or
may not be secure, depending on the value of lowValue.
i f lowValue > 0then d := highChannele l s e d := lowChannel
end;
send highValue to d

• We present an extended version of the hybrid monitor first presented in our previous article [7]. The extension consists in generalizing the flow- and progresssensitive enforcement to general lattices. As in theconference paper, the combination of channel-valued
variables, flow-sensitivity and progress-sensitivity
presents a couple of issues that we have solved.

Listing 1: Statically uncertain channel level

Purely static mechanisms would need to reject this program entirely, and indeed, to the best of our knowledge,
all previous work either cannot express this program orreject it. This is because it would be unsound to staticallytreat d as being a private channel, since that might incorrectly allow private values to be sent to public channel
lowChannel. Similarly, it would be unsound to staticallytreat d as a public channel, since that might incorrectly
allow values read from private channel highChannel to betreated as public values. By contrast, our hybrid approach
recognizes that the security of this program depends on theruntime value of d, and instruments it to track whether drefers to a high-security channel or a low-security channel,
in order to intervene only in the latter case. We use setsof levels in our security types in order to track the different possibilities during our static analysis (e.g., d has type
{L,H} after the conditional). To push the permissivenessa little more, we treat value variables similarly as channel
variables.

• The hybrid approach is based on the distinction between a leak of information that may occur from aleak that definitely occurs. This distinction is madepossible using sets of security levels.
• We present two additional ideas to increase the precision of the static analysis and the permissivenessof the dynamic analysis: propagating constraints on
the set of possible security levels and using conditional updates.
• We prove the soundness of our inlined monitor andthat the semantics of the original program is preserved, as long as it is secure.
1.1. Examples
We present several examples of programs in our source
language, to both provide background on information-flow
control, and highlight some of the features of our hybrid
monitor. For simplicity, we assume that the variables
lowValue, highValue, lowChannel, and highChannel exist,
have arbitrary values and have the suggested value security levels denoted L, for low, a public value, and H, forhigh, a private one.

Progress channels. The progress of a program, which isobservable through its outputs, can also reveal information. For example, in the following program, whether or
not the output on the low-security channel occurs depends
on whether the preceding loop terminates, which in turndepends on confidential information.
21.2. Structure
In Section 2, we present the imperative language used
to illustrate our approach. Section 3 defines the noninterference property. Section 4 describes our typed-based
instrumentation mechanism, explains the type system, andpresents the target language in which the instrumented
programs are written; it is an extension of the source language with dynamic security levels. Section 5 proves thatthe instrumented programs are non-interferent. Section 6presents two ways to increase the precision and permissiveness of our monitor. Section 7 is a summary of related
work. Finally, we conclude in Section 8.

while highValue > 0 do
skip
end;
send 42 to lowChannel
Listing 2: Progress leak

Although this example leaks only 1 bit of information,
progress channels can be used to leak a significant amountof information [6]. The most common way to prevent leaks
through progress channels is to forbid loops whose execution depends on confidential information [12, 13], but it
leads to the rejection of many secure programs, such as
the following.

2. Source language

while highValue > 0 do
highValue := highValue - 1
end; (* loop always terminates *)send 42 to lowChannel

Source programs are written in a simple imperative
language with commands for receiving and sending information.
We suppose that the interaction of a program with its
environment (which can be a user or another program)is done through channels. Channels can be, for example, files, users, network channels, keyboards, computer
screens, etc. The security levels of these channel constants
are designated in advance by some security administrator.
This is more realistic than requiring someone to manually
define the level of every variable of the program; their levelare instead given before the analysis and the execution as
parameters. It also means that a program will not haveto be rewritten if the privacy level of a channel changes
over time: the analysis can be applied on the same program with the updated security levels for channels. The
program has to be rewritten only if a flaw is detected.

Listing 3: Loop that always terminates

To accept such programs, we follow Moore et al. [14]and use an oracle (conservative and assumed correct) todetermine the termination behavior of loops. If the oracle
determines that a loop always terminates (like the one in
Listing 3), then we know that no following output could
leak information through progress channels. On the other
hand, if the oracle says that it may diverge, then we musttake into account the fact that an output following theloop’s execution could leak information.
In our approach, the oracle is a parameter and is basedon termination analysis methods brought from the literature such as the one described in Cook et al. [15].
The inlined monitor injects another risk of leak throughprogress channels, as it can stop the execution. We treat
this risk in the same way as divergence. We do not take
into account leaks that can occur through timing channels.
Just as the one on channel variables, the permissivenesson value variables can result in a progress leak. This is
illustrated in the following example, taken from Kozyri etal. [16].

2.1. Syntax
Let V be a set of identifiers for variables, and C a setof predefined communication channels. The syntax is asfollows.
(variables)x∈
V ∪C(integer constants)n∈Z(expressions)e ::= x | n | e1 op e2 | read x(commands)
cmd ::=
skip | x := e | if e then cmd 1 else cmd 2 end |while e do cmd end | cmd 1 ; cmd 2 | send x1 to x2

i f medValue > 0then x := highValue (* x is H *)e l s e x := lowValue(* x is L *)end;(* x is {L , H } *)" guarded send " x to unknownChannel(* executed only if there is no leak *)send 1 to lowChannel

Values are integers (we use zero for false and nonzero
for true), or channel names. The symbol op stands forarithmetic or logic binary operators on integers. We write
Exp for the set of expressions.
The core language is a standard imperative language.
The expression read x returns the current value in channel
x (without modifying it). Command send x1 to x2 sends
the value of variable x1 to channel x2 and overwrites thecurrent value in the channel. In other words, it outputs
the value of x1 to channel x2 . Without loss of generality,
we consider that each channel consists of one value, it iseasy to generalize to a channel consisting in a sequence ofvalues.

Listing 4: variable level sensitivity

If the unknown channel of the first send command
happens to be of medium security level at runtime and if
the monitor does not halt the execution, then the second
send command would be reached. Then, if the output
to lowChannel occurred, it would leak information about
medValue. To prevent such a leak, we combine previous
work [7] and the dynamic mechanism of Kozyri et al. [16].

3or infinite. For finite o, hcmd , m, i ↓ o holds if there isa configuration hcmd 0 , m0 , oi such that hcmd , m, i −→∗hcmd 0 , m0 , oi. For infinite o, hcmd , m, i ↓ o holds if for
all traces o0 such that o0 is a finite prefix of o, we havehcmd , m, i ↓ o0 .

(Skip) hskip, m, oi−→hstop, m, oi
m(e) = r(Assign)hx := e, m, oi−→hstop, m[x 7→ r], oi(Send)m(x1 ) = v ∈ Z

m(x2 ) = ch ∈ C

hsend x1 to x2 , m, oi−→hstop, m[ch 7→ v], o :: (v, ch))i3. Security

hcmd 1 , m, oi−→hstop, m0 , o0 i
(Seq1)(Seq2)For our purposes, we assume a finite lattice of security
levels (L, v) which contains at least two elements: L for
the bottom of the lattice and H for the top of the lattice,i.e. ∀` ∈ L, L v ` ∧ ` v H . We define an executionas `-secure if the outputs to a channel of level ` do notreveal any information about the inputs of channels thatare not lower than or equal to `. This is a standard formof non-interference (e.g., [1, 2]) adapted for our particularlanguage model.
Before formally defining non-interference, we first introduce some helpful technical concepts. The projectionof trace o to security level `, written o  `, is its restriction
to output events whose channels’ security levels are lessthan or equal to `. Formally,

hcmd 1 ; cmd 2 , m, oi−→hcmd 2 , m0 , o0 i

hcmd 1 , m, oi−→hcmd 01 , m0 , o0 i

cmd 01 6= stop0
hcmd 1 ; cmd 2 , m, oi−→hcmd 1 ; cmd 2 , m0 , o0 i

(If)m(e) 6= 0 =⇒ i = 1

m(e) = 0 =⇒ i = 2

hif e then cmd 1 else cmd 2 end, m, oi−→hcmd i , m, oi(Loop1)m(e) 6= 0
hwhile e do cmd end, m, oi−→hcmd ; while e do cmd end, m, oi
m(e) = 0(Loop2)hwhile e do cmd end, m, oi−→hstop, m, oi` = (v, ch) :: (o  `)((v, ch) :: o)  ` =o`Figure 1: Semantics of the source language
2.2. Semantics
A memory m : V ]C → Z]C is a partial map from variables and channels to values, where the value of a channel
is the last value sent to this channel. More precisely amemory is the disjoint union of two (partial) maps of thefollowing form:
mv : V → Z ] C,

if levelOfChan(ch) v `otherwise

where levelOfChan(ch) denotes the security level of channel ch (typically specified by the administrator).
We say that two memories m and m0 are `-equivalent if
they agree on the content of variables (including channel
variables) whose security levels are ` or lower.
Definition 1 (Progress-sensitive non-interference) We saythat a program p satisfies progress-sensitive non-interference
if for any ` ∈ L, and for any two memories m and m0 thatare `-equivalent, and for any trace o such that hp, m, i ↓ o,then there is some trace o0 , such that hp, m0 , i ↓ o0 ando  ` = o0  `.

mc : C → Z,

where ] stands for the disjoint union operator. We omit
the subscript whenever the context is clear. We writem(e) = r to indicate that the evaluation of expressione under memory m returns r.
The semantics of the source language is mostly standard and is illustrated in Figure 1. Program configurations
are tuples hcmd , m, oi where cmd is the command to beevaluated, m is the current memory and o is the current
output trace. A transition between two configurations isdenoted by the −→ symbol. We write −→∗ for the reflexive transitive closure of the −→ relation.
We write v :: vs for sequences where v is the firstelement of the sequence, and vs is the rest of the sequence. We write  for the empty sequence. An output
trace is a sequence of output events: it is of the formo = (v0 , ch0 ) :: (v1 , ch1 ) :: . . . where vk ∈ Z is an integer
value, and chk is a channel, k ∈ N. The rule for sending avalue appends a new output event to the end of the trace.
We abuse notation and write o :: (v, ch) to indicate event(v, ch) appended to trace o.
We write hcmd , m, i ↓ o if execution of configuration
hcmd , m, i can produce trace o, where o may be finite

This definition of non-interference is progress-sensitivein that it assumes that an observer can distinguish an execution that will not produce any additional observable output (due to termination or divergence) from an executionthat will make progress and produce additional observable
output. Progress-insensitive definitions of non-interference
typically weaken the requirement that o  ` = o0  ` to instead require that o  ` is a prefix of o0  `, or vice versa.
Among the previously presented examples, only Listing 3 satisfies progress-sensitive non-interference. Nevertheless, we accept the program of Listing 1, since we transform it to a program that does satisfy progress-sensitive
non-interference.
4. Type-based instrumentation
We enforce non-interference by translating source programs to a target language that enables the program to4track the security levels of its variables. The translation
performs a type-based static analysis of the source program, and rejects programs that definitely leak information (i.e., the translation fails).
In this section, we first present the security types forthe source language (in order to provide intuition for the
type-directed translation) followed by the description of
the target language, which extends the source languagewith runtime representation of security levels. We thenpresent the translation from the source language to thetarget language.

Variables types associate a security level with a value
type. Intuitively, σ`0 represents the type of a variable
whose value type is σ, and whose variable type is `0 , thelatter is an upper bound of the information level influencing the value of the variable. When a variable type ` is
associated with a value type ` for a channel, it means thatthe sensitivity of the content of the channel is `0 , and thesensitivity of the channel itself is `. This approach wasused by [7]. When a variable type ` is associated with avalue type `0 for an integer, it means that the sensitivityof the integer is `0 , and the sensitivity of `0 is `0 . This approach was used in [16] to prevent leakage through guarded
sends.
Consider the program in Listing 1, page 2. Immediately following the conditional command, the type systemgives variable d the type (int {L,H} chan){L} . This typereflects that only low information determines which channel is assigned to d (i.e., variable lowValue determines d’svalue), and whether d is a low channel or a high channel
is statically unknown.
A similar situation occurs in Listing 4, page 3. Immediately following the conditional command, the typesystem gives variable x the type (int {L,H} ){M } . This typereflects that an information of medium level determines
which value is assigned to x (i.e., variable medValue determines x’s value), and that the information contained
within x is either of low security level or of high security
level. It is necessary to keep track of the context level inwhich x has been assigned its value. This information isused to halt the execution of the second send and prevent
observers from deducing that medValue is less or equal to0.
We instrument source programs to track at runtime
the security levels that are statically unknown. In order
to track these security levels, our target language allows
their runtime representation.

4.1. Source language types
Source language types are defined according to the following grammar. The security types are defined as follows:(security labels, Lab)(value types, ValT )(variable types, VarT )` ::= P(L) \ {∅}σ ::= int ` | int ` chan
τ ::= σ`Security labels are non-empty sets of security levels. They
represent the possible security levels of a variable at runtime. If a security label contains more than one element,
it means that its security level is statically unknown. For
example, variable x of Listing 5 would be labeled {L, H}
after the if command as it could contain information ofeither level at runtime.
i f lowValue thenx := read lowChannelelse
x := read highChannel
end;
send x to lowChannel
Listing 5: Variable of an uncertain level

We derive two order relations that allow us to deal withthe sets of possible levels.

4.2. Sets of levels
We use sets of levels not only to increase the precision of the analysis, but also because we have to due toour use of channel variables. Indeed, one of the issues
that we encountered is the fact that we cannot conservatively approximate the level of a channel variable, due toBell-Lapadula’s principle of no write down, no read up.
Listing 6 illustrates why.

Definition 2 The relations vs , surely less than, and vm ,maybe less than, are defined as follows`1 vs `2∀e1 ∈ `1 , e2 ∈ `2 .e1 v e2 .

`1 vm `2∃e1 ∈ `1 , e2 ∈ `2 .e1 v e2 .

Intuitively, we have ` vs `0 when we can be sure statically that ` v `0 will be true at runtime, and we have
` vm `0 when it is possible that ` v `0 at runtime.

i f lowValue > 0 thend := lowChannelelse
d := highChannel
end
send highValue to d (* Pessimist : d is L *)x := read d (* Pessimist : d is H *)send x to lowChannel

Definition 3 The supremum and infimum on sets of levels
are defined as follows`1 t `2 = {e1 ∈ `1 , e2 ∈ `2 .e1 t e2 }`1 u `2 = {e1 ∈ `1 , e2 ∈ `2 .e1 u e2 }Value types are the types of integers and channels.
Type int ` is the type of integers whose values are of security level `, and type int ` chan is the type of a channel
whose values are of security level `.

Listing 6: We cannot be pessimistic about channel variables

After the conditionals, d has type (int {L,H} chan){L} because it contains either a low or high channel and its value
5

Furthermore we assume that Vlevel contains variables_pc and _hc, and two level variables xval and xctx associated with each variable x ∈ V \ Vlevel . They are used to
track the security levels of variables at runtime. For example, if x is a channel variable of security type (int ` chan)`0 ,then the values of these variables should be xval = ` andxctx = `0 (this will be ensured by our instrumentation).
Variables _pc and _hc hold the security levels of the context and halting context respectively, they represent the
security level in which a command is executed.
The simultaneous assignment (x1 , . . . , xn ) := (e1 , . . . , en )is introduced for the sake of clarity. Any assignment implies an immediate update of the concerned level variables.
For all common commands, the semantics of the target
language is the same as in the source language.

is assigned in a context of level L. Our typing system accepts this program, but makes sure that a runtime checkis inserted. If the condition lowValue > 0 happens to betrue at runtime, then there is no leak. If it is false, theprogram will be rejected, thanks to the inserted runtime
check controlling the send command. The uncertainty is
unavoidable in the presence of flow sensitivity and channel
variables. Indeed, we point out that we cannot be pessimistic about the level of d in this program. The output
command suggests that a safe approximation for d would
be a low security level. Yet, the input command suggeststhat a safe approximation for d would be a high security
level, which contradicts the previous observation.
Consequently, in order to accept the program in Listing 6, we chose to use sets of security levels. As a consequence, we will obtain fewer false positives as we do notconsider the worst possible case in our analysis, we leaveit to the execution to check whether the information flow
turns out to be secure or not.

4.4. Instrumentation as a type system
Our instrumentation algorithm is specified as a typesystem in Figure 2. Its goal is to inline monitor actionsin the program under analysis, thereby generating a safe
version of it, or to reject it when it contains obvious leaksof information. The inlined actions are essentially updatesof level variables and checks on these variables in order
to control the execution of potentially leaking send commands. After a check, a send command is either executed
if it is safe or its execution is prevented and the programis aborted.
The typing rules of variables and constants have judgements of the form Γ ` e : σ` , stating that σ` is the type ofe under the typing environment Γ. The instrumentation
judgements are of the form

4.3. Syntax and semantics of target language
Our target language is inspired by the work of Zheng
and Myers [9], which introduced a language with first-classsecurity levels, and a type system that soundly enforces
non-interference in this language. The syntax of our target language is defined as follows. The main differencewith the source language is that it adds support for levelvariables (regrouped in the set Vlevel ), a runtime representation of security levels.
(variables)x(level variables)x̃(integer constants)n(basic levels)k(level expressions)`(integer expressions) exp

∈
∈
∈
∈
::=
::=

V ∪C
VlevelZLk | x̃ | `1 t `2
x | n | exp1 op exp2 |read xexp | `

Γ, pc, hc ` cmd : t, h, Γ0 , [[cmd ]]where Γ, Γ0 : V ] C → VarT are typing environments (initially empty), cmd is the command under analysis, pc isthe program context, hc is the halting context, t is thetermination type of cmd , h is the updated halting context, and [[cmd ]] is the instrumented command. The latter
is often presented using a macro whose name starts withgen. The program context, pc, is used to keep track of the
security level in which a command is executed, in orderto detect implicit flows. The halting context, hc, is used
to detect progress channels leaks. It represents the levelof information that could have caused the program to halt(due to a failed guarded send command) or diverge (dueto an infinite loop). In other words, it is the level of information that could be leaked through progress channels byan output. The termination t of a command is propagatedin order to keep the halting context up to date. We distinguish three termination types T = {T, D, M` }, where
T means that a command terminates for all memories, D,diverges for all memories, M` means that a command’s
termination is unknown statically; the subscript is used toindicate on which level(s) the termination depends. For
example, the termination of the loop in Listing 2 is M{H}because it can either terminate or diverge at runtime, and(expressions)e ::=(commands)
cmd ::=
skip | (x1 , . . . , xn ) := (e1 , . . . , en ) |if e then cmd 1 else cmd 2 end | cmd 1 ; cmd 2 |while e do cmd end | send x1 to x2 |if `1 v `2 then (send x1 to x2 ) else fail end

Dynamic types will allow a verification of types at runtime: this is the goal of the new send command, nested
in a conditional – call it a guarded send – that permits tocheck some conditions on security levels before sending agiven variable to a channel. If the check fails, the program
aborts.
For simplicity, we assume that security levels can be
stored only in a restricted set of variables Vlevel ⊆ V. Thus,
the variable part mv of a memory m now has the following
type
mv : (Vlevel → L) ] (V \ Vlevel → Z ] C)

6

(S-Chan)(S-Var)(S-read)levelOfChan(nch) = `Γ ` nch : (int {`} chan){L}Γ(x) = τΓ`x:τΓ ` c : int ` chan `cΓ ` read c : (int ` )`c(S-Int) Γ ` n : (int {L} ){L}

(S-Op)Γ ` e1 : (int `1 )`01Γ ` e2 : (int `2 )`02

(S-Skip)Γ ` e1 op e2 : (int `1 t`2 )`01 t`02
(S-Assign)(S-Send)Γ, pc, hc ` skip : T, hc, Γ, skipΓ ` e : σ`0e
Γ, pc, hc ` x := e : T, hc, Γ[x 7→ σpct`0e ], genassign

Γ(x) = (int `x )`0x
Γ(c) = (int `c chan)`0c(pc t hc t `x t `0x t `0c ) vs `c
Γ, pc, hc ` send x to c : T, hc, Γ, send x to cΓ(x) = (int `x )`0x
Γ(c) = (int `c chan)`0c(pc t hc t `x t `0x t `0c ) 6vs `c(pc t hc t `x t `0x t `0c ) vm `c(S-GSend)
Γ, pc, hc ` send x to c : T, pc t hc t `0x t `0c , Γ, gengsend

h=0Γ
pc 0 = pc t `e t `0e
hd = hasGSend({cmd 1 , cmd 2 }, pc0 )[` e : (int `e )`e0(hj t hd t level (t1 ⊕pc 0 t2 ))Γ, pc , hc ` cmd j : tj , hj , Γj , [[cmd j ]] j ∈ {1, 2}

j∈{1,2}(S-If)

Γ, pc, hc ` if e then cmd 1 else cmd 2 end : t1 ⊕pc 0 t2 , h, Γ1 tpc 0 Γ2 , genifΓ = Γ tpc 0 Γ0
Γ ` e : (int `e )`0e
O(e, cmd , Γ) = topc 0 = pc ∪ (pc t `e t `0e )000hc = hc ∪ (hc t level (t ) t h )hd = hasGSend({cmd }, pc )Γ, pc 0 , hc 0 ` cmd : t0 , h0 , Γ0 , [[cmd ]](S-Loop1)
Γ, pc, hc ` while e do cmd end : to , hd t h0 t level (to ), Γ tpc 0 Γ0 , genwhile0Γ 6= Γ tpc 0 Γ0
Γ ` e : (int `e )`0e
Γ, pc t `e t `0e , hc ` cmd : t0 , h0 , Γ0
pc 0 = pc ∪ (pc t `e t `0e )
0
0
0
0
0
0
hc = hc ∪ (hc t level (t ) t h )Γ , pc , hc ` while e do cmd end : to , h00 , Γ00 , instCode(S-Loop2)
Γ, pc, hc ` while e do cmd end : t00 , h00 , Γ00 , instCodeΓ, pc, hc ` cmd 1 : D, h, Γ1 , [[cmd 1 ]](S-Seq1)
Γ, pc, hc ` cmd 1 ; cmd 2 : D, h, Γ1 , [[cmd 1 ]]t1 6= DΓ, pc, hc ` cmd 1 : t1 , h1 , Γ1 , [[cmd 1 ]]
Γ1 , pc, h1 ` cmd 2 : t2 , h2 , Γ2 , [[cmd 2 ]](S-Seq2)
Γ, pc, hc ` cmd 1 ; cmd 2 : t1 o9 t2 , h2 , Γ2 , [[cmd 1 ]]; [[cmd 2 ]]Figure 2: Instrumentation and typing rules for the source language7

this depends on information of level H. The loop in Listing 3 on the other hand is of termination type T because,
no matter what the value of h is, it will always eventuallyterminate. Similarly, a loop whose condition is always true
will have termination type D since it always diverges. Recall that, of course, the precision of this analysis depends
on the precision of the oracle.
The instrumentation of a program p begins by inserting
commands to initialize a few level variables: _pc, _hc are
initialized to L, as well as the level variables xctx and xval
for each variable x ∈ V appearing in p. Similarly, levelvariables cctx and cval associated with each channel c usedin p are also initialized, but the latter rather gets initialized
to levelOfChan(c), which is an input parameter for the
analysis. After the initialization, the instrumentation is
given by the rules of Figure 2. We now explain these rules.
Rules (S-Chan) and (S-Int) specify the type of channel and integer constants respectively.
Rule (S-Var) infers the type of a variable from theenvironment Γ.
Rule (S-Op) infers the type of an expression from thetypes of its operands and it reflects the fact that operations
on channels are not allowed.
Rule (S-Read) returns the security type of the current
value in channel c.
Rule (S-Assign) updates the type of x in the environment as the supremum of the type of e (to prevent explicit
flows) and the type of pc (to prevent implicit flows). Its
instrumentation is given by the following macro, which
represents a simultaneous assignment x := e, xval := eval ,and xctx := ectx t _pc.
genassign =(x, xval , xctx ) := (e, eval , ectx t _pc)

a guarded send at runtime, and hence, it is updated withthe level of information that influences its success/failure.
Particularly, the halting context is updated with the sensitivity of the context and of the two variables involved,
the channel variable [7] and the regular variable [16]. For
example, Listing 7 shows why cctx must be included in thisupdate.
i f unknownValue > 0 (* H at runtime *)then c := lowChannele l s e c := highChannel
end;
send highValue to c (* guarded send *)send lowValue to lowChannel
Listing 7: Dangerous runtime halting

Assume that unknownValue is high and false at runtime.
Then the first guarded send is accepted, but allowing an
output on a low security channel subsequently would leakinformation about unknownValue. This is because, had
unknownValue been true, then the first send would havefailed. However, c has level int {L,H} chan {H} after theconditional. Updating _hc with cctx will affect the checkof all subsequent guarded send and prevent such leaks.
If none of the send rules can be applied, it means thatthe program under analysis contains a send command thatalways leaks information and so, the program is rejected.
Before explaining the rules for composed commands,
we first define a few functions and operators. For the conditional rules, we need a supremum of environments.
Definition 4 The supremum of two environments is given
as dom(Γ1 tpc Γ2 ) = dom(Γ1 ) ∪ dom(Γ2 ), and(Γ1 tpc Γ2 )(x) =Γi (x)
if x ∈ dom(Γi )\dom(Γj ),
{i,j}={1,2} ∨ Γ1 (x) = Γ2 (x)
0 ∪`0 )tpc if Γ1 (x) = (int` chan)`0
(int
chan)

`
∪`
(`
1
2
1
1
1
2



∧Γ2 (x) = (int`2 chan)`02∧Γ1 (x) 6= Γ2 (x)
0 ∪`0 )tpc
(int)
if Γ1 (x) = (int `1 )`01 ∧

`
∪`
(`
1
2

1
2


Γ2 (x) = (int `2 )`02 ∧





Γ1 (x) 6= Γ2 (x)


Error
otherwise.

We write ectx to represent the expression made of thesupremum of variables appearing in expression e. For example if e = x + read c, then ectx = xctx t cctx . If e = x + ythen ectx = xctx t yctx . The idea is the same for eval .
Rule (S-Send) checks whether a send command is statically safe by requiring (pc t hc t `x t `0x t `0c ) vs `c (i.e.,
all possible values of the left-hand side are always lower or
equal to the right-hand side). The variables on the lefthand side correspond to the level of information that canbe revealed by the output to c. If so, the instrumentation
inserts the send command as it is.
Rule (S-GSend) checks whether a send command may
be safe, by requiring (pc t hc t `x t `0x t `0c ) vm `c . The
instrumentation then transforms it into a guarded send, as
follows
gengsend =When a typing inconsistency occurs, e.g., when a variable is used as an integer in one branch and as a channel
in another, the analysis stops and an error is returned,
causing the program to be rejected.
The function level : T → P(L) \ {∅} returns the termination level (i.e., the level that the termination dependson) and is defined as:
{L} if t ∈ {T, D}
level (t) =`if t = M`i f _pc t _hc t xval t xctx t cctx v cval then(send x to c)
else
fail
end;
_hc := _pc t _hc t xctx t cctx ;Two operators are used to compose terminations types,⊕, used in the typing of conditionals, and o9, used in thetyping of sequences. They are defined as follows.

The halting context must record the possible failure of8

by the if is the join of those two, defined in Definition 4,
so that it contains the possibilities of both branches. Similarly, variable h is used to calculate the possible values
that the halting context may have after the conditional,
hence the union.
Its instrumentation is given by the following macro:
if t1 = t2 ∈ {T, D} t1
Mpct(`1 ∪`2 ) otherwise,t1 ⊕pc t2 =

`1 = level (t1 ), `2 = level (t2 )M`1 t`2 if t1 = M`1 and t2 = M`2ot1 9 t2 = ti
if tj = T, {i, j} = {1, 2}Dotherwise

genif =

The following example illustrates the use of these operators:
i f highValue thenwhile 1 do skip end (* D *)elseskip (* T *)end_oldpcν := _pc;
i f e then_pc:=_pc t eval t ectx ;[[cmd 1 ]];update(mv2 )
else_pc:=_pc t eval t ectx ;[[cmd 2 ]];update(mv1 )end;_pc := _oldpc

where update is defined as follows
update(mv) =if mv = ∅ skip;
else
for each x ∈ mv xctx := xctx t _pc;
if _hc ∈ mv _hc := _hc t _pc;

The termination type of an if command is computed using
the ⊕ operator, from three parameters: the termination
types of each of the two branches and the security levelof the guard condition. Hence, in this example, we obtain
D ⊕H T = M{H} .
One more function needs to be defined. Its motivation
is given by the following example. Assume that in Listing 8
unknownChannel turns out to be a low channel at runtime.
If the last send command is reached and executed it would
leak information about highValue. The same leak would
happen if instead of the guarded send we had a diverging
loop.

and where tj is the termination type of cmd j , mvj is theset of modified variables in cmd j (we include _hc in thisset if the termination of the two branches can differ i.e. if¬(t1 = t2 ∈ {T, D}) or if at least one guarded send occurs
in the other branch), and eval tectx is the guard condition’slevel expression.
The instrumented code starts by saving the current
context to _oldpcν (the symbol ν indicates that it is a
fresh variable). The program context is updated with thesecurity level of the guard condition. The if itself is thengenerated.
The function update generates the command skip; if theparameter set mv is empty otherwise it generates updatesof the context level of each modified variable in the otherbranch as well as the update of _hc if necessary. The
underlying reason is to ensure that the value of these levelvariables is at least pc.
In a situation like the following listing, this function
allows to update x’s level, to protect unknownValue.

i f highValue > 0 theni f ` v `0then send highValue to unknownChannele l s e f a i l end;
end;
send lowValue to lowChannel
Listing 8: A guarded send can generate a progress leak

To prevent this kind of leak, we verify if the branchesof a conditional contains guarded send commands using
the function

x := 0;i f unknownValue then (* H at runtime *)x := 1e l s e skip end;
send x to lowChannel

hasGSend : P(Cmd) × Lab → Lab,
where Cmd is the set of commands and Lab the set of
security labels. If one of the commands given in parametercontains a guarded send, then it returns the security label
given in parameter, otherwise L is returned. This function
is used to update the halting context to pc when there is arisk that one of the branch halts the execution. Without
this update, hc could leak information about the condition
in a subsequent send.
(S-If) When typing an if command, we type the two
branches under pc0 , which is the supremum of the conditional’s guard expression and current context. The resulting typing environments, Γ1 and Γ2 , then contain the
security levels that variables may have after executing thefirst or second branch. The typing environment returned

Listing 9: Modified variables

Here, even if the else branch is taken at runtime, the levelof variable x must be updated. Otherwise, information
about unknownValue would be revealed by the send command (even with a guarded send).
(S-Loop1), (S-Loop2) rules specify the while command typing. They involve computing a fixed point toderive the right typing environment. This is necessary
because of the flow sensitivity feature. Typing rule (SLoop2) is applied recursively until a fixpoint is found,at which point (S-Loop1) is applied and its result is returned. The union operator is used to update the pc 0 and
9hc 0 variables so that we keep track of all their possible values. Due to our use of finite lattices, and the monotonicityof the union and supremum on levels, it is easy to showthat this computation converges, the proof is given in Appendix B, Lemma 7. The typing relies on O, an oracle
that returns the termination type of the loop (to ). It is
worth noting that the call to the oracle is performed statically. Calling it dynamically would enhance precision, but
increase significantly the overhead. If the loop contains
guarded send commands, which could fail and reveal information about the condition of the loop, then we update
the halting context to prevent this leak. The presence ofat least one guarded send command is detected using thefunction hasGSend().
genwhile = _oldpcν := _pc;
while e do
_pc := _pc t eval t ectx ;[[cmd ]];

The first two conditions ensure that level variables exist
in the domain of the memory, whereas the last ones makes
sure that it is compliant with the security policy for channels.
The definition of `-equivalent memories, which is basedon [16], must handle level variables. Whenever the levelvariable xctx corresponding to a variable x is such thatm(xctx ) v ` in one memory, then it must have the samevalue in both memories, otherwise a leak can happen.
Definition 5 `-equivalent memories. We say that twocomplete memories of the target language m1 and m2 are`-equivalent, written m1 ≡` m2 , iff they satisfy the following properties
1. if mi (_pc) v ` for some i ∈ {1, 2}, then m1 (_pc) =m2 (_pc). The same property holds for _hc.
2. x ∈ m−1
i,v (Z ∪ C), ∧ mi (xctx ) v `, for some i = 1, 2,
then

end;
_pc := _pc t eval t ectx ;update(mv);_pc := _oldpc• m1 (xctx ) = m2 (xctx )The inserted commands are similar to those of the if command. The level variables and halting context are updated
after the loop in case an execution does not enter the loop.
The context needs to be updated at the begining of each
iteration as the value, and hence level, of expression e may
change.
(S-Seq1) is applied if cmd 1 always diverges; we thenignore cmd 2 , as it will never be executed. Otherwise, (SSeq2) is applied. The halting context returned is h2 instead of h1 t h2 because h2 already takes into account h1 .
Examples of instrumented programs are available inAppendix A.

• m1 (xval ) = m2 (xval )• if m1 (xval ) v ` then m1 (x) = m2 (x)3. c ∈ C ∧ levelOfChan(c) v ` ⇒ m1c (c) = m2c (c)It may seem surprinsing that the memories may differ
on a level variable such as xval ; this is because they may
differ on the value of high variables. Too see this, here isa variation of Listing 1.
i f highValue > 0then d := highChannele l s e d := lowChannelend;

5. Soundness

Listing 10: The security type of d’s content is sensible

In order to prove that the instrumented program generated by Figure 2 correctly enforces non-interference, weneed to adapt the definitions of non-interference and `equivalent memories to our target language, because oflevel variables. Recall that a memory for the target language is the union of two maps of the following form:

In this example, the content of d depends on a private
condition, and hence its level variable dctx should be H;
moreover, variable dval , containing the level of the content
of d, may have different values in two `-equivalent memories. Another example, for non-channel variables, is Listing 4, reproduced below (and taken from Kozyri et al. [16]),
where medValue has security level M , with L v M v H.

mv : (Vlevel → L) ] (V \ Vlevel → Z ] C),i f medValue > 0then x := highValue (* x is H *)e l s e x := lowValue(* x is L *)end;(* x is {L , H } *)send x to unknownChannel
send 1 to lowChannel

mc : C → Z.
We write doml (m) := dom(mv ) ∩ Vlevel = m−1
v (L). A
memory m is called complete for a program p if
• {xval , xctx } ⊆ doml (m) for any x ∈ C∪dom(m)\Vlevelthat appears in p.

In this example, variable xval contains information of level
M . If unknownChannel turns out to be of level M at execution then reaching or not the last send command will depend on xval . The program will be blocked or not, and thiswill reveal which branch was taken in the preceding conditional. Interestingly, this problem does not arise when thelattice is restricted to only two levels, {L, H}, as arguedin Kozyri et al.

• _pc and _hc are in doml (m)• if c ∈ C appears in p, then mv (cval ) = levelOfChan(c)and mv (cctx ) = L• if m(x) ∈ C then mv (xval ) = levelOfChan(m(x)).

10Here is the definition of non-interference for the target language. The difference from Definition 1 is the requirement of the memories to be complete and the use of
Definition 5.

x := read c ; (* so x is { H } *)send x to lowChannel (* always leaks , so
statically rejected *)Listing 12: Constraint on the security type of a channel variable

Definition 6 Progress-sensitive non-interference. We saythat a program p satisfies progress-sensitive non-interference
if for any ` ∈ L, and for any two complete memories m
and m0 that are `-equivalent, and for any trace o suchthat hp, m, i ↓ o, then there is some trace o0 , such that
hp, m0 , i ↓ o0 and o  ` = o0  `.
Using these updated definitions, we prove that the instrumented programs are non interferent.
Theorem 1 (Soundness of enforcement) If a program p iswell typed according to the type system of Figure 2, thenthe generated program [[p]] satisfies progress sensitive noninterference.
We also show that the instrumentation preserves thesemantics of the original program. That is, the instrumentation of a program p, written [[p]], produces exactly
the same output as p as long as it is allowed to continue;
it may be stopped at some point to prevent a leak. If m
is a memory for the target language we write m̂ for the
restriction of m to V \ Vlevel .

i f lowValue > 0 thenc := lowChannelelse
c := highChannel
end;
x := read c ; (* x is {L , H } *)send x to lowChannel ; (* will betransformed into a guarded send *)(* to reach here , x must be { L } *)send x to lowChannel (* no need totransform into a guarded send *)Listing 13: Constraint on the security type of an integer
variable

Using these constraints in our static analysis would increase the detection rate of programs that definitely leakinformation, rather than having them fail at runtime.

Theorem 2 (Semantics preservation) Let p be a program,m a memory, and o, o0 output traces. Then

6.2. Conditional updates of the halting context
While we chose to always update the halting context_hc after a guarded send withh[[p]], m, i ↓ o ⇒ hp, m̂, i ↓ o(hp, m̂, i ↓ o ∧ h[[p]], m, i ↓ o0 ) ⇒ o  o0 ∨ o0  o
0The same idea applies to integer variables. For example, we know that the instructions after the first send of
Listing 13 will only be reached if variable x is low. For thisreason, we can consider that x’s type after the send willbe (int L ){L} instead of (int {L,H} ){L} .

_hc := _pc t _hc t xctx t cctx ,0where o  o means that o is a prefix of o.

there are cases where we can be more precise. One suchcase is illustrated in Listing 14.

The proofs are available in Appendix B.

i f medValue thenx := read highChannelelse
x := read highChannel2
end;
send x to unknownChannel ; (* guarded send *)send lowValue to lowChannel

6. Increasing precision and permissiveness
During the course of this work, we thought of two ways
to improve the precision of our static analysis and permissiveness of our dynamic analysis. While we chose not to
use them into this work (to keep things as simple as possible), we think they are worth pointing out.

Listing 14: Example where _hc does not need to be updatedwith xctx

6.1. Security type constraints
In Listing 12, only executions where c is a high channel
will get past the first guarded send. For this reason, we
can consider, for the rest of the analysis, that its type isint {H} chan {L} instead of int {L,H} chan {L} .

In this example, while x’s value may differ, its type
is constant and equal to (int {H} ){M } . Since the value of
medValue does not affect its type, it means that it has noinfluence on the guarded send’s decision to block or allow
the output. Hence, in this case, the update to _hc variable
after the guarded send does not need to include variable
xctx .
Similarly, when a channel c whose type is constant isused in a guarded send command, the update to _hc does
not need to include variable cctx .
Hence, using conditional updates would allow the dynamic analysis to be more permissive as the updates to_hc are less conservative.

i f lowValue > 0 thenc := lowChannelelse
c := highChannel
end;
send highValue to c ; (* will be transformed
into a guarded send *)(* to reach here , c must be { H } *)11

7. Related workof a dynamic information security monitor. We speculatethat we could extend their ideas to allow on–the fly instrumentation.
Askarov and Sabelfeld [22] use hybrid monitors to enforce information security in dynamic languages. In thissetting, dynamic evaluation of programs (e.g., eval statements in JavaScript) requires on-the-fly static analysis ofprograms. They provide a model to define non-interference
that is suitable to progress-sensitivity and they quantify
information leaks due to termination [6].
Hritcu et al. [23] introduces an error-handling mechanism that allows all errors (even those caused by an information-flow control violation) to be safely recoverable. They
support dynamic levels. To help prevent leaks throughcovert channels, they provide a discretionary access control mechanism called clearance that allows them to put
an upper bound on the pc. Contrarily to our approach,the detection (and prevention) of leaks through progresschannels is not done automatically.
Askarov et al. [24] introduce a hybrid monitoring framework capable of handling concurrent programs. They illustrate their approach on a simple imperative language
similar to ours, but it does not support channel variables.
In their framework, each thread is guarded by its own local monitor (progress- and flow-sensitive). There is also asingle global monitor that synchronizes the threads. Likeus, they make use of an oracle to approximate the termination behaviour of branches. This oracle is called uponat runtime (making it a kind of on-the-fly static analysis),whereas ours is called only statically. The main difference between their approach and ours, exluding the concurrency of course, is the fact that our monitor is inlined
whereas theirs is not.

There has been much research into language-based techniques for controlling information flow over the last two
decades. In this section, we focus on hybrid techniques for
information-flow control.
Hybrid techniques are attractive as they have the potential to offer the advantages of both static and dynamic
analyses: the low runtime overhead of static approaches
combined with the precision and flexibility of dynamic
techniques.
Le Guernic et al. [5] present the first hybrid informationflow control monitor. The enforcement is based on a monitor that is able to perform static checks during the execution. The enforcement is not flow-sensitive. Le Guernic, in [17], extends this work to concurrent programs.
Russo and Sabelfeld [8] generalize their work, presenting
a series of hybrid monitors that differ on the action to
perform in the event of a security violation. They also
state that purely dynamic enforcements are more permissive than purely static enforcements but they cannot be
used in case of flow-sensitivity. They propose a hybrid
flow-sensitive enforcement based on calling static analysis
during the execution. This enforcement is not progresssensitive.
Kozyri et al. [16] show that it is not trivial to design dynamic enforcement mechanisms that support general lattices and do not leak information through termination. In
particular, they show that labels on labels are necessary
for lattices with more than two elements, but that twolevels of labels is enough.
Bedford et al. [18] generate instrumented code, enforcing information flow based on static analysis (i.e., an
information-flow monitor is inlined). The approach supports channel variables and is flow sensitive, but does nottake into account leaks due to progress. Also, the inlined
monitor does not use dynamic security levels, but employsa heavy-handed approach which is not as amenable tostandard optimization techniques as the present one. The
target language is not formally defined and no soundness
proof of the instrumented code is provided.
Moore et al. [14] consider precise enforcement of flowinsensitive progress-sensitive security. Progress sensitivity
is also based on an oracle’s analysis, but they call uponit dynamically while we do it statically. We have also
introduced additional termination types to increase thepermissiveness of the monitor.
Chudnov and Naumann [19] inline a flow-sensitive hybrid monitor (based on a monitor of Russo and Sabelfeld[8]) and extend it to Javascript [20]. They prove its soundness by showing that the execution of the inlined monitor isbisimilar to the execution of a non-inlined monitor. We inline a flow-sensitive progress-sensitive hybrid monitor and,as we did not have already have a non-inlined monitor, we
proved its soundness by showing that the output traces
produced by two `-equivalent executions will always be
the same. Magazinius et al. [21] present on-the-fly inlining

8. Conclusion
We have presented a hybrid information flow enforcement mechanism, which detects and prevents leaks that
may occur through the data-flow or the progress of a program. It uses information inferred during a phase of static
analysis to instrument the program; this helps to reduce
the number of false positives during the execution. The
instrumented program uses level variables, a simple yet
powerful way, to perform its dynamic analysis. This instrumented code can then be partially evaluated in orderto reduce the amount of added commands.
Our main contributions are the following.
(a) We present an extended version of the hybrid monitor first presented in our previous article [7]. It is capable of enforcing flow- and progress-sensitive information
security on general lattices. It is more precise and introduces less overhead than currently available solutions (e.g.,[12, 14]) for two reasons: it makes use of a static termination oracle and does not approximate the level of a variable
at the join of a conditional. Since our monitor is inlined,
it can be easily optimized using classical partial evaluation
techniques, [10].
12(b) We prove the soundness of our inlined monitor andthat the semantics of the original program is preserved, aslong as it is secure.
(c) We show that, thanks to the use of sets of levels, it
is possible to distinguish programs that definitely containleaks of information from programs that may leak information.
(d) We present two ideas to increase the precision of
the static analysis and the permissiveness of the dynamic
analysis: propagating constraints on the set of possible security levels and using conditional updates. We chose not
to use them in this work in order to increase readability.
Future work includes extensions to concurrency, declassification and information leakage due to timing. 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, [28], to enhance the static analysis
is also to be considered in future work.

[18] A. Bedford, J. Desharnais, T. G. Godonou, and N. Tawbi, “Enforcing information flow by combining static and dynamic analysis,” in Proceedings of the International Symposium on Foundations & Practice of Security, 2013.
[19] A. Chudnov and D. A. Naumann, “Information flow monitor
inlining,” in Proceedings of the 23rd IEEE Security Foundations
Symposium, 2010.
[20] ——, “Inlined information flow monitoring for javascript,”in Proceedings of the 22Nd ACM SIGSAC Conference on
Computer and Communications Security, ser. CCS ’15. New
York, NY, USA: ACM, 2015, pp. 629–643. [Online]. Available:
http://doi.acm.org/10.1145/2810103.2813684[21] J. Magazinius, A. Russo, and A. Sabelfeld, “On-the-fly inliningof dynamic security monitors,” Computers & Security, vol. 31,
no. 7, pp. 827–843, 2012.
[22] A. Askarov and A. Sabelfeld, “Tight enforcement of informationrelease policies for dynamic languages,” in CSF, 2009.
[23] C. Hritcu, M. Greenberg, B. Karel, B. C. Pierce, and G. Morrisett, “All your ifcexception are belong to us,” in Security andPrivacy (SP), 2013 IEEE Symposium on. IEEE, 2013, pp.
3–17.
[24] A. Askarov, S. Chong, and H. Mantel, “Hybrid monitors forconcurrent noninterference,” in Computer Security Foundations
Symposium, 2015.
[25] A. Banerjee and D. A. Naumann, “Secure information flow andpointer confinement in a java-like language.” in CSFW, vol. 2,
June 2002, p. 253.
[26] D. Hedin and D. Sands, “Noninterference in the presence of nonopaque pointers,” in 19th IEEE Computer Security Foundations
Workshop, (CSFW-19 2006), July 2006, pp. 217–229.
[27] T. Amtoft, S. Bandhakavi, and A. Banerjee, “A logic for information flow in object-oriented programs,” in Conference Recordof the 33rd ACM SIGPLAN-SIGACT Symposium on Principles
of Programming Languages, Jan. 2006, pp. 91–102.
[28] P. Cousot and R. Cousot, “Abstract interpretation: A unified
lattice model for static analysis of programs by construction orapproximation of fixpoints,” in POPL, R. M. Graham, M. A.
Harrison, and R. Sethi, Eds. ACM, 1977, pp. 238–252.

[1] A. Sabelfeld and A. C. Myers, “Language-based informationflow security,” IEEE Journal on Selected Areas in Communications, vol. 21, no. 1, 2003.
[2] D. Volpano, C. Irvine, and G. Smith, “A sound type system
for secure flow analysis,” Journal of computer security, vol. 4,
no. 2, pp. 167–187, 1996.
[3] T. H. Austin and C. Flanagan, “Efficient purely-dynamic information flow analysis,” in Proceedings of the Workshop on
Programming Languages and Analysis for Security, 2009.
[4] F. B. Schneider, “Enforceable security policies,” ACM Transactions on Information and System Security, vol. 3, no. 1, pp.
30–50, 2000.
[5] G. Le Guernic, A. Banerjee, T. Jensen, and D. A. Schmidt,“Automata-based confidentiality monitoring,” Asian Computing
Science Conference, 2006.
[6] A. Askarov, S. Hunt, A. Sabelfeld, and D. Sands, “Terminationinsensitive noninterference leaks more than just a bit,” in Proceedings of the European Symp. on Research in Computer Security: Computer Security, 2008.
[7] A. Bedford, S. Chong, J. Desharnais, and N. Tawbi, “A progresssensitive flow-sensitive inlined information-flow control monitor,” in ICT Systems Security and Privacy Protection - 31st
IFIP TC 11 International Conference, SEC 2016, Ghent, Belgium, May 30 - June 1, 2016, Proceedings, 2016, pp. 352–366.
[8] A. Russo and A. Sabelfeld, “Dynamic vs. static flow-sensitive
security analysis,” in CSF. IEEE Computer Society, 2010, pp.
186–199.
[9] L. Zheng and A. C. Myers, “Dynamic security labels and noninterference,” in Formal Aspects in Security and Trust. Springer,
2005, pp. 27–40.
[10] N. D. Jones, C. K. Gomard, and P. Sestoft, Partial evaluation
and automatic program generation. Prentice Hall, 1993.
[11] D. E. Denning, “A lattice model of secure information flow,”
Communications of the ACM, vol. 19, pp. 236–243, May 1976.
[12] K. R. O’Neill, M. R. Clarkson, and S. Chong, “Information-flow
security for interactive programs,” in CSFW. IEEE, 2006.
[13] G. Smith and D. Volpano, “Secure information flow in a multithreaded imperative language,” in POPL, 1998.
[14] S. Moore, A. Askarov, and S. Chong, “Precise enforcement ofprogress-sensitive security,” in CCS 2012, 2012.
[15] B. Cook, A. Podelski, and A. Rybalchenko, “Proving program
termination,” Commun. ACM, vol. 54, no. 5, pp. 88–98, May
2011.
[16] E. Kozyri, J. Desharnais, and N. Tawbi, “Block-safe information flow control,” Department of Computer Science, Cornell
University, Tech. Rep., Aug. 2016.
[17] G. L. Guernic, “Automaton-based confidentiality monitoring of
concurrent programs,” in CSF, 2007.

13

Appendix A. Examples(* while *)_oldpc1 := _pc;
while 1 do
_pc := _pc t L t L;(* skip *)skip ;
end;_pc := _pc t L t L;
_pc := _oldpc1

In order to simplify the examples, we assume that thevariables lVal, mVal, hVal and channels lChan, mChan, hChan
already exist, have random values and have the suggested
security levels. We also assume that all other level variables have been initialized to L. Boolean values are represented as integer where 0 means false and any other integermeans true.

After partial evaluation, it results in the following program:

Guarded send
The following example illustrates a situation where theguarded send is used to prevent a possible leak of information.

while 1 do
skip
end

if

mVal > 0 thenc := mChanelse
c := hChan
end;
send hVal to c ; (* may leak information *)Notice that because the code is statically safe, the partial
evaluation is able to get rid of the instructions added by
the instrumentation algorithm. This is because, if the codeis statically safe, then the conditions of the guarded sendcommands are all true. If guarded send commands are notneeded, then level variables are also not needed.

Here is its instrumentation :(* if *)
_oldpc1 := _pc;
i f lVal > 0 then_pc := _pc t lValval t lValctx t L;

Appendix B. Proofs
We prove that the type system of Figure 2 generates
non-interferent programs (i.e., we prove its soundness).

(* assign *)(c, cval , cctx ) := (lChan, lChanval , lChanctx t _pc);

Theorem 1 (Soundness of enforcement) If a program p iswell typed according to the type system of Figure 2, thenthe generated program [[p]] satisfies progress sensitive noninterference.

(c, cctx ) := (c, cctx t _pc); (* update *)else_pc := _pc t lValval t lValctx t L;

The theorem is a consequence of the following results.
(* assign *)(c, cval , cctx ) := (hChan, hChanval , hChanctx t _pc);

Lemma 3 If two memories are `-equivalent, then theyagree on every expressions involving level variables thatwere generated by the instrumentation and whose value isv `; these expressions include _pc, _hc, eval , ectx , etc.

(c, cctx ) := (c, cctx t _pc); (* update *)end_pc := _oldpc1 ;Sketch. The proof is by induction. The idea is to showthat all such expressions either only use level variables ofthe form xctx which are v `, on which `-equivalent memories agree by definition, or that whenever these expressions
use some xval , then they protect this potentially dangerous
variable by xctx . The program context, _pc, is modified
in the conditional and the loop, where the supremum istaken from the level of the condition.

(* guarded send *)i f _hc t _pc t hValval t hValctx t cctx v cval then(send hVal to c)e l s e f a i l end;
_hc := _pc t _hc t hValctx t cctx ;Divergence
Commands after a loop that always diverges are ignored. Hence, the following program is statically safe.

Notation If Γ(x) = σ`0x , we write Γctx (x) to mean `0x . If
Γ(x) = (int `x chan)`0x or (int `x )`0x , then we write Γval (x)to mean `x .
The following lemma states that security types of variables calculated by the typing system of Figure 2 include
all possible runtime values.

while 1 do
skip
end;
send hVal to lChan

Even if it is statically safe, it is instrumented :14

Lemma 4 For any execution starting with a complete memory, if the runtime memory is m when an instrumented
command [[cmd ]] is executed, and m0 is the memory after
the execution, assuming the typing generated by Figure 2isΓ, pc, hc ` cmd : t, hc0 , Γ0 , [[cmd ]],we have• Γ, pc, hc ` cmd 1 : t1 , hc1 , Γ1 , [[cmd1 ]].
Induction hypothesis gives us that m00 (the memory after
executing [[cmd 1 ]]) and Γ1 satisfy (1)-(4). If t1 = D then[[cmd 1 ; cmd 2 ]] is simply [[cmd 1 ]], and we are done since all
executions diverge. If t1 6= D, then we have for [[cmd 2 ]]that:
• Γ1 , pc, h1 ` cmd 2 : t2 , h2 , Γ2 , [[cmd2 ]](1) m(_pc) ∈ pc and m(_pc) = m0 (_pc)

Since the same program context as for cmd 1 is fed to thetyping rule, then by the induction hypothesis and the factthat m00 and Γ1 satisfy (1)-(4), we have the result for m0
and Γ2 .

and the following invariants in the program execution(2) m(_hc) ∈ hc
(3) m(xval ) ∈ Γval (x)(4) m(xctx ) ∈ Γctx (x)Case [[if e then cmd 1 else cmd 2 end]] =_oldpcν := _pc;
i f e then_pc:=_pc t eval t ectx ;[[cmd 1 ]];update(mv2 )else

Proof. The proof is by structural induction.
Base Cases:
Initially, we have pc = hc = {L}, m(_pc) = m(_hc) = L,
similarly for xval and xctx , so the conditions are true at theinitial state.

_pc := _pc t eval t ectx ;[[cmd 2 ]];update(mv1 )end;_pc := _oldpc

For (1) we observe that _pc has the same value before
and after the instrumented code. Moreover, before cmd i ,i = 1, 2, the value of _pc is in pc 0 , the context used totype these commands. For (3), by induction, we have thatthe invariants are true after the execution of [[cmd 1 ]] or[[cmd 2 ]]. Hence we have (3). The update function in eachbranch inserts commands that, for every modified variable
x, updates its xctx with _pc. This corresponds to what
is done in the supremum of environments (Definition 4),
so we have (4). Finally, since the update function updates
the _hc with _pc when the termination behavior of thetwo branches can differ, and that the _hc is updated by
update if one of the branch contains a guarded send, we
have (2) as this corresponds to the union done in (S-If).

Case [[skip]] is trivial.
Case [[x := e]] = (x, xval , xctx ) := (e, eval , ectx t _pc)
Since the execution of this code does not modify _pc or_hc, we have (1) and (2).
For every variable tval in expression eval , we have thatm(tval ) ∈ Γval (t). Similarly, for every variable tctx in expression ectx , we have that m(tctx ) ∈ Γctx (t). Hence, by
the definition of the supremum on sets (Definition 3) and(S-Op), we have (3) (i.e., m0 (xval ) ∈ Γ0val (x)). We also have(4) due to the updated environment returned (S-Assign).
Case [[send x to c]]
Subcase [[send x to c]] = send x to c
Trivial since no variable type is modified.

Case [[while e do cmd end]]_oldpcν := _pc;
while e do
_pc := _pc t eval t ectx ;[[cmd ]];

Subcase [[send x to c]] =i f _pc t _hc t xval t xctx t cctx v cvalthen (send x to c)else f a i l
end;_hc := _pc t _hc t xctx t cctx ;end;_pc := _pc t eval t ectx ;update(mv);_pc := _oldpc

The case is similar to the conditional. Variable _pc is
updated at the beginning of each iteration, it belongs to
pc t `e t `0e , as wanted for the induction step involving[[cmd ]], and we get (1), as pc 0 contains all the possible
values of _pc when [[cmd ]] is executed. By induction, we
have that the invariants are true after executing [[cmd ]].
Hence we have (3). We also have (2) and (4) using thesame arguments as in the conditional.

Initially we have that m(_pc) ∈ pc, m(_hc) ∈ hc, m(xctx ) ∈Γctx (x) and m(cctx ) ∈ Γctx (c). Only _hc is modified by thiscommand, hence we have (1), (3) and (4). We also have(2) by the supremum on sets and the hc0 returned by (SGSend).

The following proposition shows that any step of two
executions performed from `-equivalent memories resultsin `-equivalent outputs. Theorem 1 follows as a corollary
from it and from the next lemma.

Induction Cases:
Case [[cmd 1 ; cmd 2 ]]We can use induction on [[cmd 1 ]], with the following hypothesis:
15

Subcase [[send x to c]] =Proposition 5 Let mi , i = 1, 2 be two `-equivalent complete memories, oi be a trace and [[cmd ]] be a command
generated by Figure 2, that isi f _pc t _hc t xval t xctx t cctx v cvalthen (send x to c)else f a i l
end;_hc := _pc t _hc t xctx t cctx ;Γ, pc, hc ` cmd : t, h, Γ0 , [[cmd ]].
Then if both [[cmd ]], mi terminate, that is, we have maximal executions h[[cmd ]], mi , oi i −→∗ hstop, m0i , o0i i, thenthe following statements are invariants:

We have to prove (a) and (b). For (a), we only have toprove conditions (1) and (3) as only the value of _hc andthe content of the channel may change.
If mi (_pc t _hc t xctx t cctx ) v ` for one memory i ∈{1, 2} then, by `-equivalence, it is also the case for theother memory and we get (1). It also implies that the twomemory agree on xval and cval as they are `-equivalent.
This means that they either both fail, in which case there
is nothing more to prove, or the send command is executedin both. If it is executed, then mi (_pc t _hc t xval t xctx t
cctx ) v mi (cval ), for i = 1, 2, and by `-equivalence again,oi  ` = o0i  ` in both executions and (b) is true, as well as(3).
If m0i (_hc) = mi (_pct_hctxctx tcctx ) 6v ` for i = 1, 2,
then we get (1) and we have that the send command could
succeed in m1 and fail in m2 . But since mi (_pc t _hc t
xctx tcctx ) 6v `, we know that it cannot succeed on a channel
whose level is v ` and we get (b) and (3).

(a) the memories are `-equivalent (Def 5)(b) `-projections of observations are equal
Proof. The proof is by structural induction.
Base Cases:
Initially, we have mi , i = 1, 2 two `-equivalent memories
where the level variables have been initialized, so (a) and(b) are straightforward.
Case [[skip]] is trivial.
Case [[x := e]] = (x, xval , xctx ) := (e, eval , ectx t _pc)
We have to prove (a), as (b) is trivial since this command
does not modify the output traces. For `-equivalence,since _pc, _hc and the contents of channels are not modified, we obtain conditions (1) and (3) of Definition 5.
For condition (2): since m1 and m2 are `-equivalent, if
m01 (x, xval , xctx ) 6= m02 (x, xval , xctx ), then by Lemma 3 it
implies that m0i (xctx ) = mi (_pc t ectx ) 6v `. Meaningthat there is at least one variable tctx in ectx such thatmi (tctx ) 6v `, or that _pc 6v `. Hence, m01 and m02 are still`-equivalent. If m01 (x, xval , xctx ) = m02 (x, xval , xctx ), thenm01 and m02 are `-equivalent.

Induction Cases:
Case [[cmd 1 ; cmd 2 ]]The hypothesis gives that m1 and m2 satisfy (a) and (b).
Then we can use induction on [[cmd 1 ]], with the following
hypotheses:• Γ, pc, hc ` cmd 1 : t1 , h1 , Γ1 , [[cmd1 ]].
• h[[cmd 1 ]], mi , oi i −→∗ hstop, m00i , o00i i
Induction hypothesis gives us that m001 and m002 satisfy (a)and (b). We have for [[cmd 2 ]] that:

Case [[send x to c]]
Subcase [[send x to c]] = send x to c
By the typing rule, we have• Γ1 , pc, h1 ` cmd 2 : t2 , h2 , Γ2 , [[cmd2 ]]pc t hc t `x t `0x t `0c vs `c• h[[cmd 2 ]], m00i , o00i i −→∗ hstop, m0i , o0i iusing the property of supremum, combining with Lemma 4
and converting the notation, we obtain

By the induction hypothesis and the fact that m001 and m002
satisfy (a) and (b), we obtain that m01 and m02 satisfy (a)and (b).

mi (_pc) ∈ pc vs Γval (c)mi (_hc) ∈ hc vs Γval (c)Case [[if e then cmd 1 else cmd 2 end]] =mi (xval ) ∈ Γval (x) vs Γval (c)_oldpcν := _pc;
i f e then_pc := _pc t eval t ectx ;[[cmd 1 ]];update(mv2 )else

mi (xctx ) ∈ Γctx (x) vs Γval (c)mi (cctx ) ∈ Γctx (c) vs Γval (c)By the definition of vs , this implies mi (_pc t _hc t xval t
xctx t cctx ) v mi (cval ), which means that the sending of x
on c is safe. Hence we obtain (a) and (b) by `-equivalenceof the memories.

_pc := _pc t eval t ectx ;[[cmd 2 ]];update(mv1 )end;_pc := _oldpc

Assume that m1 and m2 satisfy (a) and that o1  ` = o2  `.
If mi (eval t ectx ) = tt∈Var(e) mi (tval t tctx ) v `, i = 1, 2
(symmetry is given by `-equivalence), we have the result
by induction since both memories take the same branch,
say i.
16

Now assume that mi (eval tectx ) 6v `, i = 1, 2. If m1 (e) =m2 (e) we are in the same situation as above. So assume
w.l.o.g. that m1 (e) is true but m2 (e) is false; hence undermemory mi , code [[cmd i ]] will be executed.
If both commands terminate, that is:• h[[cmd 1 ]], m1 , o1 i −→∗(b) if only one execution fails or diverges, say m1 , theno2  ` = o02  ` and m02 (_hc) 6v `.
(c) if mi (_pc) 6v ` or mi (_hc) 6v ` then oi  ` = o0i  `(d) if both executions fail or both diverge, then the `projections of observations are equal

hstop, m01 , o01 i

Proof. (a) is straightforward since _hc is always includedin the right-hand side when updating _hc.

• h[[cmd 2 ]], m2 , o2 i −→∗ hstop, m02 , o02 i
Then we know, by Lemma 6(c), that(b) is proven by induction, following the lines of Proposition 5. The interesting cases are the guarded send subcase and the inductive cases.

o01  ` = o1  ` = o2  ` = o02  `.
because before executing cmd i , variable _pc is updatedwith the value of mi (eval t ectx ) which is 6v `. Hence, theexecution of [[cmdi ]] will produce no output on channels oflevel v `. Hence, (b) is proven for the induction step.
This also proves (a) on channels, but we need to proveit on variables (level and non level).
Let x ∈ V and mv = mv1 ∪ mv2 , where mvi the setof variables that may be modified in cmd i , i = 1, 2. By
definition, variable _hc is also included in this set if thetermination of the branches may differ or if one of them
contains a guarded send. If x 6∈ mv and the mi ’s agree
on x, xctx and xval , then the m0i ’s also agree on x, xctx andxval .
If x ∈ mvi , we have that xctx w _pc t eval t ectx due tothe commands inserted by the update function. Thus wehave (a).

Case [[send x to c]]Let’s assume that the send command is transformed
into a guarded send. The only case where only one
execution fails, say m1 , is one where m02 (_hc) 6v `,and where no observation is made on a channel oflevel ` or lower, as wanted.
Case [[cmd 1 ; cmd 2 ]]Let m00i and o00i be the memories and output traces
after executing cmd 1 . Let m0i and o0i be the memories
and output traces after executing cmd 1 ; cmd 2 . If one
execution fails or diverges, say m1 on cmd 1 , thenby induction, m002 (_hc) 6v `, and by (c), we obtaino2  ` = o002  `. By (a) and (c) and induction, we thenget o2  ` = o02  `, as wanted. By (a), and (c) again,
we also obtain m02 (_hc) 6v `. If m1 fails or diverges
on cmd 2 instead, the argument is similar.

Case [[while e do cmd end]] =_oldpcν := _pc;
while e do
_pc := _pc t eval t ectx ;[[cmd ]];

Case [[if e then cmd 1 else cmd 2 end]]
There are two situations in which only one execution,
say m1 , can fail: (1) only one execution executesa guarded send or (2) they both execute the same
guarded send but the result is different. In case (1),
we have that mi (_pc) 6v ` (a consequence of Proposition 5 and Lemma 3), and that at least one of the
if ’s branch contains a guarded send, which is always
followed by an update to variable _hc. Since one of
the branch modifies variable _hc, it also means thatthe update function updates _hc to _pc, which is
6v `. Hence, we have (b) in this case. In case (2), theonly way that the result of a guarded send can bedifferent is if mi (_pc t _hc t xctx t cctx ) 6v `, where
x is the variable sent and c the channel on which thesend occurs. In this case, the update to _hc that immediately follows the guarded send will ensure thatm2 (_hc) 6v `. Hence we also have (b) in this case.
Similarly, for only only one execution to diverge, twothings must be true: (1) mi (_pc) 6v `, and (2) the
termination type of the if command is M . Since
the termination type is M , we have that the update
function inserted after the conditional updates the_hc to _pc, which is 6v `. Hence, we also have (b)in this case.

end;_pc := _pc t eval t ectx ;update(mv);_pc := _oldpc

As a loop is essentially a (possibly infinite) sequence of if ,the case is similar to the conditional. Assume that m1 andm2 satisfy (a) and (b). If mi (eval tectx ) = tt∈Var(e) mi (tval t
tctx ) 6v `, then we know that the execution of [[cmd]] willproduce no output on channels of level v ` since variable_pc is updated before entering the loop, and that every
variable that is or could have been modified by [[cmd]] will
have a tctx that is 6v ` due to the update function. Hence,
we have (a) and (b).
If instead we have that mi (eval tectx ) v `, then we havethe result by induction since both memories will always
take the same branch.
Lemma 6 With the premises of the previous theorem, if
one step of [[cmd ]] fails or diverges for one memory thenit also fails or diverges for the other or no more output
on channels of level ` or lower will be performed on that
execution. More precisely, for i = {1, 2}(a) mi (_hc) v m0i (_hc)
17Case [[while e do cmd end]]
The argument is similar to the if command.

Theorem 2 (Semantics preservation.) Let p be a program, m a memory, and o an output trace. Then

For (c), there are two cases where there are observations, the send case and the guarded send case. For thelatter, the condition is taken care of by the guard. For
the former, if mi (_pc) 6v ` or mi (_hc) 6v ` then, by
Lemma 4 (1) and (2), one of the sets pc or hc contains
a security level `0 6v `. By the typing rule, this implies
that `0 vs Γval (c). By definition of vs , all elements ofΓval (c) are greater than or equal to `0 and hence, again
by Lemma 4 (3), `0 vs mi (cval ) and ` 6vs mi (cval ), thusoi  ` = o0i  `.

h[[p]], m, i ↓ o ⇒ hp, m̂, i ↓ o(hp, m̂, i ↓ o ∧ h[[p]], m, i ↓ o0 ) ⇒ o  o0 ∨ o0  owhere o0  o means o0 is a prefix of o.
Note that m̂ is a memory for the source language, andhence it is of type : V ] C → Z ] C whereas m can, in
addition, map variables to levels.
Sketch. By structural induction. The program generated
by our instrumentation contains the same commands as
the original program, in the same order. The only difference being the additional assignments on level variables
and checks. For this reason, the only non-trivial case is
the send command, since it modifies the output trace, or
halts the program. Hence assume that cmd = send x to c.
There are two cases: (1) [[cmd ]] = cmd and (2) [[cmd ]] =if _pc t _hc t xval t xctx t cctx vs cval then (send x1 to x2 )else fail end; _hc := _pc t _hc t xctx t cctx .
In the first case, the claim is trivial. In the second case,the send is guarded by a condition. If this condition istrue, the sending will happen and the output trace will be
updated with o::(m(x1 ), m(x2 )), as would have been doneby cmd . Otherwise, the program [[cmd ]] will be stopped,and hence, no more output will happen, although cmd
could produce other outputs.

Finally, for (d), we have three cases: both executions
fail, both executions diverge and mi (_pcteval tectx ) v ` orboth executions diverge and mi (_pcteval tectx ) 6v `, where
e is the guard expression of the loop that diverges. If both
executions fail, then there will be no more outputs andso the `-projections remain equivalent. If both executions
diverge and mi (_pc t eval t ectx ) v `, then by Lemma 3 wehave that the `-projections of observations are equal. If
both executions diverge and mi (_pc t eval t ectx ) 6v `, thenthe update to the _pc inside the body of the loop ensuresthat mi (_pc) 6v ` before executing cmd , and so that there
will be no more outputs on channels of level lower or equal
to `.
Lemma 7 (Fixed-point) The fixed-point computed by typing rules (S-Loop1) and (S-Loop2) always converges toa value.
Proof. First let’s observe that the pc 0 computed by SLoop always reaches a fixed-point due to the fact that
it is a set of levels on which we add elements at each iteration; elements are never removed. Hence, in the worst
case, pc 0 will be equal to L (since L is a finite set).
Let x ∈ dom(Γ).
We have that Γval (x) ⊆ (Γtpc 0 Γ0 )val (x) by Definition 4,
as it states that (Γ tpc 0 Γ0 )val (x) = Γval (x) ∪ Γ0val (x). Hence,Γval (x) ultimately reaches a fixed point since L is finite.
Depending on the type associated to pc 0 , we either havethat Γctx (x) ⊆ (Γ tpc 0 Γ0 )ctx (x) or that the elements ofΓctx (x) are replaced by levels that are greater than them,by Definition 4 and Definition 3. Since pc 0 reaches a fixed
point, the subsequent modifications of Γctx (x) amounts toa union operation. Hence, the typing of Γctx (x) reaches a
fixed point eventually as the lattice L is finite.

18