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.