=Paper=
{{Paper
|id=None
|storemode=property
|title=Information Flow and Concurrent Imperative Languages
|pdfUrl=https://ceur-ws.org/Vol-928/0123.pdf
|volume=Vol-928
|dblpUrl=https://dblp.org/rec/conf/csp/Gruska12
}}
==Information Flow and Concurrent Imperative Languages==
https://ceur-ws.org/Vol-928/0123.pdf
Information Flow and Concurrent Imperative
Languages ?
Damas P. GRUSKA
Institute of Informatics, Comenius University,
Mlynska dolina, 842 48 Bratislava, Slovakia,
gruska@fmph.uniba.sk.
Abstract. Information flow for concurrent imperative languages is de-
fined and studied. As a working formalism we use UNITY, where pro-
grams consist of sets of assignments executed randomly, i.e. without con-
trol flow. We study noninterference for programs which reach and do not
reach fixed point - a state which is not changed by a subsequent exe-
cution. We present logic formulation of noninterference as well as type
system for it.
Keywords: information flow, noninterference, concurrent imperative lan-
guage, fixed point, safety and progress properties, type system
1 Introduction
Several formulations of a notion of a system security can be found in the litera-
ture. Many of them are based on a concept of noninterference (see [GM82]) which
assumes an absence of any information flow between private and public systems
activities. More precisely, systems are considered to be secure if from observations
of their public activities no information about private activities can be deduced.
This approach has found many reformulations for different formalisms (Process
algebras, Petri nets, simple imperative programming languages, see [SM03] for
an overview, multi-threaded programs, see, for example, [SS00,VS98], and so
on), for different computational models (labeled transition systems, determinis-
tic models and so on) and for the nature or “quality” of observations (see, for
example, [BKMR06,Gru07]).
Presence of information flow can be checked statically, i.e. on the program’s
code or system’s description, or dynamically, i.e. at runtime. In the first case
there are several methods, which include typing (see, for example [VSI96]), model
checking (see, for example, [HN,HB11]).
The aim of the paper is to define and to study information flow in the case
of concurrent imperative languages. Concurrency brings several new challenges
with respect to sequential or parallel computations. There is no given control
flow, there is no scheduler and program may not terminate. This brings new spe-
cific problems how to handle information flow. As a working formalism we take
?
Work supported by the grant VEGA 1/1333/12.
UNITY programs with corresponding specification logic (see [CM88]). These
programs consist of sets of assignments which are randomly chosen at runtime.
Every run of UNITY program is infinite but it can happen that during the run
a fixed point is reached, i.e. point when a subsequent computation does not
change values of program variables, which somehow corresponds to termination.
Moreover, another source of nondeterminism comes from randomly chosen val-
ues of variables if they are not specified at the beginning. On the other side, it
makes no sense to study covert channels caused by specific scheduler policy since
statements to be executed are chosen randomly (see [SS00,VS98]) and there is a
natural way how to compose programs and how to study their composition prop-
erties. We will study noninterference for two groups of programs - those which
always reach fixed point(s) (there might by more then one) and those which
do not. We exploit techniques developed for imperative languages as well as for
process algebras. Then we characterize some of these noninterference properties
by UNITY logic and by type system.
Organization of the paper. In Section 2 we present UNITY semantics, syntax
and logic. In Section 3 we present and investigate absence of information flow for
programs which reach fixed points (what somehow correspond to termination)
and in the next section we concentrate on non-terminating programs. Section 4
is devoted to logical characterizations of noninterference properties and Section
5 to the type system.
2 Unity
In this section we briefly recall a slightly simplified version of UNITY programs
and the underlying logic for describing program properties. For more details see
[CM88].
2.1 Syntax
UNITY programs consist of three parts: declare, initially and assign sections,
while the second one is optional. Note that originally UNITY programs could
contain also section always but this is optional and does not bring anything new
for our purposes. Hence formally:
Program program-name
declare declare-section
initially initially-section
assign assign-section
end
The assign section, which consists of set of statements - assignments, is the
crucial part of a program. The statements are separated by 2. Each statement
consists of list of variables on the left hand side and list of expressions (of the
same length) on the right hand side.
Expressions might by simple (examples: in x, y := 3, z + 2 on the right hand
side there are the simple expressions) or conditional (in x, y := 3 if y > 0 ∼
2 if y < 0, 4 on the right hand side there is a conditional expression, the assign-
ment assigns value 3 to x if y > 0, value 2 if y < 0 and leaves it unchanged if
y = 0 and assigns value 4 to y). Formally:
assign-section ::= s{2 s}∗
s ::= variable-list := expression-list
variable-list ::= variable{, variable}∗
expression-list ::= expression{, expression}∗
expression ::= simple-expression |conditional-expression
conditional-expression ::= simple-expression
if boolean-expression
∼ simple-expression
if boolean-expression
We assume that if more boolean expressions within one conditional expression
are valuated as true then corresponding simple expressions have to be equal, i.e.
every execution of every statement is deterministic.
Initially section assigns initial values to (some) variables. It is similar to
assign section (we use here = instead of :=) and we require that if a value of a
variable is initialized then it is done uniquely. Declare section declares types of
variables.
By P 2P 0 we denote composition of programs P and P 0 , respectively. The
sections of the resulting program are given by unions of corresponding sections
of P and P 0 . It is assumed that there are no conflicts between their declare and
initially sections, i.e. if a variable is declared in both programs, then it has to
have the same type and if a variable is initialized in both programs, then it has
to by initialized equally.
2.2 Operational semantics
The UNITY programs are executed in the following way: initial values of vari-
ables are given in initial section or they are randomly chosen within appropriate
type if they are not initialized. By Initially(V ar) we denote set of variables
which have initialized values by initially section. In general, ∅ ⊆ Initially(V ar) ⊆
V ar, where V ar is the set of all program variables. Then execution proceeds with
randomly chosen statement, its execution and again new statement is randomly
chosen and executed. This is repeated infinitely many times in such a way that
every statement is executed infinitely many times. Hence an underlying seman-
tics is given by the set of infinite sequences (runs) R, R = R0 , R1 , . . . where
Ri = (Ri .state, Ri .statement) i.e. each element of the run contains state - i.e.
values of all variables (defined by mapping υ : V ar → υ(dom)) and the state-
ment which is to be executed as the next. By R.state we will denote the sequence
of states of run R, i.e. R.state = R0 .state, R1 .state, . . .. We assume that every
statement of the program appears infinitely many times in every run. Note that
Ri+1 .state is uniquely determined by Ri = (Ri .state, Ri .statement) since exe-
cution of any statement is deterministic. R0 .state is an initial state. If initial
values of all variables are given in initial section, then every run starts with this
unique initial state. Otherwise there are many possible initial states depending
on variables which are not initialized. For example, if there is only one boolean
variable not initialized, then there are two possible initial states. By initial con-
dition (predicate Initially) we mean condition which is given by initial section.
Roughly speaking, it is a predicate obtained from initially section by replacing
:= by =, 2 by ∧ and conditional expression x = e1 if b1 ∼ . . . ∼ en if bn is re-
placed by (b0 ⇒ (x = e0 )) ∧ . . . ∧ (bn ⇒ (x = en )). For simplicity we assume that
the variables have integer values. Note that considering other types of variables
does not bring anything fundamentally new with respect to studied concepts
and properties. We use 0 for false and nonzero for true. Formally, a state (we
will alternatively use also denotation memory) is defined as mapping υ which
assigns integer value to every variable, i.e. Ri .state ≡ υ : V ar → Z. The formal
definition of υ is the following:
x ∈ dom(υ)
x:=e
υ −→ υ[x := υ(e)]
x ∈ dom(υ)
x:=e if b
υ −→ υ[x := υ(e)] if b
x ∈ dom(υ)
x:=e if b
υ −→ υ if ¬b
s s0
υ −→ υ 0 , υ 0 −→ υ 00
s.s0
υ −→ υ 00
We write υ −→ υ 0 if there exists a sequence of statements t = s1 . . . . sn such
t
that υ −→ υ 0 .
2.3 Logic
Let p, q are predicates and s statement. The assertion {p}s{q} denotes that
execution of s in any state that satisfies predicate p results in a state that
satisfies predicate q.
Let us consider program P which contains at least one statement. We write
s ∈ P if assign section of P contains s. We will use standard logical opera-
tors as ∨, ∧, ¬, ⇒, . . . and moreover, we define UNITY logic operators for safety
properties unless, stable, invariant, constant and for progress properties ensures,
leads-to. We start with basic safety property unless which is defined as follows.
p unless q ≡ ∀s, s ∈ P :: {p ∧ ¬q}s{p ∨ q}
Derived operators are defined as follows: p is stable iff p unless f alse, p is
constant iff both p and ¬p are stable. Predicate p is invariant iff it is stable and
Initially ⇒ p.
Now we can define two progress properties ensures, leads-to (denoted as 7→).
p ensures q ≡ ∃s, s ∈ P :: {p ∧ ¬q}s{q} and p unless q
Leads-to is defined by a finite number of application of the following inference
rules. The first inference rule says that ensures is a special case of leads to.
p ensures q
p 7→ q
The second inference rule defines transitivity of 7→.
p 7→ q, q 7→ r
p 7→ r
The third inference rule defines weakening (W is a set of indexes).
∀m ∈ W :: pm 7→ q
(∃m ∈ W :: pm ) 7→ q
By fixed point we mean a state for which it holds that for each statement
of the program valuations of variables on the left hand side and right hand side
are equal, i.e. any subsequent execution of the program does not change state of
the program. Formally,
F P ≡ ∀s ∈ P, if s is ”X := E” then X = E
where X and E is variable and expression lists, respectively. In case of conditional
expressions, if neither of conditions is evaluated to true, then the statement does
not change the value of variable on the left hand side and we consider this as
that the both sides are equal. By true 7→ F P we will denote that fixed point
will be reached.
By υp we denote that predicate p holds for valuation υ. In special case valua-
tion υinitially has to satisfy initial condition, i.e. if variable x initializes its value
to m than υInitially (x) = m.
3 Non-interference for programs with fixed points
Suppose that the set of variables V ar is divided into two subsets, namely the
set of public (low level) variables V arL and private (high level) ones V arH . This
division does not vary at runtime. We denote low level variables as l, l0 , l1 , . . .,
high level ones as h, h0 , h1 , . . . and constants as c, c0 , c1 , . . ..
First we define termination-insensitive security (see for example [VS97]) for
imperative programs based on an absence of information flow between private a
and public variables.
Definition 1. (BTNI) A deterministic program C satisfies batch-job
termination-insensitive noninterference (BTNI) if, for any memory (valuation)
υ1 and υ2 that agree on public (low) variables, the final memories υ10 and υ20
produced by running P also agree on public variables if both runs terminate suc-
cessfully.
Roughly speaking, BTNI property requires that programs represent functions
for which low level outputs do not depend on high level inputs.
Examples of programs which clearly violate BTNI condition are l := h (the
explicit information flow) and l := 1 if h = 0 (the implicit information flow).
We cannot apply BTNI property for UNITY programs from the several rea-
sons. They are undeterministic, there might have several initial states of compu-
tations and they do not terminate. So we have to elaborate new noninterference
definition for UNITY programs.
First we need some preparatory work. Let υ1 and υ2 be valuations. We write
υ0 =M υ1 iff υ0 (x) =M υ1 (x) for every variable x, x ∈ M . We will write υ0 =L υ1
instead of υ0 =V arL υ1 i.e. if valuations υ0 , υ1 agree on low level variables. From
now on we assume that high level variables are not initialized if it is not said
otherwise.
Definition 2. Program P is called fixed point deterministic with respect to M ,
M ⊆ V ar (P ∈ F P D(M ), for short) iff it always reaches fixed point and more-
over this is unique for variables from M , i.e. values of variables from M are
equal at any fixed point.
Example 1. Let us consider assignment l := l + 1 if l < l0 . For program P con-
sisting of (only) this assignment and if both values l, l0 are initialized then it is
F P D(L). If any of them, or both, are not initialized, then it is not F P D(L)
despite the fact that it always reaches fixed point but for different runs it can
reach different fixed points. On the other side, initialization of all variables is
not necessary condition to be fixed point deterministic even with respect to set
which does not contain non-initialized variables.
Definition 3. Program P satisfies fixed point deterministic noninterference
(FPDNI, for short) iff it is FPD(L).
For programs such that Initially(V ar) = L property FPDNI corresponds to
BT N I property (see Definition 1). If some low level variables are not initialized,
then it is stronger. Sometimes it might be too strong since it requires that
program reaches the same (from low level point of view) fixed point even for
low level variables which initial values are chosen randomly. We could weaken
FPDNI property by requiring that program is deterministic only with respect
to initialized low level variables.
Definition 4. Program P satisfies weak fixed point deterministic noninterfer-
ence (WFPDNI, for short) iff it is F P D(Initially(V ar) ∩ L).
Lemma 1. Let P satisfy fixed point noninterference then it satisfies also weak
fixed point noninterference
Proof. Clearly, if P satisfies fixed point noninterference then it is fixed point
deterministic for all low level variables and hence also for any subset of low level
variables. Note that an inverse of the lemma does not hold (see Example 1).
Requiring deterministicity is a strong requirement for concurrent programs.
They often lead to different states (results) depending on factors which cannot
be predicted (say, random factors). To capture noninterference for such cases
requires a different approach. An intruder cannot learn nothing about initial
value of high level variable h, if for any computation starting with some value
of h there exists a computation starting with different value of h which leads to
the same fixed point as regards low level variables. This leads us to the following
definition.
Definition 5. Program P satisfies fixed point noninterference with respect to
M, M ⊆ H(P ∈ F P N I(M ), for short) iff it always reaches fixed point and for
every valuation υ0 for which it holds Initially ⇒ υ0 there exists υ00 for which it
holds Initially ⇒ υ00 such that υ(x) 6= υ 0 (x) for every x ∈ M and υ0 → υF P ,
υ00 → υF0 P and moreover υF P =L υF0 P .
If program has F P N I(M ) then, then an intruder cannot learn (exact) value
of any of its high level variables from M . For F P N I(M ) property we have the
following lemma, which say that noninterference for a set of high level variables
can be obtained separately from its subsets.
Lemma 2. F P N I(M1 ) ∩ F P N I(M2 ) = F P N I(M1 ∪ M2 ).
Proof. By case analysis of all possible runs.
Lemma 3. Let M1 ⊆ M2 then F P N I(M2 ) ⊆ F P N I(M1 ).
Proof. Directly from definition of F P N I(M ) property.
We conclude this section by comparing above proposed noninterference prop-
erties by the following proposition.
Proposition 1. F P DN I ⊂ W F P DN I ⊂ F P N I(M ) for every M, M ⊆ H.
Proof. Main idea. One part of the proposition comes from Lemma 1. The other
part comes from the fact that we can always find different values of high level
variables (thanks to their domain and not being initialized as it is assumed at
the beginning of this section) for initial states and deterministic programs leads
to unique fixed point form low level point of view. The following example shows
that also this inclusion is proper.
Example 2. Let us consider program P .
Program P
initially l :=c
assign l := l + 1 if l < l0 ∼ h if l ≥ l0
end
The program always reaches the fixed point. Then it holds l = h if c ≥ l0 and
l = l0 otherwise. Since we do not know an initial value of l0 we do not know
neither value of h. Hence P ∈ F P N I({h}) but P 6∈ W F P DN I since the final
value of l is not uniquely determined.
4 Non-interference for programs without fixed points
In this section we will deal with programs which do not reach any fixed point(s)
and to which the previous definitions of noninterference cannot be applied.
Definition 6. Let P be program and let R be a run of P such that R.state =
υ0 , υ1 , . . . . We say that P satisfies non-fixed point noninterference (P ∈ N F P N I,
for short) if for every υ00 such that υ0 =L υ00 there exists run R0 such that
R0 .state = υ00 , υ10 , . . . such that υi =L υi0 for every i.
N F P N I corresponds to an observer who can see values of public variables
at every state but cannot deduce from them values of private variables.
Proposition 2. Let P ∈ N F P N I, Initially(V ar) = L, and true 7→ F P is a
property of P . Then P ∈ F P N I(M ) for every M, M ⊆ H.
Proof. Main idea. Let P ∈ N F P N I and true 7→ F P is a property of P . Since
all low level variables are initialized and we can emulate on low level every two
runs then we get that P ∈ F P N I(M ) for every M, M ⊆ H.
Now we can formulate a compositional property for two UNITY programs
which are N F P N I.
Proposition 3. Let P, P 0 ∈ N F P N I. Then it holds that P 2P 0 ∈ N F P N I
Proof. Sketch. Program P 2P 0 is obtained by set unions (with same preliminary
requirements on conflicts - see Section 1 and under our assumption that vari-
ables from V arH are not initialized). Hence if we have a run of P 2P 0 then it
corresponds to interleaving of executions of assignments of P and P 0 .
Special case of unity programs are those which are low level deterministic,
i.e. there is no choice between statements which change low level variables. For
such programs it is meaningful to define stronger variant of NFPNI property
which requires that all runs agree on low level variables. Formally:
Definition 7. Let P be program and let R be a run of P such that R.state =
υ0 , υ1 , . . . . We say that P satisfies strong non-fixed point noninterference (P ∈
SN F P N I, for short) if for every υ00 such that υ0 =L υ00 then for every run R0
such that R0 .state = υ00 , υ10 , . . . it holds υi =L υi0 for every i.
Lemma 4. SN F P N I ⊆ N F P N I. Moreover, if P is low level deterministic
then P ∈ SN F P N I iff P ∈ N F P N I.
Proof. Sketch. The first part of the proof is straightforward. If P is low level
deterministic, since there is no choice between runs from low level point of view
and there exists at least one which is identical (from low level of view) to given
run, we have that P ∈ SN F P N I iff P ∈ N F P N I.
5 Logic characterization of noninterference
In this section we will define characterization of some noninterference properties
by UNITY logic. Let P be a program, l1 , . . . , ln are its (all) low level variables
and υ is its valuation. By υK , where K = (k1 , . . . , kn ), we denote predicate
υ(K) ≡ (υ(l1 ) = k1 ) ∧ . . . ∧ (υ(ln ) = kn ).
Proposition 4. Let P be a program and υ, υ 0 its two valuations. Then P has
FPDNI property iff (true 7→ F P ) ∧ ((υF P ∧ υF0 P ∧ υ(K) ∧ υ(K 0 )) ⇒ (K = K 0 )).
Proof. Sketch. Let P be a program with FPDNI property. The property requires
that it reaches fixed point (true 7→ F P ) and that valuations on any fixed points
are equal with respect to low level variables. This property is expressed by (υF P ∧
υF0 P ∧ υ(K) ∧ υ(K 0 )) ⇒ (K = K 0 ).
Proposition 5. Let P be a program. Then P has NFPNI property iff ((υ1 =L
υ2 ) ∧ (υ1 7→ υ10 )) ⇒ (υ2 7→ υ20 ) ∧ (υ10 =L υ20 ) for some υ20 .
Proof. Main idea. N F P N I property requires that for every run and every its
state there exists a run with the same initial state (up to values of high level
variables) which reaches the same states (up to values of high level variables).
Proposition 6. Let P be low level deterministic. Then P ∈ SN F P N I iff υ =L
υ 0 is stable for every pair of valuations υ, υ 0 of P .
Proof. Main idea. Since P is low level deterministic every two runs are equal for
low level variables, i.e. every two valuations which once become equal for low
level variables remain so, i.e. equality is stable.
6 Type system
Before we define type system which can capture NFPNI property, we need some
preparatory work. We begin with program equivalency. Note that due to mech-
anism of choosing statements for execution, we do not need to work with bisim-
ulation or other branching sensitive relations - at any point of any computation
every statements could be executed as the next one.
Definition 8. We say that programs P and P 0 are equivalent (denoted P ' P 0 ),
if for every run R of P there exists a run R0 of P 0 such that Ri .state = Ri0 .state
for every i and vice versa.
Two equivalent programs exhibit exactly the same behaviour and are indis-
tinguishable from semantical point of view.
The next lemma allow us to simplify program syntax while increasing number
of statements.
Lemma 5. For every program P there exists equivalent program P 0 such that it
contains only one conditional expression on the right side of every assignment.
Proof. Sketch. We replace (split) every assignment with more conditional ex-
pressions with a set of assignments with only one (of) conditional expression. It
is easy to prove that resulting program is equivalent to the original one.
Lemma 6. Let P ' P 0 and P ∈ N F P N I then also P 0 ∈ N F P N I.
Proof. Sketch. Two equivalent programs exhibit the same semantical behaviour
and hence satisfy the same semantically defined properties.
Lemma 7. Let P ∈ N F P N I iff P 0 ∈ N F P N I where P 0 is obtained from P
by replacing every statement of P of the form x1 , . . . , xn := e1 , . . . , en by the
statement x1 := e1 2 . . . 2xn := en (we will call P 0 sequentialization of P ).
Proof. Sketch. The difference between P and P 0 is that the first one can do
parallel assignments while the second one cannot, but it can still emulate any
parallel assignments by a sequence of sequential ones.
Let us consider the following type system for UNITY programs. Here c stands
for a constant (it is a special case of expression e), op for an operational symbol
which is allowed in expressions. We use two types High and Low.
` h : High ` l : Low
` e1 : T, ` e1 : T
` c : Low ` e1 op e2 : T
` e : Low
` e : High [High] ` h := e
` e : Low ` e : Low, ` b : Low
[Low] ` l := e [Low] ` l := e if b
` e : T, ` b : T [High] ` s
[High] ` h := e if b [Low] ` s
[Low] ` s for every s ∈ P
[Low] ` P
Type system for UNITY programs.
Proposition 7. (Soudness) Let P be a UNITY program. If typing judgment
[Low] ` P 0 can be derived where P 0 is sequentialization of P then P ∈ N F P N I.
Proof. Main idea. Thanks to Lemmas 5,6 and 7 we can assume that P does
not contain more conditional expressions on the right hand side and only one
variable on left hand side. If typing judgment [Low] ` P 0 can derived then there
are no assignments to low level variable which right hand side depend on high
level variable. Hence if we have a run υo , υ1 , . . . then regardless on values of
high level variables there exists run υo0 , υ10 , . . . such that they agree on low level
variables.
Example 3. Let us consider program P and P 0 which consists of one statement
h := 1if l = 1 and l := 1if h = 1, respectively. Then we have [Low] ` P but
[Low] ` P 0 cannot be derived.
We cannot obtain complete type system since we would need to differ between
high type expressions which are constant and which really depend on high level
variables. For example, l := h − h and l := c if l = h ∼ c if l 6= h is not low level
assignments while ”semantically” it is since a value of l does not depend on a
value of h.
Note that the similar type systems can be applied also for other above defined
properties as SFPNI and FPDNI. Moreover if program contains, for example,
statements of type h := c for every high level variable then initial values of those
variables cannot be deduced from any fixed point. In this way we could extend
the presented type system by introducing new type Const to cover this case.
7 Conclusions and further work
In this paper we have defined and studied information flow for concurrent im-
perative languages. We had to deal with four challenges - an absence of control
flow, possibly more initial states, an absence of a scheduler which schedules
which statement is to be executed as the next and with possibly nonterminating
behaviour. Each of thess properties causes that, in general, programs cannot be
treated as functions (they are not deterministic and do not output ”final val-
ues”). Our working formalism - UNITY programs and UNITY logic are very
simple but still can capture various noninterference properties. On the other
hand we can exclude covert channels produced by specific scheduler policies.
Concurrent imperative languages are something between simple imperative
languages and models of concurrency as labeled transition systems or process
algebras, as regards treatment of noninterference. If they are ”deterministic”
and they ”terminate” (in a sense) then they could be handled as former ones
but if they are undeterministic and/or do not terminate as later ones. Hence
we have exploited ”noninterference” techniques developed for both imperative
languages as well as for process algebras. We have also characterized some of
these noninterference properties by UNITY logic and by type system.
Regarding the further work, we consider to exploit an idea studied in process
algebra setting, namely property called Non-Deducibility on Composition (NDC
for short, see in [FGM03]). Program P would have property NDC if for every
program A which changes only high level variables, i.e. υK i stable for every K,
then P 2A ' P .
In [BBM94] for nondeterministic languages authors associate with a program
variable x a set of called security variable of x, denoted x̄. It is the set of all
variables whose values can influence the value of x (directly or undirectly). This
approach could be used also for UNITY programs.
Another possible direction of a further research might be quantification of
information obtained from low level variables. For example, program l := 1
if (h mod 2) = 1 ∼ 0 if (h mod 2) 6= 1 cannot leak exact value of h but it leaks
via l parity of h. By similar techniques as it was done in [CHM07] we could try
to quantify an amount of information on high level variables obtained from low
level ones via information theory.
References
[BBM94] Banatre C., C. Bryce and D. Le Metayer: Compile-time Deytection of Infor-
matioin Flow in Sequential Programs. European Symposium on Research
in Computer Security, LNCS 875, Springer, Berlin, 1994.
[BKMR06] Bryans J., M. Koutny, L. Mazare and P. Ryan: Opacity Generalised to
Transition Systems. In Proceedings of the Formal Aspects in Security and
Trust, LNCS 3866, Springer, Berlin, 2006.
[CHM07] Clark D., S. Hunt and P. Malacaria: A Static Analysis for Quantifying
the Information Flow in a Simple Imperative Programming Language. The
Journal of Computer Security, 15(3). 2007.
[CM88] Chandy, K. M. and J. Misra: Parallel Program Design. Addison-Wesley
1988.
[FGM03] Focardi, R., R. Gorrieri, and F. Martinelli: Real-Time information flow
analysis. IEEE Journal on Selected Areas in Communications 21 (2003).
[HN] Huisman M. and T.M. Ngo: Scheduler-specific Confidentiality for Multi-
threaded Programs and Its logic-based Verification. In proceedings of
Formal Verification of Object-Oriented Systems (FoVeOos 2011). LNCS,
Springer. To appear.
[HB11] Huisman, M. and H.-C. Blondeel: Model-checking Secure Information Flow
for Multi-Threaded Programs. In Proceedings of Theory of Security and
Applications (Tosca) LNCS 6993, pages 148 - 165 , Springer, 2011.
[GM82] Goguen J.A. and J. Meseguer: Security Policies and Security Models. Proc.
of IEEE Symposium on Security and Privacy, 1982.
[Gru09] Gruska D.P.: Quantifying Security for Timed Process Algebras, Funda-
menta Informaticae, vol. 93, Numbers 1-3, 2009.
[Gru08] Gruska D.P.: Probabilistic Information Flow Security. Fundamenta Infor-
maticae, vol. 85, Numbers 1-4, 2008.
[Gru07] Gruska D.P.: Observation Based System Security. Fundamenta Informati-
cae, vol. 79, Numbers 3-4, 2007.
[SM03] Sabelfeld, A and A.C. Myers: Language-Based Information-Flow Security,
IEEE Journal on Selected Areas in Communications, 21(1):5-19, January
2003.
[SS00] Sabelfeld, A and D. Sands: Probabilistic Noninterference for Multi-
Threaded Programs, Proceedings of the 13th IEEE workshop on Computer
Security Foundations, 2000.
[Sch00] Schneider, F. B.: Enforceable Security Policies. ACM Transactions on In-
formation and System Security, Volume 3 Issue 1, Feb. 2000.
[VS98] Volpano D. and G. Smith: Secure Information Flow in a Multi-threaded
Imperative Language, Proc. 25th ACM Symposium on Principles of Pro-
gramming Languages, pp. 355-364, San Diego, CA, Jan 1998.
[VS97] Volpano D. M. and G. Smith: Eliminating Covert Flows with Minimum
Typings. In Proc. CSFW, 1997.
[VSI96] Volpano D., G. Smith and C. Irvine: A Sound Type System for Secure Flow
Analysis, Journal of Computer Security, Vol. 4, No. 3, pp. 167-187, 1996.