arXiv:1605.02778v1 [cs.CR] 9 May 2016

Calculational Design of Information Flow Monitors
(extended version)
Mounir Assaf

David A. Naumann

Stevens Institute of Technology

Stevens Institute of Technology

a high branch, yielding false positives in cases like this:
if inhi then outlo := 0 else outlo := 0. Another technique
which has been investigated extensively is to rely on static
analysis to determine which locations might have been updated
in executions that do not follow the same branch as the actual
execution. The monitor tags all such locations when the control
join point is reached. These techniques provide monitoring
that is provably sound with respect to idealized semantics that
ignores covert channels like timing (e.g., [9], [15], [42], [52],
[56]).
These and related techniques have been investigated and
implemented but had quite limited practical impact. One
I. I NTRODUCTION
obvious reason is the difficulty of specifying policies with
Runtime monitoring can serve to test a program’s security or sufficient flexibility to capture security goals without excessive
to ensure its security by detecting violations. Monitoring is a restriction. Another impediment to practical use is that keeping
good fit for access control policies, which are safety properties. track of possible alternate control paths has high performance
A run either does or does not satisfy the policy, and a monitor cost. Lowering precision to reduce cost can result in intolerably
can be precise in the sense of raising an alert only when the many false positives. It is an active area of research to improve
run is poised to violate the policy. Information flow policies are monitors for better performance, better precision, and more
about dependency, e.g., an untrusted (resp. secret) input should subtle policies. (See Section VI for related work.)
not influence a trusted (resp. public) output. Formal definitions
Another impediment to practical IF monitoring is that, if
of information flow (IF) security are “hyperproperties” [25] enough is at stake to motivate paying the costs of policy
involving multiple runs. Suppose an observer classified as “low” specification, performance degradation, and possible false
knows the code, the set of possible secret inputs, and the low positives, there should be high assurance of correctness. The
input (from which they can deduce the possible runs and low complexity of monitoring grows with the complexity of the
outputs). A policy specifies what can be learned about the programming language and the monitoring techniques. While
secret upon observing a particular low output. Learning means there are machine-checked correctness proofs for theoretical
determining a smaller set of possible values of the secret. How models, there are few for practical implementations. The proofs
is a monitor, acting only on the actual execution, to detect known to us have been done “from scratch”, rather than building
violations of a property defined with respect to all (pairs of) on and reusing prior results (though of course one can identify
runs? Remarkably, this was shown to be possible [42]. In this common techniques). Such proofs are not easily maintained as
paper we show how to design such monitors systematically.
the monitored language and platform evolves.
A popular way to monitor dependency is to tag secret
This paper addresses the impediments related to the precision
data and propagate tags whenever tagged data is involved of monitors as well as the complexity of their design and
in computing other data. If an output is not tagged, we might correctness proofs.
conclude that in all possible runs, the output would have the
For safety properties, the theory of abstract interpretation
same value, i.e., nothing has been learned about the secret. The [29] is well established and widely used to guide and validate
conclusion is wrong, owing to information channels besides the design of static analyses [30]. Like the best theories
data flow. The most pervasive and exploitable such channel in engineering, abstract interpretation allows designs to be
is control flow. If some branch condition depends on a secret, derived from their specification instead of merely helping
the low observer may learn the secret from the absence of an to justify them after the fact [27]. Abstract interpretation
observable action that happens in the other branch.
underlies the static analysis part of some IF monitors [16],
Owing to the possibility of such implicit flow, sound [46], but the monitor design and justification remains ad hoc.
monitors are not in general precise. A simple technique Abstract interpretation has also been used for static analysis
is to raise an alert if a low assignment is attempted in of noninterference [40].
Abstract—Fine grained information flow monitoring can in
principle address a wide range of security and privacy goals,
for example in web applications. But it is very difficult to
achieve sound monitoring with acceptable runtime cost and
sufficient precision to avoid impractical restrictions on programs
and policies. We present a systematic technique for design
of monitors that are correct by construction. It encompasses
policies with downgrading. The technique is based on abstract
interpretation which is a standard basis for static analysis of
programs. This should enable integration of a wide range of
analysis techniques, enabling more sophisticated engineering of
monitors to address the challenges of precision and scaling to
widely used programming languages.

Chudnov et al. [23] suggest that an IF monitor should be
viewed as computing an abstract interpretation to account for
alternate runs vis-à-vis the monitored run. The key observation
is that typical IF policies are 2-safety [25]: a violation has
the form of a pair of runs, so the monitored run (major run)
need only be checked with respect to each alternate (minor
run) individually. What needs to be checked about the minor
run is a safety property, defined in terms of the major run
(and thus fully known to the monitor only upon completion of
the major run). This view offers a path to more sophisticated
monitoring and systematic development of monitors for real
world languages and platforms, and modular machine checked
correctness proofs. But the paper [23] is devoid of Galois
connections or other trappings of abstract interpretation! It
offers only a rational reconstruction of an existing monitor for
the simple while language, augmented with downgrading and
intermediate release policies.

interpretation, especially collecting semantics. For commands
we choose standard denotational semantics, because it facilitates
streamlined notations in what follows. Sec. III presents the ideal
monitor and shows how extant security policies are defined in
terms of this semantics. Sec. IV defines a Galois connection
for the lattice of relational formulas. That connection induces a
specification of a monitor that approximates the ideal monitor.
We sketch the derivation, from that specification, of a generic
monitor. Sec. V derives several monitors, by refining the generic
monitor to use different abstract interpretations for the minor
runs. These include a new purely dynamic monitor as well as
improvement on prior monitoring techniques. Sec. VI discusses
related work. Sec. VII discusses ideas for monitoring richer
languages and for gaining precision by leveraging existing
static analyses.
An appendix, providing detailed proofs for all results, can
be found in the end of this technical report.

Contribution: ideal monitor We reformulate the idea of
“tracking set” in Chudnov et al. [23] as a novel variation
of the standard notion of collecting semantics [28], which
serves as specification for—and basis for deriving—static
analyses. We generalize collecting semantics to depend
on the major run, in an ideal monitor which we prove
embodies checking of noninterference for the major
execution.
Contribution: derived monitors We derive several monitors from the monitoring semantics, using techniques of
abstract interpretation to show the monitors are correct by
construction. That is, the definitions are obtained by calculation, disentangling routine steps from inventive steps
and design choices, inspired by Cousot [27]. We identify
two main ways in which a monitor can glean information
from the major run and the abstractly interpreted collective
minor runs, accounting for existing monitors as well as
showing the way to further advances that can be made in
precision and efficiency.

II. BACKGROUND
A. Language syntax and standard semantics
To expose the main ideas it suffices to work with the simple
imperative language with integer variables. The only nonstandard features are the annotation commands, assert and
assume. These use relational formulas as in Chudnov et al. [23],
and are explained in due course.
Program syntax
e ::= n | id | e1 ⊕ e2 | b

b ::= e1 < e2 | e1 = e2 | ¬b | b1 ∧ b2

c ::= id := e | c1 ; c2 | if b then c1 else c2 | while b do c
| skip | assume Φ | assert Φ

Φ ::= Ae | Bb | Bb ⇒ Ae (basic formulas)
| Φ, Φ

Expressions are integer-valued. They include constants n,
variables id, binary operators (indicated by ⊕), and boolean
expressions b.
A state is a mapping from variables id to values v ∈ Z. For
σ ∈ States we define the denotation JeKσ of an expression e
as usual. For example, JidKσ , σ(id). Boolean expressions
evaluate to either integer 0 or 1, e.g., J¬bKσ is 1 if JbKσ = 0.
We omit the details, which are standard, and for simplicity we
assume that every expression has a value in every state.
We define the set of outcomes States⊥ , States ∪ {⊥}
where ⊥ is distinct from proper states (representing divergence).
We denote by 4 the approximation partial order over the flat
domain States⊥ , and 4̇ its lifting to functions over outcomes.
Therefore, the denotation of a command c is a function

A key abstraction used in our monitors is one for relational
formulas as in [23], here formulated as a Galois connection.
In the cited paper, the derived monitor exhibits ad hoc features
that reflect implementation details, e.g., simple agreement
relations are represented both by taint tags on variables and by
formulas. Here we refrain from dwelling on implementation
and instead explore how some existing static analyses can
be used in monitoring with little or no change. For example,
one of our monitors uses an interval analysis, known to have
good performance in practice. Other analyses, like constant
propagation could as well be incorporated, as we discuss. As in
standard static analysis, the notion of reduced product [26], [29],
[35] serves to share information between different analyses,
increasing their precision and efficiency.
These first steps are a proof of principle. In the future, solid
theoretical underpinnings can enable aggressive engineering of
monitors while retaining high assurance.
Outline: Sec. II introduces the simple language used to
present our ideas, and reviews key notions from abstract

JcK ∈ States⊥ → States⊥
For background on denotational semantics, see [58].
The clause JcK⊥ , ⊥ indicates that JcK is ⊥-strict for all
c and we ignore ⊥ in the subsequent cases. The annotation
commands act like skip. In the clause for if/else, we confuse
2

1 and 0 with truth and falsity in the metalanguage, to avoid
writing JbKσ = 1 etc. Throughout this paper, we denote the
least fixpoint of a monotonic function f ∈ A → A that is
v-greater than x ∈ A by lfpv
x f.

Relational formulas are closed under conjunction, written
Φ, Ψ as a reminder that sometimes we abuse notation and treat
a relational formula as a set of basic formulas.

Standard semantics of commands

Usually, abstract interpretation-based static analyses introduce a collecting semantics (also known as a static semantics [28, Section 4]) aimed at formalizing the possible
behaviours of a program wrt. a property of interest. This serves
as a starting point for the derivation of sound approximate
representations of program behaviours. The collecting semantics lifts the standard semantics to apply to arbitrary sets of
proper states, ignoring the ⊥ outcome that indicates divergence
because — like most work on information flow monitoring —
we aim for termination-insensitive security [19].

JcK⊥ , ⊥

Jid := eKσ , σ[id 7→ JeKσ]

C. Collecting semantics and abstract interpretation

J−K

Jc1 ; c2 Kσ , Jc2 K ◦ Jc1 Kσ
(
Jc1 Kσ if JbKσ
Jif b then c1 else c2 Kσ ,
Jc2 Kσ if ¬JbKσ
Jassume ΦKσ , σ

Jassert ΦKσ , σ

Jwhile b cKσ , (lfp4̇
(λσ.⊥) F)(σ)(
ρ
where F(w)(ρ) ,
w ◦ JcKρ

JskipKσ , σ

⦃c⦄ ∈ P(States) → P(States)

⦃c⦄Σ , {JcKσ | σ ∈ Σ and JcKσ 6= ⊥}

if ¬JbKρ
otherwise

The powerset P(States), with set inclusion as a partial order,
is a complete lattice. The collecting semantics can be given a
direct definition that makes explicit the fixpoint computation
over a set of states, rather than relying on the underlying
fixpoint of the functional F used in the standard semantics of
while.

B. Relational formulas
Relational formulas relate two states. The agreement formula
Ax says the two states have the same value for x. In relational
logics, initial and final agreements indicate which variables are
“low”, as in the low-indistinguishability relations used to define
noninterference [1]. In this paper we internalize specifications
using annotation commands as in [23]. Given a command c,
consider the command
assume Ax, Ay; c; assert Az

σpτ |= Ae iff. JeKσ = JeKτ

⦃−⦄

Collecting semantics

grdb

grdb (Σ) , {τ ∈ Σ | JbKτ = true}
⦃id := e⦄Σ = {σ[id 7→ JeKσ] | σ ∈ Σ}
⦃c1 ; c2 ⦄Σ = ⦃c2 ⦄ ◦ ⦃c1 ⦄Σ

(1)

This expresses that the final value of z may depend on the
initial values of x and y but not on other variables. If, from two
states that agree on x and y, executions of c lead to different
values of z, the assertion will fail.
Assumptions at intermediate points in the program serve
to specify downgrading, similar to explicit code annotations
in some work [21], [48], [49]. Although we do not model
intermediate output as such, one may model an output channel
as a variable, say out; the policy that it is low can be specified
by asserting agreement over what is assigned to out.
Relational formulas also feature a “holds in both” operator:
Two states σ and τ satisfy Bb iff. they both evaluate the
conditional expression b to 1. The third basic form is conditional
agreement [2], [23], Bb ⇒ Ae, which can be used to encode
multilevel security policies as well as to encode conditional
downgrading (e.g., [11], [20]).
Semantics of relational formulas

(2)

⦃if b then c1 else c2 ⦄Σ =

⦃c1 ⦄ ◦ grdb (Σ)
∪ ⦃c2 ⦄ ◦ grd¬b (Σ)

⦃assume Φ⦄Σ = Σ

⦃assert Φ⦄Σ = Σ
⦃skip⦄Σ = Σ


⦃while b c⦄Σ = grd¬b lfp⊆
Σ ⦃if b then c else skip⦄

Lemma 1 . The displayed equations define the same semantics
as Equation (2).
1
The proof is by structural induction on commands.
γ
−−
−− (A; v), comA Galois connection, written (C; ≤) ←
−−
α→
prises partially ordered sets with monotonic functions α, γ
such that α(x) v y iff. x ≤ γ(y) for all x ∈ C, y ∈ A.
In case C is P(States) and A is some lattice of abstract
states, a sound approximation for command c is t ∈ A → A
such that the following holds (writing v̇ for the pointwise lift
of v):

σpτ |= Φ

σpτ |= Bb iff. JbKσ and JbKτ

α ◦ ⦃c⦄ ◦ γ v̇ t

σpτ |= (Bb ⇒ Ae) iff. σpτ |= Bb implies σpτ |= Ae

(3)

1 While this formulation of the collecting semantics “is sometimes taken as
standard in abstract interpretation works” [22], Cachera and Pichardie [22]
provide the first precise proof relating it to a small-step operational semantics.

σpτ |= Φ, Ψ iff. σpτ |= Φ and σpτ |= Ψ

3

The best abstract transformer for c is α ◦ ⦃c⦄ ◦ γ. It is not
computable, in general, but it serves to specify the abstract
interpretation t. The idea is to derive an abstract semantics
⦃ − ⦄] so that, for all c, ⦃c⦄] is a sound approximation of c
and can be implemented efficiently.

monitoring semantics continues tracking all minor states that
also evaluate the guard to true. As for the minor states that
evaluate the conditional guard to false, they are propagated
through the else-branch by the collecting semantics. Notice
that the monitor semantics of conditionals ignores annotation
commands in non-executed branches. We revisit this later.

III. I DEAL M ONITOR

Ideal monitor

We introduce a concrete monitoring semantics which serves
as basis to define the security property by interpreting annotation commands with respect to both the actual execution
(major run) and all possible alternatives (minor runs). Readers
familiar with Chudnov et al. [23] may see this as a principled
account of their notion of “tracking set”, adapted to denotational
semantics. Sections IV and V derive monitors as abstract
interpretations of this ideal monitor.
The main difference between the collecting semantics and
the ideal monitor is that the ideal monitor is parametrised by
the current state σ of the major run – we call this a major state.
The ideal monitor is responsible for interpreting annotation
commands in order to track and verify the relational formulas
satisfied by all minor states τ in the tracking set Σ, wrt. the
major state σ.
The ideal monitor also has to signal security violations due
to assertion failures. We use the term fault, denoted by . We
define P (States) , P(States) ∪ { }. Therefore, the ideal
monitor

snd(σ, Σ) , Σ
LcMσ ,

Lid := eMσ Σ , {Jid := eKτ | τ ∈ Σ}
◦

Lc1 Mσ Σ

LskipMσ Σ , Σ

Lassume ΦMσ Σ , {τ ∈ Σ | σpτ |= Φ}
(
Σ if ∀τ ∈ Σ, σpτ |= Φ
Lassert ΦMσ Σ ,
otherwise

Lif(b then c1 else c0 Mσ Σ ,
Lc1 Mσ ◦ grdbσ Σ t ⦃c0 ⦄ ◦ grd¬b Σ
⦃c1 ⦄ ◦ grdb Σ t Lc0 Mσ ◦ grdσ¬b Σ
Lwhile b do cMσ Σ , snd



if JbKσ
otherwise



4̇×v̇
lfpλ(σ,Σ).(⊥,∅)
G (σ, Σ)

(
if ¬JbKσ
(σ, ⦃while b do c⦄Σ)
G(w)(σ, Σ) ,
w (JcKσ, Lif b then c else skipMσ Σ) otherw.

is applied to the initial major state and maps an input tracking
set Σ to an output set Σ0 or fault . We also introduce only
one rule (LcMσ , ) to mean that the ideal monitor maps
fault to fault.
In order to use the framework of abstract interpretation, we
provide the set P (States) with a lattice structure. To this end,
we lift set inclusion, the natural partial order over the powerset
P(States), to the set P (States). Therefore, we let be the
top element of the set P (States) and we denote by v the
lifting of set inclusion ⊆ to the set P (States):
Σ v Σ0 iff. (Σ0 =

grdσb

grdbσ (Σ) , {τ ∈ Σ | JbKτ = true}

Lc1 ; c2 Mσ Σ , Lc2 MJc1 Kσ

LcM ∈ States⊥ → P (States) → P (States)

∀Σ, Σ0 ∈ P (States),

L−M−

For assume Φ, the ideal monitor reduces the initial tracking
set Σ to the set of minor states τ whose pairing with the major
state σ satisfy the relational formula Φ. The monitor rules out
all alternative executions on the same control path that do not
comply with the assumption Φ. These are termed “assumption
failures” in [23].
For assert Φ, the ideal monitor checks whether all minor
states in the initial tracking set Σ satisfy the relational formula
Φ when paired with the current major state σ. If so, the
monitor returns Σ. Otherwise, the monitor concludes that one
of the alternative executions — that satisfies all assumptions
encountered so far — falsifies the assertion when paired with
the major state. So the semantics signals a security violation
by returning fault .
For while loops, the ideal monitor is defined as the least
fixpoint of a functional G that formalises the simultaneous
evaluation on both the major state and the tracking set. Erasing
operations related to tracking sets in the functional G yields
the functional F used in the standard denotational semantics.
Along the iteration of the major state on the loop body, the ideal
monitor iterates the tracking set on a conditional — ensuring
only minor states that have not yet reached a fixpoint go through
an additional iteration of the loop body. When the major state
reaches a fixpoint (i.e. ¬JbKσ), the tracking set is fed to the

∨ Σ ⊆ Σ0 )

Let t denote the lifting of set union to the set P (States).
The ideal monitor relies on the collecting semantics for
branching commands. Therefore, we also lift the collecting
semantics to the set P (States), by letting ⦃c⦄ , . This
guarantees that both the ideal monitor and the collecting
semantics are monotonic.
The ideal monitor can be seen as a hybrid monitor comprised
of a dynamic part and a static part. It directly handles the
dynamic part, but delegates the static part to the collecting
semantics. The dynamic part consists of tracking the minor
states that follow the same execution path as the major state,
whereas the static part consists in tracking the minor states that
follow a different execution path. The monitor semantics of
conditional commands best illustrates the intertwining between
the dynamic and static part of this ideal monitor. When
the major state evaluates the conditional guard to true, the
4

In summary, the idea is that from an initial state σ, a
monitored execution evaluates JcKσ and in parallel should
evaluate an abstraction of LcMσ , written LcM]σ . The monitored
execution yields σ 0 , with JcKσ = σ 0 , if it can guarantee
that LcM]σ States 6= . Otherwise, there is a potential security
violation. This parallel evaluation can be formalized, as it is
in the functional G for the monitor semantics of loops, but to
streamline notation in the rest of the paper we focus on what
is returned by the ideal monitor.

collecting semantics before exiting the loop — ensuring all
minor states reach their fixpoint.
Like the collecting semantics, the ideal monitor is defined
over concrete executions. Therefore, there is no loss of
information, in the sense that the ideal monitor returns a fault
iff. there is a minor state that falsifies the assertion.
The semantics of the ideal monitor is the concrete specification for a more abstract monitor whose transfer functions are
computable. We will rely on the framework of abstract interpretation in order to derive sound monitors by approximating
both the concrete collecting semantics and the ideal monitor.
The ideal monitor and the collecting semantics are equivalent
for annotation-free commands, as long as the major run
terminates.

IV. L ATTICE OF R ELATIONAL F ORMULAS
The derived monitors use abstract interpretations based on
relational formulas. This section defines the abstraction and
uses it to derive a generic monitor that is refined in Section V.
First we define the lattice of relational formulas. To make it
finite, expressions in relational formulas are restricted to those
that occur in the program to be monitored, as well as their
negations to facilitate precision in the monitors we derive.
A set of formulas is interpreted conjunctively. To streamline
notation we confuse a conjunctive formula, say “Ax, Ay”, with
the set {Ax, Ay}. That is why the lattice is defined in terms
of basic formulas.

Lemma 2 . For all annotation-free commands c, all σ ∈ States
such that JcKσ 6= ⊥, and all sets Σ ⊆ States, it holds that
LcMσ Σ = ⦃c⦄Σ
In fact LcMσ Σ ⊆ ⦃c⦄Σ as long as c is assertion-free. The
proof is by structural induction.
If the major run diverges, the least fixpoint of the functional
G yields an undefined outcome ⊥, paired with an empty set ∅
of minor states.
Assuming a set in of variables considered low inputs, and a
set out considered low outputs, let us use the notation Ain and
Aout to abbreviate the conjunction of basic agreements for
these variables. Theorem 1 states that, for c annotated following
the pattern of Equation (1), the ideal monitor, parametrised with
a major state σ1 , does not result in a fault iff. the standard
notion of termination-insensitive noninterference (TINI) holds
for c and σ1 .

Lattice of relational formulas

L

P (L)

Assumption: for a given command c, let L be a finite set
of basic relational formulas that is closed under negation of
boolean expressions and which contains at least Bb, Ae, and
Bb ⇒ Ae for every b and e that occur in c.
We use the powerset P(L) as a lattice ordered by ⊇ with
∅ on top and intersection as join: (P(L); ⊇, L, ∅, ∩, ∪). Let
P (L) be P(L) ∪ { }. Let v] be the lifting of the partial
order ⊇ such that is the top element of the lattice P (L):

Theorem 1 . Let in and out be two sets of variables and c
be an annotation-free command. Let command ĉ be defined
as assume Ain; c ; assert Aout. For all σ1 , σ10 ∈ States such
that JcKσ1 = σ10 , we have LĉMσ1 States 6= iff.

(P (L); v] , L, , t] , u] )
We also let t] (resp. u] ) denote the lifting of set intersection
∩ (resp. the lifting of set union ∪) to the lattice P (L).

∀σ2 , σ20 ∈ States, JcKσ2 = σ20 ∧ σ1 =in σ2 =⇒ σ10 =out σ20

The notation elides dependence of L on c because c should
be the main program to be monitored; a fixed L will be used
in the context of the monitor semantics which is recursively
applied to sub-programs of c.
The monitor will maintain an over-approximation of the
relational formulas satisfied by the major state σ and every
minor state τ of interest. A set of formulas is interpreted to
mean all the formulas hold for every such pair (σ, τ ). The
empty set indicates no relations are known, whereas serves
to indicate that some required relation fails to hold.
Given a major state σ, we aim to define an approximation
of a tracking set Σ, in order to account for relational formulas
satisfied by the major state σ and each minor state τ ∈ Σ.
Subsequently, we lift this abstraction in order to approximate
the monitoring collecting semantics and obtain sound
computable abstract transfer functions of a monitor tracking
relational formulas. We formalise this abstraction of the

Here we write =in to indicate agreement on the variables in.
The security property in [23] allows intermediate annotations,
but disallows them in high branches, to ensure robustness of
declassification etc. In an Appendix we provide an alternative
ideal monitor and an alternative collecting semantics, both of
which fault if an assertion or assumption occurs in a high
conditional — one for which some minor states do not agree
with the major state on its conditional guard.
Strong conjecture: for terminating executions, the security
property in [23] holds iff. the alternative ideal monitor does
not fault.
The alternative ideal monitor is a simple variation, but with
the notational complication of threading an additional parameter
through the definitions. So we do not use it in the body of the
paper. However, for each of the derived monitors, there is a
very similar one derived from the alternate ideal monitor, and
therefore sound with respect to the security property in [23].
5

tracking set Σ as a function ασ that is parametrised by a state σ:
ασ ∈ P (States) → P (L)
(
ασ (Σ) ,

{Φ | ∀τ ∈ Σ, σpτ |= Φ}

In the process of deriving a sound abstract monitoring semantics LcM]σ approximating the monitoring collecting semantics
LcMσ , we also have to derive a sound abstract static semantics
⦃c⦄] ∈ P (L) → P (L) approximating the static collecting
semantics ⦃c⦄ ∈ P (States) → P (States).
Equation (3) provides a notion of soundness for static
semantics, whereas Equation (4) provides a notion of soundness
for monitoring semantics. While approximating the monitoring
collecting semantics, we will find good ways for the abstract
static and monitoring semantics to interact. In particular, the
abstract static analyses we propose will account for that
interaction by additional parameters. Additionally, we will also
prove soundness results in Lemmas 5, 6 and 9 that embody not
only the soundness condition of Equation (3), but also variations
on that property that take into account this interaction between
the dynamic and static analyses.
The derivation of a sound abstract monitoring semantics is by
structural induction over commands. As an example, consider
the case of a conditional command c , if b then c1 else c0 , an
initial state σ and a final state σ 0 such that σ 0 = JcKσ. Let us
consider the case where the guard evaluates to true (JbKσ = 1),
so that σ 0 = Jc1 Kσ. Then, assuming a sound approximation
⦃c⦄] of the static collecting semantics, we can derive a generic
abstract monitoring semantics by successive approximation,
beginning as follows:

if Σ =
otherwise

The associated concretisation function γσ is also parametrised
by a major state σ. The concretisation of a set ∆ ∈ P(L)
of relational formulas yields a set Σ of minor states, such
that every minor state τ ∈ Σ and the major state σ satisfy all
relational formulas Φ ∈ ∆.
γσ ∈ P (L) → P (States)
(
γσ (∆) ,

{τ ∈ States | ∀Φ ∈ ∆, σpτ |= Φ}

if ∆ =
otherwise

Lemma 3 . For all σ ∈ States, the pair (ασ , γσ ) is a Galois
γσ
−−
−−
−
− (P (L); v] ). That is,
connection: (P (States); v) ←
−−
→
ασ
∀Σ ∈ P (States), ∀∆ ∈ P (L):
ασ (Σ) v ∆ ⇐⇒ Σ v] γσ (∆)
Figure 1 illustrates the best abstraction of the monitoring
collecting semantics LcMσ . If a set Σ of minor states is
abstracted wrt. a major state σ by a set ∆ of relational
formulas (Σ v γσ (∆)), then the resulting set Σ0 = LcMσ Σ
of minor states is abstracted wrt. the resulting major state
σ 0 = JcKσ by the set ασ0 ◦ LcMσ ◦ γσ (∆) of relational formulas
(Σ0 v γσ0 (ασ0 ◦ LcMσ ◦ γσ (∆))). This best abstract transformer
P (L)

ασ0 ◦LcMσ ◦γσ

ασ0

◦

Lif b then c1 else c0 Mσ

= ασ0

Lc1 Mσ ◦ grdbσ ◦

◦

γσ (∆)

γσ (∆) t ⦃c0 ⦄ ◦ grd¬b

ασ 0

◦

Lc1 Mσ
◦

◦

grdbσ

◦

σ

σ

⦃c0 ⦄ ◦ grd¬b

◦

γσ (∆)

v Hασ0 , Lc1 Mσ , and ⦃c1 ⦄ are monotone, γσ

0

extensive: λΣ.Σ v̇ γσ

ασ 0

ασ 0

◦

Lc1 Mσ

ασ0

P (States)

Figure 1.

◦

LcMσ

◦

Best abstract transformer

]

γσ v̇ LcM]σ

where σ 0 = JcKσ

(4)

γσ v̇ γσ0

◦

LcM]σ

and

ασ

◦

⦃c0 ⦄ ◦ γσ

◦

grdbσ

◦

ασ

◦

γσ (∆) t]

◦

grd¬b

The above derivation is a routine use of abstract interpretation
techniques. The last step uses a soundness property for the
static part of the monitor that is similar to Equation (3). So far,
we relied on an approximation of the monitoring collecting
semantics of command c1 and an approximation of the static
collecting semantics of command c0 . To continue this generic
derivation, we need to derive a sound approximation for the
guard operators grdbσ and grd¬b .

Lemma 4 Soundness conditions. Consider any c, σ, σ 0 such
that σ 0 = JcKσ. Equation (4) is equivalent to each of the
following:
◦

◦

]

Note that we denote by v̇ (resp. v̇ ) the pointwise lifting to
functions of the partial order v over P (States) (resp. of the
partial order v] over P (L)).

LcMσ

γσ

ασ I

ασ is

◦ γσ (∆)
]
v HLc1 Mσ is sound by induction hypothesis of Equation (4)I
Lc1 M]σ ◦ ασ ◦ grdbσ ◦ γσ (∆) t]
ασ0 ◦ ⦃c0 ⦄ ◦ γσ ◦ ασ ◦ grd¬b ◦ γσ (∆)
]
v] HThe static analysis is sound: ασ0 ◦ ⦃c0 ⦄ ◦ γσ v̇ ⦃c0 ⦄] I
Lc1 M]σ ◦ ασ ◦ grdbσ ◦ γσ (∆) t]
⦃c0 ⦄] ◦ ασ ◦ grd¬b ◦ γσ (∆)
(5)

is not computable in general. An abstract interpretation LcM]σ
is sound if it satisfies the following condition:
ασ0

◦

◦

◦

]

P (States)

LcMσ



γσ (∆) t]

]

JcK

γσ (∆)

= HSince ασ0 is additive: ασ0 (Σ ∪ Σ0 ) = ασ0 (Σ) t] ασ0 (Σ0 )I

P (L)

ασ0
γσ

◦

ασ0

◦

]

LcMσ v̇ LcM]σ

◦

ασ
6

The approximation of grdbσ proceeds as follows:
ασ

◦

grdbσ

first one treats high branching commands pessimistically by
forgetting all known formulas. The second one relies on an
approximation of the modified variables in order to determine
which relational formulas cannot be falsified, a usual technique
in hybrid monitors. The third one deduces new relational
formulas by comparing the results of an interval value analysis
to the current values in the monitored execution.

γσ (∆)

◦

= ασ ({τ ∈ γσ (∆) | JbKτ = 1})

= Hsince the major state evaluates b to trueI
ασ ({γσ (∆) ∩ {τ ∈ States | σpτ |= Bb})

= ασ ({γσ (∆) ∩ γσ ({Bb}))

= Hγσ is multiplicative: γσ (∆ u] ∆0 ) = γσ (∆) u γσ (∆0 )I
ασ

v] Hασ

◦

◦

A. Purely-Dynamic Monitor

]

γσ (∆ u {Bb})

γσ is reductive: ασ

]

∆ u {Bb}

◦

Let us start by deriving a purely-dynamic monitor tracking
relational formulas. This monitor is an instance of EM
mechanisms [55]. Thus, it must observe only the execution
steps of the major state. In particular, this monitor should not
look aside [52], meaning that it does not rely on information
about minor states that do not follow the same execution path as
the major state. This scenario corresponds to approximating the
collecting semantics ⦃c⦄ by an abstract static semantics D⦃c⦄]
that returns the top element of the lattice P(L), providing no
information about minor states that do not follow the same
execution path as the major state.
Definition 1 introduces such an abstract static semantics. We
ensure it is strict by mapping the bottom element L of the
lattice P(L) to itself.

]

γσ v̇ λ∆.∆I

(6)

As for the approximation of grdb , we have:
ασ

◦

grdb

γσ (∆) v] Hασ is monotone and grdb v̇λΣ.ΣI

◦

ασ

]

◦

γσ (∆)

v Hsince ασ

◦

γσ is reductiveI

∆

(7)

To sum up, we rewrite the approximations of operators grdbσ
and grdb of Equations (6) and (7) in the intermediate abstraction
of conditionals obtained in Equation (5), so we can conclude:
ασ0

Lif b then c1 else c0 Mσ ◦ γσ (∆)


]
v Lc1 M]σ (∆ u] {Bb}) t] ⦃c0 ⦄] ∆

Definition 1 . The abstract static semantics D⦃c⦄] for a purelydynamic monitor is given by:

◦

(8)

D⦃c⦄] ∈ P (L) → P (L)


if ∆ =

]
D⦃c⦄ ∆ , L if ∆ = L


∅ otherwise

This equation yields one of the generic approximations of conditional commands. It says that when the conditional guard is true,
monitor the then branch and statically analyse the else branch.
In the following section, we specialise this generic approximation by relying on different approximations of the static
collecting semantics.
Given the importance of relational formulas as an abstraction,
it should be no surprise that some monitors rely on entailments
among formulas. Precision can be improved by providing the
monitor with strong means of logical deduction, but there is
a cost in performance. This engineering trade-off can be left
open, by just specifying what we need. We use the notation
∆ ⇒] Φ, which is either true or false, as follows (cf. [23]).
Approximate entailment

Lemma 5 soundness of D⦃ − ⦄] . For all c, σ, σ 0 ∈ States,
]
it holds that: ασ0 ◦ ⦃c⦄ ◦ γσ v̇ D⦃c⦄] .
Mapping L to L is sound because the bottom element L is
concretised to the empty set of states (since L is closed under
negation, thus it contains Bb and B¬b for some b).
A detailed derivation of the purely dynamic monitor, as well
as subsequent derivations, are found in the Appendix.
Figure 2 presents the derived monitor. In it we use the
notation ∆⇒] Φ for the approximate implication specified at the
end of Section IV. The semantics for conditional commands is
obtained from the generic derivation for conditionals, presented
in Equation (8), by unfolding the definition of the static analysis
D⦃c⦄] .
The abstract monitoring semantics of any command maps
fault to fault (LcM]σ , ). For assignments id := e, the monitor
invalidates all relational formulas that involve variable id. It
also deduces that all resulting minor states agree with the major
state on variable id, if ∆ ⇒] Ae. For a sequence c1 ; c2 , the
initial state σ is used to monitor c1 , and then the resulting
major state Jc1 Kσ is used to monitor c2 .
For assumptions, the monitor adds the assumed formula to
the input set. For asserts, the monitor returns fault if it cannot
determine that the known ∆ implies the asserted Φ.

∆ ⇒] Φ

Assumption: For any ∆, Φ, if ∆ ⇒] Φ then the implication is
valid. That is, for all σ, τ ∈ States, if σpτ |= ∆ then σpτ |= Φ.
V. M ONITOR D ERIVATION
We derive three different monitors from the ideal monitoring
semantics. By relying on the framework of abstract interpretation, these monitors are correct by construction. Unless it
is clear from context, we will differentiate the three abstract
semantics of these monitors by prefixing them with the letters
D, M and I.
These three monitors illustrate different ways of reasoning
about relational formulas in high branching commands. The
7

LcM]σ ,

LskipM]σ ∆ , ∆
(

Lid :=

eM]σ ∆

(
Lassert

ΦM]σ ∆

,

, {Φ ∈ ∆ | id 6∈ fv(Φ)} u

]

]

∆ u {Φ}

if ∆ ⇒ Φ
otherwise

]

Aid if ∆ ⇒] Ae
∅
otherwise

Lc1 ; c2 M]σ ∆ , Lc2 M]Jc1 Kσ

◦

Lc1 M]σ ∆

Lassume ΦM]σ ∆ , ∆ u] {Φ}

(

Lc1 M]σ (∆ u] {Bb})



 ∅
Lif b then c1 else c0 M]σ ∆ , (
 Lc0 M]σ (∆ u] {B¬b})



 ∅

if ∆ ⇒] Ab
otherwise
if ∆ ⇒] Ab
otherwise

if JbKσ
if ¬JbKσ



]
v̇
]
Lwhile b do cM]σ ∆ , snd (lfp4̇×
G
)(σ,
∆)
λ(σ,∆).(⊥,L)

σ,
if ¬JbKσ and ∆ =



σ, ∆ u] {B¬b}
if ¬JbKσ and ∆ ⇒] Ab
where G ] (w] )(σ, ∆) ,

σ, {B¬b}
otherwise if ¬JbKσ



 ]
w JcKσ, Lif b then c else skipM]σ ∆
otherwise
Figure 2.

Purely-dynamic monitor DL−M]− , as abstract semantics derived from the ideal monitor

For conditionals, if the monitor is unable to determine that
all minor states agree with the major state on the value of the
conditional guard, it must treat it as a “high conditional”. So
the purely-dynamic monitor conservatively forgets all known
relational formulas.
Similarly to the standard denotational semantics and the ideal
monitor semantics, the abstract monitoring semantics of loops is
defined as a fixpoint of an abstract functional G ] . This abstract
fixpoint behaves as a finite sequence of conditionals. To each
iteration of the major state through the loop body corresponds
a simultaneous iteration of the monitor on a conditional. It is
important that the monitor treats each iteration of the loop body
as a conditional, in order to soundly track formulas satisfied
by minor states that exit the loop before the major state. When
the major state exits the loop, the monitor relies on the static
analysis in order to account for minor states that may continue
iterating through the loop.

0
1
2
3
4
5
6
7
8
9

Listing 1.

ασ0

◦

LcMσ

◦

γσ v̇

Example program

all variables as high. Thus, at the assignment to variable y,
our monitor deduces that all minor states agree with the major
state on the value of y, which means that no security violation
is raised since the relational assertion is satisfied. Notice that
if this example program asserts Apublic instead of Ay, our
monitor would always signal a violation , whereas a NSU
approach would not signal a fault when the conditional guard
evaluates to false (secret ≤ 0).

Theorem 2 . The abstract monitoring semantics DLcM]σ of the
purely-dynamic monitor is sound. For all commands c, for all
σ, σ 0 ∈ States such that σ 0 = JcKσ, it holds that:
]

/ / σ0 , [secret → 1; public → 0], ∆0 = ∅
assume Apublic ; / / [secret → 1; public → 0], {Apublic}
i f ( s e c r e t > 0 ) then {
public := public + 1;
} / / [secret → 1; public → 1], {Apublic, B(secret > 0)}
else {
skip ;
} / / [secret → 1; public → 1], ∅
y : = 0 ; / / [secret → 1; public → 1, y → 0], {Ay}
assert Ay ; [secret → 1; public → 1, y → 0], {Ay}

B. Hybrid Monitor with the Modified Variables

DLcM]σ

To achieve more precision, we need non-trivial static analysis
to provide information about minor runs that do not follow the
same execution path as the major run (“high branches”). The
next monitor relies on an over-approximation of variables that
are modified by a command.

Similarly to the No-Sensitive Upgrade (NSU) approach [59,
Section 3.2] [8], the purely-dynamic monitor of Figure 2 is
relatively efficient, at the cost of precision (i.e., it rejects many
secure executions). However, notice that both purely-dynamic
approaches are incomparable. Indeed, consider for instance the
program in Listing 1 where only variable secret is high. An
NSU approach would stop the program when the assignment
to public is executed, signaling a possible security violation. In
contrast, our purely dynamic monitor simply forgets all known
relational formulas at the merge point of the conditional; in
the case of simple agreements, this is tantamount to labelling

Modifiable variables

Mod

Assumption: Mod ∈ Com → P(V ar) satisfies the following:
for all c, id, if there is σ with JcKσ 6= ⊥ and JcKσ(id) 6= σ(id)
then id ∈ Mod(c).
For our simple language, the obvious implementation is to
8

return the set of assignment targets.
Instead of conservatively forgetting about all known
relational formulas at the merge point of high conditionals,
the monitor will be able to retain information about variables
that are modified in neither conditional branches, similarly
to existing hybrid monitors [42], [52].
Guided by the soundness condition, we derive an abstract
static semantics that leverages modified variables.

leverages the abstract static analysis of Definition 2 and
Lemma 6, in order to treat more precisely high branching
commands.
Although we avoid relying on explicit tracking of a security
context, for reasons of precision, that is useful for another
purpose: enforcing security policies such as robust declassification [60]. Recall the strong conjecture following Theorem 1.
One can replay the derivation of all three of our monitors,
starting from the alternative ideal monitor in Appendix A, with
minimal changes. We thus obtain three alternative monitors
that track a security context and are conjectured to be sound
for the semantics in [23].

Definition 2 . For all commands c and c0 , the abstract static
semantics M⦃c⦄]c0 for modified variables is given by:
M⦃c⦄]c0 ∈ P (L) → P (L)




L
]
M⦃c⦄c0 ∆ , 
 Φ ∈ ∆ | ∀id ∈ fv(Φ),



id 6∈ Mod(c) ∪ Mod(c0 )

C. Hybrid Monitor with Intervals

if ∆ =
if ∆ = L

We now derive a hybrid monitor that relies on a static
analysis approximating the range of values each variable may
take. This allows to infer agreements even for locations that
are modified in high branches.

otherwise

The soundness condition is similar to Lemma 5, adapted to
the extra parameter.

Interval analysis

⦃ − ⦄],Int

Assumptions: StatesInt is a set of abstract environments mapping variables to intervals (and StatesInt , StatesInt ∪ { }).
⦃c⦄],Int ∈ StatesInt → StatesInt is an interval static
For a given set ∆ of relational formulas that hold between analysis satisfying: αInt ◦ ⦃c⦄ ◦ γ Int ≤
˙ ],Int ⦃c⦄],Int , with
an initial major state σ and every initial minor state τ ∈ Σ, (αInt , γ Int ) being the Galois connection enabling its derivation:
γ Int
this abstract static semantics deduces a set ∆0 of relational
←
−−
−−
−→
− (StatesInt ; ≤],Int )
(P
(States);
v)
0
0
−
−
formulas that hold between an output major state σ = Jc Kσ
αInt
and every output minor state τ 0 = JcKτ . Intuitively, the set ∆0
is deduced from ∆ by keeping only the relational formulas that
Interval static analysis is standard [28]; we present one in
cannot be falsified since their free variables are not modified. full detail in the long version of the paper.
Figure 3 introduces the abstract semantics MLcMσ of the
Unlike the previous hybrid monitor relying on the modified
hybrid monitor relying on a static analysis of modified variables. variables, this monitor reasons on the values variables may
Most transfer functions are essentially the same as the ones take, in order to establish relational formulas in the case of
introduced for the purely-dynamic monitor. Thus, we refer high branching commands. Similarly to the condition stated in
to Figure 2 and redefine only the ones that are different, Lemmas 5 and 6, the abstract static analysis ⦃c⦄] must satisfy:
namely conditionals and loops. The main difference compared
]
ασ0 ◦ ⦃c⦄ ◦ γσ v̇ ⦃c⦄]
to the purely-dynamic monitor resides in the treatment of high
branchings. For a high conditional, the abstract static analysis Let us derive such an abstract static analysis by relying on the
of modified variables enables the hybrid monitor to deduce interval analysis ⦃c⦄],Int . Observe that
that if a relational formula Φ holds before the conditional
command and if its free variables are modified in neither ασ0 ◦ ⦃c⦄ ◦ γσ
]
conditional branches, then Φ also holds after the execution
v̇ Hsince ασ0 , ⦃c⦄ are monotone, γ Int ◦ αInt is extensiveI
of the conditional command. This behaviour is similar to the
ασ0 ◦ γ Int ◦ αInt ◦ ⦃c⦄ ◦ γ Int ◦ αInt ◦ γσ
treatment of high conditionals by existing hybrid information
]
flow monitors [42], [52]. However, our hybrid monitor does not
v̇ Hsince ασ0 , γ Int are monotone, ⦃c⦄],Int is soundI
rely on labelling the program counter with a security context in
ασ0 ◦ γ Int ◦ ⦃c⦄],Int ◦ αInt ◦ γσ
(9)
order to track implicit flows. This is similar to Besson et al.’s
Consequently, we can leverage an interval static analysis
approach [16]; it facilitates better precision, as they show and
to
derive a monitor tracking relational formulas, provided
we see in the next subsection.
that
we derive an interface between the two abstractions.
Theorem 3 soundness of ML−M]− . The hybrid monitor
First,
we have to approximate the operator αInt ◦ γσ which
MLcM]σ is sound in the sense of Equation (4): for all c, σ:
translates relational formulas — that holds wrt. a major state
]
σ — to interval constraints over variables. Second, we need to
ασ0 ◦ LcMσ ◦ γσ v̇ MLcM]σ where σ 0 = JcKσ
approximate the operator ασ0 ◦ γ Int which translates interval
The derivation proof of this monitor is similar to the constraints over variables to relational formulas — that holds
derivation of the previous purely-dynamic monitor. It mostly wrt. a major state σ 0 .
Lemma 6 soundness of M⦃ − ⦄]− . For all c, c0 , σ, σ 0 such
]
that σ 0 = Jc0 Kσ, it holds that: ασ0 ◦ ⦃c⦄ ◦ γσ v̇ M⦃c⦄]c0 .

9

]
Lif b 
then
( c1 else c0 Mσ ∆ ,

Lc1 M]σ (∆ u] {Bb})



 Lc M] (∆ u] {Bb}) t] {Φ ∈ ∆ | fv(Φ) ∩ (Mod(c ) ∪ Mod(c )) = ∅}
1
0
( 1 σ
 Lc0 M]σ (∆ u] {B¬b})



 Lc M] (∆ u] {B¬b}) t] {Φ ∈ ∆ | fv(Φ) ∩ (Mod(c ) ∪ Mod(c )) = ∅}
0 σ

1

0

if ∆ ⇒] Ab
otherwise
if ∆ ⇒] Ab
otherwise

if JbKσ
if ¬JbKσ



]
v̇
]
Lwhile b do cM]σ ∆ , snd (lfp4̇×
G
)(σ,
∆)
λ(σ,∆).(⊥,L)

σ,



σ, ∆ u] {B¬b}
 ]
G ] (w] )(σ, ∆) ,
]

σ,
{Φ
∈
∆
|
fv(Φ)
∩
Mod(c)
=
∅}
t
∆
u {B¬b}



 ]
]
w JcKσ, Lif b then c else skipMσ ∆
Figure 3.

if ¬JbKσ and ∆ =
if ¬JbKσ and ∆ ⇒] Ab
otherwise if ¬JbKσ
otherwise

Hybrid monitor ML−M]− using modified variables

These two operators αInt ◦ γσ and ασ ◦ γ Int are similar defines a Granger’s reduced product for the Cartesian product
to Granger’s reduced product operators [26], [36] over the of intervals and relational formulas, in Lemma 8.
Cartesian product of both intervals and relational formulas, as
A Granger’s reduced product
tointσ toforσ
we shall explain.
Since combining different static analyses independently by
relying on a Cartesian product does not yield optimal results in
tointσ (ı, ) , ı
toforσ ( , ∆) , ∆
general, abstract interpretation relies on a notion of a reduced
products [29], in order to enable the sharing of information
tointσ (ı, ∆) , u],Int tointσ (ı, {Φ})
between the different abstractions and gain more precision.
Φ∈∆
Let (ασInt , γσInt ) be the Galois connection associated with
tointσ (ı, {Ae}) , ı u],Int grd],Int
with v , JeKσ
the Cartesian product of both abstractions:
e=v (ı)
Int
Int
Int
Int
γσ (ı, ∆) , γ (ı) u γσ (∆) and ασ (Σ) , (α (Σ), ασ (Σ)).
tointσ (ı, {Bb}) , ı u],Int grd],Int
(ı)
max([a, b]) , b
b
Definition 3 . A Granger’s reduced product for the Cartesian abstraction StatesInt × P (L) is a pair of operators
tointσ (ı, {Bb ⇒] Ae}) , ı
min([a, b]) , a
tointσ ∈ StatesInt × P (L) → StatesInt and toforσ ∈
StatesInt × P (L) → P (L), parametrised by a state σ ∈ toforσ (ı, ∆) , ∆ u] {Ax | min(ı(x)) = max(ı(x)) = σ(x)}
States and satisfying two conditions:
Int
Int
• Soundness: γσ (tointσ (ı, ∆), ∆) = γσ (ı, ∆) and
Int
Int
γσ (ı, toforσ (ı, ∆)) γσ (ı, ∆)
],Int
• Reduction: tointσ (ı, ∆) ≤
ı and toforσ (ı, ∆) v] ∆
Lemma 8 . For all σ ∈ States, the pair of operators
tointσ , toforσ is a Granger’s reduced product.
Lemma 7 . For all σ ∈ States, any pair of operators that is a
The proof derives the definition from the required properties.
Granger’s reduced product (tointσ , toforσ ) for the Cartesian
Int
The operator tointσ reduces an interval environment ı by
abstraction States × P (L) provides a sound approximation
accounting
for the additional constraint that a set of relational
of the interface between intervals and relational formulas:
formulas
must
hold wrt. to a state σ. For instance, reducing ı
˙ ],Int λ∆. tointσ ( , ∆) and
αInt ◦ γσ ≤
to account for a set of constraints ∆ amounts to computing the
]
intersection over the reduced interval environments wrt. each
ασ ◦ γ Int v̇ λı. toforσ (ı, )
formula Φ ∈ ∆. Also, reducing ı to account for the constraint
The proof of this result applies to any abstraction and is that Ae holds wrt. to a major state σ amounts to reducing ı to
not limited to an interval analysis. In a nutshell, for any off- account for the additional constraint that expression e evaluates
the-shelf static analysis, we can define a Granger’s reduced to a particular value JeKσ that is determined by the major
product for its Cartesian product with the relational formulas in state σ. This reduction can be achieved by using an abstract
],Int
that over-approximates the concrete operator
order to interface this analysis with our monitor, and guarantee operator grdb
b
soundness by Equation (9). Therefore, we introduce in the grd . The soundness of grd],Int
guarantees the soundness of
b
following a pair of operators (tointσ , toforσ ), that we prove operator tointσ , and the abstract meet with the initial interval
10

environment also guarantees the reduction condition stated in
Definition 3.
The operator toforσ reduces interval constraints over variables to a set of relational formulas that hold wrt. a major state
σ. Whenever an interval environment ı maps a variable x to a
singleton value that matches σ(x), we can deduce that all the
minor states abstracted by ı agree with σ on the value of x.
Notice that toforσ does not iterate over the finite lattice
P(L), though in theory that can be done in order to determine 0
all relational formulas that hold. A smarter way to improve the 1
precision of toforσ would take hints from the monitored branch, 2
3
by trying to prove that some particular relational formulas are 4
satisfied wrt. the major state. This would improve precision 5
6
for the statically analysed branch.
7
Having derived a sound approximation of the interface 8
between intervals and relational formulas, we can resume the 9
derivation started in Equation (9), using Lemmas 7 and 8, to 10
obtain a sound abstract static semantics.
11
12

Definition 4 . For all σ, σ 0 ∈ States, the abstract static 13
14
semantics I⦃c⦄]σ,σ0 based on ⦃c⦄],Int is given by:
I⦃c⦄]σ,σ0 ∈ P (L) → P (L)




L
]
I⦃c⦄σ,σ0 ∆ ,

λı. toforσ0 (ı, ) ◦



⦃c⦄],Int ◦ tointσ ( , ∆)

if ∆ =
if ∆ = L

analysis determines that all minor states agree with the major
state on the value of variable seed — at the merge point of
the conditional, which corresponds to labelling this variable
as low. Our hybrid monitor is similar in spirit to the hybrid
monitor of Besson et al. [16] that is also able to deduce that
variable seed does not convey any knowledge about sensitive
data, by relying on a constant propagation static analysis.
/ / σ0 , [seed → 3; secret conf → 1 . . .], ∆0 = ∅
assume Aseed ; / / [seed → 3; secret conf → 1 . . .], {Aseed}
a : = secret base ;
i f ( s e c r e t c o n f ) then {
b : = secret number ; / / [seed → 3 . . .], {Aseed, Bsecret conf}
/ / Complicated hash computation on t h e seed , a & b .
r : = seed ∗ a ∗ b ;
seed : = 1 + seed ; / / [seed → 4 . . .], {Aseed, Bsecret conf}
}
else { / / value-sensitivity:
seed is initialised to a singleton interval

/ / ı , seed → [3, 3]; r → [−∞, +∞] . . .
/ / Complicated hash computation
on t h e seed & a . 

r : = seed ∗ a ∗ 4 2 ; / / seed → [3, 3]; r → [−∞, +∞] .. .
seed : = 1 + seed ; / / seed → [4, 4]; r → [−∞, +∞] . . .
} / / [seed → 4 . . .], {Aseed}
assert Aseed ; / / [seed → 4 . . .], {Aseed}
Listing 2.

Example program inspired by [47]

VI. R ELATED W ORK

Abstract interpretation has been used for static analysis of noninterference in a number of works including
otherwise
Kovàcs et al. [40], where security is explicitly formulated
as 2-safety. Giacobazzi and Mastroeni show how abstract
Lemma 9 soundness of I⦃ − ⦄]−,− . For all c, c0 and σ, σ 0 interpretation can be used to reason about downgrading policies
in States it holds that:
and observational power of the attacker [34]. Here we focus
]
]
on related work that addresses the challenge areas for IF
0
0
ασ0 ◦ ⦃c⦄ ◦ γσ v̇ I⦃c⦄σ,σ0 where σ = Jc Kσ
monitoring identified in Sec. I: expressive policy, precision
Figure 4 introduces the abstract monitoring semantics we versus performance, and assurance of correctness.
To facilitate expression of the range of practical IF policies,
derive for the hybrid monitor relying on intervals. Most abstract
transfer functions are similar to the ones introduced for the researchers have proposed language based approaches that use
purely-dynamic monitor. Thus, we refer to Figure 2 and redefine types and other program annotations to label channels and for
only the ones that are different, namely conditionals and loops. downgrading directives [6], [11], [20], [21], [48], [53], [57],
The main difference concerns branching commands, since we [60]. In various ways, policies can refer to meaningful events
and conditions in terms of program control and data state
rely on the novel abstract static analysis of Definition 4.
(including instrumentation to express policy [20]). Relational
]
Theorem 4 . The abstract monitoring semantics ILcMσ of the
Hoare logic features assertions that express agreement or “low
hybrid monitor, introduced in Figure 4, is sound: For all σ, σ 0 ∈
indistinguishability”, enabling direct specification of conditional
0
States such that σ = JcKσ, it holds that:
and partial dependency properties [1], [4], [14], [50]. A strength
]
]
of the logic approach is that it can offer precise reasoning about
◦
◦
0
ασ LcMσ γσ v̇ ILcMσ
complex data and control structures [3], [12], [50]. For endThis monitor is sensitive to runtime values. It deduces to-end semantics of IF policies, epistemic formulations are
new relational formulas for high branching commands, by effective [5]–[7], [10] and have been connected with relational
comparing the major state with the results of an interval static logic [11]. Such a connection is evident in the IF property
analysis. Consider for instance the program in Listing 2, that of [23], although it is not formalized there.
is inspired by Müller and al. [47]. Despite being modified in
The generality and expressiveness of relational logic comes at
conditional branches that depend on a high guard, variable the cost that it does not inherently enforce desirable constraints
seed does not leak sensitive data. Unlike the hybrid flow- on policy. For example, consider the policy that the initial
sensitive monitors of Le Guernic et al. [42] and Russo and value of card number is secret, but the low four digits may
Sabelfeld [52], as well as the ones we introduce previously be released upon successful authentication between merchant
in Sections V-A and V-B, our monitor relying on an interval and customer. The relevant condition could be asserted at a
11

]
Lif b 
then
( c1 else c0 Mσ ∆ ,

Lc1 M]σ (∆ u] {Bb})
if ∆ ⇒] Ab



],Int
 Lc M] (∆ u] {Bb}) t] λı. tofor
],Int
◦ grd
◦ tointσ ( , ∆) otherwise
Jc1 Kσ (ı, ) ◦ ⦃c0 ⦄
¬b
( 1 σ
]
]
 Lc0 Mσ (∆ u {B¬b})
if ∆ ⇒] Ab




 Lc M] (∆ u] {B¬b}) t] λı. tofor
(ı, ) ◦ ⦃c ⦄],Int ◦ toint ( , ∆) otherwise
Jc0 Kσ

0 σ

σ

1

if JbKσ
if ¬JbKσ



]
4̇×v̇
Lwhile b do cM]σ ∆ , snd (lfpλ(σ,∆).(⊥,L)
G ] )(σ, ∆)

σ,



σ, ∆ u] {B¬b}
G ] (w] )(σ, ∆) ,

σ, ∆ t] λı. toforσ (ı, ) ◦ ⦃while b do c⦄],Int



 ]
w JcKσ, Lif b then c else skipM]σ ∆
Figure 4.

◦


tointσ ( , ∆) u] {B¬b}

if ¬JbKσ and ∆ =
if ¬JbKσ and ∆ ⇒] Ab
otherwise if ¬JbKσ
otherwise

Hybrid monitor IL−M]− with an interval analysis

point in the code where the release takes place, together with work relies on the framework of abstract interpretation for
assumed agreement on the expression ccnum%10000, but the the systematic design and derivation of security monitors. We
policy analyst could also assert that ccnum refers to its initial hope our work will pave the way for the formal verification
value at this point — assert B(ccnum = oldcc) where oldcc of practical security monitors, by reusing some of the recent
is a variable set to the initial value of ccnum and not changed. developments in formal verification of abstract interpretation
Concerning precision of purely dynamic monitors, the basic analysers [32], [38], [51].
technique of No Sensitive Upgrade (NSU) [8], [59] has been
VII. D ISCUSSION AND C ONCLUSION
refined [9], [17] and several implementations exist [18], [24],
In this paper we propose an ideal monitor as a variation of
[37], [54]. Experience suggesting NSU is too imprecise —
a collecting semantics. We prove that this monitor enforces
rejecting many secure executions — led Hedin et al. [37] to
noninterference, for policies expressed using relational formuaugment their monitor with static analysis of modified locations
las, to which many other policy formalisms can be translated.
that heuristically suggests label upgrades, while relying on
We also conjecture (following Theorem 1) a relation with the
NSU for soundness. Hybrid monitors typically feature static
security property proposed in [23] and taking into account
analysis of modified variables. For the simple while language,
intermediate assumptions (for downgrading) and assertions (for
a simple approximation is to find all assignment targets [42],
modularity and intermediate output). We would like to prove
[52]. For more complex data structure this requires memory
that conjecture, and strengthen it to account for intermediate
abstraction [46]. For more precision it is better to take into
assertions in divergent major runs. We believe this can be done
account the actual low values [41]. The term “value-sensitive”
using either transition semantics or trace based denotational
is used by Hedin et al. [37] and Bello et al. [13] for the use
semantics.
of low values in the major run to determine the observable
The ideal monitor is a specification that serves for deriving
modifications.
monitors that are sound by construction. We derive three
As our third monitor shows, there is a second important way monitors that illustrate various ways of tracking low indisin which precision can be gained by sensitivity to low values. tinguishability and other relational formulas between states for
This is also done by Besson et al. [16] who propose a generic high branchings. Although we provide a systematic approach
hybrid monitor for quantitative information flow by tracking the by which precision can be fine tuned, we do not systematically
knowledge about sensitive data that is stored in each program evaluate the precision of the derived monitors. Several notions
variable. Their monitor is also parametrised by a static analysis. of evaluation have been proposed in the literature, using terms
The monitors we derive by relying on abstract interpretation such as permissiveness and transparency. Bielova and Rezk [19]
share some similarities with their monitors. Indeed, they also disentangle these notions. In their terms, precision in our
model a purely-dynamic monitor by a static analysis that replies sense — allowing more secure executions — is termed “true
with top, forcing the monitor to treat high branching commands transparency”.
pessimistically. Additionally, their monitors do not rely on
A benefit of monitoring, relative to type systems or other
labelling the program counter with a security context.
static analyses for security, is the potential to leverage runFor formal assurance of IF monitor correctness, several time values for precision. Almost all prior work uses valueworks provide detailed formal proofs [37], [54]; some are sensitivity, if at all, as a means of improving precision to
machine checked [15], [33], including Besson et al. [16]. Our determine modifiable locations. An exception is Besson et
12

al. [16] who rely on constant propagation to delimit implicit
flows based on actual values. A similar result is provided by
our value-sensitive hybrid monitor using interval analysis. We
rely on a classical notion in abstract interpretation, reduced
product [29], to formalize the interactions between both the
dynamic and the static part of the monitor. Lemma 7 and
Equation (9) in particular are key results. By defining a
Granger’s reduced product, we can immediately leverage other
off-the-shelf static analyses, such as polyhedra [31], trace
partitioning [45], and constant propagation. Existing monitors
already incorporate such complex static analyses that are
spawned during or before the monitored execution [16], [43],
[44]. Two challenges remain for the adoption of IF monitors:
scaling them to complex and richer languages, and lowering
the incurred overhead. We believe this paper makes a dent
wrt. the first dimension, by linking the design of information
flow monitors to the design of static analyses by the wellestablished theory of abstract interpretation [28]. As to the
second challenge, we would like to investigate what static
information can be pre-computed and how a monitor can
take advantage of such information (beyond the easy case
of modified variables in a toy language).
Acknowledgments: Thanks to Anindya Banerjee, Andrey
Chudnov, and the anonymous reviewers for helpful feedback.
The authors were partially supported by NSF award CNS1228930.
R EFERENCES
[1] T. Amtoft and A. Banerjee, “Information Flow Analysis in Logical Form.”
Static Analysis Symposium, pp. 100–115, 2004.
[2] ——, “Verification condition generation for conditional information flow,”
in ACM Workshop on Formal Methods in Security Engineering, 2007,
pp. 2–11.
[3] T. Amtoft, J. Hatcliff, and E. Rodrı́guez, “Precise and automated
contract-based reasoning for verification and certification of information
flow properties of programs with arrays,” in European Symposium on
Programming, ser. LNCS, vol. 6012, 2010.
[4] T. Amtoft, J. Hatcliff, E. Rodrı́guez, Robby, J. Hoag, and D. Greve, “Specification and checking of software contracts for conditional information
flow,” in Formal Methods, ser. LNCS, vol. 5014, 2008.
[5] A. Askarov and A. C. Myers, “Attacker control and impact for
confidentiality and integrity,” Logical Methods in Computer Science,
vol. 7, no. 3, 2011.
[6] A. Askarov and A. Sabelfeld, “Gradual release: Unifying declassification,
encryption and key release policies,” in IEEE Symposium on Security
and Privacy, 2007.
[7] ——, “Tight enforcement of information-release policies for dynamic
languages,” in IEEE Computer Security Foundations Symposium, 2009.
[8] T. H. Austin and C. Flanagan, “Efficient purely-dynamic information flow
analysis,” in ACM Workshop on Programming Languages and Analysis
for Security, vol. 44, no. 8, Aug. 2009, pp. 20–31.
[9] ——, “Permissive Dynamic Information Flow Analysis,” in ACM
Workshop on Programming Languages and Analysis for Security. ACM,
2010, pp. 1–12.
[10] M. Balliu, M. Dam, and G. Le Guernic, “Epistemic temporal logic
for information flow security,” in ACM Workshop on Programming
Languages and Analysis for Security (PLAS), 2011.
[11] A. Banerjee, D. A. Naumann, and S. Rosenberg, “Expressive Declassification Policies and Modular Static Enforcement,” in IEEE Symposium
on Security and Privacy. IEEE, 2008, pp. 339–353.
[12] B. Beckert, D. Bruns, V. Klebanov, C. Scheben, P. H. Schmitt, and
M. Ulbrich, “Information flow in object-oriented software,” in LogicBased Program Synthesis and Transformation LOPSTR, ser. LNCS, no.
8901, 2014.

13

[13] L. Bello, D. Hedin, and A. Sabelfeld, “Value sensitivity and observable
abstract values for information flow control,” in Logic for Programming,
Artificial Intelligence, and Reasoning (LPAR), 2015, pp. 63–78.
[14] N. Benton, “Simple relational correctness proofs for static analyses
and program transformations,” in ACM Symposium on Principles of
Programming Languages, 2004.
[15] L. Beringer, “End-to-end multilevel hybrid information flow control,” in
Asian Symposium on Programming Languages and Systems (APLAS),
ser. LNCS, 2012, vol. 7705, pp. 50–65.
[16] F. Besson, N. Bielova, and T. Jensen, “Hybrid information flow monitoring against web tracking,” in IEEE Computer Security Foundations
Symposium. IEEE, 2013, pp. 240–254.
[17] A. Bichhawat, V. Rajani, D. Garg, and C. Hammer, “Generalizing
permissive-upgrade in dynamic information flow analysis,” in ACM
Workshop on Programming Languages and Analysis for Security (PLAS),
2014.
[18] ——, “Information flow control in WebKit’s JavaScript bytecode,” in
Principles of Security and Trust (POST), 2014, pp. 159–178.
[19] N. Bielova and T. Rezk, “A Taxonomy of Information Flow Monitors,”
in POST, 2016, to appear.
[20] N. Broberg and D. Sands, “Flow Locks: Towards a Core Calculus for
Dynamic Flow Policies,” in European Symposium on Programming.
Berlin, Heidelberg: Springer Berlin Heidelberg, 2006, pp. 180–196.
[21] N. Broberg, B. van Delft, and D. Sands, “Paragon for Practical
Programming with Information-Flow Control,” in Asian Symposium on
Programming Languages and Systems, 2013, pp. 217–232.
[22] D. Cachera and D. Pichardie, “A Certified Denotational Abstract
Interpreter,” in Interactive Theorem Proving (ITP), 2010, pp. 9–24.
[23] A. Chudnov, G. Kuan, and D. A. Naumann, “Information Flow Monitoring as Abstract Interpretation for Relational Logic,” in IEEE Computer
Security Foundations Symposium. IEEE, 2014, pp. 48–62.
[24] A. Chudnov and D. A. Naumann, “Inlined information flow monitoring
for JavaScript,” in ACM SIGSAC conference on Computer and Communications Security, 2015, pp. 629–643.
[25] M. R. Clarkson and F. B. Schneider, “Hyperproperties.” Journal of
Computer Security, vol. 18, no. 6, pp. 1157–1210, 2010.
[26] A. Cortesi, G. Costantini, and P. Ferrara, “A Survey on Product Operators
in Abstract Interpretation.” Festschrift for Dave Schmidt, vol. 129, pp.
325–336, 2013.
[27] P. Cousot, “The calculational design of a generic abstract interpreter,” in
Calculational System Design, M. Broy and R. Steinbrüggen, Eds. NATO
ASI Series F. IOS Press, Amsterdam, 1999, vol. 173, pp. 421–506.
[28] P. Cousot and R. Cousot, “Abstract interpretation: a unified lattice model
for static analysis of programs by construction or approximation of
fixpoints,” in ACM Symposium on Principles of Programming Languages,
New York, New York, USA, Jan. 1977, pp. 238–252.
[29] ——, “Systematic design of program analysis frameworks,” in ACM
Symposium on Principles of Programming Languages. ACM, 1979, pp.
269–282.
[30] P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and
X. Rival, “Combination of abstractions in the ASTRÉE static analyzer,”
in Asian Computing Science Conference (ASIAN), 2006, pp. 272–300.
[31] P. Cousot and N. Halbwachs, “Automatic Discovery of Linear Restraints
Among Variables of a Program.” in ACM Symposium on Principles of
Programming Languages, 1978, pp. 84–96.
[32] D. Darais, M. Might, and D. V. Horn, “Galois transformers and modular
abstract interpreters: reusable metatheory for program analysis,” in
Object-Oriented Programming, Systems, Languages, and Applications
(OOPSLA), 2015.
[33] A. A. de Amorim, N. Collins, A. DeHon, D. Demange, C. Hritcu,
D. Pichardie, B. C. Pierce, R. Pollack, and A. Tolmach, “A verified
information-flow architecture,” in ACM Symposium on Principles of
Programming Languages, 2014, pp. 165–178.
[34] R. Giacobazzi and I. Mastroeni, “Adjoining classified and unclassified
information by abstract interpretation,” Journal of Computer Security,
vol. 18, no. 5, 2010.
[35] P. Granger, “Static analysis of arithmetical congruences,” International
Journal of Computer Mathematics, 1989.
[36] ——, “Improving the Results of Static Analyses Programs by Local
Decreasing Iteration.” in Foundations of Software Technology and
Theoretical Computer Science, vol. 652, 1992, pp. 68–79.
[37] D. Hedin, L. Bello, and A. Sabelfeld, “Value-sensitive hybrid information
flow control for a javascript-like language,” in IEEE Computer Security
Foundations Symposium, 2015, pp. 351–365.

[38] J.-H. Jourdan, V. Laporte, S. Blazy, X. Leroy, and D. Pichardie, “A
Formally-Verified C Static Analyzer,” in ACM Symposium on Principles
of Programming Languages. New York, New York, USA: ACM Press,
2015, pp. 247–259.
[39] M. Kindahl, “The galois connection in interval analysis,” Uppsala University, Sweden, Tech. Rep., 1994, http://user.it.uu.se/∼matkin/interval.ps.gz.
[40] M. Kovács, H. Seidl, and B. Finkbeiner, “Relational abstract interpretation
for the verification of 2-hypersafety properties,” in ACM SIGSAC
conference on Computer and Communications Security. New York,
New York, USA: ACM Press, 2013, pp. 211–222.
[41] G. Le Guernic, “Precise dynamic verification of confidentiality,” in
Proceedings of the 5th International Verification Workshop in connection
with IJCAR, 2008.
[42] G. Le Guernic, A. Banerjee, T. P. Jensen, and D. A. Schmidt, “Automatabased confidentiality monitoring,” in Asian Computing Science Conference (ASIAN). Springer-Verlag, Dec. 2006.
[43] P. Mardziel, S. Magill, M. Hicks, and M. Srivatsa, “Dynamic enforcement
of knowledge-based security policies,” in IEEE Computer Security
Foundations Symposium. IEEE, 2011, pp. 114–128.
[44] ——, “Dynamic enforcement of knowledge-based security policies
using probabilistic abstract interpretation,” Journal of Computer Security,
vol. 21, no. 4, pp. 463–532, Jan. 2013.
[45] L. Mauborgne and X. Rival, “Trace partitioning in abstract interpretation
based static analyzers,” in European Symposium on Programming. Berlin,
Heidelberg: Springer-Verlag, Apr. 2005, pp. 5–20.
[46] S. Moore and S. Chong, “Static Analysis for Efficient Hybrid InformationFlow Control,” in IEEE Computer Security Foundations Symposium.
IEEE, 2011, pp. 146–160.
[47] C. Müller, M. Kovács, and H. Seidl, “An Analysis of Universal
Information Flow Based on Self-Composition,” in IEEE Computer
Security Foundations Symposium. IEEE, 2015, pp. 380–393.
[48] A. C. Myers, “JFlow: Practical Mostly-Static Information Flow Control.”
in ACM Symposium on Principles of Programming Languages, 1999, pp.
228–241.
[49] A. C. Myers, N. Nystrom, L. Zheng, and S. Zdancewic, Jif: Java Information Flow, May 2001, software release. http://www.cs.cornell.edu/jif.
[50] A. Nanevski, A. Banerjee, and D. Garg, “Dependent type theory for
verification of information flow and access control policies,” ACM Trans.
Program. Lang. Syst., vol. 35, no. 2, 2013.
[51] D. Pichardie, “Modular Proof Principles for Parameterised Concretizations,” in Construction and Analysis of Safe, Secure, and Interoperable
Smart Devices Second International Workshop, CASSIS , Revised Selected
Papers, G. Barthe, B. Grégoire, M. Huisman, and J.-L. Lanet, Eds.
Springer Berlin Heidelberg, 2006, pp. 138–154.
[52] A. Russo and A. Sabelfeld, “Dynamic vs. Static Flow-Sensitive Security
Analysis,” in IEEE Computer Security Foundations Symposium. IEEE,
2010, pp. 186–199.
[53] A. Sabelfeld and D. Sands, “Declassification: Dimensions and principles,”
Journal of Computer Security, vol. 17, no. 5, Oct. 2009.
[54] J. Santos and T. Rezk, “An information flow monitor-inlining compiler
for securing a core of javascript,” in ICT Systems Security and Privacy
Protection, ser. IFIP Advances in Information and Communication
Technology, 2014, vol. 428.
[55] F. B. Schneider, “Enforceable security policies,” ACM Transactions on
Information and System Security, vol. 3, no. 1, pp. 30–50, Feb. 2000.
[56] P. Shroff, S. F. Smith, and M. Thober, “Dynamic dependency monitoring
to secure information flow,” in IEEE Computer Security Foundations
Symposium, 2007, pp. 203–217.
[57] D. Volpano, C. Irvine, and G. Smith, “A Sound Type System for Secure
Flow Analysis,” Journal of Computer Security, vol. 4, no. 2-3, pp. 167–
187, 1996.
[58] G. Winskel, The Formal Semantics of Programming Languages: an
Introduction. Cambridge, 1993.
[59] S. A. Zdancewic, “Programming languages for information security,”
Ph.D. dissertation, Cornell University, 2002.
[60] S. Zdancewic and A. C. Myers, “Robust declassification,” in IEEE
Computer Security Foundations Workshop, 2001, pp. 15–23.

14

A PPENDIX A

A LTERNATIVE I DEAL M ONITOR

The alternative ideal monitor relies on an alternative collecting semantics. In a nutshell, both collecting semantics
are instrumented to keep track of a boolean a, that signals
if annotation commands are allowed in the current context.
Intuitively, in a low context, the boolean a is set to true, meaning
that annotation commands are allowed. Otherwise, the boolean
a is set to false, signifying that the current context is high, and
disallowing annotation commands.
How does the monitoring semantics determine the security context? It simply checks what happens for branching
commands: Are we already in a high security context? if not,
are there some states that follow a conditional branch that is
different from the one taken by the major state? If there are
some states that follow a different control path, this means
that both conditional branches ought to be treated as high
branches. If the conditional is in a low security context and no
minor states follow a different conditional branch, then both
conditional branches are to be treated as low branches.
In high conditional branches, both the monitoring semantics
and the collecting semantics return an error if an annotation
command is encountered. This way, the monitoring semantics
implicitly signals an alignment failure, as proposed in [23].
Figures 5 and 6 introduce the alternative ideal monitor and
the alternative collecting semantics. We conjecture that this
alternative ideal monitor returns an error iff. the monitor that
is defined in [23] in terms of a tracking set results in either
an alignment failure or an assertion failure. This conjecture
remains to be proved.

LcMann=a
,
σ

LskipMann=a
Σ,Σ
σ

Lc1 ; c2 Mann=a
Σ , Lc2 Mann=a
σ
Jc1 Kσ
Lassert

◦

Lid := eMann=a
Σ , {Jid := eKτ | τ ∈ Σ}
σ
(
{τ ∈ Σ | σpτ |= Φ} if a = true
Lassume ΦMann=a
Σ,
σ
if a = f alse

Lc1 Mann=a
Σ
σ

ΦMann=a
Σ
σ

,

(
Σ

if ∀τ ∈ Σ, σpτ |= Φ and a = true
otherwise

(

Lif b then c1 else

c0 Mann=a
Σ
σ

0

0

∧a ◦
Lc1 Mann=a
grdbσ Σ t ⦃c0 ⦄ann=a ∧ a
σ
,
ann=a ∧ a0 ◦
∧ a0
⦃c1 ⦄
grdb Σ t Lc0 Mann=a
σ
(
(grd¬b (Σ) = ∅) if JbKσ
with a0 ,
(grdb (Σ) = ∅)
if ¬JbKσ

Lwhile b do cMann=a
Σ , snd
σ



grd¬b Σ
¬b
◦ grdσ Σ
◦

if JbKσ
otherwise



4̇×v̇
lfpλ(σ,Σ).(⊥,∅)
G a (σ, Σ)

(
if ¬JbKσ
σ, ⦃while b do c⦄ann=a Σ
with G (w) , λ(σ, Σ).
ann=a
Σ) otherwise
w (JcKσ, Lif b then c else skipMσ
a

Figure 5.

⦃skip⦄ann=a Σ = Σ

⦃id := e⦄ann=a Σ = {τ [id 7→ JeKτ ] | τ ∈ Σ}

⦃if b then c1 else c2 ⦄ann=a Σ = ⦃c1 ⦄ann=a
(
⦃assert Φ⦄ann=a Σ =

Alternative ideal monitor

Σ if a
if ¬ a

◦

grdb (Σ) t ⦃c2 ⦄ann=a

◦

⦃c1 ; c2 ⦄ann=a Σ = ⦃c2 ⦄ann=a

grd¬b (Σ)

⦃c1 ⦄ann=a Σ
(
Σ if a
ann=a
⦃assume Φ⦄
Σ=
if ¬ a
◦



ann=a
⦃while b do c⦄ann=a Σ = grd¬b lfpv
Σ ⦃if b then c else skip⦄
grdb (Σ) , {τ ∈ Σ | JbKτ = true}
Figure 6.

Alternative collecting semantics

15

A PPENDIX B

TABLE OF S YMBOLS

States , V ar * Z mappings from vars to integers
⊥ undefined outcome

States⊥ , States ∪ {⊥} set of outcomes
σ ∈ States proper state
σ̂ ∈ States⊥ outcome

security violation, or fault

P(States) powerset of States

P (States) , P(States) ∪ { }

Σ ∈ P(States) set of states

Σ̂ ∈ P (States) set of states or fault

Φ, Ψ ∈ L relational formulas

L the set of relational formulas

∆ ∈ P(L) a set of relational formulas

P (L) , P(L) ∪ { }
ˆ ∈ P (L) a set of relational formulas of fault
∆

JcK ∈ States⊥ → States⊥ denotational sem. of com.

JeK ∈ States → Z denotational sem. of exp.

⦃c⦄ ∈ P (States) → P (States) collecting sem.

LcMσ ∈ P (States) → P (States) ideal monitor sem.

DLcM] purely-dynamic monitor.

MLcM] hybrid mon. with modified vars

ILcM] hybrid mon. with modified intervals

D⦃c⦄] static analysis for purely-dynamic mon.

M⦃c⦄]c0 static analysis for hybrid mon. with modified vars

I⦃c⦄]σ,σ0 static analysis for hybrid mon. with intervals
v set inclusion lifted to P (States)
t set union lifted to P (States)

u set intersection lifted to P (States)

v] “includes” (⊇) lifted to P (L)

t] set intersection lifted to P (L)
u] set union lifted to P (L)
4 approximation order

ασ ∈ P (States) → P (L) abstraction function param. by σ

γσ ∈ P (L) → P (States) concretisation function param. by σ

αB ∈ States ×P (States) → States ×P (L) generalised ασ
γ B ∈ States ×P (L) → States ×P (States) generalised γσ

16

A PPENDIX C
C-A



b
= grd¬b Σ ∪ gn⦃c⦄◦grd (Σ)
[
= (for all Σ, gnΣ =
(⦃c⦄ ◦ grdb )(k) (Σ) )

BACKGROUND

Collecting Semantics

Lemma 1 . The displayed equations define the same semantics
as Equation (2).

0≤k≤n−1

grd

b
◦
lfp⊆
∅ λX. Σ ∪ ⦃c⦄ grd (X) =

lfp⊆
∅ λX.Σ ∪ ⦃if b then c else skip⦄X

Indeed, let the sequence (fnΣ )n≥0 be defined as:

= {σ[id 7→ JeKσ] | σ ∈ Σ and Jid := eKσ 6= ⊥}

f0Σ , ∅

= {σ[id 7→ JeKσ] | σ ∈ Σ}

Σ
fn+1
, Σ ∪ ⦃if b then c else skip⦄fnΣ

2 – Case: skip
1 – Case: loops.
1.1 – Let us first prove the following intermediate result:

Therefore, by induction on n ∈ N, it holds that fn = gn :
- f0Σ = g0Σ = ∅.
- let n ∈ N, such that fnΣ = gnΣ . Then:

⦃while b do c⦄Σ =
grd

lfp⊆
∅ λX. Σ

b



1.2 – Let us now prove that :

⦃id := e⦄Σ , {Jid := eKσ | σ ∈ Σ and Jid := eKσ 6= ⊥}



Σ
gn+1

Σ
= yn+1

Proof. The proof of equivalence of both collecting semantics
is by structural induction on commands. We feature in this proof
one simple case (assignments) as well as the most interesting
case that is the case of while loops.
1 – Case: assignments

¬b

¬b

Σ
gn+1
= Σ ∪ ⦃c⦄ ◦ grdb (gn )



∪ ⦃c⦄ ◦ grd (X) .

= (grd¬b (gn ) ⊆ gn ⊆ gn+1 )

Σ ∪ ⦃c⦄ ◦ grdb (gn ) ∪ grd¬b (gn )

Indeed, let the sequence (xΣ
n )n≥0 be defined as:

= Σ ∪ ⦃if b then c else skip⦄gn

(n)
xΣ
(⊥)(σ) ∈ States | σ ∈ Σ}
n , {F

Notice that for all σ ∈ Σ, the sequence (F (n) (⊥)(σ))n≥0
converges and is equal to the evaluation of the while loop in
the state σ (Jwhile b do cKσ = F (∞) (⊥)(σ)), by definition of
the denotational semantics of loops.
Let also the sequences (ynΣ )n≥0 and (gnΣ )n≥0 be defined as:

ynΣ , grd¬b gnΣ

Σ
gn+1
, Σ ∪ ⦃c⦄ ◦ grdb gnΣ
g0Σ , ∅

= (By induction hypothesis)
=

Σ ∪ ⦃if b then c else skip⦄fnΣ

Σ
fn+1

1.3 – Finally,
⦃while b do c⦄Σ


b
◦ grd (X)
= grd¬b lfp⊆
⦃c⦄
λX.
Σ
∪
∅
= grd¬b lfp⊆
∅ λX.

Σ ∪ ⦃if b then c else skip⦄X

Then, it holds that:

= grd¬b

Σ
∀Σ ∈ P(States), ∀n ∈ N, xΣ
n = yn .


lfp⊆
Σ ⦃if b then c else skip⦄

Indeed, the proof proceeds by induction on n.
Σ
- xΣ
0 = ∅ = y0
Σ
- Let n ∈ N such that: ∀Σ ∈ P(States), xΣ
n = yn . Then:
(n+1)
xΣ
(⊥)(σ) ∈ States | σ ∈ Σ}
n+1 = {F

= grd¬b (Σ) ∪

{F (n) (⊥)(JcKσ) ∈ States | σ ∈ grdb (Σ)}

= grd¬b (Σ) ∪

{F (n) (⊥)(τ ) ∈ States | τ ∈ ⦃c⦄ ◦ grdb (Σ)}
b

◦grd
= grd¬b (Σ) ∪ x⦃c⦄
n

(Σ)

= (By induction hypothesis)
b

grd¬b (Σ) ∪ yn⦃c⦄◦grd

(Σ)
b

= (By definition of yn⦃c⦄◦grd (Σ) )


b
grd¬b (Σ) ∪ grd¬b gn⦃c⦄◦grd (Σ)
17



A PPENDIX D M ONITORING C OLLECTING S EMANTICS
Lemma 2 . For all annotation-free commands c, all σ ∈ States
such that JcKσ 6= ⊥, and all sets Σ ⊆ States, it holds that

Finally, we deduce that:
Lwhile b do cMσ Σ


= grd¬b lfp⊆
⦃if
b
then
c
else
skip⦄
Σ

LcMσ Σ = ⦃c⦄Σ

= ⦃while b do c⦄Σ

Proof.
The proof is by structural induction on commands.
1 – Cases skip and assignments stem from the definition of
the collecting semantics and the monitoring semantics.
2 – Case: sequence c1 ; c2
Let σ, σ 0 ∈ States, such that Jc1 ; c2 Kσ = σ 0 . Then in
particular, we know that Jc1 Kσ ∈ States, meaning that it
terminates.
Lc1 ; c2 Mσ Σ = Lc2 MJc1 Kσ

◦

Notice that if c is an assertion-free command, we have
LcMσ Σ ⊆ ⦃c⦄Σ. The proof is exactly the same, and the
only difference proceeds by noticing that Lassume ΦMσ Σ ⊆
⦃assume Φ⦄Σ.
Let us now prove the soundness of the monitoring semantics
wrt. TINI.
Theorem 1 . Let in and out be two sets of variables and c
be an annotation-free command. Let command ĉ be defined
as assume Ain; c ; assert Aout. For all σ1 , σ10 ∈ States such
that JcKσ1 = σ10 , we have LĉMσ1 States 6= iff.

Lc1 Mσ Σ

= (By induction twice, since Jc1 Kσ ∈ States)
⦃c2 ⦄ ◦ ⦃c1 ⦄Σ

∀σ2 , σ20 ∈ States, JcKσ2 = σ20 ∧ σ1 =in σ2 =⇒ σ10 =out σ20

= ⦃c1 ; c2 ⦄Σ
3 – Case: conditionals
Let σ, σ 0 ∈ States such that Jif b then c1 else c2 Kσ = σ 0
Let us also assume that JbKσ = true.
Then:
LcMσ Σ = Lc1 Mσ

◦

Proof.
Let σ1 , σ10 ∈ States such that JcKσ1 = σ10 .
Assume LĉMσ1 States 6= .
Let σ2 , σ20 ∈ States and assume σ1 =in σ2 , and prove
σ10 =out σ20 .
Therefore, we have:

grdb (Σ) ∪ ⦃c2 ⦄ ◦ grd¬b (Σ)

(By induction on c1 )

⦃c1 ⦄Σ ◦ grdb (Σ) ∪ ⦃c2 ⦄ ◦ grd¬b (Σ)

Lassume Ain; c; assert AoutMσ1 States
= Lc; assert AoutMσ1

= ⦃c⦄Σ

= Lassert AoutMσ10

4 – Case: loops
Let σ, σ 0 ∈ States such that Jwhile b do cKσ = σ 0 . Since
the loop terminates, there exists a smallest k ∈ N∗ such that
F (k) (σ) = σ 0 . The natural k is intuitively the number of
executed iterations that must be executed before exiting the
loop.
Therefore:

◦

6= (by assumption)

◦

Lassume AinMσ1 States

LcMσ1

◦

Lassume AinMσ1 States

Notice that σ2 ∈ Lassume AinMσ1 States, since σ1 =in σ2 .
Therefore, σ20 ∈ LcMσ1 ◦ Lassume AinMσ1 States, since the
monitoring semantics is equivalent to the collecting semantics
for annotation-free commands (Lemma 2), and the collecting
semantics is the lifting of the denotational semantics over a
set of states (Lemma 1 and σ20 ∈ States).
This means that Lassert AoutMσ10 {σ20 } =
6
, by monotonicity
of the monitoring semantics. Therefore:

Lwhile b do cMσ Σ


= snd G (k) (λ(σ, Σ).(⊥, ∅))(σ, Σ)

= (Σ0 , L(if b then c1 else skip)(k−1) Mσ Σ)


grd¬b lfp⊆
Σ0 ⦃if b then c else skip⦄

σ10 =out σ20

Notice that we write (c)(k−1) as a shorthand for the sequence
of commands c; c; c; c; . . ., where c is sequentially composed
with itself k − 1 times.
Additionally, by using the same proof as for conditionals,
we have:

– Case TINI =⇒ LĉMσ1 States 6= :
Assume for all σ2 , σ20 ∈ States such that JcKσ2 = σ20 , then
σ1 =in σ2 =⇒ σ10 =out σ20 . Prove LĉMσ1 States 6= .
Note that:

Σ0 = ⦃(if b then c1 else skip)(k−1) ⦄Σ

∀τ ∈ Lassume AinMσ1 States, σ1 =in τ

(k−1)

= ⦃if b then c1 else skip⦄

Σ

Therefore, ∀τ 0 ∈ LcM ◦ Lassume AinMσ1 States, ∃τ ∈
Lassume AinMσ1 States such that τ 0 = JcKτ and σ =in τ .
Thus, we deduce by assumption that ∀τ 0 ∈ LcM ◦
Lassume AinMσ1 States, σ 0 =out τ 0 .
Consequently, it holds that:

Therefore, the fixpoint over Σ0 can be formulated as a
fixpoint over Σ:
lfp⊆
Σ0 ⦃if b then c else skip⦄
= lfp⊆
Σ ⦃if b then c else skip⦄

Lassert AoutMσ0
18

◦

LcM

◦

Lassume AinMσ1 States 6= .

Lemma 10 The monitoring semantics is monotone. For all
major states σ̂ ∈ States⊥ , it holds that:
∀Σ̂, Σ̂0 ∈ P (L),

Σ̂ v Σ̂0 =⇒ LcMσ̂ Σ̂ v LcMσ̂ Σ̂0

Proof.
The monitoring semantics is monotone, since the collecting
semantics is monotone, and the monitoring semantics of both
annotations is also monotone. Notice in particular that the
monotonicity of assert annotations stems from the extension
of the partial order ⊆ to let be the top element of P (L).

19

A PPENDIX E

A BSTRACT D OMAIN OF R ELATIONAL
F ORMULAS

–
ασ

Lemma 3 . For all σ ∈ States, the pair (ασ , γσ ) is a Galois
γσ
−−
−−
−
− (P (L); v] ). That is,
connection: (P (States); v) ←
−−
→
ασ
∀Σ ∈ P (States), ∀∆ ∈ P (L):
ασ (Σ) v ∆ ⇐⇒ Σ v] γσ (∆)

LcMσ0

=⇒ ∀τ ∈ Σ, τ ∈ γσ (∆)
=⇒ Σ ⊆ γσ (∆)

– Case Σ ⊆ γσ (∆) =⇒ ∆ ⊆ ασ (Σ):
Σ ⊆ γσ (∆) =⇒ ∀τ ∈ Σ, τ ∈ γσ (∆)

=⇒ ∀τ ∈ Σ, ∀Φ ∈ ∆, σpτ |= Φ

=⇒ ∀Φ ∈ ∆, Φ ∈ ασ (Σ)

=⇒ ∆ ⊆ ασ (Σ)

Lemma 4 Soundness conditions. Consider any c, σ, σ 0 such
that σ 0 = JcKσ. Equation (4) is equivalent to each of the
following:
]

LcMσ v̇ LcM]σ

◦

ασ

Proof.
Let σ0 , σ ∈ Σ such that σ = JcKσ0 . The best abstraction of
the state transformer LcMσ0 consists in concretising an abstract
state ∆, applying LcMσ0 and then abstracting again using ασ :
ασ ◦ LcMσ0 ◦ γσ0 . Therefore, the monitoring abstract semantics
is sound if it holds that:
LcMσ0

◦

◦

◦

γσ0

◦

ασ0 v̇ γσ

γσ ◦ LcM]σ0 ◦
]

LcMσ0 v̇ ασ

=⇒ (ασ
ασ

◦

LcM]σ0
◦

◦

ασ0

ασ0 being extensive)

ασ0

◦

◦

◦

γσ

γσ reductive)
]

LcMσ0 v̇ LcM]σ0

◦

◦

LcM]σ0

]

γσ0 v̇ LcM]σ0 .

Let us now prove the equivalence of the 3 conditions.
20

◦

ασ0

ασ0

–
ασ

◦

]

LcMσ0 v̇ LcM]σ0

◦

ασ0

=⇒ (By monotony)
ασ
ασ

=⇒ ∀τ ∈ Σ, ∀Φ ∈ ∆, σpτ |= Φ

◦

LcM]σ0

LcM]σ0

◦

LcMσ0

◦

LcMσ0

◦

]

γσ0 v̇ LcM]σ0

=⇒ (By monotony and ασ0

ασ (Σ) ⊇ ∆ =⇒ ∆ ⊆ {Φ | ∀τ ∈ Σ, σpτ |= Φ}

ασ

◦

ασ

– Case ασ (Σ) ⊇ ∆ =⇒ Σ ⊆ γσ (∆):

◦

γσ0 v̇ γσ

◦

=⇒ (By monotony)

ασ (Σ) ⊇ ∆ ⇐⇒ Σ ⊆ γσ (∆).

ασ0

◦

LcMσ0 v̇

Proof.
Notice first that if Σ = , then ασ ( ) v] ∆ implies ∆ = ,
therefore Σ v γσ (∆). Additionally, v γσ (∆) also implies
∆ = , therefore ασ (Σ) v] ∆.
Also, if ∆ = , then both Σ v γσ (∆) and ασ (Σ) v] ∆ are
equivalent since they both hold.
Let us now assume Σ ∈ States and ∆ ∈ L, and prove that:

and

γσ0 v̇ γσ

=⇒ (By monotony and γσ0

γσ (∆) , {τ ∈ States | ∀Φ ∈ ∆, σpτ |= Φ}.

LcM]σ

◦

LcMσ0

γσ ∈ P (L) → P (States)

◦

LcMσ0

=⇒ (By monotony)

ασ (Σ) , {Φ | ∀τ ∈ Σ, σpτ |= Φ}.

γσ v̇ γσ0

◦

–

ασ ∈ P (States) → P (L)

◦

]

γσ0 v̇ LcM]σ0

LcMσ0

=⇒ ((ασ , γσ ) is a Galois connection)

Let us recall the definitions of ασ and γσ :

LcMσ

◦

◦

]

γσ0 v̇ LcM]σ0

◦

ασ0

◦

γσ0 being reductive)

◦

γσ0

A PPENDIX F
F-A

2.1 – Note that ∀Φ ∈ ∆, such that id 6∈ fv(Φ), it holds
that [23, Lemma 2 in Section II.B]:

M ONITOR D ERIVATION

Purely-Dynamic Monitor

σpτ |= Φ =⇒ σ 0 pτ [id 7→ JeKτ ] |= Φ.

We first start by proving the soundness of the abstract static
analysis that the purely-dynamic monitor relies on.
Lemma 5 soundness of D⦃ − ⦄] . For all c, σ, σ 0 ∈ States,
]
it holds that: ασ0 ◦ ⦃c⦄ ◦ γσ v̇ D⦃c⦄] .
Let us recall the definition of this abstract static semantics:

Therefore, ∀Φ ∈ ∆ such that id 6∈ fv(Φ), it holds that:
Φ ∈ ασ0


τ ∈ γσ (∆) ∧ (∆ ⇒] Ae)

⦃c⦄ ∈ P (L) → P (L)


if ∆ =

⦃c⦄] ∆ , L if ∆ = L


∅ otherwise

=⇒ σ[id 7→ JeKσ]pτ [id 7→ JeKτ ] |= Aid

=⇒ (since σ 0 = σ[id 7→ JeKσ])
σ 0 pτ [id 7→ JeKτ ] |= Aid

It is worthwhile to note that this proof explicitly uses the fact
that σ 0 is the result of evaluation of the assignment id:=e
on σ. This means that if we were to derive an abstract static
semantics tracking relational formulas, we would not be able to
deduce Ae, even if ∆ ⇒] Ae. This is because we have no way
of relating the abstraction of relational formulas wrt. σ to an
abstraction of relational formulas wrt. σ 0 , without additional
information.
Therefore, if ∆ ⇒] Ae, then it holds that:

Proof.
Let σ, σ 0 ∈ States.
Notice first that ⦃c⦄] = , therefore
◦

⦃c⦄ ◦ γσ ( ) v] ⦃c⦄] .

Let us now assume that ∆ ∈ P(L).
If ∆ = L, and since γσ (L) = ∅ (L contains at least an
expression e and its negation ¬e, therefore L is concretised to
the empty set), we have:
ασ0

◦

⦃c⦄ ◦ γσ (L) = ασ0

◦

Aid ∈ ασ0

⦃c⦄∅ = ασ0 (∅) = L

◦

ασ0

⦃c⦄ ◦ γσ (∆) v] ∅

◦

LcMσ

◦

Lid := eMσ

◦

ασ0

]

γσ v̇ DLcM]σ

⦃c⦄ ◦ γσ ( ) =

◦

LskipMσ

◦

◦

Lid := eMσ

= ασ0

◦

= ασ0

◦

◦

γσ (∆)

⊇∆

ασ 0

◦

◦

◦

⦃c2 ⦄ ◦ grd¬b
Lc1 Mσ
◦

grdb

◦

γσ (∆)

γσ (∆) ∪

γσ (∆)

◦

◦

γσ (∆) ∩

⦃c2 ⦄ ◦ grd¬b

◦

Lc1 Mσ

◦

grdb

◦

◦

γσ (∆)

γσ (∆)

⊇ (by monotonicity and γσ
α

σ0

◦

Lc1 Mσ ◦

γσ ◦

ασ

grdb

ασ ◦

◦

ασ being extensive)

grdb

◦

γσ (∆)

⊇ (by induction hypothesis)
Lc1 M]σ

γσ (∆)

Lid := eMσ

grdb ◦

We will now treat both branches separately before merging
them.
3.1 – Then-branch:

2 – Case: assignments
Let σ, σ 0 ∈ States such that σ 0 = Jid := eKσ. Then:
◦

Lc1 Mσ ◦

ασ 0

, LskipM]σ ∆

ασ0

Lif b then c1 else c2 Mσ

= ασ0

, LcM]σ

γσ (∆) = ασ

◦

= ασ0

1 – Case: skip
ασ

if ∆ ⇒] Ae
otherwise

3 – Case: conditionals
Let σ, σ 0 ∈ States such that σ 0 = Jif b then c1 else c2 Kσ.
Let us consider the case that JbKσ = true. Then:

Proof.
Let us first rule out the error case:
ασ0

γσ (∆)

◦

, Lid := eM]σ ∆

Theorem 2 . The abstract monitoring semantics DLcM]σ of the
purely-dynamic monitor is sound. For all commands c, for all
σ, σ 0 ∈ States such that σ 0 = JcKσ, it holds that:
◦

{τ [id 7→ JeKτ ] | ∀Φ ∈ ∆, σpτ |= Φ}.

(
Aid
⊇ {Φ ∈ ∆ | id 6∈ fv(Φ)} ∪
∅

Let us now prove the soundness of the abstract semantics
of the purely-dynamic monitor we derive.

ασ0

◦

2.3 – Finally:

Additionally, we can always approximate an element of
P(L) by the top element of P(L). Therefore, it holds that:
ασ0

{τ [id 7→ JeKτ ] | ∀Φ ∈ ∆, σpτ |= Φ}.

2.2 – Otherwise, it holds that:

]

ασ0

◦

{τ | ∀Φ ∈ ∆, σpτ |= Φ}

◦

Note that grdb

{τ [id 7→ JeKτ ] | ∀Φ ∈ ∆, σpτ |= Φ}

ασ
21

◦

◦

◦

◦

γσ (∆)

γσ (∆) ⊆ γσ (∆), therefore:

grdb

◦

γσ (∆) ⊇ ασ

◦

γσ (∆) ⊇ ∆

Let σ1 = Jc1 Kσ and σ2 = Jc2 Kσ1 . Then:

Additionally, since JbKσ = true, and also:
∀τ ∈ grdb

ασ2

γσ (∆), JbKτ = true

◦

◦

grdb

◦

◦

grdb

ασ2

◦

Lc1 Mσ

◦

grdb

◦

◦

⦃c2 ⦄ ◦ grd¬b

ασ

◦

⦃c2 ⦄ ◦ γσ

◦

ασ

◦

◦

=

γσ (∆) ⊇ Lc1 M]σ (∆ ∪ {Bb}).

Lc1 Mσ

◦

γσ (∆)

ασ1 is extensive)

Lc2 Mσ1

◦

γσ1

◦

ασ1

◦

◦

Lc1 Mσ

◦

γσ (∆)

Lc1 M]σ ∆

Lassume ΦMσ
ασ ◦

◦

γσ (∆)

{τ ∈ γσ (∆) | σpτ |= Φ}

⊇ ∆ ∪ {Φ}

, Lassume ΦM]σ ∆
6 – Case: assertions

⊇ (by monotonicity and γσ
ασ0

◦

5 – Case: assumptions

γσ (∆)

◦

γσ (∆)

Lc2 Mσ1

, Lc1 ; c2 M]σ ∆

3.2 – Else-branch:
ασ0

◦

Lc2 M]σ1

Therefore, in the then-branch we have:
ασ0

◦

◦

⊇ (By induction hypothesis)

γσ (∆).

γσ (∆) ⊇ ∆ ∪ {Bb}

◦

◦

⊇ (γσ1

To sum up, we obtain an approximation of grdb :
ασ

Lc1 ; c2 Mσ

= ασ2

then it holds that: ∀τ ∈ grdb ◦ γσ (∆), σpτ |= Bb. Notice that
we explicitly use the assumption that the major state evaluates
to true. Therefore:
Bb ∈ ασ

◦

◦

ασ being extensive)

grd¬b

◦

ασ

γσ (∆)

Since the major state σ is assumed to evaluate to true, it
holds that:
(
L if ∆ ⇒] Ab
ασ ◦ grd¬b ◦ γσ (∆) ⊇
∆ otherwise

Lassert ΦMσ ◦ γσ (∆)
(
γσ (∆) if ∀τ ∈ γσ (∆), σpτ |= Φ
= ασ ◦
otherwise
(
∆ ∪ {Φ} if ∆ ⇒] Φ
⊇
otherwise
◦

7 – Case: loops
Therefore, in the else branch we have:
ασ0

⦃c2 ⦄ ◦ grd¬b



˙
⊆
Lwhile (e) do cMσ Σ , snd (lfp4×
G)(σ,
Σ)
λ(σ,Σ).(⊥,∅)

γσ (∆)
⦃c2 ⦄ γσ ◦ ασ ◦ grd¬b ◦ γσ (∆)
⊇α
(
L if ∆ ⇒] Ab
] ◦
⊇ ⦃c2 ⦄ λ∆.
∆ otherwise
(
L if ∆ ⇒] Ab
=
∅ otherwise
◦

σ0

◦

◦

with:

◦

G(w) , λ(σ, Σ).
(
if ¬JbKσ
σ, ⦃while b do c⦄Σ
w (JcKσ, Lif b then c else skipMσ Σ) otherwise

3.3 – Finally, we merge both approximations of the thenbranch and the else-branch:

and:
C , States ×P (States) ∪ {(⊥, ∅), (>, )}

ασ0

◦

Lif b then c1 else c2 Mσ

⊇ ασ0

◦

Lc1 Mσ

ασ0

◦

grdb

◦

◦

A , States ×P (L) ∪ {(⊥, L), (>, )}

γσ (∆)

γσ (∆) ∩

⦃c2 ⦄ ◦ grd¬b ◦ γσ (∆)
(
L if ∆ ⇒] Ab
]
⊇ Lc1 Mσ (∆ ∪ {Bb}) ∩
∅ otherwise
(
Lc1 M]σ (∆ ∪ {Bb}) if ∆ ⇒] Ab
=
∅
otherwise
◦

αB ∈ C → A


if σ, Σ = ⊥, ∅
⊥, L
B
α (σ, Σ) , >,
if σ, Σ = >,


σ, ασ (Σ) otherwise
γB ∈ A → C


if σ, ∆ = ⊥, L
⊥, ∅
B
γ (σ, ∆) , >,
if σ, ∆ = >,


σ, γσ (∆) otherwise

, (when JbKσ = true)

Lif b then c1 else c2 M]σ ∆

The case where JbKσ = f alse is symmetric.
4 – Case: sequences.
22

1 – First, we prove that (αB , γ B ) is a Galois connection:
γB

−−
−−
−
− (A ; 4 ×v] )
(C ; 4 × v) ←
−−
→
B
α

Let (σ, Σ) ∈ C , and (σ , ∆) ∈ A .
1.1 – Assume αB (σ, Σ) 4 × v] (σ 0 , ∆).
Prove (σ, Σ) 4 × v γ B (σ 0 , ∆).
If (σ, Σ) = (⊥, ∅), then it holds that (σ, Σ) 4 × v
γ B (σ 0 , ∆).
Otherwise, if (σ, Σ) = (>, ), then (σ 0 , ∆) = (>, ), and
it holds that (σ, Σ) 4 × v γ B (σ 0 , ∆).
Otherwise, if (σ, Σ) ∈ States ×P (States), then either σ =
σ 0 , or σ 0 = >. If σ 0 = top, then ∆ = and it holds that
(σ, Σ) 4 × v γ B (σ 0 , ∆). If σ = σ 0 , then ασ (Σ) ⊇ ∆ =⇒
Σ v γσ (∆) since (ασ , γσ ) is a Galois connection. Therefore,
it also holds that (σ, Σ) 4 × v γ B (σ 0 , ∆).
1.2 – Assume (σ, Σ) 4 × v γ B (σ 0 , ∆).
Prove αB (σ, Σ) 4 × v] (σ 0 , ∆).
If (σ 0 , ∆) = (⊥, L), then (σ, Σ) = (⊥, ∅), thus it holds that
B
α (σ, Σ) 4 × v] (σ 0 , ∆).
Otherwise, if (σ 0 , ∆) = (>, ), then it holds that
B
α (σ, Σ) 4 × v] (σ 0 , ∆).
Otherwise, if (σ 0 , ∆) ∈ States ×P (L), then σ 4 σ 0 implies
that either σ = ⊥, or σ = σ 0 . If σ = ⊥, then Σ = ∅ and
it holds that αB (σ, Σ) 4 × v] (σ 0 , ∆). If σ = σ 0 , then Σ v
γσ (∆) =⇒ ασ (Σ)v] ∆ since (ασ , γσ ) is a Galois connection.
Therefore, it holds that: αB (σ, Σ) 4 × v] (σ 0 , ∆).
v̇
◦ B
2 – Approximating the fixpoint lfp4×
λ(σ,Σ).(⊥,∅) G γ (σ, ∆).
2.1 – Applying the fixpoint transfer theorem:
0

αB

◦

v̇
◦ B
(lfp4̇×
λ(σ,Σ).(⊥,∅) G) γ (σ, ∆)

4 × v] (assuming G ] is a sound approximating of G)
]

v̇
]
(lfp4̇×
λ(σ,∆).(⊥,L) G )(σ, ∆)

2.2 – Deriving a sound approximation of G ] :
αB

G(w) ◦ γ B (σ, ∆)


σ, ⦃while b do c⦄γσ (∆) if ¬JbKσ
B ◦
=α
w JcKσ,



Lif b then c else skipMσ ◦ γσ (∆) oth.


σ, ασ ◦ ⦃while b do c⦄ ◦ γσ (∆) if ¬JbKσ
= αB ◦ w JcKσ,



Lif b then c else skipMσ ◦ γσ (∆) oth.


σ, ασ ◦ ⦃while b do c⦄ ◦ γσ (∆) if ¬JbKσ
]
4 × v αB ◦ w ◦ γ B ◦ αB ◦ JcKσ,



Lif b then c else skipMσ ◦ γσ (∆) oth.

σ, ασ ◦ ⦃while b do c⦄ ◦ γσ (∆) if ¬JbKσ



αB ◦ w ◦ γ B ◦ JcKσ,
4 × v]

αJcKσ ◦ Lif b then c else skipMσ ◦




γσ (∆)
oth.
◦

23


σ, ασ ◦ ⦃while b do c⦄ ◦ γσ (∆) if ¬JbKσ



w] ◦ JcKσ,
4 × v]

αJcKσ ◦ Lif b then c else skipMσ ◦




γσ (∆)
oth.


σ, ασ ◦ ⦃while b do c⦄ ◦ γσ (∆) if ¬JbKσ
]
4 × v w] ◦ JcKσ,



Lif b then c else skipM]σ ∆ oth.

(Notice that the derivation above is still generic.)

(Specialising it with the abstract static semantics now.)


σ,
if ¬JbKσ ∧ ∆ =





σ,
∆
∪
{B¬b}
if ¬JbKσ ∧ (∆ ⇒] Ab)

4 × v] σ, {B¬b}
otherwise if ¬JbKσ


] ◦

w
JcKσ,



 Lif b then c else skipM] ∆ otherwise
σ
3 – Finally,

]

4̇×v̇
snd(lfpλ(σ,∆).(⊥,L)
G ] )(σ, ∆)

Lwhile b do cM]σ ∆ ,

with:
G ] , λw] .λ(σ, ∆).


σ,
if ¬JbKσ ∧ ∆ =





if ¬JbKσ ∧ (∆ ⇒] Ab)
σ, ∆ ∪ {B¬b}
σ, {B¬b}
otherwise if ¬JbKσ


] ◦

w
JcKσ,



 Lif b then c else skipM] ∆ otherwise
σ

F-B

Hybrid Monitor with the Modified Variables

Proof.
Let Σ ∈ States and ∆ ∈ L. Let us derive a hybrid monitoring semantics relying on a static analysis over-approximating
the set of variables that may be modified by a command c.
We will consider only the case of branching instructions, since
the derivation of the abstract monitoring semantics of the other
commands is similar to the one in Theorem 2.
1 – Case : conditionals
Let σ, σ 0 ∈ States such that σ 0 = Jif b then c1 else c2 Kσ. Let
us also assume that JbKσ = true, which means that σ 0 = Jc1 Kσ.
Then, similarly to Theorem 3 we have:

We start by first proving an intermediate result, introduced
in Lemma 11. We denote by σV the restriction of the state σ
to the set V of variables. Lemma 11
Lemma 11 . ∀σ, τ, τ 0 ∈ States, ∀Φ ∈ L, ∀V ⊆ V ar, if:
1) σpτ |= Φ
2) τV = τV0
3) fv(Φ) ⊆ V
then,
σpτ 0 |= Φ
Proof. The proof of this lemma is straightforward, by
structural induction on relational formulas as well as a
structural induction on expressions, by remarking that ∀e ∈
Exp, (fv(e) ⊆ V =⇒ JeKτ = JeKτ 0 ).

ασ0

with

= ασ0

⦃c⦄ ◦ γσ (L) = ασ0

◦

ασ 0

◦

⦃c⦄ ◦ γσ ( ) = ασ0

◦

◦

⦃c⦄ = ασ0 ( ) =

ασ0

0

ασ0

◦

]

v

0

γσ ({Φ ∈ ∆ | fv(Φ) ∩ Mod(c) = ∅})

σ 0 = Jc0 Kσ, σ 0 =V ar\ Mod(c0 ) σ, and by defining ∆0 as

∆0 , {Φ ∈ ∆ | fv(Φ) ∩ Mod(c) = ∅})
{Φ ∈ ∆0 | fv(Φ) ∩ Mod(c0 ) = ∅}

= {Φ ∈ ∆ | fv(Φ) ∩ (Mod(c) ∪ Mod(c0 )) = ∅}
Theorem 3 soundness of ML−M]− . The hybrid monitor
MLcM]σ is sound in the sense of Equation (4): for all c, σ:
LcMσ

◦

]

γσ v̇ MLcM]σ

◦

γσ (∆) ∩

⦃c2 ⦄ grd¬b
◦

◦

γσ (∆)

Lc1 Mσ

◦

grdb

◦

γσ (∆) v] Lc1 M]σ (∆ ∪ {Bb}).

if ∆ ⇒] Ab
otherwise

Lif b then c1 else c2 Mσ
◦

α

Lc1 Mσ
◦

Lc1 M]σ (∆

◦

grdb

◦

∪ {Bb}) ∩

γσ (∆)

γσ (∆) ∩

⦃c2 ⦄ grd¬b
◦

◦

◦

γσ (∆)



L

Φ ∈ ∆ | ∀id ∈ fv(Φ),


id 6∈ Mod(c1 ) ∪ Mod(c2 )

if ∆ ⇒] Ab

2 – Case: loops
We rely on the generic derivation of loops in Theorem 2,
and specialize it with the static analysis relying on the modified
variables.
Therefore, we continue the derivation from the generic
approximation obtained in Theorem 2:

, M⦃c⦄]c0 ∆

◦

grdb

otherwise

]

if ∆ ⇒] Ab
Lc1 Mσ (∆ ∪ {Bb})
= Lc1 M]σ (∆ ∪ {Bb}) ∩


{Φ ∈ ∆ | fv(Φ) ∩ (Mod(c1 ) ∪ Mod(c2 )) = ∅} otherwise

v (By applying Lemma 11, since for all σ, σ 0 such that

ασ0

◦

σ0

for all τ such that τ = JcKτ, τ =V ar\ Mod(c) τ )

]

◦

v ασ 0

ασ being extensive)

v] (By applying Lemma 11, since for all τ ∈ γσ (∆),
0

◦

◦ ⦃c2 ⦄ ◦ grd¬b ◦ γσ (∆)


L

]
v
Φ ∈ ∆ | ∀id ∈ fv(Φ),


id 6∈ Mod(c1 ) ∪ Mod(c2 )

]

◦

◦

σ0

Finally,

⦃c⦄ ◦ γσ (∆)

(By monotonicity of ασ0 , and γσ
ασ0 ◦ γσ ◦ ασ ◦ ⦃c⦄ ◦ γσ (∆)

Lc1 Mσ

ασ0

⦃c⦄∅ = ασ0 (∅) = L

Additionally, assuming ∆ 6= L and ∆ 6= :
ασ0

◦

γσ (∆)

γσ (∆) ∪

◦ γσ (∆)

◦

As for the non-executed branch, we have a more precise
abstract static semantics by Lemma 6:

otherwise

Also,
ασ0

grdb

◦

as well as:
if ∆ =
if ∆ = L

Proof.
Let a command c’ and σ, σ 0 ∈ States such that σ 0 = Jc0 Kσ.
Then:
◦

◦

⦃c2 ⦄ ◦ grd¬b

α

defined as:

M⦃c⦄]c0 ∈ P (L) → P (L)




L
]
M⦃c⦄c0 ∆ , 

Φ ∈ ∆ | ∀id ∈ fv(Φ),



id 6∈ Mod(c) ∪ Mod(c0 )

ασ0

Lif b then c1 else c2 Mσ

= ασ0 Lc1 Mσ

Lemma 6 soundness of M⦃ − ⦄]− . For all c, c0 , σ, σ 0 such
]
that σ 0 = Jc0 Kσ, it holds that: ασ0 ◦ ⦃c⦄ ◦ γσ v̇ M⦃c⦄]c0 .
M⦃c⦄]c0

◦

where σ 0 = JcKσ
24

αB

G(w) ◦ γ B (σ, ∆)


σ, ασ ◦ ⦃while b do c⦄ ◦ γσ (∆) if ¬JbKσ
4 × v] w] ◦ JcKσ,



Lif b then c else skipM]σ ∆ oth.
◦

4 ×v]

σ,
if ¬JbKσ ∧ ∆ =





σ, ∆ ∪ {B¬b}
if ¬JbKσ ∧ (∆ ⇒] Ab)



σ, {Φ ∈ ∆ | fv(Φ) ∩ Mod(c) = ∅} ∩


∆ ∪ {B¬b} otherwise if ¬JbKσ





w] ◦ JcKσ,




Lif b then c else skipM]σ ∆ otherw.
Therefore:



]
4̇×v̇
Lwhile b do cM]σ ∆ , snd (lfpλ(σ,∆).(⊥,L)
G ] )(σ, ∆)
with:
G ] , λw] .λ(σ, ∆).

σ,
if ¬JbKσ ∧ ∆ =





σ,
∆
∪
{B¬b}
if ¬JbKσ ∧ (∆ ⇒] Ab)



σ, {Φ ∈ ∆ | fv(Φ) ∩ Mod(c) = ∅} ∩


∆ ∪ {B¬b} otherwise if ¬JbKσ





w] ◦ JcKσ,




Lif b then c else skipM]σ ∆ otherw.

25

F-C

Proof.
Let ∆ ∈ P (L). Then:

Hybrid Monitor with Intervals

The abstract semantics of an interval analysis, inspired by
[39], is presented in Figure 7.

αInt

γσ (∆)

◦

= αInt γ Int ( ) ∩ γσ (∆)

grd],Int
( ),
b

= (By definition of γσInt )

blw([a, b]) , [−∞, b]

αInt

abv([a, b]) , [a, +∞]

◦

γσInt ( , ∆)

= (By the soundness condition of a Granger’s pair)

2 ))
1 ))
grde],Int
(ı) , appblw(ı(e
(ı) u] appabv(ı(e
(ı)
e1
e2
1 ≤e2

αInt

◦

γσInt (tointσ ( , ∆), ∆)

= (By definition of ασInt )

blw(ı(e2 )−1)
1 )+1)
grd],Int
(ı) u] appabv(ı(e
(ı)
e1 <e2 (ı) , appe1
e2

fst ασInt

◦

Similarly, let ı ∈ StatesInt . Then:
ασ

],Int
],Int
]
grd],Int
b1 ∨b2 (ı) , grdb1 (ı) t grdb2 (ı)

◦


γ Int (ı) = ασ γ Int (ı) ∩ γσ ( )

appix (ı) , ı[x 7→ ı(x) u] i]

u

ı(e1 − e2 ) , ı(e1 ) − ı(e2 )

⦃c⦄

⦃skip⦄],Int ı , ı

,

⦃c1 ; c2 ⦄],Int ı , ⦃c2 ⦄],Int
],Int

⦃id := e⦄

ı , ı[id 7→ ı(e)]

⦃assert Φ⦄],Int ı , ı
⦃c1 ⦄],Int

◦

◦

⦃c1 ⦄],Int ı

= snd ασInt

◦

γσInt (ı, toforσ (ı, ))

Φ∈∆

],Int

⦃assume Φ⦄

ı,ı

Indeed,

⦃if b then c1 else c2 ⦄],Int ı ,

grd],Int
(ı) t] ⦃c2 ⦄],Int
b

γσInt (ı, )

Proof.
The error cases are straightforward: tointσ (ı, ) , ı and
toforσ ( , ∆) , ∆.
Let us restrict ourselves to ı ∈ StatesInt and ∆ ∈ P(L).
1 – tointσ is sound.
1.1 – Case : tointσ (ı, ∆).
We will prove that:


γσInt u] tointσ (ı, {Φ}) , ∆ = γσInt (ı, ∆)

ı(e1 + e2 ) , ı(e1 ) + ı(e2 )

],Int

◦

Lemma 8 . For all σ ∈ States, the pair of operators
tointσ , toforσ is a Granger’s reduced product.

1 )−i
appı(e
(ı)
e2

appin (ı) , >Int
ı(n) , [n, n]

= snd ασInt

v] toforσ (ı, )

2)
1)
appie1 +e2 (ı) , appi−ı(e
(ı) u] appi−ı(e
(ı)
e1
e2

,

γσInt is reductive)

= tointσ ( , ∆)

],Int
]
grd],Int
b1 (ı) u grdb2 (ı)

]

◦

fst (tointσ ( , ∆), ∆)

],Int
],Int
grd],Int
¬(e1 =e2 ) (ı) , grd(e1 <e2 )∧(e2 >e1 ) (ı) , grdb1 ∧b2 (ı) ,

2)
appi+ı(e
(ı)
e1

γσInt (tointσ ( , ∆), ∆)

≤],Int (Since ασInt

]
ı(e1 )
2)
grde],Int
(ı) , appı(e
e1 (ı) u appe2 (ı)
1 =e2

appie1 −e2 (ı)



◦

γσInt (ı, ∆)
= γ Int (ı) ∩ γσ (∆)

grd],Int
¬b (ı)

= (∆ is interpreted conjunctively by γσ )

⦃while (e) c⦄],Int ı ,

γ Int (ı) ∩ γσ ({Φ})
Φ∈∆



]
],Int
grd],Int
lfpv
ı ⦃if b then c1 else skip⦄
¬b

= ∩ γ Int (ı) ∩ γσ ({Φ})

Figure 7.

= ∩ γσInt (ı, {Φ})

Φ∈∆

Abstract semantics of an interval analysis

Φ∈∆

Φ∈∆

= (By cases 1.2 and 1.3, proven below)
Lemma 7 . For all σ ∈ States, any pair of operators that is a
Granger’s reduced product (tointσ , toforσ ) for the Cartesian
abstraction StatesInt × P (L) provides a sound approximation
of the interface between intervals and relational formulas:
αInt
ασ

◦

◦

],Int

˙
γσ ≤

∩ γσInt
Φ∈∆
Int

= ∩ γ
Φ∈∆

(tointσ (ı, {Φ}) , {Φ})

(tointσ (ı, {Φ})) ∩ γσ ({Φ})
Φ∈∆

= (∆ is interpreted conjunctively by γσ )
∩ γ Int (tointσ (ı, {Φ})) ∩ γσ (∆)

λ∆. tointσ ( , ∆) and

Φ∈∆
Int

]

γ Int v̇ λı. toforσ (ı, )

= (γ
26

is multiplicative)


γ
u tointσ (ı, {Φ}) ∩ γσ (∆)
Φ∈∆


= γσInt u] tointσ (ı, {Φ}) , ∆
Int



]

As for the non-executed branch, we have a more precise
abstract static semantics by Lemma 9:
ασ0

◦ ⦃c2 ⦄ ◦ grd¬b ◦ γσ (∆)


if ∆ =

]
v L
if ∆ ⇒] Ab


λı. toforσ0 (ı, ∅) ◦ ⦃c2 ⦄],Int

Φ∈∆

,

γσInt

(toint(ı, ∆), ∆)

with toint(ı, ∆) , u] tointσ (ı, {Φ})
Φ∈∆

1.2 – Case : tointσ (ı, {Ae})

◦

grd],Int
¬b

◦

γσ (∆)

◦

tointσ (>Int , ∆)oth.

Finally,

γσInt (ı, {Ae})

= γ Int (ı) ∩ γσ ({Ae})

ασ0

= γ Int (ı) ∩ {τ ∈ States | σpτ |= Ae}

v

= γ Int (ı) ∩ {τ ∈ States | JeKτ = JeKσ}
=γ

Int

=γ

Int

e=JeKσ

(ı) ∩ grd

e=JeKσ

(ı) ∩ grd

(States)
◦

γ

Int

(ı)

γσ ({Ae})

= γ Int ı u],Int grd],Int
e=JeKσ (ı) ∩ γσ ({Ae})


= γσInt ı u],Int grd],Int
e=JeKσ (ı), {Ae}
1.3 – Case: tointσ (ı, {Bb})
Similarly to case 1.2, we have:

Theorem 4 . The abstract monitoring semantics ILcM]σ of the
hybrid monitor, introduced in Figure 4, is sound: For all σ, σ 0 ∈
States such that σ 0 = JcKσ, it holds that:
◦

αB

]

γσ v̇ ILcM]σ

Proof.
Let Σ ∈ States and ∆ ∈ L. Let us derive a hybrid
monitoring semantics relying on an interval static analysis.
We will consider only the case of branching instructions, since
the derivation of the abstract monitoring semantics of the other
commands is similar to the one in Theorem 2.
1 – Case : conditionals
Let σ, σ 0 ∈ States such that σ 0 = Jif b then c1 else c2 Kσ. Let
us also assume that JbKσ = true. Then, similarly to Theorem 3
we have:
ασ0

◦

Lif b then c1 else c2 Mσ

= ασ0

◦

Lc1 Mσ

ασ0

◦

◦

grdb

◦

◦

γσ (∆)

◦

γσ (∆)

◦

Lc1 Mσ

◦

grdb

◦

ασ0

◦

Lc1 M]σ (∆

grdb ◦

γσ (∆) ∩

⦃c2 ⦄ ◦ grd¬b

◦

γσ (∆)

G(w) ◦ γ B (σ, ∆)


σ, ασ ◦ ⦃while b do c⦄ ◦ γσ (∆) if ¬JbKσ
4 × v] w] ◦ JcKσ,



Lif b then c else skipM]σ ∆ oth.
◦

4 ×v]

σ,
if ¬JbKσ ∧ ∆ =





σ, ∆ ∪ {B¬b}
if ¬JbKσ ∧ (∆ ⇒] Ab)



σ, λı. tofor (ı, ∅) ◦ ⦃while b do c⦄],Int ◦
σ

Int

toint
(>
, ∆) ∩ ∆ ∪ {B¬b} otherwise if ¬JbKσ
σ





w] ◦ JcKσ,




Lif b then c else skipM]σ ∆ otherw.



]
4̇×v̇
Lwhile b do cM]σ ∆ , snd (lfpλ(σ,∆).(⊥,L)
G ] )(σ, ∆)

as well as:
ασ0

Lc1 Mσ ◦

Therefore:

γσ (∆) ∩

⦃c2 ⦄ ◦ grd¬b

ασ0 ◦

2 – Case : loops
We rely on the generic derivation of loops in Theorem 2,
and specialize it with the static analysis relying on the modified
variables.
Therefore, we continue the derivation from the generic
approximation obtained in Theorem 2:

γσInt (ı, {Be})


= γσInt ı u],Int grd],Int
(ı),
{Bb}
b

LcMσ

Lif b then c1 else c2 Mσ

v
∪ {Bb}) ∩


if ∆ ⇒] Ab
L
],Int
◦
λı. toforσ0 (ı, ∅) ◦ ⦃c2 ⦄


],Int
Int
◦
grd¬b
tointσ (> , ∆) otherwise

]
if ∆ ⇒] Ab
Lc1 Mσ (∆ ∪ {Bb})



Lc M] (∆ ∪ {Bb}) ∩
1 σ
v]

λı. toforσ0 (ı, ∅) ◦ ⦃c2 ⦄],Int ◦



◦ tointσ (>Int , ∆) otherwise
grd],Int
¬b



◦

]

]

= (By soundness of grd],Int
e=JeKσ )
],Int
Int
Int ◦
γ (ı) ∩ γ
grde=JeKσ (ı) ∩

ασ0

◦

γσ (∆) v] Lc1 M]σ (∆ ∪ {Bb}).

with:
27

G ] , λw] .λ(σ, ∆).

σ,
if ¬JbKσ ∧ ∆ =




σ, ∆ ∪ {B¬b}
if ¬JbKσ ∧ (∆ ⇒] Ab)



σ, λı. tofor (ı, ∅) ◦ ⦃while b do c⦄],Int ◦
σ

Int

toint
(>
,
∆)
∩
∆
∪ {B¬b} otherwise if ¬JbKσ
σ



]


w ◦ JcKσ,




Lif b then c else skipM]σ ∆ otherw.

28

