10.6092/issn.1972-5787/3690
We perform a formal analysis of compositionality techniques for proving possibilistic noninterference for a while language with parallel composition. We develop a uniform framework where we express a wide range of non-interference variants from the literature and compare them w.r.t. their contracts: the strength of the security properties they ensure weighed against the harshness of the syntactic conditions they enforce. This results in a simple implementable algorithm for proving that a program has a specific noninterference property, using only compositionality, which captures uniformly several security type-system results from the literature and suggests a further improved type system. All formalism and theorems have been mechanically verified in Isabelle/HOL.
application/pdf
1972-5787
3690
1
en
Tobias Nipkow
Journal of Formalized Reasoning
Formal Verification of Language-Based Concurrent Noninterference
Text.Serial.Journal
https://jfr.unibo.it/
6
Articles
2013-08-27
2013-05-14
2013-08-27
2016-01-29
1-30
JFR
Tobias Nipkow
2013/08/27
10.6092/issn.1972-5787/3690
1
Technische Universität München
1972-5787
1
en
30
Formal Verification of Language-Based Concurrent Noninterference
https://jfr.unibo.it/article/download/3690/3326
6
Formal Verification of Language-Based Concurrent
Noninterference
Andrei Popescu
Technische Universität München and Institute of Mathematics Simion Stoilow of the
Romanian Academy
Johannes Hölzl
Technische Universität München
and
Tobias Nipkow
Technische Universität München


We perform a formal analysis of compositionality techniques for proving possibilistic noninterference for a while
language with parallel composition. We develop a uniform framework where we express a wide range of non-
interference variants from the literature and compare them w.r.t. their contracts: the strength of the security
properties they ensure weighed against the harshness of the syntactic conditions they enforce. This results in a
simple algorithm for proving that a program has a specific noninterference property, using only compositionality,
which captures uniformly several security type-system results from the literature and suggests a further improved
syntactic criterion. All formalism and theorems have been mechanically verified in Isabelle/HOL.




1.   INTRODUCTION
Language-based noninterference is an important and well-studied security property. To
state this property, one assumes the program memory is separated into a low, or public,
part, which an attacker is able to observe, and a high, or private, part, hidden to the attacker.
Then a program satisfies noninterference if, upon running it, the high part of the initial
memory does not affect the low part of the resulting memory. Thus, the program has
no information leaks from the private part of the memory into the public one, so that a
potential attacker should not be able to obtain information about private data by inspecting
public data.
   Noninterference comes in different variants, depending on what type of channels one
accepts as capable of transmitting leaks—besides the normal channels represented by pro-
gram variables, so-called covert channels include termination and timing channels. More-
over, when nondeterminism is involved, one can distinguish between possibilistic and
probabilistic noninterference (the latter also taking probabilistic channels into account).
   In this paper, we deal with noninterference in the presence of possibilistic concurrency.
The literature abounds in notions of concurrent possibilistic noninterference and tech-
niques to enforce it [3–7, 20, 32–34, 37, 42, 47], many of them surveyed in [36]. There
is usually a tradeoff between the strength of a security property and the harshness of the

This is an extended version of the conference paper [31]; it additionally includes more detailed explanations of
the discussed concepts and techniques, proof sketches, a presentation of the Isabelle formalization, and addresses
more related work. The work reported here has been supported by the DFG project Ni 491/13–2 (part of the DFG
priority program Reliably Secure Software Systems–RS3) and by NI 491/15-1.

                                                               Journal of Formalized Reasoning Vol. 6, No. 1, 2013, Pages 1–30.
2       ·      A. Popescu, J. Hölzl and T. Nipkow

conditions imposed on the programs in order to satisfy it (typically, a type system). Yet,
new methods for establishing noninterference are often presented as improvements over
older methods (e.g., a more lenient type system) while being rather brief on the notion
that in effect the whole contract is being changed: less pressure on the programs, weaker
noninterference ensured.
   The paper presents the first comparison of a variety of noninterference notions and re-
sults, in a unified and formalized framework, where complex results from the literature are
given uniform and simpler proofs. As a preview of the kind of properties we analyze and
classify in this paper, here is a selection of informal notions of a command c being secure
(noninterfering):
   (1) Given any two initial memory states that are indistinguishable by the attacker (have
the same low, i.e., public, part), the executions of c proceed identically w.r.t. both the
program counter and the updates on the low part of the memory—we call this property self
isomorphism.
   (2) c may never change the low part of the memory during its execution—we call this
discreetness (often in the literature this is called highness).
   (3) If started in two indistinguishable memory states, the executions of c are lock-step
bisimilar, performing the same updates to the low part of the memory—we call this self
strong bisimilarity, i.e., strong bisimilarity to itself (called strong security in [38]).
   (4) A relaxation of strong bisimilarity with lock-step synchronization replaced by 01-
bisimilarity (simply called bisimilarity in [6]), where only attacker-visible (i.e., low-memory
changing) steps in one execution are required to be matched by corresponding steps in the
other, while “discreet” (i.e., low-memory unchanging) steps need not be matched. Thus,
one step may be matched by either zero or one steps.
   (5) A further relaxation of strong bisimilarity—weak bisimilarity [22] (used in [5, 42] in
a security context) where one step may be matched by any number of steps.
   Property 1 (self isomorphism) is a very strong security notion, ensuring that an attacker
controlling the low inputs of c is not able to infer any information about the high inputs,
not even if he is allowed to observe the low part of intermediate memory states and the
program counter. In particular, self isomorphism exhibits no leaks on covert channels
such as timing or termination. Property 2 (discreetness) is neither weaker nor stronger
than self isomorphism, but it no longer guarantees indistinguishability w.r.t. the program
counter, and moreover the attacker may infer confidential information by measuring ex-
ecution time. Property 3 (strong bisimilarity) prevents leaks on standard channels (low
variable values) and timing channels, but, unlike self isomorphism, does not guarantee that
execution starting in indistinguishable states follow the very same paths (taking the same
branches). Properties 4 (01-bisimilarity) and 5 (weak bisimilarity) are weakenings of all of
the above three. They are only able to guarantee the absence of leakage through standard
channels.
   E XAMPLE 1. Consider the following commands, where k is parallel composition with
interleaving semantics, l is a low variable and h, h0 are high variables:
—c0 :       h := 0
—c1 :       if l = 0 then h := 1 else l := 2
—c2 :       if h = 0 then h := 1 else h := 2
—c3 :       if h = 0 then h := 1 ; h := 2 else h := 3

Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
               Formal Verification of Language-Based Concurrent Noninterference                     ·      3

—c4 :    l := 4 ; c3
—c5 :    c3 ; l := 4
—c6 :    c1 k c4 k c5
—c7 :    c1 k c2
—c8 :    l := h
—c9 :    h0 := 0 ; while h > 0 do {h := h − 1 ; h0 := h0 + 1} ; l := 4
—c10 :    c9 k l := 1 k h := 0 k h := h + 1
   c0 is both self isomorphic and discreet. c1 is self isomorphic (since it is not testing any
high variable), but not discreet. c2 and c3 are discreet (as they are not updating any low
variable), but not self isomorphic. c1 and c2 , but not c3 , are self strongly bisimilar—the
reason why c3 is not is its branching on a high test in conjunction with one branch taking
longer than the other.
   c4 is self 01-bisimilar because, after a self isomorphic assignment, it transits to a discreet
continuation. c5 is not self 01-bisimilar because, one of the branches of its prefix c3 being
faster, it reaches the visible step l := 4 at a time when this step is not immediately available
on the alternative branch; but c5 is self weakly bisimilar, since weak bisimilarity allows the
alternative branch to catch up using multiple discreet steps.
   c6 is a pool consisting of three threads running in parallel: a self isomorphic one c1 , a self
01-bisimilar one c4 and a self weakly bisimilar one c5 . One would hope, in a compositional
framework, that the pool satisfies the weakest of the security properties of its threads, here,
weak self bisimilarity. As we shall see, this is indeed the case if the above informal notions
of security are formalized in an interactive manner, taking into consideration the possibility
that the environment too may change the program state. But how about c7 ? It is a pool of a
self isomorphic thread c1 and a discreet thread c2 . Since these two security notions are not
comparable, we should have c7 secure according to the strongest available security property
that is weaker than both—amongst our considered properties, this is self 01-bisimilarity.
   c8 is not secure according to any of the five criteria—it exhibits a direct leak from high
to low. If we ignore timing channels and assume that initially h ≥ 0, then it is reasonable
to consider c9 secure, since it has the same effect as the program h0 := h ; l := 4. How-
ever, whether or not we should deem c9 secure when placed in parallel with other threads
depends on the assumption we make on these threads—e.g., are they allowed to increase
h, thus preventing termination of c9 ? For instance, the pool c10 containing c9 is harmless,
since:
—the thread l := 1 does not affect the termination of c9 , not writing the counter h;
—the thread h := 0 helps the termination of c9 by setting the counter to an exit value;
—the thread h := h + 1, although it delays the termination of c9 , does not prevent its ter-
 mination.
Later we shall phrase this termination-conditional notion of security in a compositional
manner.
  Here is an overview of this paper, where we use “security” and “noninterference” as
synonyms. We start by introducing the concurrent setting where we operate: a while lan-
guage with parallel composition and a fixed attacker-indistinguishability relation on pro-
gram states (Section 2). Then we systematize and compare bisimilarity-based notions from

                                                         Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
4      ·       A. Popescu, J. Hölzl and T. Nipkow

the literature (Section 3). A formal study of the compositionality of, and of the implica-
tions between, these notions (Section 4) yields a novel proof methodology: To show that
c is secure according to some notion N, first try to reduce the goal to proving N for the
components of c; if this is not feasible due to failure of the required compositionality of N
w.r.t. the language construct Cns located at the top of c (e.g., Cns can be an If , or a While,
etc.), try to identify a stronger notion M that is (more) compositional w.r.t. Cns, and so on,
recursively. The compositionality caveats of existing notions suggests the definition of a
fully compositional security notion (Section 5). We then look at existing work on security
type systems in the light of our analysis (Section 6)—the aforementioned simple proof
technique turns out quite insightful, capturing these type system criteria uniformly. Our
novel security notion from Section 5 yields a more permissive syntactic criterion than the
existing ones, but the result targets only terminating programs. We also discuss end-to-end
security aspects of the studied bisimilarity-based notions (Section 7). Finally, we present
the mechanization of our constructions and results in Isabelle/HOL (Section 8).

2.    THE PROGRAMMING LANGUAGE
We consider a simple while language with parallel composition, whose set com of com-
mands, ranged over by c, d, e, is given by the following grammar:
                        c ::= atm | Seq c1 c2 | If tst c1 c2 | While tst c | Par c1 c2
Above, atm ranges over an unspecified set atom of atomic commands (atoms). Standard
examples of atoms are assignments such as x := x + y. Seq c1 c2 is the sequential composi-
tion of c1 and c2 , written in concrete syntax as c1 ; c2 . If tst c1 c2 is the conditional, written
in concrete syntax as if tst then c1 else c2 , where tst ranges over an unspecified set test of
tests. Standard examples of tests are Boolean expressions such as x = y. While tst c is the
usual while loop, in concrete syntax, while tst do c. Par c1 c2 is the parallel composition
of c1 and c2 , in concrete syntax, c1 k c2 . We generally prefer abstract syntax in theoretical
results and concrete syntax in examples.
   To give semantics to the language, we assume:
—a set of (memory) states, state, ranged over by s,t; an execution function for the atoms,
 aexec : atom → state → state;
—an evaluation function for the tests, tval : test → state → bool.
Then we define a standard small-step semantics [27] as a pair of inductive predicates →T :
(com × state) → state and →C : (com × state) → (com × state) (where the subscripts T
and C stand for “termination” and “continuation”) specified in Figure 1. Intuitively, we
interpret (c, s)→T s0 as stating: in state s, command c may take a step terminating while
changing the state to s0 ; and (c, s)→C (c0 , s0 ) as saying: in state s, command c may take a
step yielding the continuation c0 while changing the state to s0 . The pairs (c, s), which we
call configurations, are thus thought of as consisting of the part of the program that remains
to be executed, c, and the current state, s. We carefully distinguish between continuation
and terminating steps (as the two predicates →C and →T ), since termination-sensitiveness
will be crucial in our development.
   →C∗ denotes the reflexive-transitive closure of →C , and →T∗ the composition of →C∗ with
→T . Thus, (c, s)→C∗ (c0 , s0 ) means that (c0 , s0 ) is reachable from (c, s) by zero or more con-
tinuation steps, and (c, s)→T∗ s0 that (the final state) s0 is reachable from (c, s) by zero or
more continuation steps followed by a terminating step.
Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
                    Formal Verification of Language-Based Concurrent Noninterference                                   ·      5

                                                   (c1 , s)→T s0                           (c1 , s)→C (c01 , s0 )
     (atm, s) →T aexec atm s
                                             (Seq c1 c2 , s)→C (c2 , s0 )           (Seq c1 c2 , s)→C (Seq c01 c2 , s0 )
               tval tst s                                   ¬ tval tst s                              ¬ tval tst s
      (If tst c1 c2 , s)→C (c1 , s)                 (If tst c1 c2 , s)→C (c2 , s)                  (While tst c, s)→T s
             (c1 , s)→C (c01 , s0 )                                                    tval tst s
      (Par c1 c2 , s)→C (Par c01 c2 , s0 )                            (While tst c, s)→C (Seq c (While tst c), s)
             (c2 , s)→C (c02 , s0 )                        (c2 , s)→T s0                           (c1 , s)→T s0
      (Par c1 c2 , s)→C (Par c1 c02 , s0 )           (Par c1 c2 , s)→C (c1 , s0 )            (Par c1 c2 , s)→C (c2 , s0 )

                                                Fig. 1: Small-step semantics


   The freeness of the command constructors in conjunction with the inductive definitions
of →C and →T provide us with the obvious inversion rules. E.g., the inversion rule for →C
w.r.t. Seq is the following: If (Seq c1 c2 , s)→C (c0 , s0 ), then one of the following holds:
—either (c1 , s)→T s0 and c0 = c2 ,
—or there exists c01 such that (c1 , s)→C (c01 , s0 ) and c0 = Seq c01 c2 .
Similar, but slightly more complex rules can be proved for the “star” relations, e.g., for →C∗
w.r.t. Seq: If (Seq c1 c2 , s)→C∗ (c0 , s0 ), then one of the following holds:
—either there exist c01 and s00 such that (c1 , s)→T s00 and (c2 , s00 )→C∗ (c0 , s0 ).
—or there exists c01 such that (c1 , s)→C∗ (c01 , s0 ) and c0 = Seq c01 c2 .
     Another useful fact will be the following progress property of the operational semantics:


     P ROPOSITION 1. For all c and s, either there exists s0 such that (c, s)→T s0 or there exist
c0   and s0 such that (c, s)→C (c0 , s0 ).
     P ROOF. By a straightforward structural induction on c.

3.     NOTIONS OF NONINTERFERENCE
Next we proceed to a uniform description of several notions of noninterference from the
literature. We fix a relation ∼ on states, called indistinguishability, where s ∼ t is meant to
say “s and t are indistinguishable by the attacker.” The only assumption we make about ∼
is that it is an equivalence relation. While the results of this paper work abstractly for any
such ∼, in the literature on language-based security it is often the case that one considers
a particular ∼, which we shall also use in our examples and informal discussions.
   E XAMPLE 2. We assume that atomic statements and tests are built by means of arith-
metic and boolean expressions applied to variables taken from a set var. States are as-
signments of values to variables, i.e., the set state is var → val, where val is a set of
values (e.g., integers). Variables are classified as either low (lo) or high (hi) by a given se-
curity level function sec : var → {lo, hi}. Then ∼ is defined as coincidence on the low




                                                                            Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
6      ·       A. Popescu, J. Hölzl and T. Nipkow

variables, with the intuition that the attacker is only able to observe these. Formally,
s ∼ t ≡ ∀x ∈ var. sec x = lo =⇒ s x = t x. 1
3.1    Security Notions Given by Unary Predicates
We start with some very simple notions of security, describable directly as unary predicates.
Namely, we define the following predicates on commands coinductively as greatest fixed
points, i.e., as the weakest2 predicates satisfying the indicated clauses:
—Self isomorphism, siso, by siso c ≡
 (∀s t c0 s0 . s ∼ t ∧ (c, s)→C (c0 , s0 ) =⇒ (∃t 0 . (c,t)→C (c0 ,t 0 ) ∧ s0 ∼ t 0 )) ∧
 (∀s t s0 . s ∼ t ∧ (c, s)→T s0 =⇒ (∃t 0 . (c,t)→Tt 0 ∧ s0 ∼ t 0 )) ∧
 (∀s c0 s0 . (c, s)→C (c0 , s0 ) =⇒ siso c0 )
—Discreetness, discr, by discr c ≡
 (∀s c0 s0 . (c, s)→C (c0 , s0 ) =⇒ s ∼ s0 ∧ discr c0 ) ∧ (∀s s0 . (c, s)→T s0 =⇒ s ∼ s0 )
Note that here ≡ does not introduce a definition in the usual sense, but rather expresses
an equality that, together with the greatest fixed point assumption, identifies uniquely the
introduced concept. This will be the case with all the coinductive definitions throughout
this paper.
   According to the definition of siso, a command c is self isomorphic iff the following hold
for all indistinguishable states s and t:
—Any single-step continuation c0 of c available from state s is also available from t, yield-
 ing indistinguishable states s0 and t 0 . (This is stated in the first conjunct from the defini-
 tion of siso.)
—Any single-step terminating state s0 of c available from state s has an indistinguishable
 counterpart, t 0 , available from t. (This is stated in the second conjunct.)
—The above 2 facts hold for all single-step continuations c0 of c, and for all single-step
 continuations c00 of c0 , and so on, indefinitely. (This is stated in the third conjunct,
 together with the maximal interpretation of siso, as greatest fixed point.)
3.2    Interactiveness and Possibilism
The coinductive definition of self isomorphism expresses that the command execution pro-
ceeds absolutely independently of the indistinguishability class of the state, and this is true
interactively, i.e., regardless of the intervention of the environment, provided this interven-
tion is itself compatible with the state indistinguishability relation. And similarly for the
definition of discr, expressing that the command execution changes the indistinguishability
class, regardless of what that class has become through potential environment action.
   Interactivity is expressed by the universal quantification over the indistinguishable states
s and t in the definition of siso. Indeed, even though transitions operate on (command, state)
pairs, the siso predicate operates on commands alone, forgetting each time the result state
s0 from the continuation (c0 , s0 ). Thus, at each resumption point, the predicate quantifies
universally over all states s (“overwriting” the previous s0 ), to account for the fact that the

1 In the mechanization described in Section 8, we consider the more general case of multilevel security, via a
lattice of security levels—however, this brings neither much additional difficulty, nor much additional insight, so
here we focus on this 2-level lattice, with lo < hi.
2 The conference version of this paper [31] erroneously used the superlative “strongest” instead of “weakest”.



Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
              Formal Verification of Language-Based Concurrent Noninterference                          ·      7

new state produced by the command under consideration may have been changed by the
environment (perhaps consisting of other threads running in parallel, and/or of the attacker)
before that command gets to perform an other step.
   For example, the command c ≡ h := 0 ; l := h (with h high and l low) would be consid-
ered self isomorphic if it were not for the interactivity constraint. Indeed, if no interference
from the environment is assumed, the execution of c proceeds the same way regardless of
the initial value of h, as it first assigns 0 to h. However, siso c does not hold, since the
continuation l := h is required to be secure given any value of h arising as the effect of a
secure thread running in parallel, say, h := h0 with h0 high.
   This interactivity twist (originating from [35, 38]) is convenient for compositionality,
since it ensures that a command is secure not only in isolation, but also if placed in any pool
of secure threads running in parallel. In other words, interactivity ensures compositionality
w.r.t. parallel composition. As a consequence, most of the security notions discussed in this
paper will be interactive.
   Another prominent aspect of the notions discussed in this paper is their possibilistic
nature, indicated by existential quantification on the right of some of their defining clauses
(for self-isomorphism, ∃t 0 ): given two indistinguishable states, for any (multi-)step taken
from one state, there exists a matching (multi-)step taken from the other so that the results
are again indistiguishable.
   We shall also need the following notion of termination possibility at each point during
execution, via the coinductively defined predicate mayT (read “may terminate”):
            mayT c ≡ ∀s c0 s0 .(c, s)→C (c0 , s0 ) =⇒ (∃s00 .(c0 , s0 )→T∗ s00 ) ∧ mayT c0 .

Thus, may-termination means: for any continuation of the command and any given state,
there is a possible terminating execution.
3.3   Security Notions Given by Bisimilarities
Self isomorphism and discreetness were expressible as unary predicates. However, inter-
esting noninterference properties may require binary relations. In order to illustrate this,
let us assume we wish to express that c is secure in that the executions of c are (multi)step-
wise equivalent if started in indistinguishable states. Suppose c branches according to a
high test. Then indistinguishable states may yield different continuations, say, c1 and c2 ,
and so we are faced with the problem of proving the executions of c1 and c2 (multi)step-
wise equivalent, i.e., proving c1 and c2 bisimilar. (The above two notions have by-passed
this problem in trivial ways: self isomorphism forbids this situation by disallowing the pro-
gram counter to diverge, hence disallowing high tests, while discreetness of c also requires
c1 and c2 to be discreet, hence trivially “equivalent”.)
   In order to define relevant notions of bisimilarity, it will be useful to first introduce
matching operators (or matchers) that express various choices of rules for bisimilarity.
   Parenthesis. Before doing this, we give some context for readers unfamiliar with process
algebra. Suppose we have a single-step transition relation between processes. Then two
processes p and q are called bisimilar if the following hold:
(1) for all continuations p0 of p, there exists a continuation q0 of q such that p0 and q0 are
    again bisimilar;
(2) and vice versa (with p and q switched).


                                                             Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
8      ·        A. Popescu, J. Hölzl and T. Nipkow

    matchCC θ c d ≡
    ∀s t c0 s0 . s ∼ t ∧ (c, s)→C (c0 , s0 ) =⇒
    (∃d 0 t 0 . (d,t)→C (d 0 ,t 0 ) ∧ s0 ∼ t 0 ∧ θ c0 d 0 )
    matchC01C θ c d ≡                                            matchCMC θ c d ≡
    ∀s t c0 s0 . s ∼ t ∧ (c, s)→C (c0 , s0 ) =⇒                  ∀s t c0 s0 . s ∼ t ∧ (c, s)→C (c0 , s0 ) =⇒
    (∃d 0 t 0 . (d,t)→C (d 0 ,t 0 ) ∧ s0 ∼ t 0 ∧ θ c0 d 0 ) ∨    (∃d 0 t 0 . (d,t)→C∗ (d 0 ,t 0 ) ∧ s0 ∼ t 0 ∧ θ c0 d 0 )
    (s0 ∼ t ∧ θ c0 d)                                            matchCM θ c d ≡
    matchC01 θ c d ≡                                             ∀s t c0 s0 . s ∼ t ∧ (c, s)→C (c0 , s0 ) =⇒
    ∀s t c0 s0 . s ∼ t ∧ (c, s)→C (c0 , s0 ) =⇒                  (∃d 0 t 0 . (d,t)→C∗ (d 0 ,t 0 ) ∧ s0 ∼ t 0 ∧ θ c0 d 0 ) ∨
    (∃d 0 t 0 . (d,t)→C (d 0 ,t 0 ) ∧ s0 ∼ t 0 ∧ θ c0 d 0 ) ∨    (∃t 0 . (d,t)→T∗ t 0 ∧ s0 ∼ t 0 ∧ discr c0 )
    (s0 ∼ t ∧ θ c0 d) ∨                                          matchTMT c d ≡
    (∃t 0 . (d,t)→T t 0 ∧ s0 ∼ t 0 ∧ discr c0 )                  ∀s t s0 . s ∼ t ∧ (c, s)→T s0 =⇒
    matchTT c d ≡                                                (∃t 0 . (d,t)→T∗ t 0 ∧ s0 ∼ t 0 )
    ∀s t s0 . s ∼ t ∧ (c, s)→T s0 =⇒                             matchTM c d ≡
    (∃t 0 . (d,t)→T t 0 ∧ s0 ∼ t 0 )                             ∀s t s0 . s ∼ t ∧ (c, s)→T s0 =⇒
    matchT01 c d ≡                                               (∃t 0 . (d,t)→T∗ t 0 ∧ s0 ∼ t 0 ) ∨
    ∀s t s0 . s ∼ t ∧ (c, s)→T s0 =⇒                             (∃d 0 t 0 . (d,t)→C∗ (d 0 ,t 0 ) ∧ s0 ∼ t 0 ∧ discr d 0 )
    (∃t 0 . (d,t)→T t 0 ∧ s0 ∼ t 0 ) ∨
    (∃d 0 t 0 . (d,t)→C (d 0 ,t 0 ) ∧ s0 ∼ t 0 ∧ discr d 0 ) ∨
    (s0 ∼ t ∧ discr d)

                                                       Fig. 2: Matchers


    We can think of these conditions as an infinitary two-player game between an “attacker”
who tries to distinguish two processes p and q (and thus disprove bisimilarity) and a “de-
fender” who tries to prevent this. At each moment, the state of the game consists of a pair
(p, q). The attacker picks a process, say, p, and a transition from it, say, p → p0 , the new
state becoming (p0 , q). Then the defender has to find a transition from q, say q → q0 , the
new state becoming (p0 , q0 ), and so on. The attacker wins if, upon his turn, the defender
can no longer move; otherwise, i.e., if (upon his turn) the attacker can no longer move
or if the defender manages to stay in the game indefinitely, then the defender wins. Two
processes p and q are bisimilar iff the attacker has no winning strategy. (Here, we are in
a very simple setting where two processes are only distinguishable by means of termina-
tion, i.e., if, at some point, one cannot move while the other can. In general, however, one
assumes further means for the attacker to inspect processes, e.g., an observer function on
their current state.)
    Technically, the above amounts to defining bisimilarity as the weakest symmetric rela-
tion θ for which the following holds for all p and q such that θ p q: for all p0 such that p →
p0 , there exists q0 such that q → q0 and θ p0 q0 . If we extract the core of this characterization
into a predicate match defined as match θ p q ≡ ∀p0 . p → p0 =⇒ (∃q0 . q → q0 ∧ θ p0 q0 ),
then bisimilarity ≈ can be defined as the weakest symmetric relation θ for which θ p q is
equivalent to match θ p q for all processes p, q. We write this briefly as the fixed point def-
inition ≈ p q ≡ match ≈ p q, interpreted maximally in the space of symmetric relations.
    The advantage of employing the auxiliary concept of a matcher is of course the technical
ease of varying the notion of bisimilarity. For instance, if we want weak bisimilarity (i.e.,
one step matched by multiple steps), we modify the definition of match to use →∗ , the
transitive closure of →, on the right-hand side of the implication: match θ p q ≡ ∀p0 . p →
p0 =⇒ (∃q0 . q →∗ q0 ∧ θ p0 q0 ). End of parenthesis.

Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
               Formal Verification of Language-Based Concurrent Noninterference                     ·      9

   Our relevant matchers are defined in Figure 2, where θ ranges over binary relations on
commands. In the operator names, the superscripts indicate the kind of steps being taken,
and the subscripts indicate by what kind of steps these must be simulated (matched), where:
“C” means (single) continuation step; “T” means (single) terminating step; “01C” means
0 or 1 continuation steps; “01” means 0 or 1 continuation or terminating steps, i.e., 01C
or T; “MC” means multiple continuation steps; “MT” means multiple continuation steps,
followed by a terminating step; “M” means MC or MT. E.g., matchCC refers to matching any
continuation step by a continuation step, matchC01C to matching any continuation step by 0
or 1 continuation steps, i.e., either by a continuation step or by a stutter move.
   Matchers indicate how the single steps of a command c may be matched by single or
multiple steps of a command d. In most cases, the matcher is also parameterized by a
continuation relation θ ; exceptions are matchTT and matchTMT , where, due to termination of
both the left and the right sides, no continuation makes sense. matchC01 , matchT01 , matchCM and
matchTM are termination-flexible matchers, in that they allow matching continuation steps
against termination steps and vice versa. For instance, matchC01 (“match a continuation
step against 0 or 1 steps of either kind”) requires for θ , c and d that, for all indistin-
guishable states s and t, any step (c, s)→C (c0 , s0 ) be matched by either a continuation step
(d,t)→C (d 0 ,t 0 ), or a stutter step, or a termination step (d,t)→Tt 0 . In each case, it is also
required that the resulting states are indistinguishable. Moreover, in the first two cases
(for continuation and stutter) it is required that the resulting commands are in relation θ .
For the third case though (the termination step), the latter condition does not make sense,
since on the left of the matcher we have a continuation command, c0 , while the right side
has terminated; what we require instead is that, w.r.t. the attacker-observable behavior, c0
acts as if it terminated, in that it will never change the indistinguishability class of the
state, i.e., is discreet. (Similar discreetness conditions appear in the definitions of the other
termination-flexible matchers for similar reasons.)
   We are now ready to define the following bisimilarity relations, again coinductively, by
plugging in different combinations of matchers and taking each time the weakest symmetric
relation satisfying the given clause (where the bisimilarities are written with infix notation
on the left and are passed as arguments to the matchers on the right):
—Strong bisimilarity, ≈S , by c ≈S d ≡ matchCC (≈S) c d ∧ matchTT c d
—01-bisimilarity, ≈01 , by c ≈01 d ≡ matchC01 (≈01) c d ∧ matchT01 c d
—Termination-sensitive 01-bisimilarity (01T-bisimilarity), ≈01T , by
 c ≈01T d ≡ matchC01C (≈01T) c d ∧ matchTT c d
—Weak bisimilarity, ≈W , by c ≈W d ≡ matchCM (≈W) c d ∧ matchTM c d
—Termination-sensitive weak bisimilarity (weak T-bisimilarity), ≈WT , by
 c ≈WT d ≡ matchCMC (≈W) c d ∧ matchTMT c d
   To be more precise, the above relations are defined using the Knaster-Tarski theorem,
stating that every monotonic function P : L → L on a complete lattice (L, ≤) has a greatest
fixpoint gfp P ∈ L, i.e., such that P (gfp P) = gfp P and ∀x ∈ L. P x = x =⇒ x ≤ gfp x. In
fact, gfp P is also the greatest postfixpoint, i.e., ∀x ∈ L. x ≤ P x =⇒ x ≤ gfp x. This forms
the basis of the coinduction principle: to prove x ≤ gfp P, it suffices to prove x ≤ P x; or,
in a slightly more convenient form: to prove x ≤ gfp P, it suffices to prove x ≤ P (x ∨
gfp x), where ∨ is lattice (binary) supremum. We call an x such that x ≤ P (x ∨ gfp x) a
generalized postfixpoint. Thus, the coinduction principle, which will be heavily employed

                                                         Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
10       ·       A. Popescu, J. Hölzl and T. Nipkow

in this paper, is about proving that certain items are generalized postfixpoints of certain
monotonic functions.
   In our case, L is the set of symmetric binary relations θ : com → com → bool and ≤ is
inclusion (point-wise implication), and the various operators P are given by combinations
of matchers. For example:
— ≈S is the gfp of λ θ . λ c d. matchCC θ c d ∧ matchTT c d
— ≈01T is the gfp of λ θ . λ c d. matchC01C θ c d ∧ matchTT c d
   All these bisimilarity relations are by definition symmetric and can also be proved tran-
sitive, but they are not reflexive. In fact, the notion of a command c being bisimilar with
itself (e.g., c ≈S c, c ≈01 c, etc.), which we call self bisimilarity of c (e.g., self strong bisim-
ilarity, self 01-bisimilarity, etc.) is taken in this paper as the formalization of the informal
notion of security of a command.
3.4      Attacker Models
Next we explain how different bisimilarities correspond to different attacker models. In all
cases, one assumes the attacker has access to the program (command) source code3 and
the low part of the state, and the ability to set, at the beginning of the command execution,
the low part of the state in any desired way. As usual, the attacker does not know the
initial values of the high variables and is trying to infer information about them—security
thus refers to the impossibility of the attacker to infer anything by running the program
and performing experiments on its states, perhaps also while the program is still running.
Security of a command c is therefore expressed as: For what the attacker knows, the initial
values of the high variables could have been any. That is, provided the initial state is,
say, s, any indistinguishable state t (i.e., for the standard choice of ∼ from Example 2, a
state t agreeing with s on the low variables, but not necessarily on the high ones) would
have exhibited the same attacker-observable behavior. If we also factor in interactivity
(meaning that, due to the intervention of the environment, fresh indistinguishable states
s and t may replace the existing ones at any point during the execution), we obtain the
following property: By keeping experimenting on the continuations of c with different
indistinguishable states s and t, the attacker cannot discover any differences in the resulting
states s0 and t 0 or (in the termination-sensitive cases) in the fact that execution terminates.
The latter is (self) bisimilarity.
   The various notions of bisimilarity differ in further assumptions on how precisely is
the attacker assumed to be able to experiment on the running program and its states. For
strong bisimilarity (≈S), we assume the attacker’s ability to repeatedly stop the program
after single execution steps and inspect the (low part of the) state, 4 or, equivalently, take
snapshots of the state after controlled numbers of execution steps. Technically, this shows
in the two involved matchers, matchCC and matchTT , being one-to-one (w.r.t. continuation or
termination steps). Moreover, we assume the attacker can detect termination—this shows
in the fact that the two matchers preserve the type of transition: continuation vs. continua-
tion and termination vs. termination. For weak bisimilarity (≈W), the attacker may still stop
the program repeatedly, but has no control on the number of steps that the program takes

3 This is a worse-case-scenario assumption. E.g., in Trojan Horse attacks, the attacker is assumed to own the
program code.
4 Here and elsewhere, by the attacker “inspecting the state” we mean “inspecting the low part of the state”.


Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
             Formal Verification of Language-Based Concurrent Noninterference                  ·      11

between two stops. (For what the attacker knows, zero, one, or more steps could have been
taken.) This shows in the one-to-many nature of the matchers. The termination-sensitive
version of weak bisimilarity (≈WT) additionally assumes the attacker is able to detect ter-
mination. Thus, ≈WT allows, via matchTMT , matching a termination step by a sequence of
steps only if the latter ends in a termination step. 01-bisimilarity (≈01), also coming with a
termination-sensitive variant (≈01T), is intermediate between strong and weak bisimilarity.
Here, the attacker may keep running the program for 0 or 1 steps, without knowing which
of the two situations has actually occurred.

3.5   Hierarchy of the Security Notions
The following proposition orders the different notions of self bisimilarity according to their
strength:
  P ROPOSITION 2. The implications in Figure 3 hold.
  P ROOF. We distinguish two types of stated facts:
  1) Implications between genuinely unary predicates and other predicates:
—discr c =⇒ c ≈01 c
—discr c ∧ mayT c =⇒ c ≈WT c
—siso c =⇒ c ≈S c
After suitably rephrasing them, e.g., discr c ∧ c = d =⇒ c ≈01 d, these facts follow by
routine coinduction on the right-hand side predicates, ≈01 and ≈S.
   2) Implications between predicates stemming from binary relations—for these we prove
the more general binary versions:
—c ≈S d =⇒ c ≈01T d
—c ≈01T d =⇒ c ≈01 d
—etc.
Instead of doing coinductive proofs here, we invoke a general result stating that greatest
fixed points are monotonic: If P, Q : L → L are monotonic functions on a complete lattice
(L, ≤) and P ≤ Q (that is to say, ∀x ∈ L. P x ≤ Q x), then gfp P ≤ gfp Q. In our case, P ≤ Q
amounts to implications between conjunctions of matchers:
—matchCC θ c d ∧ matchTT c d =⇒ matchC01 θ c d ∧ matchT01 c d
—matchC01 θ c d ∧ matchT01 c d =⇒ matchC01C θ c d ∧ matchTT c d
—etc.
These follow from implications between matchers:
—matchCC θ c d =⇒ matchC01C θ c d =⇒ matchCMC θ c d =⇒ matchCM θ c d
—matchC01C θ c d =⇒ matchC01 θ c d =⇒ matchCM θ c d
—matchTT c d =⇒ matchT01 c d =⇒ matchTM c d
—matchTT c d =⇒ matchTMT c d =⇒ matchTM c d
The last implications are trivial.



                                                      Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
12       ·        A. Popescu, J. Hölzl and T. Nipkow

   Note that discreetness trivially implies self 01-bisimilarity; however, it does not imply
self 01T-bisimilarity, since intuitively it does not exclude that, starting in different indistin-
guishable states, one execution terminates while the other has no possibility to terminate
immediately. In fact, the other execution may not have the possibility to ever terminate,
which shows that discreetness does not imply weak T-bisimilarity either. The last coun-
terexample is excluded by may-termination, a property that postulates precisely that there
is always a way to terminate; in fact, in the presence of may-termination, discreetness
does imply self weak T-bisimilarity. This will be the key to understanding compositionally
the syntactic criteria à la Smith and Volpano, which accept discreet non-self-isomorphic
programs only if they have finite behavior. (See also the discussion on page 20.)

                                                              1           2           3       4        5
                                                       1      c         mayT c     discr c   ϕc       ψc
                                                       2     atm         True     pres atm cpt atm cpt atm
                                      3; c ≈KS W c
                                  nnn
                                                                                                    ψT c1
                                nn
                             nnn
                                                                        mayT c1   discr c1   ϕ c1   ψ c2
                       nnn
                                                       3 Seq c1 c2
                                                                        mayT c2   discr c2   ϕ c2   ψ c1
             c ≈KS 01 c ck            c ≈@H WTKS c                                                  discr c2
                           PPPP
                               PPPP                                     mayT c1   discr c1
                                                                                            cpt tst cpt tst
                                   PPP                 4 If tst c1 c2                       ϕ c1     ψ c1
                                                                        mayT c2   discr c2
                                        c ≈01T                                              ϕ c2     ψ c2
                                           KS c
                                                                                            cpt tst
                                                       5 While tst d     False     discr d           False
                                                                                            ϕd
                                         c ≈KS S c                      mayT c1   discr c1   ϕ c1    ψ c1
                KS c
             discr                                     6 Par c1 c2
                                                                        mayT c2   discr c2   ϕ c2    ψ c2
                                                           ϕ ∈ {siso, ≈S, ≈01T, ≈WT} ψ ∈ {≈01, ≈W}
                                                                          
     discr c ∧ mayT c                    siso c                             ≈01T, if ψ = ≈01
                                                                  ψT ≡
                                                                            ≈WT, if ψ = ≈W
Figure 3: Implications between security notions                Figure 4: Compositionality table

   Example 1 already illustrates most of the above bisimilarities. Here are some further
illustrations that also take Proposition 2 into account (using the Example 1 notations).
   E XAMPLE 3. (1) c3 is self 01-bisimilar, as any two discreet processes are 01-bisimilar.
(2) However, c3 is not self 01T-bisimilar, as shown by the following reasoning: depending
on h, c3 can transit in one step (according to the operational semantics) to either d ≡ h :=
1 ; h := 2 or e ≡ h := 3; but d and e are not 01T-bisimilar, as d is not able to 01T-match
the immediate terminating step from e; then, by the definition of bisimilarity, c3 is not
self-01T-bisimilar either.
(3) The above is not a problem for weak T-bisimilarity though, since here d can catch up
with e by taking multiple steps. Thus, c3 is self weakly T-bisimilar (as any two discreet
processes with finite behavior are weakly T-bisimilar).
(4) c5 ≡ c3 ; l := 4 is self weakly T-bisimilar, since alternative executions (starting in
indistinguishable states) of its first part c3 are able to ≈WT -synchronize, so that they can
proceed strongly synchronously with the remaining non-discreet step l := 4.
(5) However, c5 is not self 01-bisimilar since the above e-continuation of c3 is able to
terminate first, putting itself in a position to take the non-discreet step l := 4, not available
at that time for the other continuation, d.
Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
              Formal Verification of Language-Based Concurrent Noninterference                  ·      13

(6) while h = 0 do h := 0 is discreet, hence self 01-bisimilar, but not weakly T-bisimilar,
as a diverging execution from h = 0 cannot match a terminating one from h 6= 0.
   The weak and 01-bisimilarities provide the most fruitful notions in type-system ap-
proaches to noninterference. (The others, namely, self isomorphism, discreetness and
strong bisimilarity, are too harsh requirements, but, as we shall see, turn out as useful
auxiliaries.) Smith and Volpano [42] focus on termination-sensitive weak bisimilarity. On
the other hand, Boudol and Castellani [6, 7] prefer termination-insensitive 01-bisimilarity,
while later Boudol [5] also considers weak bisimilarity, but in its termination-insensitive
form. In these works, the newly introduced bisimilarities are not formally compared with
preexisting ones—instead, the focus is on comparing the end-product type systems, i.e.,
the condition part of the contract (while the bisimilarities are the guarantee part). In order
to properly revisit and compare type-system results, we first need an analysis of composi-
tionality for these bisimilarities.

4.    COMPOSITIONALITY
We now move to the central concept of this paper—compositionality of noninterference
w.r.t. the language constructs.
   The following definitions of ∼- preservation and compatibility for tests and atoms will
represent basic building blocks in our compositionality analysis. All atoms will be as-
sumed at least ∼-compatible and occasionally tests will be assumed ∼-compatible as side-
conditions for compositionality w.r.t. If and While.
   An atom atm is called ∼-preserving, written pres atm, if ∀s. aexec atm s ∼ s; it is called
 ∼-compatible, written cpt atm, if ∀s t. s ∼ t =⇒ aexec atm s ∼ aexec atm t. A test tst is
called ∼-compatible, written cpt tst, if ∀s t. s ∼ t =⇒ tval tst s = tval tst t.
   In the setting of Example 2, the above notions can be understood as follows. For atoms,
∼-preservation means no assignment to low variables and ∼-compatibility means no direct
leaks, i.e., no assignment to low variables of expressions depending on high variables (high
expressions). For tests, ∼-compatibility means no dependence on high variables.
   The next proposition states various compositionality results, schematically represented
in Figure 4, as follows. The first column lists the possible forms of a command c (c may
be an atom atm, or have the form Seq c1 c2 , etc.). The next columns list conditions under
which the predicates stated on the first row hold for c. Thus, e.g., row 3 column 3 says: if
discr c1 and discr c2 then discr (Seq c1 c2 ). The horizontal line in row 3 column 5 represents
an “or” – thus, row 3 column 5 says: if either [ψT c1 and ψ c2 ] or [ψ c1 and discr c2 ] then
ψ (Seq c1 c2 ). The involved bisimilarities are considered in their unary, “self” form, e.g.,
ψ c means c ≈01 c or c ≈W c.
     P ROPOSITION 3. The compositionality facts stated in Figure 4 hold.
   P ROOF. As before, for statements involving binary relations, we prove the more general
form that does not assume the arguments equal. Thus, e.g., for ψ = ≈01 in row 3 column 5,
we prove facts (1) and (2) below; for ϕ = ≈S in row 5 column 4 we prove fact (3) below:
(1) c1 ≈01T d1 ∧ c2 ≈01 d2 =⇒ Seq c1 c2 ≈01 Seq d1 d2
(2) c1 ≈01 d1 ∧ discr c2 =⇒ Seq c1 c2 ≈01 Seq d1 c2
(3) cpt tst ∧ c ≈S d =⇒ While tst c ≈S While tst d
All the proofs are performed by coinduction on the right-hand side predicate, again, after
suitable rephrasing, e.g.:
                                                       Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
14       ·       A. Popescu, J. Hölzl and T. Nipkow

(1) (∃c1 d1 c2 d2 . c = Seq c1 c2 ∧ d = Seq d1 d2 ∧ c1 ≈01T d1 ∧ c2 ≈01 d2 ) =⇒ c ≈01 d
    is proved by coinduction on ≈01
(2) (∃c1 d1 c2 . c = Seq c1 c2 ∧ d = Seq d1 c2 ∧ c1 ≈01 d1 ∧ discr c2 ) =⇒ c ≈01 d
    is proved by coinduction on ≈01
(3) Assuming cpt tst, (∃c1 d1 . c = While tst c1 ∧ d = While tst d1 ∧ c1 ≈S d1 ) =⇒ c ≈S d
    is proved by coinduction on ≈S
The coinduction proofs proceed rather straightforwardly, albeit very tediously—they are
similar to the bisimilarity-preservation proofs for process algebra operators [2, 22]. One
needs to prove that the left-hand side of the implication (or occasionally, a slightly stronger
relation) is a generalized postfixpoint of the operator defining the right-hand side (i.e., a
bisimulation of a certain kind)—this process involves considering the operational seman-
tics back and forth, that is, using inversion rules followed by the direct rules used in the
definition of the semantics.
   E.g., for (1), we define θ c d ≡ ∃c1 d1 c2 d2 . c = Seq c1 c2 ∧ d = Seq d1 d2 ∧ c1 ≈01T d1 ∧
c2 ≈01 d2 . Recall from page 10 that the complete lattice L used to define our notions of se-
curity is the set of symmetric binary relations on commands. We first show that θ ∈ L, i.e.,
that θ is symmetric—this is immediate. It remains to show that θ ≤ ≈01 . Applying coin-
duction, it suffices to show that θ is a generalized postfixpoint of P, i.e., θ ≤ P (θ ∨ ≈01),
where P : L → L is the operator that defines ≈01 as its greatest fixpoint. By the definition of
P, this amounts to assuming that (A) θ c d holds, and showing that (B) matchC01 (θ ∨ ≈01) c d
and (C) matchT01 c d hold.
   We shall prove goal (B). ((C) follows by a similar reasoning.) Unfolding the definition
of matchC01 , we reduce (B) to the following: We fix s,t, c0 , s0 and assume (E) s ∼ t and (F)
(c, s)→C (c0 , s0 ). We need to show that one of the following three facts hold:
(G1) ∃d 0 t 0 . (d,t)→C (d 0 ,t 0 ) ∧ s0 ∼ t 0 ∧ (θ c0 d 0 ∨ c0 ≈01 d 0 )
(G2) s0 ∼ t ∧ (θ c0 d ∨ c0 ≈01 d)
(G3) ∃t 0 . (d,t)→Tt 0 ∧ s0 ∼ t 0 ∧ discr c0
From (A), we obtain c1 , d1 , c2 , d2 such that
(A1) c = Seq c1 c2 , (A2) d = Seq d1 d2 , (A3) c1 ≈01T d1 , and (A4) c2 ≈01 d2 .
From (A3) and the property of ≈01T of being a fixpoint , we obtain
(A31) matchC01C (≈01T) c1 d1 and (A32) matchTT c1 d1
From (A1) and (F), using the inversion rule for →C w.r.t. Seq, we split in 2 cases:
Case 1: c0 = c2 and (c1 , s)→T s0 . With (A32) and (E), we obtain t 0 such that s0 ∼ t 0 and
  (d1 ,t)→Tt 0 . Hence, from (A2) and the (direct) rules for →C , (d,t)→C (d2 ,t 0 ). Thus, taking
  d 0 = d2 , with (A4) we obtain (G1) (by satisfying the c0 ≈01 d 0 part of the disjunction), as
  desired.
Case 2: c0 has the form Seq c01 c2 for some c01 such that (c1 , s)→C (c01 , s0 ). With (A31) and
  (E), we split in 2 subcases:
  Case 2.1: There exist d10 and t 0 such that (d1 ,t)→C (d10 ,t 0 ), s0 ∼ t 0 , and c01 ≈01T d10 . By the
      definition of →C , we have (Seq d1 d2 ,t)→C (Seq d10 d2 ,t 0 ). Hence, taking d 0 = Seq d10 d2 ,
      we obtain (G1) (by satisfying the θ c0 d 0 part of the disjunction), as desired.
  Case 2.2: s0 ∼ t and c01 ≈01T d1 . Hence, taking d 0 = Seq d1 d2 , we obtain (G2) (by satis-
      fying the θ c0 d part of the disjunction), as desired.
   Occasionally, we have to strengthen the coinduction hypothesis. E.g., for (3), the rela-
tion we prove to be a generalized postfixpoint is not θ c d ≡ ∃c1 d1 . c = While tst c1 ∧
Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
               Formal Verification of Language-Based Concurrent Noninterference                         ·      15

d = While tst d1 ∧ c1 ≈S d1 , but rather θ c d ∨ θ 0 c d, where θ 0 c d ≡ ∃c2 d2 c1 d1 . c =
Seq c2 (While tst c1 ) ∧ d = Seq d2 (While tst d1 ) ∧ c2 ≈S d2 ∧ c1 ≈S d1 .

   E XAMPLE 4. The informal arguments in Examples 1 and 3 can be made rigorous using
the compositionality table in Figure 4 in conjunction with the implication graph in Figure 3.
We illustrate the emerging proof methodology for c4 from Example 1. c4 has the form
Seq (l := 4) c3 , where c3 has the form If (h = 0) (Seq (h := 1) (h := 2)) (h := 3). According
to the table (row 3 column 5), for c4 ≈01 c4 to hold, it suffices that (l := 4) ≈01T (l := 4) and
c3 ≈01 c3 . The former is true by the table (row 3 column 4), since l := 4 is compatible.
However, the table cannot help (yet) in proving c3 ≈01 c3 , because there (in row 4 column
5) the required side condition is cpt (h = 0), which does not hold. Therefore we turn to
the implication graph, and try to prove the fact for one of the predecessors of ≈01. One
predecessor is ≈01T , which again requires cpt (h = 0), and so does its predecessor ≈S ,
and so does the predecessor of the latter, siso, which is a bottom node—therefore this
attempt fails. The other predecessor of ≈01 is discr, for which the table does not require the
problematic side-condition. And the proof of discr c3 goes smoothly according to the table,
since it is reduced (by row 4 column 3) to discr (Seq (h := 1) (h := 2)) and discr (h := 3),
and further (by row 3 column 3) to discr (h := 1), discr (h := 2) and discr (h := 3), all being
true thanks to their ∼-preservation (by row 2 column 3).
   Note that we appeal to the Figure 3 graph whenever the table result is not sufficiently
strong, i.e., the given security notion is not sufficiently compositional w.r.t. the given lan-
guage construct. For this table-and-graph proof technique, it is instructive to compare the
termination-sensitive security notions with the termination-insensitive ones, that is, ϕ with
ψ in Figure 4. ϕ is more compositional than ψ w.r.t. Seq.5 Indeed, for ψ (Seq c1 c2 ) to go
through, the table requires strengthening ψ either for c1 to its termination-sensitive variant,
ψT , or for c2 to discreetness.
   A consequence of the above is also the lack of compositionality of ψ w.r.t. While (since
the semantics of While involves iteration of Seq)—hence the side-condition False in the ψ-
While column. False may seem like a very crude approximation, but one cannot hope for
anything better without engaging in a static analysis deeper than compositionality. Indeed,
as soon as alternative executions of c are allowed to desynchronize w.r.t. termination, their
iterations through While may desynchronize completely; an exception is the case when c is
in fact discreet, but this is covered in the overall scheme by “falling back” from ψ to discr
and applying compositionality of the latter.
   On the other hand, ψ enjoys better compositionality w.r.t. If . This is not visible by
looking at the table alone, where the If rules of ϕ and ψ are the same, and they are
both conditioned by the ∼-compatibility of tst. The difference appears when tst is not
compatible—then, according to the graph, unlike ϕ, ψ can again fall back on discr, which
does not require tst to be compatible. Indeed, unlike ϕ, ψ is above discr in the graph.
   Note that, among the ϕ’s, ≈WT is the best located with this respect, since it is above the
conjunction of discr c and mayT c in the graph. But this is still worse than ψ, since falling
back on discr c ∧ mayT c forbids while loops, as shown in the table for mayT.
   An interesting theoretical question is whether we can have the best of both worlds
and define a relation that is both above discreetness in the graph and fully compositional

5 Recallfrom page 7 that interactivity of the considered security notions ensures their Par-compositionality;
termination-sensitiveness plays a similar role for Seq-compositionality.

                                                               Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
16        ·      A. Popescu, J. Hölzl and T. Nipkow

w.r.t. Seq, without sacrificing compositionality with the other constructs. A positive answer
to this question is presented next.

5.     A MORE COMPOSITIONAL SECURITY NOTION
The rough idea of the proposed solution is as follows. If we knew that the whole program
terminates, then discreetness would imply ≈WT. And to integrate termination information
into our coinductive interactiveness, we note that, given a thread c running in parallel with
others so that all executions of the whole pool (including c) from a given state s are known
to terminate, the following are true: (1) the execution of c alone starting in s must termi-
nate; (2) between resumption points of the execution of c, the other threads are guaranteed
to change the state in such a way that termination of what remains to be executed from
c is preserved. Indeed, a violation of (1) or (2) would immediately yield a possibility of
nontermination for the whole pool. This leads us to ≈T , a relaxation of ≈WT with interac-
tivity restricted to mustT (“must terminate”) configurations, where mustT(c, s) is defined
to mean that there exists no infinite chain (c0 , s0 ), . . . , (cn , sn ), . . . such that (c0 , s0 ) = (c, s)
and ∀i. (ci , si )→C (ci+1 , si+1 ):
—matchCTMC θ c d ≡ ∀s t c0 s0 . mustT (c, s) ∧ mustT (d,t) ∧ s ∼ t ∧ (c, s)→C (c0 , s0 )
                                =⇒ (∃d 0 t 0 . (d,t)→C∗ (d 0 ,t 0 ) ∧ s0 ∼ t 0 ∧ θ c0 d 0 )
—matchTTMT c d ≡ ∀s t s0 . mustT (c, s) ∧ mustT (d,t) ∧ s ∼ t ∧ (c, s)→T s0
                           =⇒ (∃t 0 . (d,t)→T∗t 0 ∧ s0 ∼ t 0 )
—c ≈T d ≡ matchTMC (≈T) c d ∧ matchTTMT c d
                 C



   And, indeed, ≈T achieves the targeted properties, as can be shown by an argument similar
to those of Propositions 2 and 3:
   P ROPOSITION 4.
(1) The compositionality facts stated in Figure 4 for ϕ also hold for ≈T.
(2) discr c =⇒ c ≈T c and ≈WT c =⇒ c ≈T c
   P ROOF. (1): Similarly to Proposition 3.
(2) Similarly to Proposition 2.
   Note that ≈T does not require, for the involved programs, termination (a liveness prop-
erty), but rather preservation of termination (a safety property). In Example 1, c9 is the
program h0 := 0 ; d ; l := 4 where d is while h > 0 do {h := h − 1 ; h0 := h0 + 1}. We can
establish that c9 ≈T c9 :
—Intuitively, two alternative executions E0 and E1 of c9 starting with different initial values
 of h6 can be continuously synchronized as required by ≈T’s mathcers (continuation step
 against multiple continuation steps and termination step against multiple continuation
 steps followed by termination step) regardless of the intervention of the environment,
 provided this intervention does not break termination:
 —as long as Ei is still in the while loop, E1−i can also stay in the while loop;
 —as soon as Ei exits the while loop, thanks to preservation of termination, E1−i can also
    exit the while loop; hence E1−i can synchronize with Ei on the visible step l := 4.

6 We   may ignore (from the leakage point of view) the other high variable, h0 , since it is immediately rewritten.



Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
             Formal Verification of Language-Based Concurrent Noninterference                     ·      17

—Formally, the fact follows by the table-and-graph method: h0 := 0 and d are both discreet,
 hence their sequential composition is discreet, a fortiori self bisimilar w.r.t. ≈T ; l := 4 is
 self isomorphic, again a fortiori self bisimilar w.r.t. ≈T ; by the table, the composition c9
 is self bisimilar w.r.t. ≈T .
In the above “formal” argument, we used that ≈T is implied by both discreetness and self
isomorphism and is compositional w.r.t. sequential composition, which is not the case for
the other security notions. In fact, c9 is not secure according to these other notions—it
is not self weakly bisimilar essentially because, depending on the initial value of h, the
execution may loop (if h < 0) or may terminate assigning 4 to l (if h ≥ 0).
   But neither is ≈T implied by ≈W , not even by ≈01 . The program e, given by if h > 0 then
{l := 1 ; h := 0} else l := 1, is self 01-bisimilar. But e is not self bisimilar according to ≈T ;
this is essentially because, branching on the high variable h, the left branch may take the
continuation step l := 1 while the right branch only has a termination step l := 1 available,
thus failing to satisfy ≈T’s termination-versus-termination matcher.
   The fact that programs like e are self 01-bisimilar cannot be established by a syntactic
type-system-like criterion, as it depends on semantic behavior—to see this, imagine that,
instead of l := 1, we have l := E on the left branch and l := F on the right branch, where E
and F are complex expressions that happen to evaluate to the same value in this particular
context. In fact, as we show in the next section, if we only apply syntactic criteria based on
compositionality (which is what most security type systems from the literature do), there is
nothing we can prove about ≈W or ≈01 that we cannot also prove about ≈T —this is because
 ≈T is better located in the table-and-graph scheme.

6.    SYNTACTIC CRITERIA
The (compositionality based) table-and-graph proof technique described in Example 4 can
be automated, yielding a collection of recursive syntactic predicates corresponding to the
various security notions. The recursive clauses for these predicates will simply perform
the necessary lookups: first in the table, then, if needed, in the graph.
6.1   Extraction of Syntactic Criteria
Before listing these clauses, we first simplify the Figure 3 graph, noticing that ≈S and ≈01T
are redundant nodes on top of siso. Indeed, the compositionality conditions for ≈S and ≈01T
from the Figure 4 table are identical to those of all nodes below, hence identical to those
of siso. This means that, when proving c ≈S c or c ≈01T c, one cannot do better than proving
compositionality of the stronger (more desirable) siso notion of security. We therefore drop
 ≈S and ≈01T from the graph. Figure 5 shows this new graph, where ≈T is also integrated.
In the Figure 4 table, we also redefine ψT by redirecting ≈01 to siso:
                                         
                                           siso, if ψ = ≈01
                                 ψT ≡
                                           ≈WT , if ψ = ≈W
   Let us introduce some notation for the Figure 4 table and the Figure 5 graph. A (syn-
tactic) constructor Cns is any of the following: Seq, If tst where tst ∈ test, While tst where
tst ∈ test, Par. In addition, for uniformity, we also introduce a constructor Atm atm for
every atm ∈ atom, and assume Atm atm is the same as atm. Thus, any command c has the
form Cns c1 . . . ck , where Cns is a constructor and c1 . . . ck are k commands, the components
of c, with k either 0, 1 or 2, depending on Cns (it is 0 for Atm atm).

                                                         Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
18       ·       A. Popescu, J. Hölzl and T. Nipkow


                                                                                                            ≈TKS c


                          c >F ≈T cai                   c ≈W c
                                       KKKKK sss 5= KS                                                          ≈W c
                                            KKKKssss
                                                sKsK                                                    tt
                                                                                                         t tt 6> KS
                                           ssssKKKKKKK                                          tttttt
                                                                                                        t
                                      sssss
                         c ≈KS 01X` c                   c ≈>F WT                        tttttt
                                   8888                       KS c
                                       8888                               ≈01KS W_ c
                                                                                     7777
                                                                                                               ≈?G WT
                                                                                                                    KS c
                                                                                                              
                                           8888                                    7777                
                                              8888                                        7777 
                                                  8                                             7777
                            KS c 88888
                         discr
                                                                                                    77
                                                     8                        KS c  7777
                                          888888
                                                                            discr
                                                      888                                           7777
                                                                                                    7777
                  discr c ∧ mayT c                                                    
                                                                                                             77
                                                      siso c
                                                                      discr c ∧ mayT c                     siso c
      Figure 5: Simplified implication graph of
      security notions                                               Figure 6: Syntactic implications



   Henceforth, we let χ range over the notions in the table, namely, χ ∈ {mayT, discr,
siso, ≈S, ≈01T, ≈WT, ≈01, ≈W, ≈T}. The table has an entry corresponding to every combination
(χ, Cns), for which we define the following:
—sideχ,Cns is its side condition, i.e., the part of it not depending on the components. If this
 part is empty, we put True. E.g., sidemayT,Atm atm = sidesiso,Seq = True, sidesiso,If tst = cpt tst.
—rcondχ,Cns (c1 , . . . , ck ) is its recursion condition, i.e., the part involving the components
 of c. Again, if this part is empty, we put True. E.g., rcondmayT,Atm atm = True,
 rcondsiso,Seq (c1 , c2 ) = rcondsiso,If tst (c1 , c2 ) = (siso c1 ∧ siso c2 ).
For any element χ in the graph, we let Pred χ denote its set of predecessors. E.g.,
            / Pred ≈01 = {discr, siso}, Pred ≈W = {≈01, ≈WT}.
Pred siso = 0,
     Note that, for all χ, Cns, and c of the form Cns c1 . . . ck ,
—The table ensures that sideχ,Cns ∧ rcondχ,Cns (c1 , . . . , ck ) =⇒ χ c;
—The graph ensures that ( χ 0 ∈Pred χ χ 0 c) =⇒ χ c.
                          W

We define, for each security notions χ, a syntactic predicate χ on commands by turning
the above implications into recursive clauses for each constructor Cns, where one first tries
the table, and then, if the table fails, one tries the graph:
                                  
                                    rcondχ,Cns (c1 , . . . , ck ), if sideχ,Cns (c1 , . . . , ck ),
           χ (Cns c1 . . . ck ) ≡   W              0
                                      χ 0 ∈Pred χ χ (Cns c1 . . . ck ),    otherwise,
where rcondχ,Cns is rcondχ,Cns with all the involved security predicates χ 0 replaced by their
syntactic counterparts χ 0 .
  We define the above χ’s one at a time, traversing the graph in Figure 5 bottom-up, in
some order consistent with the graph. Thus, at the time we define some χ, we have χ 0
available for all χ 0 ∈ Pred χ.
  For example, taking Cns = If tst, we have:
(1) discr (If tst c1 c2 ) = (discr c1 ∧ discr c2 ).
Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
               Formal Verification of Language-Based Concurrent Noninterference                            ·      19
                             
                                 siso c1 ∧ siso c2 , if cpt tst
(2) siso (If tst c1 c2 ) =
                                 False, otherwise.
                          
                             ≈01 c1 ∧ ≈01 c2 , if cpt tst
(3) ≈01 (If tst c1 c2 ) =
                            discr (If tst c1 c2 ) ∨ siso (If tst c1 c2 ), otherwise
                        
                           ≈01 c1 ∧ ≈01 c2 , if cpt tst
    = (by 1 and 2) =
                          discr c1 ∧ discr c2 , otherwise.
(Recall that, when we instantiate χ to a bisimilarity such as ≈WT , we refer to its unary
version, taking χ c to be c ≈WT c. Hence, an instance of χ is the unary predicate ≈WT .)
   Note that the functions χ are not entirely syntactic, since for test and atoms they employ
the semantic notions of compatibility and preservation. For instance, the atom l := h − h
is ∼-compatible, since it merely assigns 0 to l, but a standard syntactic analysis would
reject it since its left-hand side contains h and hence it may depend on h. In what follows,
we ignore this aspect and pretend that ∼-compatibility and ∼-preservation are already
“syntactic”; but the results of this paper still hold if one replaces these notions with any
syntactic notions that approximate them.
6.2   Soundness
We can show that the automatically extracted syntactic criteria are valid approximations of
the semantic notions:
  P ROPOSITION 5. The syntactic criteria χ are sound for the security notions χ in Fig-
ure 5, in that χ c =⇒ χ c for all commands c.
  P ROOF. We prove χ c =⇒ χ c separately, for each χ, observing the implication-graph
order: we prove the fact for χ only after it has been proved for all χ 0 ∈ Pred χ. With the
semantic implication and compositionality results in place, the facts follow by structural
induction on c. Schematically, assuming inductively that c has the form Cns c1 . . . ck and
χ c holds, we distinguish 2 cases:
—If sideχ,Cns (c1 , . . . , ck ) holds, then χ c = rcondχ,Cns (c1 , . . . , ck ). By the induction hypoth-
 esis rcondχ,Cns (c1 , . . . , ck ) implies rcondχ,Cns (c1 , . . . , ck ), which in turn, by Proposition 3
 or 4(1), implies χ (Cns c1 . . . ck ), i.e., χ c. Thus, χ c =⇒ χ c.
—If sideχ,Cns (c1 , . . . , ck ) does not hold, then χ c = χ 0 ∈Pred χ χ 0 c. Since we assume the
                                                               W

 fact proved for the predecessor of χ, χ 0 ∈Pred χ χ 0 c implies χ 0 ∈Pred χ χ 0 c, which in
                                                 W                                W

 turn, by Proposition 2 or 4(2), implies χ c. Thus, again χ c =⇒ χ c.
This concludes the proof.
   A remarkable property of the χ’s is that they preserve the Figure 5 hierarchy of χ’s. Even
more remarkable is that they actually refine it. The hierarchy refinement from Figure 5 to
Figure 6 consists of the advance of ≈T to the top, even though ≈T is not weaker than ≈W
or ≈01.
   P ROPOSITION 6. The implications listed in Figure 6 hold.
   P ROOF. Let ϕ and χ be such that ϕ is located below χ in the Figure 6 graph. We have
2 cases.
   Case 1: ϕ is also located below χ in the implication graph of Figure 5, (which means,
by Proposition 3 or 4(1), that ∀d. ϕ d =⇒ χ d). There are 2 crucial facts to notice about
the recursive clauses for ϕ and χ:
                                                                  Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
20       ·       A. Popescu, J. Hölzl and T. Nipkow

(1) sideχ,Cns (c1 , . . . , ck ) =⇒ sideϕ,Cns (c1 , . . . , ck )
(2) Assuming sideχ,Cns (c1 , . . . , ck ) holds and ∀i ∈ {1, . . . , k}. ϕ ci =⇒ χ ci , then
    rcondϕ,Cns (c1 , . . . , ck ) =⇒ rcondχ,Cns (c1 , . . . , ck ).

   We now prove ϕ c =⇒ χ c by induction on c. Assume inductively                            that c has the
form Cns c1 . . . ck . If sideχ,Cns (c1 , . . . , ck ) does not hold, then χ c = χ 0 ∈Pred χ χ 0 c and
                                                                                   W

the proof is done, since ϕ ∈ Pred χ. On the other hand, if sideχ,Cns (c1 , . . . , ck ) holds,
then ,by (1), sideϕ,Cns (c1 , . . . , ck ) also holds. Thus ϕ c = rcondϕ,Cns (c1 , . . . , ck ) and χ c =
rcondχ,Cns (c1 , . . . , ck ), and hence the desired fact follows from the induction hypothesis and
(2).
   Case 2: ϕ = ≈W and χ = ≈T . We first prove
(3) ≈01 c =⇒ ≈T c,
by induction on c. Assume inductively that c has the form Cns c1 . . . ck .
   First assume side ≈01 ,Cns (c1 , . . . , ck ) holds. Then so does side ≈T ,Cns (c1 , . . . , ck ) (immedi-
ate verification). Thus, ≈01 c = rcond ≈01 ,Cns (c1 , . . . , ck ) and ≈T c = rcond ≈T ,Cns (c1 , . . . , ck ).
If Cns 6= Seq, then the desired fact follows by the induction hypothesis. If Cns = Seq,
then the desired fact follows from the induction hypothesis together with two facts already
proved at Case 1, namely, ∀d. discr d =⇒ ≈T d and ∀d. ≈WT d =⇒W≈T d.
   Next assume side ≈01 ,Cns (c1 , . . . , ck ) does not hold. Then ≈01 c = χ 0 ∈Pred ≈01 χ 0 c, and
from Case 1 we know that χ 0 c =⇒ ≈T c for all χ 0 ∈ Pred, hence the desired fact follows.
   Finally, we prove ≈W c =⇒ ≈T c by induction on c. The proof goes similarly to that
of (3), but now using ∀d. ≈01 d =⇒ ≈T d (i.e., fact (3)) and ∀d. ≈WT d =⇒ ≈T d in case
side ≈W ,Cns (c1 , . . . , ck ) holds and Cns = Seq.

  Note that the rationale behind why ≈T “wins the battle” against ≈01 and ≈W , advancing
above them in the syntactic graph (in spite of its semantic counterpart ≈T not being above
 ≈01 or ≈W the semantic graph), is that, on the one hand, ≈T is more compositional than ≈01
and ≈W, and, on the other, it dominates their (semantic) graph predecessors.
6.3    Connections with Syntactic Criteria from the Literature
So far, our analysis was purely semantic and local: for semantic notions of security χ,
we studied compositionality w.r.t. each language construct, inferring from these syntactic
criteria χ automatically. Now it is time to have a closer look at the recursive clauses of χ
and see what they tell us about χ independently of χ. First the easy cases:
—mayT c holds iff c does not contain while loops.
—discr c holds iff all atoms in c are ∼-preserving, a.k.a. high.
—siso c holds iff all tests in c are ∼-compatible, a.k.a. low, and all atoms are ∼-compatible.
In what follows, we invoke syntactic criteria from the literature. Usually these results are
presented as “security type systems”, while we employ a syntax-directed presentation as
structurally recursive functions χ on the syntax of programs. For readers familiar with
language-based noninterference, it should be intuitively obvious that the two styles of pre-
sentation are equivalent—we examine this equivalence in detail in the technical report [28].
   siso c corresponds to a type system from Smith and Volpano [42] for scheduler indepen-
dent security – this criterion is extremely harsh, forbidding high tests at If and While.
   We now move to the more interesting cases. ≈WT c is equivalent to another, possibilistic
type system from Smith and Volpano [42]. Here, high tests are allowed at If provided the

Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
             Formal Verification of Language-Based Concurrent Noninterference                     ·      21

branches are discreet. However, high tests are entirely disallowed at While:
                       
                        ≈WT c, if cpt tst                           
                                                                       ≈WT c, if cpt tst
   ≈WT (While tst c) = discr (While tst c) ∧ mayT (While tst c), =
                                                                       False, otherwise
                                  otherwise
                       

The above harsh condition on While is the starting point of work by Boudol and Castellani
in [6, 7], where a type system equivalent to ≈01 is introduced. ≈01 allows high tests for
While provided the body of the While is discreet. This is possible because, unlike ≈WT ,
 ≈01 can fall back on discr:
   ≈01 (While tst c) = discr (While tst c) ∨ siso (While tst c) = discr c ∨ (cpt tst ∧ siso c)
(as we have seen, a limitation shared by all termination-insensitive notions). Indeed, ≈WT
commutes smoothly with Seq as
                           ≈WT (Seq c1 c2 ) = ( ≈WT c1 ∧ ≈WT c2 )
but ≈01 needs either siso on the left or discr on the right:
                ≈01 (Seq c1 c2 ) = (siso c1 ∧ ≈01 c2 ) ∨ ( ≈01 c1 ∧ discr c2 )
Thus, ≈01 requires that either c1 has only low tests, or c2 has only high atoms. Hence, e.g.,
the command c5 from Example 1 is accepted by ≈WT , but rejected by ≈01 .
   An improvement of ≈01 that accepts c5 also is proposed by Boudol in [5], where the
idea is that, in the c1 part of Seq c1 c2 , one should no longer restrict to low tests everywhere,
but rather only in places that may affect termination (i.e., inside While loops). Interestingly,
this condition on c1 is the one imposed by ≈WT , and therefore the approach of [5] can be
seen as a carefully designed combination of ≈WT and ≈01 . Remarkably, it turns out to be
equivalent to ≈W , whose Seq clause is:
                ≈W (Seq c1 c2 ) = ( ≈WT c1 ∧ ≈W c2 ) ∨ ( ≈W c1 ∧ discr c2 )
   In the above cited work, the soundness theorems for the proposed type systems (results
corresponding to Proposition 5) are given rather elaborate proofs, defining global bisim-
ulation relations that involve multiple language constructs combined in ingenious and ad
hoc ways. These proofs are often hard to understand and mechanize. Moreover, they are
not exploiting the uniformities, commonalities and inter-dependencies of the various ap-
proaches. By contrast, our proof methodology is entirely local and uniform: we choose
a language construct and a notion of security, and essentially do our best at proving (par-
tial) compositionality. Then syntactic criteria follow automatically by our table-and-graph
method. We were pleasantly surprised to find that this general method could capture such
a variety of ad hoc results. Note that these criteria are expressed not relationally, as type
systems, but functionally, as recursively defined operators on syntax, which makes them
trivially syntax-directed.
   Finally, we discuss ≈T , which is our own novel type-system-like criterion for noninter-
ference. It turns out to be a natural extension of the original Volpano-Smith-Irvine typing
of sequential programs [46], using the same clauses for the sequential part together with
                             ≈T (Par c1 c2 ) = ( ≈T c1 ∧ ≈T c2 )
The reason why such a natural type system is absent from the literature is probably that its
associated semantic notion of security, ≈T , was overlooked.
                                                         Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
22       ·       A. Popescu, J. Hölzl and T. Nipkow

   ≈T accepts the commands c9 and c10 ≡ c9 k l := 1 k h := 0 k h := h + 1 from Example
1 (as shown by immediate computation with the clauses of ≈T and its predecessors in the
graph), while the most permissive criterion studied so far, ≈W , rejects them. However, as
discussed, the security property that ≈T guarantees, ≈T , is different from ≈W , the main
restriction of ≈T being that it only makes sense under the termination assumption. Thus,
 ≈T provides a useful guarantee for c9 and c10 only in cases when the initial state s ensures
termination, here, if it has h ≥ 0. On the other hand, ≈W rejects c10 out of fear that its
c9 component may not terminate, which could in principle yield the pipelining of the c9
termination channel into a standard channel for c10 . Termination knowledge excludes such
behavior, and this is where the new criterion ≈T is advantageous. In summary, ≈T is
superior to the other criteria if and only if the termination behavior can be analyzed in
some way.

7.    AFTER-EXECUTION NONINTERFERENCE
The bisimilarity-based notions of security studied so far are rather complex, assuming an
elaborate attacker model that interacts continuously with program execution—we call these
during-execution noninterference. Often one is interested in a more tractable notion, as an
input-to-output property, such as: a command is secure if, upon execution starting in indis-
tinguishable states, the result states (after the command has finished executing) are again
indistinguishable. We call such input-to-output properties after-execution noninterference.
   So what are the after-execution guarantees of the various bisimilarities from Section 3?
To answer this, we need some terminology. Given a configuration (c, s):
—A finite execution trace starting in (c, s) (finite (c, s)-trace for short) is a finite sequence
 of the form (c0 , s0 ), (c1 , s1 ), . . . , (cn−1 , sn−1 ), sn (consisting of a number of configurations
 followed by a state) such that (c0 , s0 ) = (c, s), (ci , si )→C (ci+1 , si+1 ) for all i < n − 1, and
 (cn−1 , sn−1 )→T sn . Then n is said to be the length of the trace and sn the final state of the
 trace.
—An infinite execution trace starting in (c, s) (infinite (c, s)-trace for short) is an infinite
 sequence of the form (c0 , s0 ), (c1 , s1 ), . . . (consisting of configurations only) such that
 (c0 , s0 ) = (c, s) and ∀i. (ci , si )→C (ci+1 , si+1 ).
   Given a finite (c, s)-trace tr, length(tr) denotes its length and fstate(tr) denotes its final
state. Thus, finite (c, s)-traces represent the terminating computations starting in (c, s), and
infinite (c, s)-traces the divergent computations starting in (c, s). Note that (c, s) “must
terminate” (as defined in Section 5) iff there exist no infinite (c, s)-traces.
   We first need to establish a property of the “weak” notions of bisimilarity concerning
matching multi-steps by suitable multi-steps:
     P ROPOSITION 7.
(1) If c ≈WT d, s ∼ t and (c, s)→C∗ (c0 , s0 ), then there exist d 0 and t 0 such that (d,t)→C∗ (d 0 ,t 0 ),
    s0 ∼ t 0 , and c0 ≈WT d 0 .
(2) If c ≈WT d, s ∼ t and (c, s)→T∗ s0 , then there exists t 0 such that (d,t)→T∗t 0 and s0 ∼ t 0 .
(3) If c ≈W d, s ∼ t and (c, s)→C∗ (c0 , s0 ), then one of the following holds:
    —discr c0 holds and there exists t 0 such that (d,t)→T∗t 0 and s0 ∼ t 0 .
    —There exist d 0 and t 0 such that (d,t)→C∗ (d 0 ,t 0 ), s0 ∼ t 0 , and c0 ≈W d 0 .
(4) If c ≈W d, s ∼ t and (c, s)→T∗ s0 , then one of the following holds:
Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
               Formal Verification of Language-Based Concurrent Noninterference                       ·      23

    —There exists t 0 such that (d,t)→T∗t 0 and s0 ∼ t 0 .
    —There exist d 0 and t 0 such that (d,t)→C∗ (d 0 ,t 0 ), s0 ∼ t 0 , and discr d.
(5) If mustT c, mustT d, c ≈T d, s ∼ t and (c, s)→C∗ (c0 , s0 ), then there exist d 0 and t 0 such
    that (d,t)→C∗ (d 0 ,t 0 ), s0 ∼ t 0 , and c0 ≈T d 0 .
(6) If mustT c, mustT d, c ≈T d, s ∼ t and (c, s)→T∗ s0 , then there exists t 0 such that (d,t)→T∗t 0
    and s0 ∼ t 0 .
   P ROOF. (1), (3), (5): By a straightforward induction on the the definition of →C∗ , using
the definitions of the matchers involved in ≈WT , ≈W and ≈T .
(2), (4), (6): From (1), (3) and (5), respectively, using again the definitions of the involved
matchers.
   As a technical tool for the proofs that follow, we define a partial trace to be a fi-
nite sequence of the form (c0 , s0 ), (c1 , s1 ), . . . , (cn−1 , sn−1 ) such that (c0 , s0 ) = (c, s) and
(ci , si )→C (ci+1 , si+1 ) for all i < n − 1. Note that any finite trace consists of a partial trace
as above together with a terminating state sn , such (cn−1 , sn−1 )→T sn .
   We can now to prove the following about the termination-sensitive bisimilarities:
   P ROPOSITION 8.
(1) If c ≈S c and s ∼ t, then, for every finite (c, s)-trace tr, there exists a finite (c,t)-trace tr0
with fstate(tr0 ) ∼ fstate(tr) and length(tr0 ) = length(tr).
(2) If c ≈01T c and s ∼ t, then, for every finite (c, s)-trace tr, there exists a finite (c,t)-trace
tr0 with fstate(tr0 ) ∼ fstate(tr) and length(tr0 ) ≤ length(tr).
(3) If c ≈WT c and s ∼ t, then, for every finite (c, s)-trace tr, there exists a finite (c,t)-trace
tr0 with fstate(tr0 ) ∼ fstate(tr).
   P ROOF. As usual, we prove the facts in the more general binary format, e.g.:
If c ≈S d and s ∼ t, then, for every finite (c, s)-trace tr, there exists a finite (d,t)-trace tr0
with fstate(tr0 ) ∼ fstate(tr) and length(tr0 ) = length(tr).
(1) and (2): We first prove these facts for partial traces instead of finite traces, by a straight-
forward induction on the partial trace tr. Then the facts for finite traces follow from ≈S
and ≈01T . matching terminating steps with terminating steps.
(3): From Proposition 7(2), using the correspondence between terminating traces starting
at (c, s) and ending at s0 and terminating multi-steps (c, s)→T∗ s0 .
   Thus, for self strongly bisimilar commands, terminating executions starting in indistin-
guishable states have, up to indistinguishability, the same outcomes, obtained in the same
amount of time—this means both standard (low data) channels and timing channels are
secure here. For self weakly T-bisimilar commands, again the outcomes are the same up to
indistinguishability, but timing channels are no longer secured. As usual, 01T-bisimilarity
lies in between—there is a time guarantee, but weaker than perfect synchronization.
   Now, turning to the termination-insensitive notions, during-execution security faces the
difficulty that here terminating executions need not be matched by terminating executions.
However, we can still prove a termination-conditioned result:
 P ROPOSITION 9. If ∀s0 . mustT (c, s0 ) holds, then Proposition 8(3) holds with any of
≈01 and ≈W substituted for ≈WT .
   P ROOF. Again, we prove the more general, binary facts, e.g.: If ∀t 0 . mustT (d,t 0 ) holds,
c ≈W d and s ∼ t, then, for every finite (c, s)-trace tr, there exists a finite (d,t)-trace tr0 with
fstate(tr0 ) ∼ fstate(tr).
                                                             Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
24       ·       A. Popescu, J. Hölzl and T. Nipkow


     Syntactic Criteria (Sect. 6)                 Concrete (Example 2)             After Execution (Sect. 7)
                                   ffffff                                         nnn
                           ffffff                                            nnnnn
                                                                          nnn
                                                                       nnn
     Compositionality (Sect. 4, 5)
                           XXXXXX                                     n
                                   XXXXXX                            n
                                                                  nnn
                                               During Execution (Sect. 3)

                                             Language Semantics (Sect. 2)

                                   Fig. 7: Main theory structure of the formalization


   Assuming c ≈W d, s ∼ t and given a trace tr starting at (c, s) and ending at s0 , by Propo-
sition 7(4) we have two cases:
—There is a trace starting at (d,t) and ending at some t 0 with s0 ∼ t 0 . Then we are done.
—There is a partial trace tr0 starting at (d,t) and ending at some (d 0 ,t 0 ) with s0 ∼ t 0 and
 discr d 0 . By our must-terminate assumption and Proposition 1, there is a trace tr00 from
 (d 0 ,t 0 ) to some state t 00 . By the discreetness of d 0 , we have t 00 ∼ t 0 , hence t 00 ∼ s0 . There-
 fore, tr0 · tr00 , the concatenation of tr0 and tr00 , is the desired trace matching tr.
For ≈01 , the proof is similar, but the first step, namely, that obtaining the partial trace tr0 ,
requires induction on tr.
  Thus, in the termination-insensitive case, the after-execution distinction between 01-
and weak bisimilarity vanishes. As for the after-execution guarantee of our termination-
sensitive security notion ≈T from Section 5, it is weaker than that of ≈WT (Proposition 8(3)),
but stronger than that of ≈01 and ≈W (Proposition 9):
   P ROPOSITION 10. If mustT (c, s) holds, then Proposition 8(3) holds with ≈T substi-
tuted for ≈WT .
   P ROOF. We prove the binary fact: If mustT (c, s), mustT (d,t), c ≈W d and s ∼ t, then,
for every finite (c, s)-trace tr, there exists a finite (d,t)-trace tr0 with fstate(tr0 ) ∼ fstate(tr).
   The fact follows from Proposition 7(6).

8.    ISABELLE FORMALIZATION
The results presented in this paper have been formalized in Isabelle/HOL—the develop-
ment is publicly available in the Isabelle Archive of Formal Proofs [29].
   The Isabelle proofs are essentially detailing the proof sketches shown in the paper. What
we deem “trivial” or “straightforward” in the proof sketches is usually handled automati-
cally by Isabelle’s “auto” tactic.
   The formal proofs by coinduction, especially those of compositionality facts, were very
tedious, having to expand the definition of matchers, apply inversion rules and consider
several cases. There were three choices that helped keep the proof sizes under control to
some extent:
—Taking the greatest fixpoints in the space of symmetric binary relations (rather than in
 that of arbitrary binary relations) allowed us to only consider half of the bisimilarity
 game: a right step simulating a left step, but not vice versa. In exchange, we had to

Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
             Formal Verification of Language-Based Concurrent Noninterference                    ·      25

 prove that the bisimulation candidates (i.e., the relations to be proved postfixpoints)
 were symmetric, which was always immediate.
—Working with generalized postfixpoints (rather than plain postfixpoints) allowed us to
 employ smaller bisimulation candidates, namely, ones that “stop” when reaching bisim-
 ilar items. This helped reduce the size of the proofs for operators such as sequential
 composition and while.
—Using the Sledgehammer tool for deploying external automatic theorem provers [26]
 helped automate some of the tedious ∀∃ reasoning specific to coinduction/bisimilarity
 proofs. This was especially true for the simpler security predicates siso and discr.
   Proofs by coinduction are still not supported in Isabelle as well as they could be. Many
goals had a special form, namely, conditional equations with equality being bisimilarity.
To put such goals in a form suitable for coinduction, we had to rephrase them employing
existential quantification, as in the proof sketch of Proposition 3; the existential quantifi-
cation is later eliminated. A more intuitive proof would proceed directly to unfolding the
terms of the equation according to the operational semantics—an Isabelle coinduction tac-
tic providing direct unfolding for goals of this pattern would allow shorter and cleaner
proofs. This technology is under development within Isabelle’s (co)datatype project [44].
   The compositionality results account for about half of the size of the overall develop-
ment: 2729 lines out of a total of 6221. Of course, not only the length of the proofs, but
also the sheer number of facts stated in Figure 4’s table is a contributing factor to this size.
   On the bright side, the proofs of the soundness of, and implications between, the syntac-
tic criteria go very smoothly. For instance, here is the whole formal proof of Proposition 6:
theorem SC_siso_imp_SC_WbisT[intro]: "SC_siso c =⇒ SC_WbisT c"
  by (induct c) auto

theorem SC_discr_imp_SC_WbisT[intro]:
"SC_mayT c =⇒ SC_discr c =⇒ SC_WbisT c"
  by (induct c) (auto simp: presAtm_compatAtm)

theorem SC_discr_imp_SC_ZObis[intro]: "SC_discr c =⇒ SC_ZObis c"
  by (induct c) (auto simp: presAtm_compatAtm)

theorem SC_siso_imp_SC_ZObis[intro]: "SC_siso c =⇒                             SC_ZObis c"
  by (induct c) auto

theorem SC_ZObis_imp_SC_Wbis[intro]: "SC_ZObis c =⇒ SC_Wbis c"
  by (induct c) auto

theorem SC_WbisT_imp_SC_Wbis[intro]: "SC_WbisT c =⇒                              SC_Wbis c"
  by (induct c) auto

theorem SC_discr_imp_SC_BisT[intro]: "SC_discr c =⇒                              SC_BisT c"
  by (induct c) (auto simp: presAtm_compatAtm)

theorem SC_WbisT_imp_SC_BisT[intro]: "SC_WbisT c =⇒                              SC_BisT c"
  by (induct c) auto
                                                        Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
26       ·       A. Popescu, J. Hölzl and T. Nipkow



theorem SC_ZObis_imp_SC_BisT[intro]: "SC_ZObis c =⇒                      SC_BisT c"
  by (induct c) auto

theorem SC_Wbis_imp_SC_BisT[intro]: "SC_Wbis c =⇒ SC_BisT c"
  by (induct c) (auto split: split_if_asm)
   Above, the syntactic analogues of the semantics notions, indicated in the paper by
overlining, e.g., discr, are prefixed by “SC” (from “syntactic criterion”), e.g., SC discr,
SC WbisT. The proofs go fully automatically after issuing a structural induction on the
command c. However, as observed in the informal proof, the order of stating these facts is
important: one needs to start at the bottom of Figure 6’s graph and advance upwards. In
the formalization, a proved fact is declared as an introduction rule, so that proofs of facts
located above in the graph can use them automatically (via the “auto” method).
   An interesting question is whether we would have been better off had we worked schemat-
ically, as we informally did in the presentation of this paper: stating and proving facts uni-
versally quantified over the set of the considered bisimilarities, having an Isabelle operator
 T that maps each termination-insensitive notion ψ to its termination-sensitive counterpart
ψT , etc. In other words, would it have helped to employ a deep embedding of our informal
schemas? We believe the answer is no, due to the substantial bureaucracy associated with
switching from such a deep embedding back to the shallow(er) end results.

9.    CONCLUSIONS AND MORE RELATED WORK
This paper was concerned with systematizing and comparing existing type-system based
noninterference results from the literature. As a technical tool, we have introduced a
compositionality “table-and-graph” technique able to capture such results in a uniform
way. The study also suggested a novel, suitably compositional, notion, the termination-
interactive bisimilarity ≈T.
   Our approach has important precursors in the literature. [38] makes a strong case for
compositionality, and illustrates how it can be used to extend to concurrency a noninterfer-
ence result [1] in the style of Volpano and Smith. However, [38] does not pursue this idea
systematically or devise a general technique as we do in this paper.
   Another line of work focusing on compositionality in language-based security is Mor-
gan’s shadow semantics [23, 24], which defines a Hoare-style program logic together with
a notion of refinement coping with security. This work, inspired by knowledge logic [12],
goes beyond type systems and pure noninterference, allowing one to express and prove
interactively complex declassification properties. The approach is currently restricted to
nondeterministic sequential programs.
   Our bisimilarity-based treatment also employs insight from process algebra [22] in gen-
eral and from process algebra approaches to noninterference [11] in particular. In system-
based security, [12, 15, 21] provide general frameworks for trace-based system security,
the last two having a special focus on compositionality and the first also incorporating
probabilistic systems.
   While the execution traces of programs form systems in the sense of these frameworks,
language-based security has developed a specific set of concepts and methods (some of
them reviewed in this paper) whose relationship with system security is a nontrivial prob-
lem, analyzed in [16, 17, 45]. The Goguen-Meseguer-style trace-based noninterference,

Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
             Formal Verification of Language-Based Concurrent Noninterference                 ·      27

an adaptation of which we also employ in this paper, has been challenged in [10], which
proposes a refinement of the notion using partial orderings of events to account for collab-
orating adversaries.
   We only gave small examples of programs used to distinguish between the various
notions of security. However, there is no fundamental difficulty with applying these re-
sults to much larger programs—our network of syntactic criteria from Section 6 employ a
fairly efficient traversal of the program syntax. More substantial difficulties with extend-
ing the analysis to realistic programs are the programming-language and programming-
environment features. Themes missing from our compositionality framework are prob-
abilistic noninterference [19, 39–41], dynamic thread creation [19, 38, 47] and scheduler
independence [7, 19, 38, 47], known to be particularly problematic w.r.t. noninterference.
We have dedicated them a separate study in [30], where we identify a class of schedulers
that guarantee probabilistic noninterference of a thread pool assumed to satisfy possibilis-
tic noninterference; the guarantee is valid in the presence of dynamic thread creation. No
particular programming language is considered there, but the abstract relationship between
scheduler and thread pool is studied in depth.
   Amongst previous formalizations of noninterference-like properties, the most closely
related to our work are Snelting and Wasserrab’s formalization of the original Volpano-
Smith-Irvine type system for single-threaded programs [43] and Barthe and Nieto’s formal-
ization of the Boudol-Castellani approach [4], both in Isabelle. Recently, David Cock [8]
has formalized in Isabelle noninterference of a probabilistic scheduler and has discussed
its integration with the seL4 operating system kernel verification [14]. In the Coq proof
assistant, Nanevski, Banerjee and Garg have formalized the Relational Hoare Type The-
ory [25], a shallowly embedded framework for establishing security properties on top of a
realistic sequential language featuring mutable state and dynamic memory allocation.
   An exciting future direction is a framework for proving concurrent noninterference by
a combination of automated and interactive methods along the lines of approaches going
beyond type systems [3, 9, 18, 23, 24]. This would follow a rely-guarantee paradigm [13],
with information about the environment made available to individual threads by suitably
relaxing interactivity. A step towards this direction is made by our bisimilarity ≈T , where
such context information is termination, but could in principle be any liveness property.

Acknowledgements. Jasmin Blanchette made lots of suggestions that have significantly
improved the presentation of the paper. Benedict Nordhoff and Peter Lammich noticed
various technical typos. The anonymous reviewers of both the conference version and this
journal version suggested many improvements.

References
 [1] J. Agat. Transforming out timing leaks. In POPL, pages 40–53, 2000.
 [2] J. Baeten and W. Weijland. Process Algebra. Cambridge University Press, 1990.
 [3] G. Barthe, P. R. D’Argenio, and T. Rezk. Secure information flow by self-
     composition. In IEEE Computer Security Foundations Workshop, pages 100–114,
     2004.
 [4] G. Barthe and L. P. Nieto. Formally verifying information flow type systems for
     concurrent and thread systems. In FMSE, pages 13–22, 2004.
 [5] G. Boudol. On typing information flow. In ICTAC, pages 366–380, 2005.
                                                     Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
28       ·       A. Popescu, J. Hölzl and T. Nipkow

 [6] G. Boudol and I. Castellani. Noninterference for concurrent programs. In ICALP,
     pages 382–395, 2001.
 [7] G. Boudol and I. Castellani. Noninterference for concurrent programs and thread
     systems. Theoretical Computer Science, 281(1-2):109–130, 2002.
 [8] D. Cock. Practical probability: Applying pgcl to lattice scheduling. To appear in ITP
     2013.
 [9] Á. Darvas, R. Hähnle, and D. Sands. A theorem proving approach to analysis of
     secure information flow. In SPC, pages 193–209, 2005.
[10] K. Engelhardt. A note on noninterference in the presence of colluding adversaries
     (preliminary report). ARSPA-WITS’10. http://www.cse.unsw.edu.au/~kaie/
     Publications/Papers/E2010ARSPAWITS.pdf.
[11] R. Focardi and R. Gorrieri. Classification of security properties (part i: Information
     flow). In FOSAD, pages 331–396, 2000.
[12] J. Y. Halpern and K. R. O’Neill. Secrecy in multiagent systems. ACM Trans. Inf.
     Syst. Secur., 12(1), 2008.
[13] C. B. Jones. Specification and design of (parallel) programs. In IFIP Congress’83,
     pages 321–332, 1983.
[14] G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe,
     K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. seL4:
     formal verification of an os kernel. In SOSP, pages 207–220, 2009.
[15] H. Mantel. On the composition of secure systems. In IEEE Symposium on Security
     and Privacy, pages 88–, 2002.
[16] H. Mantel and A. Sabelfeld. A generic approach to the security of multi-threaded
     programs. In CSFW, pages 126–, 2001.
[17] H. Mantel and A. Sabelfeld. A unifying approach to the security of distributed and
     multi-threaded programs. Journal of Computer Security, 11(4):615–676, 2003.
[18] H. Mantel, D. Sands, and H. Sudbrock. Assumptions and guarantees for composi-
     tional noninterference. In CSF’11, pages 218–232, Cernay-la-Ville, France, 2011.
[19] H. Mantel and H. Sudbrock. Flexible scheduler-independent security. In ESORICS,
     pages 116–133, 2010.
[20] H. Mantel, H. Sudbrock, and T. Kraußer. Combining different proof techniques for
     verifying information flow security. In LOPSTR, volume 4407 of LNCS, pages 94–
     110. 2007.
[21] J. McLean. A general theory of composition for trace sets closed under selective
     interleaving functions. pages 79–93, May 1994.
[22] R. Milner. Communication and concurrency. Prentice Hall, 1989.
[23] C. Morgan. The shadow knows: Refinement and security in sequential programs. Sci.
     Comput. Program., 74(8):629–653, 2009.
[24] C. Morgan. Compositional noninterference from first principles. Formal Asp. Com-
     put., 24(1):3–26, 2012.
[25] A. Nanevski, A. Banerjee, and D. Garg. Verification of information flow and access
     control policies with dependent types. In Symposium on Security and Privacy, pages
     165–179, 2011.

Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
            Formal Verification of Language-Based Concurrent Noninterference                  ·      29

[26] L. C. Paulson and J. C. Blanchette. Three years of experience with Sledgehammer,
     a practical link between automatic and interactive theorem provers. In IWIL, 2010.
[27] G. D. Plotkin. A structural approach to operational semantics. J. Log. Algebr. Pro-
     gram., 60-61:17–139, 2004.
[28] A. Popescu. Security type systems as recursive predicates. Technical report. Available
     at http://arxiv.org/abs/1308.3472.
[29] A. Popescu and J. Hölzl.        Possibilistic noninterference.     Archive of For-
     mal Proofs, 2012. http://afp.sourceforge.net/entries/Possibilistic_
     Noninterference.shtml.
[30] A. Popescu, J. Hölzl, and T. Nipkow. Noninterfering schedulers–when possibilistic
     noninterference implies probabilistic noninterference. To appear in CALCO 2013.
[31] A. Popescu, J. Hölzl, and T. Nipkow. Proving concurrent noninterference. In CPP,
     pages 109–125, 2012.
[32] A. Russo, J. Hughes, D. Naumann, and A. Sabelfeld. Closing internal timing channels
     by transformation. In ASIAN 2006, volume 4435 of LNCS, pages 120–135. 2007.
[33] A. Russo and A. Sabelfeld. Security for multithreaded programs under cooperative
     scheduling. In Perspectives of Systems Informatics, volume 4378 of LNCS, pages
     474–480. 2007.
[34] A. Sabelfeld. The impact of synchronisation on secure information flow in concurrent
     programs. In Perspectives of System Informatics, volume 2244 of LNCS, pages 225–
     239. 2001.
[35] A. Sabelfeld. Confidentiality for multithreaded programs via bisimulation. In Inter-
     national Conference on Perspectives of System Informatics, LNCS, pages 260–273,
     2003.
[36] A. Sabelfeld and A. C. Myers. Language-based information-flow security. IEEE
     Journal on Selected Areas in Communications, 21(1):5–19, 2003.
[37] A. Sabelfeld and D. Sands. A PER model of secure information flow in sequential
     programs. In European Symposium on Programming, volume 1576 of LNCS, pages
     40–58, 1999.
[38] A. Sabelfeld and D. Sands. Probabilistic noninterference for multi-threaded pro-
     grams. In IEEE Computer Security Foundations Workshop, pages 200–214, 2000.
[39] G. Smith. A new type system for secure information flow. In IEEE Computer Security
     Foundations Workshop, pages 115–125, 2001.
[40] G. Smith. Probabilistic noninterference through weak probabilistic bisimulation. In
     IEEE Computer Security Foundations Workshop, pages 3–13, 2003.
[41] G. Smith. Improved typings for probabilistic noninterference in a multi-threaded
     language. Journal of Computer Security, 14(6):591–623, 2006.
[42] G. Smith and D. Volpano. Secure information flow in a multi-threaded imperative
     language. In ACM Symposium on Principles of Programming Languages, pages 355–
     364, 1998.
[43] G. Snelting and D. Wasserrab. A correctness proof for the Volpano/Smith security
     typing system. Archive of Formal Proofs, 2008, 2008.



                                                     Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
30       ·       A. Popescu, J. Hölzl and T. Nipkow

[44] D. Traytel, A. Popescu, and J. C. Blanchette. Foundational, compositional
     (co)datatypes for higher-order logic—Category theory applied to theorem proving.
     In LICS 2012, pages 596–605. IEEE, 2012.
[45] R. van der Meyden and C. Zhang. A comparison of semantic models for noninterfer-
     ence. Theor. Comput. Sci., 411(47):4123–4147, 2010.
[46] D. Volpano, G. Smith, and C. Irvine. A sound type system for secure flow analysis.
     Journal of Computer Security, 4(2,3):167–187, 1996.
[47] S. Zdancewic and A. C. Myers. Observational determinism for concurrent program
     security. In IEEE Computer Security Foundations Workshop, pages 29–43, 2003.




Journal of Formalized Reasoning Vol. 6, No. 1, 2013.
