Information flow for concurrent imperative languages is defined and studied. As a working formalism we use UNITY, where programs consist of sets of assignments executed randomly, i.e. without control flow. We study noninterference for programs which reach and do not reach fixed point - a state which is not changed by a subsequent execution. We present logic formulation of noninterference as well as type system for it.
Several formulations of a notion of a system security can be found in the literature. Many of them are based on a concept of noninterference (see [GM82]) which assumes an absence of any information oflw 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, deterministic 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 rfist 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 specific 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 specicfiation 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 xfied 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 values of variables if they are not specified at the beginning. On the other side, it makes no sense to study covert channels caused by specicfi 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 properties. We will study noninterference for two groups of programs - those which always reach xfied 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 xfied 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
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
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 assignment 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 coniflcts 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
The UNITY programs are executed in the following way: initial values of variables 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 innfiitely many times. Hence an underlying semantics is given by the set of innfiite 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 (denfied by mapping υ : V ar → υ (dom)) and the statement 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 execution 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 condition (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 replaced 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 denfiition 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 υ 0, υ 0 →−s0 υ 00
υ →−s.s0 υ 00
that υ →−t υ 0. 2.3
υ 0 if there exists a sequence of statements t = s1. . . . sn such Let p, q are predicates and s statement. The assertion { } { } denotes that p s q execution of s in any state that satisefis 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 operators 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 denfied 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.
The third inference rule denfies weakening ( W is a set of indexes). p ensures q
p 7→ q p 7→ q, q 7→ r
p 7→ r ∀m ∈ W :: pm 7→ q (∃m ∈ W :: pm) 7→ q
By xfied 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 valuation υ initially has to satisfy initial condition, i.e. if variable x initializes its value to m than υ Initially(x) = m. 3
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 denfie termination-insensitive security (see for example [VS97]) for imperative programs based on an absence of information oflw 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 successfully.
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 oflw) and l := 1 if h = 0 (the implicit information oflw).
We cannot apply BTNI property for UNITY programs from the several reasons. They are undeterministic, there might have several initial states of computations and they do not terminate. So we have to elaborate new noninterference denfiition 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 moreover 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 consisting 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 xfied 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 Denfiition 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 noninterference (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 xfied point noninterference then it is xfied 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 denfiition.
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 denfiition of F P N I(M ) property.
We conclude this section by comparing above proposed noninterference properties 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 xfied 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.
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 variables 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 denfie 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.
In this section we will denfie 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) ∧ υ (K0)) ⇒ (K = K0)). 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) ∧ υ (K0)) ⇒ (K = K0).
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 υ, υ 0of 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
Before we define type system which can capture NFPNI property, we need some preparatory work. We begin with program equivalency. Note that due to mechanism of choosing statements for execution, we do not need to work with bisimulation 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 indistinguishable 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 expressions 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 := e12 . . . 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 ` c : Low ` e : Low ` e : High ` e : Low [Low] ` l := e ` e : T, ` b : T [High] ` h := e if b [Low] ` s for every s ∈ P [Low] ` P
` l : Low ` e1 : T, ` e1 : T ` e1 op e2 : T [High] ` h := e ` e : Low, ` b : Low [Low] ` l := e if b [High] ` s [Low] ` s
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
In this paper we have denfied and studied information flow for concurrent imperative 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 ”nfial values”). 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 specicfi 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 inuflence 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.