Low-deterministic security for low-nondeterministic programs 1

Abstract

We present a new algorithm, together with a full soundness proof, which guarantees probabilistic noninterference (PN) for concurrent programs. The algorithm follows the “low-deterministic security” (LSOD) approach, but for the first time allows general low-nondeterminism as long as PN is not violated.

The algorithm is based on the earlier observation by Giffhorn and Snelting that low-nondeterminism is secure as long as it is not influenced by high events [International Journal of Information Security 14 (2015) 263–287]. It uses a new system of classification flow equations in multi-threaded programs, together with inter-thread/interprocedural dominators. Compared to LSOD, precision is boosted and false alarms are minimized. We explain details of the new algorithm and its soundness proof.

The algorithm is integrated into the JOANA software security tool, and can handle full Java with arbitrary threads. We apply JOANA to a multi-threaded e-voting system, and show how the algorithm eliminates false alarms. We thus demonstrate that low-deterministic security is a highly precise and practically mature software security analysis method.

Keywords

Software security information flow control probabilistic noninterference program analysis

1. Introduction

Information flow control (IFC) analyses a program’s source or byte code for security leaks, namely violations of confidentiality and integrity. IFC algorithms usually check some form of noninterference [33]. Sound IFC algorithms guarantee to find all leaks, while precise algorithms generate no false alarms. Unfortunately, perfect precision and soundness cannot be achieved together: the famous Rice theorem states that such perfect program analysis is undecideable. Thus many algorithms and definitional variations for noninterference have been proposed, which vary in precision, scalability, language restrictions, necessary annotations, and other factors.

Concurrent or multi-threaded programs introduce new threats to security, as nondeterminism and interleaving can create subtle leaks which are much more difficult to find or prevent than in sequential programs. For multi-threaded programs, probabilistic noninterference (PN) as introduced in [34–36] is the established security criterion. One of the oldest and simplest criteria which enforces PN is low-security observational determinism (LSOD), as introduced by Roscoe [32], and improved by Zdancewic, Huisman, and others [17,41]. For LSOD, a relatively simple static check can be devised; furthermore LSOD is scheduler independent – which is a big advantage. However Huisman and other researchers found subtle soundness problems in earlier LSOD algorithms (which were mostly related to nonterminating programs), so Huisman concluded that scheduler-independent PN is not feasible [16]. Worse, LSOD strictly prohibits any, even secure low-nondeterminism – which makes LSOD unsuitable for practical purposes.

It is the aim of this article to demonstrate that improvements to LSOD can be devised, which invalidate these earlier objections. An important step was already provided by Giffhorn [7,8] who discovered that

an improved definition of low-equivalent traces can solve earlier soundness problems for infinite traces and nonterminating programs;

flow- and context-sensitive program analysis is the key to a precise and sound LSOD algorithm;

the latter can naturally be implemented through the use of program dependence graphs;

additional support by may-happen-in-parallel analysis, precise points-to analysis and exception analysis makes LSOD work and scale for full Java;

secure low-nondeterminism can be allowed by relaxing the strict LSOD criterion, while maintaining soundness.

Giffhorn’s algorithm was the first to allow low-nondeterminism, while basically maintaning the LSOD approach. The algorithm was described in detail in [8,14]; it is integrated into the JOANA IFC tool.2

²
see joana.ipd.kit.edu. JOANA can analyse full Java with arbitrary threads, and was applied in various projects [10,19,21,26]. Usage of JOANA is described in [11].

But Giffhorn’s discovery was just a first step. In this paper, we describe new improvements for LSOD, which boost precision and reduce false alarms compared to original LSOD and even Giffhorn’s algorithm. We first recapitulate technical properties of PN and LSOD. We then explain the new relaxed LSOD (RLSOD)3

Giffhorn’s original criterion was called RLSOD in [4,8,38], and the new criterion was called iRLSOD in [4]. In this article, the iRLSOD criterion and its improvements are called RLSOD, while Giffhorn’s original criterion is called “Giffhorn’s algorithm”.

criterion in detail. It is based on the notion of dominance in threaded control flow graphs, and on fixpoint iteration in program dependence graphs.

The main contribution of this article, as compared to the preceding conference version [4], is a full soundness proof, which in turn led to an even more general formulation of the RLSOD criterion. RLSOD was recently integrated into JOANA. We present a case study, namely a prototypical e-voting system with multiple threads, as well as performance and scalability measurements.4

⁴

Links to all benchmark programs can be found at https://pp.ipd.kit.edu/projects/joana/rlsod-jcs.php .

Our work builds heavily on our earlier contributions [8,14], but the current article is aimed to be self-contained. We begin with an overview of the RLSOD framework and its attacker model.

2. The RLSOD framework and its assumptions

2.1. Language assumptions

The RLSOD approach is based on Program Dependence Graphs (PDGs, see Section 4.1 for details) and thus can be used with any imperative or object-oriented language for which a PDG can be constructed. PDGs are naturally flow- and context-sensitive, thus improving precision (see below). PDG construction must be sound and will then fulfill the assumptions of the slicing theorem (Section 4.1); sound PDGs have been constructed for C, full Java (see [14]), and many other languages. Thus there are no restrictions on language or control flow. In the current paper, we assume a simple imperative language with procedures and threads; a formal PDG construction for this language, together with a machine-checked soundness proof was provided in [40]. We would however like to point out some additional assumptions for multi-threaded programs.

We assume that statements resp. byte codes are deterministic, and that nondeterminism can only arise from scheduling choices. In particular, for a given statement, results and chosen branch (for conditionals) only depend on values read by the statement. The program can read input via input statements and produce output via output statements. At the beginning of execution, the $START$ statement is the only statement that can be scheduled.5

⁵
JOANA can also handle the Android Life cycle, see [26].

After executing a statement, its dynamic control flow successors can be scheduled (i.e. for conditionals, the first statement from the chosen branch; for forks the intra-thread successor and the first statement of the forked thread).

We therefore assume – like most other authors, e.g. [25,35] – interleaving semantics. Under the Java Memory Model, the compiler may, e.g. through reordering, in rare cases produce code which is not consistent with interleaving semantics. Allowing such behavior limits static analysis considerably, so most authors ignore this possibility.

We also assume that the program always terminates. Possibly nonterminating programs, e.g. truly interactive programs, lead to the problem of termination leaks [2]. Subtleties regarding nontermination are discussed in Section 4.2. Since we assume terminating programs, we can ignore those problems.

2.2. Scheduler assumptions

RLSOD requires that the scheduler is truly probabilistic. This means that for two statements $c_{1}$ and $c_{2}$ that can be scheduled, the relative probability to be scheduled next is independent of other possibly running threads, current program state, or the execution up to this point. It might however depend on the statements $c_{1}$ and $c_{2}$ themselves.6

⁶
Note that this is less restrictive than a uniform scheduler, where that relative probability is always 1. A truly probabilistic scheduler on the other hand can assign priorities to statements, e.g. increase the priorities for all statements of a specific (syntactic) thread.

The necessity of this assumption was stressed by various authors, e.g. [29,35]. To illustrate it, we assume a standard low/high classification for program variables (see Section 3 for details). A malicious scheduler can then easily read high values to construct an explicit flow by scheduling, as in

\begin{matrix} {H=0;||H=1;} {L=0;||L=1;} : \end{matrix}

the scheduler can leak H by scheduling the L assignments after reading H, such that the first visible L assignment represents H.

Even if the scheduler is not malicious, but follows a deterministic strategy which is known to the attacker, leaks can result. As an example, consider Fig. 1. Assume deterministic round-robin scheduling which executes 3 basic statements per time slice. Then for H=1 statements $2, 3, 4, 9, 5$ are executed, while for H=0, statements $2, 4, 5, 9$ are executed. Thus the attacker can observe the public event sequence 9→5 resp. 5→9, leaking H. However under the assumption of truly probabilistic scheduling, Fig. 1 is probabilistic noninterferent.

Fig. 1.

Deterministic round-robin scheduling may leak.

Thus allowing round robin schedulers severely restricts secure programs. This phenomenon has been observed by earlier authors (see Section 9 for details). RLSOD accepts the example in Fig. 1 as secure and therefore is not sound when used with round-robin. Probabilistic scheduling is the price to pay for RLSOD’s much better precision and freedom from program restrictions. We believe that in practice, scheduler restrictions are more acceptable than program restrictions or false alarms.

2.3. Attacker model

The traditional sequential attacker model assumes that the attacker can see the low part of both the initial state and the final state. Additionally, a static classification of all program variables is assumed. This means the attacker can see one part of the memory, but cannot see the other. For programming languages like C or Java, which include local variables and thus use an activation record stack, this implies that the memory addresses the attacker can observe change during execution. We therefore believe that this attacker model is unrealistic. Thus we assume that the attacker cannot see any internal memory of the program, and instead can only see low external input or low output events. The engineer has to provide information about the set of input and output statements and their classification. We further assume that the attacker might see multiple runs with the same input. For multi-threaded (nondeterministic) programs, where the probability of attacker-observable behaviors depends on the secret, the attacker might infer something about the secret by counting the different low-observable behaviors. This motivates the use of probabilistic noninterference.

2.4. The role of flow- and context-sensitivity

PDGs have been chosen as the basis for JOANA and RLSOD because PDGs are automatically flow- and context-sensitive. That is, they respect statement order, and respect call sites of procedures. In contrast, most security type systems are flow-insensitive, and even the flow-sensitive type system in [18] is not context-sensitive. Thus statement order is ignored, and all call sites of a procedure are merged; this heavily reduces precision and increases false alarms (see [13,14] for a more detailed discussion; Section 9 presents additional examples). In the current paper, all definitions and proofs assume flow-sensitivity; this explains why some definitions differ from their “classical” version.

But note that there is a price to pay for flow- and context-sensitivity: RLSOD is not compositional. That is, RLSOD always needs the complete source or byte code. In practice however, stubs for missing functions can be used, which “simulates” compositionality (see case study in Section 7). Compositionality is discussed in more detail in Section 9.

3. Noninterference and LSOD

IFC guarantees that no violations of confidentiality or integrity may occur. For confidentiality, program variables are classified as “high” (H, secret) or “low” (L, public), and it is assumed that an attacker can see low values, but cannot see any high value.7

⁷
A more detailed discussion of IFC attacker models can be found in e.g. [8]. Note that JOANA allows arbitrary lattices of security classifications, not just the simple $⊥ = L ⩽ H = ⊤$ lattice. Note also that integrity is dual to confidentiality, but will not be discussed here. JOANA can handle both.

Figure 2 presents small but typical confidentiality leaks. As usual, variable H is “High” (secret), L is “Low” (public). Explicit leaks arise if (parts of) high values are copied (indirectly) to low output. Implicit leaks arise if a high value can change control flow, which can change low behaviour (see Fig. 2 left). Possibilistic leaks in concurrent programs arise if a certain interleaving produces an explicit or implicit leak; in Fig. 2 middle, interleaving order 5, 8, 9, 6 causes an explicit leak. Probabilistic leaks arise if the probability of low output is influenced by high values; in Fig. 2 right, H is never copied to L, but if the value of H is large, probability is higher that “JCS” is printed instead of “CSJ”. Thus when the program is run multiple times, by observing the distribution of results, the attacker can obtain information about the secret, namely estimations of the value of H.

Fig. 2.

Some leaks. Left: explicit and implicit, middle: possibilistic, right: probabilistic. For simplicity, we assume that read(L) reads low variable L from a low input channel; print(H) prints high variable H to a high output channel. Note that reads of high variables are classified high, and prints of low variables are classified low.

3.1. Sequential noninterference

Before we formalize RLSOD, let us repeat the classical definition of sequential noninterference. The classic definition assumes that a global and static classification $cl (v)$ of all program variables v as secret (H) or public (L) is given. It therefore assumes that the whole memory is divided into a part the attacker can observe and a part hidden from the attacker. Note that flow-sensitive IFC such as RLSOD does not use a static, global classification of variables; this will be explained in Section 4.1 (Definition 9).

Definition 1 (Sequential noninterference).

Let $P$ be a program. Let $s, s^{'}$ be initial program states, let $[[P]] (s)$ , $[[P]] (s^{'})$ be the final states after executing $P$ in state s resp. $s^{'}$ . Noninterference holds iff $\begin{matrix} s \sim_{L} s^{'} ⟹ [[P]] (s) \sim_{L} [[P]] (s^{'}) . \end{matrix}$

The relation $s \sim_{L} s^{'}$ means that two states are low-equivalent, that is, coincide on low variables: $\forall v : cl (v) = L ⟹ s (v) = s^{'} (v)$ . Classically, program input is assumed to be part of the initial states $s, s^{'}$ , and program output is assumed to be part of the final states; the definition can be generalized to work with explicit input and output streams.

3.2. Probabilistic noninterference

In multi-threaded programs, fine-grained interleaving effects must be accounted for, thus traces are used instead of states. Through loops or recursion, a statement might be executed multiple times within a trace. To distinguish those, we use the concept of operations as in [7]. A trace is a sequence of events $t = (s_{1}, o_{1}, s_{2}), (s_{2}, o_{2}, s_{3}), \dots, (s_{ν}, o_{ν}, s_{ν + 1}), \dots,$ where the $o_{ν}$ are operations (i.e. dynamically executed program statements $c_{ν}$ ; we write $stmt (o_{ν}) = c_{ν}$ ). Operations are unique within a trace. $s_{ν}, s_{ν + 1}$ are the states before resp. after executing $o_{ν}$ . We write ε for the empty trace. Since we assume programs to be terminating, all traces are finite.

For PN, the notion of low-equivalent traces is essential. Classically, traces are low-equivalent if for every $(s_{ν}, o_{ν}, s_{ν + 1}) \in t$ , $(s_{ν}^{'}, o_{ν}, s_{ν + 1}^{'}) \in t^{'}$ , it holds that $s_{ν} \sim_{L} s_{ν}^{'}$ and $s_{ν + 1} \sim_{L} s_{ν + 1}^{'}$ . This definition enforces a rather restrictive lock-step execution of both traces. Later definitions (e.g. [35]) use stutter equivalence instead of lock-step equivalence; thus allowing one execution to run faster than the other (“stuttering” means that one trace performs additional operations which do not affect public behaviour). To formalize PN, we begin with

Definition 2.
N denotes the set of all program statements $\in P$ , $I \subseteq N$ the input statements (“sources”), $O \subseteq N$ the output statements (“sinks”), $ucl : I \cup O \to {L, H}$ the classification of sources and sinks as provided by the user (“engineer”).

The following definition of low-equivalent traces assumes flow-sensitivity. It is slightly more complex than the “classical” definition, but increases precision as explained below.
Definition 3.

For an operation o, $def (o), use (o)$ are the program variables defined (i.e. assigned) resp. used in o. For state s and $d \subseteq dom (s)$ , $s |_{d}$ is the projection of s onto d.

The low-observable part of an event is defined as $\begin{matrix} E_{L} ((s, o, s^{'})) = \{\begin{matrix} (s |_{use (o)}, o, s^{'} |_{def (o)}), & if ucl (o) = L \\ ε, & otherwise \end{matrix} \end{matrix}$

The low-observable subtrace of trace t is $\begin{matrix} L S (t) = map (E_{L}) (filter (λ e . E_{L} (e) \neq ε) (t)) . \end{matrix}$

Traces $t, t^{'}$ are low-equivalent, written $t \sim_{L} t^{'}$ , if $L S (t) = L S (t^{'})$ . Obviously, $\sim_{L}$ is an equivalence relation. Thus the low-class of t is $\begin{matrix} {[t]}_{L} = {t^{'} | t^{'} \sim_{L} t} . \end{matrix}$

Note that the $t^{'} \in {[t]}_{L}$ cannot be distinguished by an attacker, as all $t^{'} \in {[t]}_{L}$ have the same low behaviour. Thus ${[t]}_{L}$ represents t’s low behaviour. Note also that the flow-sensitive projections $s |_{def} (o)$ , $s |_{use} (o)$ are usually much smaller than a flow-insensitive, statically defined low part of s. This results in more traces to be low-equivalent without compromising soundness. This subtle observation is another reason why flow-sensitive IFC is more precise (cmp. [8], Section 3).

PN is called “probabilistic”, because it essentially depends on the probabilities for certain traces under certain inputs. Thus we define
Definition 4.

$P_{i} (t)$ is the probability that a specific trace t is executed under input i.

$P_{i} ({[t]}_{L})$ is the probability that some trace $t^{'} \in {[t]}_{L}$ (i.e. $t^{'} \sim_{L} t$ ) is executed under i.

As ${[t]}_{L}$ is recursively enumerable, $P_{i}$ is a discrete probability distribution, hence $P_{i} ({[t]}_{L}) = \sum_{t^{'} \in {[t]}_{L}} P_{i} (t^{'})$ .

The following PN definition uses explicit input streams instead of initial states. For all inputs the same initial state is assumed, but it is assumed that all inputs are classified low or high. Traditionally, input streams $i = i_{1} i_{2} \dots,$ $i^{'} = i_{1}^{'} i_{2}^{'} \dots$ are low-equivalent ( $i \sim_{L} i^{'}$ ) if they coincide on low values: $cl (i_{ν}) = L \land cl (i_{ν}^{'}) = L ⟹ i_{ν} = i_{ν}^{'}$ . But this definition is not realistic: Suppose there is a race between a high and a low input statement. Then the classification of the input depends on the race and is no longer independent of a specific execution. This makes it difficult to properly define low-equivalence of inputs. Consequently, Giffhorn used a different definition of low-equivalent inputs: instead of one input stream with input values of varying classification, Giffhorn assumes several input streams with fixed classification each. This leads to
Definition 5.

An input i of a program consists of one input stream per security level; we write $i_{l}$ for the input stream of security level l. An input statement $n \in I$ reads (and removes) the first value from $i_{ucl (n)}$ .

Inputs are considered low-equivalent if their low input streams are equal: $i \sim_{L} i^{'} ⟺ i_{L} = i_{L}^{'}$

$T (i)$ is the set of all possible traces of a program $P$ under input i.

Definition 6 (Probabilistic noninterference).

Let $i, i^{'}$ be inputs; let $Θ = T (i) \cup T (i^{'})$ . PN holds iff $\begin{matrix} i \sim_{L} i^{'} ⟹ \forall t \in Θ : P_{i} ({[t]}_{L}) = P_{i^{'}} ({[t]}_{L}) \end{matrix}$

That is, if we take any trace t which can be produced by i or $i^{'}$ , the probability that a $t^{'} \in {[t]}_{L}$ is executed is the same under i resp. $i^{'}$ . In other words, probability for any public behaviour is independent from the choice of i or $i^{'}$ and thus cannot be influenced by secret input.

If $t \notin T (i)$ , $P_{i} (t) = 0$ . Using the above sum property of $P_{i} ({[t]}_{L})$ , the PN condition is thus equivalent to $\begin{matrix} i \sim_{L} i^{'} ⟹ \forall t : \sum_{t^{'} \in {[t]}_{L}} P_{i} (t^{'}) = \sum_{t^{'} \in {[t]}_{L}} P_{i^{'}} (t^{'}) \end{matrix}$

Applying this to Fig. 2 right, we first observe that all inputs are low-equivalent as there is only high input. For any trace t there are only two possibilities: …print("J")…print("CS")… $\in t$ , or …print("CS")…print("J")… $\in t$ . There are no other low events, hence there are only two equivalence classes $\begin{array}{l} {[t]}_{L}^{1} = {t^{'} | \dots print ("J") \dots print ("CS") \dots \in t^{'}} \\ {[t]}_{L}^{2} = {t^{'} | \dots print ("CS") \dots print ("J") \dots \in t^{'}} \end{array}$ Now if i contains a small value, $i^{'}$ a large value, as discussed earlier $P_{i} ({[t]}_{L}^{1}) \neq P_{i^{'}} ({[t]}_{L}^{1})$ as well as $P_{i} ({[t]}_{L}^{2}) \neq P_{i^{'}} ({[t]}_{L}^{2})$ , hence PN is violated.

In practice, the $P_{i} ({[t]}_{L})$ are difficult or impossible to determine. So far, only simple Markov chains have been used to explicitly determine the $P_{i}$ for very small programs; where the Markow chain models the probabilistic state transitions of a program, perhaps together with a specific scheduler [28,35]. Fortunately, explicit probabilities are not needed for our soundness proofs. As a sanity check, we demonstrate that for sequential programs, PN implies sequential noninterference. Note that for sequential (deterministic) programs $| T (i) | = 1$ , and for the unique $t \in_{1} T (i)$ we have $P_{i} (t) = 1$ .

Lemma 1.
For sequential programs, probabilistic noninterference implies sequential noninterference.
Proof.
Let $s \sim_{L} s^{'}$ . For sequential NI, input is part of the initial states, thus $i \sim_{L} i^{'}$ . Now let $t \in T (i), t^{'} \in T (i^{'})$ , hence $t, t^{'} \in Θ$ . Due to PN, $P_{i} ({[t]}_{L}) = P_{i^{'}} ({[t]}_{L})$ and $P_{i} ({[t^{'}]}_{L}) = P_{i^{'}} ({[t^{'}]}_{L})$ . Due to sequentiality, $P_{i} ({[t]}_{L}) = P_{i} (t) = 1$ and $P_{i^{'}} ({[t^{'}]}_{L}) = P_{i^{'}} (t^{'}) = 1$ . Hence $P_{i^{'}} ({[t]}_{L}) = P_{i^{'}} ({[t^{'}]}_{L}) = 1$ . That is, with probability 1 the trace $t^{'}$ executed under $i^{'}$ is low-equivalent to t. Thus in particular the final states in t resp. $t^{'}$ must be low-equivalent. Hence $s \sim_{L} s^{'}$ implies $[[P]] (s) \sim_{L} [[P]] (s^{'})$ . □

3.3. Low-deterministic security

LSOD is the oldest and simplest criterion which enforces PN. LSOD demands that low-equivalent inputs produce low-equivalent traces. LSOD is scheduler-independent and implies PN (see below). It is intuitively secure: changes in high input can never change low behaviour, because low behaviour is enforced to be deterministic. This is however a very restrictive requirement and eventually led to popular scepticism against LSOD.

Definition 7 (Low-security observational determinism).

Let $i, i^{'}$ , Θ as above. LSOD holds iff $\begin{matrix} i \sim_{L} i^{'} ⟹ \forall t, t^{'} \in Θ : t \sim_{L} t^{'} . \end{matrix}$

Under LSOD, all traces t for input i are low-equivalent: $\forall t^{'} \in T (i) : t^{'} \sim_{L} t$ , thus $T (i) \subseteq {[t]}_{L}$ . If there is more than one trace for i, then this must result from high-nondeterminism; low behaviour is strictly deterministic.

Lemma 2.
LSOD implies PN.
Proof.
Let $i \sim_{L} i^{'}, t \in Θ$ . WloG let $t \in T (i)$ . Due to LSOD, we have $T (i) \subseteq {[t]}_{L}$ . As $P_{i} (t^{'}) = 0$ for $t^{'} \notin T (i)$ , we have $P_{i} ({[t]}_{L}) = \sum_{t^{'} \in {[t]}_{L}} P_{i} (t^{'}) = \sum_{t^{'} \in T (i)} P_{i} (t^{'}) = 1$ , and likewise $P_{i^{'}} ({[t]}_{L}) = 1$ , so $P_{i} ({[t]}_{L}) = P_{i^{'}} ({[t]}_{L})$ . □

Zdancewic [41] proposed the first IFC analysis which checks LSOD. His conditions require that
there are no explicit or implicit leaks,

no low-observable operation is influenced by a data race,

no two low-observable operations can happen in parallel.
The last condition imposes the infamous LSOD restriction, because it explicitly disallows that a scheduler produces various interleavings which switch the order of two low statements which may happen in parallel, and thus would generate low-nondeterminism. Besides that, the conditions can be checked by a static program analysis; Zdancewic used a security type system.

Fig. 3.
Left: insecure program, obvious explicit leak. Middle: secure program, Giffhorn’s criterion + flow-sensitivity avoid false alarm. Right: only RLSOD avoids false alarm.

As an example, consider Fig. 3. In Fig. 3 middle, statements print(L) and L=42 – which are both classified low – can be executed in parallel, and the scheduler nondeterministically decides which executes first; resulting in either 42 or 0 to be printed. Thus there is visible low-nondeterminism, which is prohibited by classical LSOD. The program however is definitely secure according to PN, because the high read can only happen after the race outcome is already decided.
4. Giffhorn’s criterion

In this section, we recapitulate PDGs, their application for LSOD, and Giffhorn’s original criterion. This discussion is necessary in order to understand the new improvements for RLSOD.

4.1. PDGs for IFC

Snelting proposed to use Program Dependence Graphs (PDGs) as a device to check integrity of software as early as 1995 [37]. Later the approach was expanded into the JOANA IFC project. It was shown that PDGs guarantee sequential noninterference [39], and that they provide improved precision as they are naturally flow- and context-sensitive [14].

Fig. 4.

Left to right: PDGs for Figure 2 middle, and for Figure 3 left and middle.

In this paper, we just present three PDG examples and some explanations. PDG nodes represent program statements or expressions; edges represent data dependencies, control dependencies, inter-thread data dependencies, or summary dependencies. Figure 4 presents the PDGs for Fig. 2 middle, and for Fig. 3 left and middle. The construction of precise PDGs for full languages is absolutely nontrivial and requires additional information such as points-to analysis, exception analysis, and thread invocation analysis [14]. We will not discuss PDG details; it is sufficient to know the Slicing Theorem for sequential programs:

Theorem 1.

If there is no PDG path $a \to^{*} b$ , it is guaranteed that statement a can never influence statement b. In particular, values computed in a cannot influence values computed in b.

Proof.

See [15]. □

Thus all statements which might influence a specific program point b are those on backward paths from this point, the so-called “backward slice” $BS (b)$ . In particular, information flow $a \to^{*} b$ is only possible if $a \in BS (b)$ . There are stronger versions of the theorem, which consider only paths which can indeed be dynamically executed (“realizable” paths); these make a big difference in precision e.g. for programs with procedures, objects, or threads [6,14,31].

As an example, consider Fig. 4. The left PDG has a data dependency edge from L=H; to print(L);, because L is defined in line 9 (Fig. 3 left), used in line 10, there is a path in the control flow graph (CFG) from 9 to 10, and L is not reassigned (“killed”) on the path. Thus there is a PDG path from read(H); to print(L);, representing an illegal flow from line 7 to line 10 (a simple explicit leak). In Fig. 4 right, there is no path from L=H; to print(L); due to flow-sensitivity: no scheduler will ever execute L=H; before print(L);. Hence no path from read(H) to print(L); exists, and it is guaranteed that the printed value of L is not influenced by the secret H.

In general, the multi-threaded PDG can be used to check whether there are any explicit or implicit leaks; technically it is required that no high source is in the backward slice of a low sink. This criterion is enough to guarantee sequential noninterference (see Theorem 2). For probabilistic noninterference, according to the Zdancewic LSOD criterion one must additionally show that public output is not influenced by execution order conflicts such as data races, and that there is no low-nondeterminism. This can again be checked using PDGs and an additional analysis called “May-happen-in-parallel” (MHP); the latter will uncover potential execution order conflicts or races. Several precise and sound MHP algorithms for full Java are available today (see e.g. [7,22,27]). Note that an imprecise MHP analysis will substantially degrade the precision of (R)LSOD, and cause many false alarms (see [7,8] for details).

In the following, we will need some definitions related to PDGs. For more details on PDGs, MHP, flow- context-, object- and time-sensitivity, see [14].

Definition 8.

Let $G = (N, \to)$ be a PDG, where N consists of program statements and expressions, and → comprises data dependencies, control dependencies, summary dependencies, and inter-thread dependencies. The (context-sensitive) backward slice for $n \in N$ is defined as $\begin{matrix} BS (n) = {m | m \to_{R}^{*} n} \end{matrix}$ where $\to_{R}^{*}$ includes only realizable (i.e. context-, object- and optionally time-sensitive) paths in the PDG.

For PDG-based analyses, the inputs (“sources”) and outputs (“sinks”) are nodes in the PDG, so $I, O \subseteq N$ . The soundness theorem for PDG-based sequential IFC can now be formalized:

Theorem 2.

Sequential noninterference holds if $\forall n \in I, n^{'} \in O : ucl (n^{'}) = L \land ucl (n) = H ⟹ n \notin BS (n^{'})$

Proof.

Snelting’s original proof was in [39]; additional details are given in [14]. □

The user (“engineer”) classifications $ucl$ in the PDG can be propagated to yield a classification $cl$ of all statements, which provides an alternate way of checking sequential noninterference. This definition will be expanded later to cover concurrent programs.

Definition 9.

The classification $cl$ can be computed from $ucl$ via the flow equation $\begin{matrix} cl (n) = ⨆_{m \to n} cl (m) \end{matrix}$ with additional constraints $\forall n \in I : ucl (n) ⩽ cl (n)$ and $\forall n \in O : ucl (n) ⩾ cl (n)$ .

For an operation o in a trace t, we have $stmt (o) \in N$ and define $cl (o) = cl (stmt (o))$ .

Concerning $cl$ it is important to note that PDGs are automatically flow- and context-sensitive, and may contain a program variable v several times as a PDG node; each occurence of v in N may have a different classification! Thus there is no global classification of variables, but only the local classification $ucl (n)$ together with the global flow constraints $cl (n) = ⨆_{m \to n} cl (m)$ . The latter can easily be computed by a fixpoint iteration on the PDG; which is initialized with the $ucl$ values for source nodes (see [14]). If fixpoint iteration eventually computes $cl (n) > ucl (n)$ for a sink n, an explicit or implicit leak has been discovered [14]. JOANA offers additional support to analyse and localize leaks [9,11].

4.2. LSOD with PDGs

In his 2012 thesis, Giffhorn applied PDGs to PN. He showed that PDGs can naturally be used to check Zdancewic’s LSOD criteria, and provided a soundness proof as well as an implementation for JOANA [7]. Giffhorn also found the first optimization relaxing LSOD’s strict low-determinism.

Giffhorn’s motivation was to repair soundness leaks which had been uncovered in some previous LSOD algorithms. In particular, treatment of nontermination without being overly restrictive or allowing implicit leaks had proven to be tricky. Giffhorn provided a new definition for low-equivalent traces:

Definition 10.
Let $t, t^{'}$ be two finite or infinite traces. $t \sim_{L} t^{'}$ iff
if $t, t^{'}$ are both finite, as usual the low events and low memory parts must coincide (see Definition 3 );

if wloG t is finite, $t^{'}$ is infinite, then this coincidence must hold up to the length of the shorter trace, and the missing operations in t must be missing due to an infinite loop (and nothing else);

for two infinite traces, this coincidence must hold for all low events, or if low events are missing in one trace, they must be missing due to an infinite loop.

The formal version of this definition can be found in [8]. It turned out that conditions 2. and 3. not only avoid previous soundness leaks, but can precisely be characterized by dynamic control dependencies in traces [8]. Furthermore, the latter can soundly and precisely be statically approximated through PDGs (which include all control dependencies). Moreover, the static conditions identified by Zdancewic which guarantee LSOD can naturally be checked by PDGs, and enjoy increased precision due to flow-, context- and object-sensitivity.

In this paper however, we ignore the issue of termination completely and concentrate on the formalization and improvement of Giffhorn’s LSOD check. We begin with some definitions.
Definition 11.

We write $MHP (n, m)$ if MHP analysis concludes that n and m may be executed in parallel. Formally, $MHP (n, m)$ holds if traces $t, t^{'}$ exist where $t = \dots (s_{ν}, o_{ν}, s_{ν + 1}) \dots (s_{μ}, o_{μ}, s_{μ + 1}) \dots,$ $t^{'} = \dots (s_{μ}^{'}, o_{μ}, s_{μ + 1}^{'}) \dots (s_{ν}^{'}, o_{ν}, s_{ν + 1}^{'}) \dots,$ $n = stmt (o_{ν})$ , $m = stmt (o_{μ})$ .

$lnd (n, n^{'}) ⟺ MHP (n, n^{'}) \land ucl (n) = ucl (n^{'}) = L$ , which denotes that $n, n^{'}$ are low-nondeterministic;

$race (n, n^{'}) ⟺ MHP (n, n^{'}) \land \exists v \in (def (n) \cap (def (n^{'}) \cup use (n^{'})))$ , which denotes there is a data race between $n, n^{'}$ which can influence the value read at $n^{'}$ .

$path (n, n^{'}) ⟺ n \to_{CFG}^{} n^{'}$ is a path in the CFG. We will also use* $path (n, n^{'})$ to denote the set of all nodes $n^{″}$ on CFG paths from n to $n^{'}$ .

Then the PDG-based LSOD criterion – a formalization of Zdancewic’s criterion using PDGs – requires:
Definition 12 (Giffhorn’s criterion).

$\forall n \in O, n^{'} \in I : ucl (n) = L \land ucl (n^{'}) = H ⟹ n^{'} \notin BS (n)$ ,

$\forall n, n^{'} \in N, n^{″} \in O : race (n, n^{'}) \land ucl (n^{″}) = L ⟹ n^{'} \notin BS (n^{″})$ ,

$\forall n, n^{'} \in I \cup O : \neg lnd (n, n^{'})$ .

Theorem 3.
Giffhorn’s criterion implies LSOD.
Proof.
For proof and implementation details, see [8]. □

Condition 1 is just sequential noninterference (no explicit/implicit leaks, see Theorem 2), condition 2 guarantees that no race is in the backward slice of a low sink, and condition 3 prohibits any low-nondeterminism. Note that the race definition8
⁸
In [7] these races were called “data conflicts”.

from Definition 11 is asymmetric: Giffhorn discovered that only two of the three classical race situations (“write-write, write-read, read-write“) are relevant. The case $v \in def (n) \cap use (n^{'}), n \in BS (n^{″})$ can never cause a leak because the value written at n is independent of the outcome of that race! Thus the example from the top of Fig. 5 is considered secure, whereas a symmetric race definition would have caused a false alarm. Also note that conditions 2 and 3 are not completely disjoint, in particular if $ucl (n) = ucl (n^{'}) = ucl (n^{″}) = L, n \in BS (n^{″})$ both conditions are violated.

Fig. 5.
Races with one node in the backward slice of a low sink. Top: $n = " L = 1 "$ , $n^{'} = " H = H + L "$ , $n^{″} = " print (X) "$ , $n \in BS (n^{″})$ . Bottom: $n = " H = 42 "$ , $n^{'} = " H - - "$ , $n^{″} = " print (L) "$ , $n^{'} \in BS (n^{″})$ .

Applying Giffhorn’s criterion to Fig. 2 right, it discovers a leak according to condition 3, namely low-nondeterminism between lines 6 and 11; which is correct. For the example in Fig. 5 bottom, condition 3 is not violated, but condition 2 is violated. In Fig. 3 left, a leak is discovered according to condition 1, which is also correct (cmp. PDG example above). In Fig. 3 middle and right, the explicit leak has disappeared (thanks to flow-sensitivity), but another leak is discovered by condition 2: we have $race (L = 42;, print (L);)$ and $print (L); \in BS (print (L);)$ , which causes a false alarm.

The example motivates Giffhorn’s optimized criterion: low-nondeterminism may be allowed, if it cannot be reached from high events. That is, there must not be a path in the control flow graph from some $n^{″}$ , where $ucl (n^{″}) = H$ , to n or $n^{'}$ , where $lnd (n, n^{'})$ . If there is no path from a high event to the low-nondeterminism, no high statement can ever be executed before the nondeterministic low statements. Thus the latter can never produce visible behaviour which is influenced by high values. This argument leads to Giffhorn’s optimized criterion, which replaces condition 3 from Definition 12 by
$\forall n, n^{'} \in I \cup O : (\exists n^{″} \in I : ucl (n^{″}) = H \land (path (n^{″}, n) \lor path (n^{″}, n^{'}))) ⟹ \neg lnd (n, n^{'})$
This condition can be rewritten by contraposition to the more practical form

$\forall n, n^{'} \in I \cup O : lnd (n, n^{'}) ⟹ \forall n^{″} \in (path (START, n) \cup path (START, n^{'})) \cap I : ucl (n^{″}) = L$

In fact Giffhorn’s optimization works for data races as well: no data race may be in the backward slice of a low sink, unless it is unreachable by high events. That is, condition 2 can be improved the same way as condition 3, leading to
$\forall n, n^{'} \in N, n^{″} \in O : race (n, n^{'}) \land cl (n^{″}) = L \land \exists n^{‴} \in I : ucl (n^{‴}) = H \land (path (n^{‴}, n) \lor path (n^{‴}, n^{'}))$ $⟹ n, n^{'} \notin BS (n^{″})$ .
By contraposition, we obtain the more practical form

$\forall n, n^{'} \in N, n^{″} \in O : race (n, n^{'}) \land ucl (n^{″}) = L \land n^{'} \in BS (n^{″}) ⟹ \forall n^{‴} \in (path (START, n) \cup path (START, n^{'})) \cap I : ucl (n^{‴}) = L$

Remember that condition $2^{'}$ is not symmetrical in $n, n^{'}$ , due to Giffhorn’s simplified race definition. Figure 2 right violates Giffhorn’s criterion, because one of the low-nondeterministic statements, namely line 11, can be reached from the high statement in line 8; thus criterion $3^{'}$ is violated. Indeed the example contains a probabilistic leak. Figure 3 middle is secure according to Giffhorn, because the data race between line 6 resp. 9 can not be reached from any high statement – condition 2 is violated (note that in this example, $n^{'} = n^{″}$ ), but $2^{'}$ holds. Indeed the program is PN. Figure 3 right is however not covered by Giffhorn’s criterion, because the initial read(H2) will reach any other statement. But the program is PN, because H2 does not influence the data race determining the low behavior!

The example shows that Giffhorn’s optimization does indeed reduce false alarms, but it removes only false alarms on low paths beginning at program start. Anything after the first high statement will usually be reachable from that statement, and does not profit from rule $3^{'}$ resp. $2^{'}$ . Still Giffhorn’s algorithm was a big step, as it allowed – for the first time – low-nondeterminism, while basically maintaining the LSOD approach.
5. RLSOD

In the following, we will generalize conditions $2^{'}$ and $3^{'}$ to obtain the much more precise RLSOD criterion.

To motivate the improvement, consider again Fig. 2 right (program $P_{1}$ ) and Fig. 3 right (program $P_{2}$ ). Both contain race conditions influencing low behavior, $P_{1}$ through low-nondeterminism and $P_{2}$ through a data race. When comparing $P_{1}$ and $P_{2}$ , a crucial difference comes to mind. In $P_{2}$ the troublesome high statement can reach both statements forming the race condition, whereas in $P_{1}$ , the high statement can reach only one of them. In both programs some loop running time depends on a high value, but in $P_{2}$ , the subsequent statements are influenced by this “timing leak” in exactly the same way, while in $P_{1}$ they are not.

In terms of the PN definition, remember that $P_{1}$ has only two low-classes ${[t]}_{L}^{1} = {t^{'} | t^{'} = \dots print ("J") \dots print ("CS") \dots}$ and ${[t]}_{L}^{2} = {t^{'} | t^{'} = \dots print ("CS") \dots print ("J") \dots}$ . Likewise, $P_{2}$ has two low-classes ${[t]}_{L}^{1} = {t^{'} | t^{'} = \dots print (42) \dots}$ and ${[t]}_{L}^{2} = {t^{'} | t^{'} = \dots print (0) \dots}$ , depending on the outcome of the data race. The crucial difference is that for $P_{1}$ , the probability for the two classes under i resp. $i^{'}$ is not the same (see above), but for $P_{2}$ , $P_{i} ({[t]}_{L}^{1, 2}) = P_{i^{'}} ({[t]}_{L}^{1, 2})$ holds!

Technically, $P_{2}$ contains a point c which dominates both racing statements $n \equiv L = 42;$ and $m \equiv print (L)$ , and all relevant high events always happen before c. Domination means that any control flow from $START$ to n or m must pass through c. In $P_{2}$ , c is the point immediately before the first fork. In contrast, $P_{1}$ has only a trivial common dominator for the low-nondeterminism, namely the $START$ node, and on the path from $START$ to $n \equiv print ("J")$ there is no high event, while on the path to $m \equiv print ("CS")$ there is.

Intuitively, the high inputs can cause strong nondeterministic high behaviour, including stuttering. But if LSOD conditions 1 + 2 are always satisfied, and if there are no high events in any trace between c and n resp. m, the effect of the high behaviour is always the same for n and m and thus “factored out”. It cannot cause a probabilistic leak – the dominator “shields” the low-nondeterminism from high influence. Note that $P_{2}$ contains an additional high statement $m^{'} \equiv read (H)$ but that is behind n (no control flow is possible from $m^{'}$ to n) and thus cannot influence the $n / m$ nondeterminism.

5.1. Improving conditions $2^{'}$ and $3^{'}$

The above example has demonstrated that low-nondeterminism may be reachable by high events without harm, as long as these high events always happen before the common dominator of the nondeterministic low statements. This observation will be even more important if dynamically created threads are allowed (as in JOANA, cmp. Section 7). We will now provide precise definitions for this idea.

Definition 13 (Common dynamic ancestor).

Let $n, m, c \in N$ be statements.

c is a dominator for n, written $c dom n$ , if c occurs on every CFG path from $START$ to n.

c is a common dominator for $n, m$ , written $c cdom (n, m)$ , if $c dom n \land c dom m$ .

c is a common dynamic ancestor for $n, m$ , written $c cda (n, m)$ , if

$c cdom (n, m) \land \neg MHP (c, n) \land \neg MHP (c, m)$ .

If $c cda (n, m)$ and $\forall c^{'} cda (n, m) : c^{'} dom c$ , then c is called an immediate common dynamic ancestor.

Efficient algorithms for computing dominators can be found in many compiler textbooks. They can be extended to calculate common dynamic ancestors. The stricter definition of common dynamic ancestors compared to common dominators is needed to deal with the possibility that the same thread can be spawned several times, as e.g. in our case study (chapter 7). Note that $START$ itself is a (trivial) common dynamic ancestor for every $n, m$ . RLSOD works with any common dynamic ancestor. We thus assume a function $cda$ which for every statement pair returns a common dynamic ancestor, and write $c = cda (n, m)$ . Note that the implementation of $cda$ may depend on the precision requirements, but once a specific $cda$ is fixed, c depends solely on n and m. Straightforward implementation of the RLSOD idea leads to the following rules, replacing rules $3^{'}$ and $2^{'}$ from Giffhorn’s optimized criterion:

$\forall n, n^{'} : lnd (n, n^{'}) \land c = cda (n, n^{'}) ⟹ \forall n^{″} \in (path (c, n) \cup path (c, n^{'})) \cap I : ucl (n^{″}) = L$

$\forall n, n^{'} \in N, n^{″} \in O : race (n, n^{'}) \land c = cda (n, n^{'}) \land ucl (n^{″}) = L \land n^{'} \in BS (n^{″}) ⟹ \forall n^{‴} \in (path (c, n) \cup path (c, n^{'})) \cap I : ucl (n^{‴}) = L$

These conditions are most precise (generate the least false alarms) if

cda

returns the immediate common dynamic ancestor, because in this case it demands that

cl (n^{″}) = L

for the smallest set of nodes “behind” the common ancestor.9

⁹
Note that in programs with procedures and threads, immediate dynamic ancestors may not be unique due to context-sensitivity [5].

Fig. 6 illustrates the RLSOD definition (condition

3^{″}

). Note that Giffhorn’s optimized criterion trivially fulfils conditions

2^{″}

and

3^{″}

, where

cda

always returns

START

. In [4], we provided a soundness proof for the case of just one low-nondeterminism. However, as the next section will show, in the case of multiple low-nondeterministic statements those rules are not sound.

Fig. 6.

Visualization of LSOD vs. Giffhorn’s criterion vs. RLSOD (condition $3 / 3^{'} / 3^{″}$ ). CFGs for Figure 2 right resp. Figure 3 right are sketched. n/m produces low-nondeterminism, c is the common dominator. LSOD prohibits any low-nondeterminism; Giffhorn allows low-nondeterminism which is not reachable by any high events; RLSOD allows low-nondeterminism which may be reached by high events if they are before the common dominator. The marked regions are those affected by low-nondeterminism; inside these regions no high events are allowed. Thus RLSOD is much more precise.

5.2. Classification revisited

Fig. 7.

A leak which goes undiscovered if classification of statements is incomplete.

Consider the program in Fig. 7 middle/right. This example contains a probabilistic leak as follows. H influences the running time of the first while loop, hence H influences whether line 10 or line 18 is performed first. The value of tmp2 influences the running time of the second loop, hence it also influences whether L1 or L2 is printed first. Thus H indirectly influences the execution order of the final print statements. Indeed the program does not fulfill Giffhorn’s criterion, as the print statements can be reached from the high statement in line 3 (middle). Applying $3^{″}$ , the common dynamic ancestor for the two print statements is line 10. But the only input statement is line 3, which is before the cda.

The classification of line 10 is thus crucial. If we had $cl (10) = H$ , then this classification propagates in the PDG (due to the flow equation $cl (n) = ⨆_{m \to n} cl (m)$ ) and lines 12/13 are classified high. RLSOD is violated, and the probabilistic leak discovered.

Hence we use the flow equation to calculate the classification propagation from line 3 to line 10, and then 12/13. Only line 3 is explicitly high and only lines 4, 7, 8 are PDG-reachable from 3. Thus $cl (10) = L$ . Hence RLSOD would be satisfied because 3, 4, 7, 8 are before the common dominator. The leak would go undiscovered! The problem is that rules $2^{″}$ and $3^{″}$ are not applied recursively. To capture the effect of recursive influence through nondeterminism, the flow equations must be extended.

In general, the rule is as follows. The standard flow equation $cl (n) = ⨆_{m \to n} cl (m)$ expresses the fact that if a high value can reach a PDG node m upon which n is dependent, then the high value can also reach n. Likewise, if there is low-nondeterminism with $MHP (n, m)$ , and $cda (n, m) = c$ , and the path $c \to_{CFG}^{*} n$ violates RLSOD – that is, it contains high statements – then the high value can reach n. Thus $cl (n) = H$ must be enforced. This rule must be applied recursively until a fixpoint is reached.

Definition 14 (Classification in PDGs).

A PDG $G = (N, \to)$ is classified correctly, if

$\forall n \in N : cl (n) ⩾ ⨆_{m \to n} cl (m)$ ,

$\forall n, m \in N : MHP (n, m) \land c = cda (n, m) \land \exists c^{'} \in path (c, n), cl (c^{'}) = H ⟹ cl (n) = H$ .

$\forall n \in I : ucl (n) = cl (n)$ and $\forall n \in O : ucl (n) ⩾ cl (n)$ .

In condition (a), ⩾ must be used because (b) can push $cl (n)$ higher than $⨆_{m \to n} cl (m)$ . Condition (b) can be rewritten as $MHP (n, m) \land c = cda (n, m) ⟹ cl (n) ⩾ ⨆_{c^{'} \in path (c, n)} cl (c^{'})$ ; making it formally similar to (a).10

¹⁰
This formulation is used by JOANA; it also has the advantage that RLSOD can be used for an arbitrary security lattice. Note that our current soundness proof works only with the $L / H$ lattice.

Note the asymmetry in condition (c): Treating a public input value as secret is sound, thus one might want to use

\forall n \in I : ucl (n) ⩽ cl (n)

in that condition. However, we assume that the attacker can observe when low input statements are executed. Thus, whether they are executed must not depend on H values, so

\forall n \in I : ucl (n) ⩾ cl (n)

must be enforced as well.

For a sequential program, $MHP$ is always false, so only rules (a) and (c) remain. Note that (a)+(c) is equivalent to Definition 9, the calculation of sequential noninterference. In Fig. 7 middle/right, Definition 14 enforces line 10 to be classified high, as we have $cda (10, 18) = 6$ , and on the path from 6 to 10, lines 7 and 8 are high.

Now, classification rules (a), (b) and (c) could be combined with $1^{″}$ , $2^{″}$ and $3^{″}$ to yield a sound RLSOD criterion. But surprisingly it turns out that this is not necessary – Section 6 will demonstrate that classifiability according to Definition 14 already implies PN! In fact, $1^{″}$ , $2^{″}$ and $3^{″}$ are necessary conditions for classifiability:

Theorem 4.

If the program can be classified according to Definition 14 , then the RLSOD conditions $1^{″}$ , $2^{″}$ , $3^{″}$ hold.

Proof.

Assume that (a), (b), (c) hold, but one of the rules $1^{″}$ , $2^{″}$ , $3^{″}$ is violated. We therefore have 3 cases:

$1^{″}$ is violated: Since an H source n is in the backward slice of an L sink $n^{'}$ , with classification rule (c) we have $cl (n) = H$ , $cl (n^{'}) = L$ and $n \to^{*} n^{'}$ . But then repeated application of rule (a) demands $cl (n^{'}) = H$ , which is a contradiction.

$3^{″}$ is violated: For the two $lnd$ statements n and $n^{'}$ we have $cl (n) = cl (n^{'}) = L$ by rule (c). But then we have a statement $n^{″}$ with $cl (n^{″}) = H$ on the control flow path from $c : = cda (n, n^{'})$ to n or to $n^{'}$ . Without loss of generality we assume that $n^{″}$ lies on the path from c to n. But then rule (b) demands $cl (n) = H$ , contradicting $cl (n) = L$ .

$2^{″}$ is violated: We have $cl (n^{″}) = L$ by rule (c), and by rule (a) we have $cl (n^{'}) = L$ since $n^{'} \in BS (n^{″})$ . Since we also have $race (n, n^{'})$ , n must write the same variable that $n^{'}$ reads or writes, and thus we have $n \in BS (n^{'})$ and $cl (n) = L$ as well. Then we can apply the same argument to n and $n^{'}$ as in the previous case. □

Henceforth, we will subsume Definition 14 under the notion of RLSOD. To actually use it as a PN checker, it uses a fixpoint iteration similar to the sequential one (Definition 9, see also [9,14]).

6. The general soundness proof

In the conference paper preceding this article [4], a soundness proof was provided for the special case that there is just one occurrence of low-nondeterminism (i.e. $| {(n, n^{'}) | lnd (n, n^{'}) \lor race (n, n^{'})} | ⩽ 1$ ). The full proof posed more difficulties than expected, but eventually led to a simpler formulation of the RLSOD criterion, namely in form of Definition 14. We thus omit the proof of the special case (see [4], Section 4.3), but will in this section describe the full soundness proof, based on Definition 14. As in [4], the proof relies on the notion of conditional probability for traces.

Definition 15.
Let $t_{1} \dots$ be the set of traces beginning with prefix $t_{1}$ , so that $P_{i} (t_{1} \dots) = \sum_{t = t_{1} \cdot t_{2}} P_{i} (t)$ is the probability that execution under input i begins with $t_{1}$ . For a set T of traces let $T \dots = ⋃_{t \in T} t \dots$ . We denote with $P_{i} (t_{2} | t_{1})$ the conditional probability that after $t_{1}$ , execution continues with $t_{2}$ ; we have $\begin{matrix} P_{i} (t_{2} | t_{1}) = P_{i} (t_{1} \cdot t_{2}) / P_{i} (t_{1} \dots) \end{matrix}$ This notion extends to sets of traces: $\begin{matrix} P_{i} (T^{'} | T) = P_{i} (T \cdot T^{'}) / P_{i} (T \dots) = \sum_{t \in T \cdot T^{'}} P_{i} (t) / \sum_{t \in T \dots} P_{i} (t) \end{matrix}$

In the following it will always hold that $T (i) \cap T \dots \neq \emptyset$ , hence $\sum_{t \in T \dots} P_{i} (t) \neq 0$ .

The following soundness theorem and its derivation will of course be based on Definition 3 (low-equivalent traces), but in the proofs we will also need a variant of this definition as an auxiliary construction: We define $E_{cl} ((s, o, s^{'}))$ , $t \sim_{cl} t^{'}$ and ${[t]}_{cl}$ exactly as $E_{L} ((s, o, s^{'}))$ , $t \sim_{L} t^{'}$ and ${[t]}_{L}$ (see Definition 3), except that in the definition $ucl$ is replaced by $cl$ . We omit a repetition of the definition details, as $E_{cl}$ , $\sim_{cl}$ and ${[]}_{cl}$ are only used in the proofs and do not appear in the soundness theorem itself.
Lemma 3.

${[t_{1}]}_{cl} {[t_{2}]}_{cl} = {[t_{1} t_{2}]}_{cl}$

$P_{i} ({[t]}_{cl}) = P_{i} ({[ε]}_{cl} | {[t]}_{cl}) \cdot P_{i} ({[t]}_{cl} \dots | {[ε]}_{cl})$

$P_{i} ({[t_{1} t_{2}]}_{cl} \dots | {[ε]}_{cl}) = P_{i} ({[t_{2}]}_{cl} \dots | {[t_{1}]}_{cl}) \cdot P_{i} ({[t_{1}]}_{cl} \dots | {[ε]}_{cl})$

Proof.

We have $L S_{cl} (t \cdot t^{'}) = L S_{cl} (t) \cdot L S_{cl} (t^{'})$ from Definition 3 for all $t, t^{'}$ since $L S_{cl}$ is a composition of $map$ and $filter$ . With the definition of $\sim_{cl}$ , this implies ${[t_{1}]}_{cl} {[t_{2}]}_{cl} = {[t_{1} t_{2}]}_{cl}$ .

$P_{i} ({[ε]}_{cl} | {[t]}_{cl}) \cdot P_{i} ({[t]}_{cl} \dots | {[ε]}_{cl}) = P_{i} ({[ε]}_{cl} {[t]}_{cl}) / P_{i} ({[t]}_{cl} \dots) \cdot P_{i} ({[t]}_{cl} \dots) / P_{i} ({[ε]}_{cl} \dots) = P_{i} ({[ε]}_{cl} {[t]}_{cl}) / P_{i} ({[ε]}_{cl} \dots) = P_{i} ({[t]}_{cl})$ , using equation (1) and the fact that all traces begin with $ε \in {[ε]}_{cl}$ , so $P_{i} ({[ε]}_{cl} \dots) = 1$ .

$P_{i} ({[t_{2} \dots]}_{cl} | {[t_{1}]}_{cl}) \cdot P_{i} ({[t_{1} \dots]}_{cl} | {[ε]}_{cl}) = P_{i} ({[t_{1}]}_{cl} {[t_{2}]}_{cl} \dots) / P_{i} ({[t_{1}]}_{cl} \dots) \cdot P_{i} ({[t_{1}]}_{cl} \dots) / P_{i} ({[ε]}_{cl}) = P_{i} ({[t_{1}]}_{cl} {[t_{2}]}_{cl} \dots) / P_{i} ({[ε]}_{cl}) = P_{i} ({[t_{1}]}_{cl} {[t_{2}]}_{cl} \dots | {[ε]}_{cl}) = P_{i} ({[t_{1} t_{2}]}_{cl} \dots | {[ε]}_{cl})$ □

For the following theorems, let $op (c)$ denote the operation of an event c, i.e. for $c = (s, o, s^{'})$ , we have $op (c) = o$ . For convenience, we first prove the following lemmas:
Lemma 4.
Let $P$ be a terminating program. Assume that classification rules (a) and (c) according to Definition 14 hold. Let $t_{1} \cdot c \cdot t_{2} \in T (i)$ and $t_{1}^{'} \cdot c^{'} \cdot t_{2}^{'} \in T (i^{'})$ with $op (c) = op (c^{'})$ , $cl (op (c)) = L$ , $t_{1} \sim_{cl} t_{1}^{'}$ and $i \sim_{L} i^{'}$ .

Then $E_{cl} (c) = E_{cl} (c^{'})$ .
Proof.
Let $o : = op (c) = op (c^{'})$ . If o reads input, we have $stmt (o) \in I$ , and $ucl (stmt (o)) = cl (stmt (o)) = L$ by rule (c), and it therefore reads from the low input stream. From rule (c) we also have that all other operations that have read from this stream before are classified as low, and thus show up in $cl$ -low-observable subtraces. This means the same reads must have happened before c and $c^{'}$ , and so c and $c^{'}$ read the same values from input.

If o reads values from memory, o is data dependent on the operations that wrote those values, so those must be classified as L by classification rule (a). But then those show up in a $cl$ -low-observable subtrace, and since $t_{1} \sim_{cl} t_{1}^{'}$ , the same of those operations must have happened for $t_{1}$ and $t_{1}^{'}$ , and they wrote the same values in the same order. Therefore, c and $c^{'}$ read the same values. Since statements themselves are deterministic, the values written by c and $c^{'}$ are equal as well. Thus we have $E_{cl} (c) = E_{cl} (c^{'})$ . □
Lemma 5.
Let $P$ be a program that always terminates and let classification rule (a) according to Definition 14 hold. Let $t = t_{1} \cdot c \cdot t_{2}$ be a possible trace for $P$ and $cl (c) = L$ . Let $t^{'} = t_{1}^{'} \cdot t_{2}^{'}$ with $t_{1}^{'} \sim_{cl} t_{1}$ also be a possible trace.

Then $op (c)$ must occur on $t_{2}^{'}$ .
Proof.
Since operations are unique in a trace, $t_{1}$ cannot contain $op (c)$ , and neither can $t_{1}^{'}$ since $cl (c) = L$ . Thus, it suffices to show that $op (c)$ is executed on $t_{1}^{'} \cdot t_{2}^{'}$ . This is trivially fulfilled for the starting operation. Else, let p be the operation that directly controls whether $op (c)$ is executed. We have $stmt (c) = stmt (p)$ or $stmt (c)$ is control dependent on $stmt (p)$ . With classification rule (a), we have $cl (p) = L$ . Since $t_{1}^{'} \sim_{cl} t_{1}$ , p was executed on $t_{1}^{'}$ as well and has read the same values as on $t_{1}$ . Therefore, it chooses the same branch, so $op (c)$ must occur on $t_{1}^{'} \cdot t_{2}^{'}$ as well. □

We now show that if a program’s PDG can be classified correctly, then for a $cl$ -low-class, the probability of observing it does not differ between low-equivalent inputs:
Theorem 5.
Let $P$ be a program that always terminates and $ucl$ a user annotation for $P$ . Let $cl$ be a correct classification of its PDG according to Definition 14 .

Now let $i, i^{'}$ be two inputs with $i \sim_{L} i^{'}$ , let t be a trace. Then $\begin{matrix} P_{i} ({[t]}_{cl}) = P_{i^{'}} ({[t]}_{cl}) . \end{matrix}$
Proof.
We will prove the equation by contradiction. So, let us assume $P_{i} ({[t]}_{cl}) \neq P_{i^{'}} ({[t]}_{cl})$ . Let $t = c_{1} \cdot c_{2} \dots c_{n}$ be the decomposition of t into single events. With the calculation rules from Lemma 3, applying rule 2 and then repeatedly applying rule 3, we get $\begin{matrix} P_{i} ({[t]}_{cl}) = (\prod_{j = 1}^{n} P_{i} ({[c_{j}]}_{cl} \dots | {[c_{1} \cdot \dots \cdot c_{j - 1}]}_{cl})) \cdot P_{i} ({[ε]}_{cl} | {[t]}_{cl}), \end{matrix}$ and the same for $i^{'}$ . Since the left sides for i and $i^{'}$ are not equal, the same must hold for at least one factor. Furthermore, we have $\begin{matrix} P_{i} ({[ε]}_{cl} | {[t]}_{cl}) = P_{i^{'}} ({[ε]}_{cl} | {[t]}_{cl}) \end{matrix}$ by the following argument: If not both sides are 1, there is a low event that is possible after a trace in ${[t]}_{cl}$ . From Lemma 5 we then have that this event occurs on every trace $t^{'} \sim_{cl} t$ , making both probabilities 0.

Thus, there is a j that the factor $\begin{matrix} P ({[c_{j}]}_{cl} \dots | {[c_{1} \dots c_{j - 1}]}_{cl}) \end{matrix}$ is different for i and $i^{'}$ . Let $t_{1} = c_{1} \dots c_{j - 1}$ and $c = c_{j}$ . Then we have $\begin{matrix} P_{i} ({[c]}_{cl} \dots | {[t_{1}]}_{cl}) \neq P_{i^{'}} ({[c]}_{cl} \dots | {[t_{1}]}_{cl}) . \end{matrix}$ In the following, we will focus on these two conditional probabilities, so we can assume that the trace that has happened until that point is $cl$ -low-equivalent to $t_{1}$ .

Without loss of generality we assume $\begin{matrix} P_{i} ({[c]}_{cl} \dots | {[t_{1}]}_{cl}) > P_{i^{'}} ({[c]}_{cl} \dots | {[t_{1}]}_{cl}) \end{matrix}$ (switch i and $i^{'}$ if necessary). $op (c)$ gets executed for i since the former probability is greater than zero, and we have $cl (c) = L$ because else both probabilities would be equal to 1. With Lemma 5 we have that $op (c)$ will be executed in every trace in ${[t_{1}]}_{cl} \dots$ .

Since the remaining trace must execute $op (c)$ given an execution in ${[t_{1}]}_{cl}$ has happened, its $cl$ -low-observable part cannot be empty. The conditional probabilities for the different $cl$ -low-observable parts of low events given ${[t_{1}]}_{cl}$ must add up to 1 for i and $i^{'}$ , but we have $\begin{matrix} P_{i} ({[c]}_{cl} \dots | {[t_{1}]}_{cl}) > P_{i^{'}} ({[c]}_{cl} \dots | {[t_{1}]}_{cl}) . \end{matrix}$ Thus, there is a $c^{'}$ with $E_{cl} (c) \neq E_{cl} (c^{'})$ such that $\begin{matrix} P_{i} ({[c^{'}]}_{cl} \dots | {[t_{1}]}_{cl}) < P_{i^{'}} ({[c^{'}]}_{cl} \dots | {[t_{1}]}_{cl}) . \end{matrix}$ Analogously to above, $op (c^{'})$ must happen after each trace in ${[t_{1}]}_{cl}$ .

If $op (c) = op (c^{'})$ , with Lemma 4 we get $E_{cl} (c) = E_{cl} (c^{'})$ , contradicting $E_{cl} (c) \neq E_{cl} (c^{'})$ . Thus $op (c) \neq op (c^{'})$ . Let $o : = op (c)$ and $o^{'} : = op (c^{'})$ . o and $o^{'}$ must be executed after a trace in ${[t_{1}]}_{cl}$ has been executed. In fact, o can be executed directly after it (at least for input i) and since $o \neq o^{'}$ , $o^{'}$ must then happen after o. Analogously, o can happen after $o^{'}$ . This makes $s : = stmt (o)$ and $s^{'} : = stmt (o^{'})$ an $MHP$ pair. Let $d : = cda (s, s^{'})$ . Then by classification rule (b) with $n = s, m = s^{'}$ all nodes in $path (d, s)$ are classified as L. o can be scheduled for input i, so the CFG predecessors of s that were already executed allow o to be executed next. Those are in $path (d, s)$ since otherwise we would have $d = s$ , which is impossible because with $MHP (s, s^{'})$ we have $MHP (d, s^{'})$ , a contradiction to Definition 13. Thus, they are $cl$ -low-observable and therefore have happened for any trace $t_{1}^{'} \sim_{cl} t_{1}$ as well. Thus, o can be scheduled for every such trace $t_{1}^{'}$ , regardless of i or $i^{'}$ . The same argument shows that $o^{'}$ can be scheduled after every such $t_{1}^{'}$ . From Lemma 4 we also have that the only possible $cl$ -low-observable part of the event for o is $E_{cl} (c)$ , so $\begin{matrix} P_{i} ({[c]}_{cl} \dots | {[t_{1}]}_{cl}) = P_{i} ({[o]}_{cl} \dots | {[t_{1}]}_{cl}) \end{matrix}$ and $\begin{matrix} P_{i}^{'} ({[c]}_{cl} \dots | {[t_{1}]}_{cl}) = P_{i}^{'} ({[o]}_{cl} \dots | {[t_{1}]}_{cl}) \end{matrix}$ (we use ${[o]}_{cl}$ here as a shorthand for $⋃_{op (c) = o} {[c]}_{cl}$ ). The same holds for $o^{'}$ and $c^{'}$ . If we go from i to $i^{'}$ , the probability of scheduling o gets smaller but the probability of scheduling $o^{'}$ gets greater. Therefore, the relative scheduling probabilities do not stay the same, even though for both inputs, both operations can be scheduled. This contradicts the assumption of a truly probabilistic scheduler. □

We now can prove that the conditions of the previous theorem guarantee PN. Corollary 1.
Let $P$ be a terminating program and $ucl$ a user annotation for $P$ . Let $cl$ be a correct classification of its PDG according to Definition 14 .

Now let $i \sim_{L} i^{'}$ according to Definition 5 , let $t \in Θ$ . Then $\begin{matrix} P_{i} ({[t]}_{L}) = P_{i^{'}} ({[t]}_{L}) . \end{matrix}$
Proof.
Classification rule (c) ensures that all sources and sinks n with $ucl (n) = L$ also fulfill $cl (n) = L$ . Thus, for all traces $t_{1}, t_{2}$ we have $t_{1} \sim_{cl} t_{2} ⟹ t_{1} \sim_{L} t_{2}$ . Therefore, we can write ${[t]}_{L}$ as disjoint union of all ${[t^{'}]}_{cl} \subseteq {[t]}_{L}$ . With the probability formula for disjoint unions we have $\begin{matrix} P_{i} ({[t]}_{L}) = \sum_{{[t^{'}]}_{cl} \subseteq {[t]}_{L}} P_{i} ({[t^{'}]}_{cl}), \end{matrix}$ and the same for $i^{'}$ . By applying Theorem 5, we get $P_{i} ({[t^{'}]}_{cl}) = P_{i^{'}} ({[t^{'}]}_{cl})$ for all ${[t^{'}]}_{cl}$ . Thus, $\begin{matrix} P_{i} ({[t]}_{L}) = \sum_{{[t^{'}]}_{cl} \subseteq {[t]}_{L}} P_{i} ({[t^{'}]}_{cl}) = \sum_{{[t^{'}]}_{cl} \subseteq {[t]}_{L}} P_{i^{'}} ({[t^{'}]}_{cl}) = P_{i^{'}} ({[t]}_{L}) \end{matrix}$ □

7. Case study: E-voting

We will now apply RLSOD to an experimental e-voting system developed in collaboration with R. Küsters et al. This system aims at a provably secure e-voting software that uses cryptography to ensure computational indistinguishability. To prove computational indistinguishability, the cryptographic functions are replaced with an “ideal variant”: The encryption creates a random number as encrypted message and remembers the connection of this message and the key to the plaintext. The decryption can then get the plaintext back by providing the key and the encrypted text.11

¹¹
Note that due to this construction, at the encryption site there is no flow from the plaintext or key to the encrypted message.

It is then checked by IFC that no flow exists between plain text, secret key and encrypted message; that is, probabilistic noninterference holds for the e-voting system with ideal crypto implementation. By a theorem of Küsters, noninterference of the ideal variant implies computational indistinguishability for the system with real encryption [19,21].

The example uses a multi-threaded client-server architecture to send encrypted messages over the network. It consists of 550 LoC with 16 classes. The interprocedural control flow is sketched in Fig. 8; Fig. 9 contains relevant parts of the code. The main thread starts in class Setup in line 2ff: First it initializes encryption by generating a private and public key, then it spawns a single Server thread before entering of the main loop. Inside the main loop it reads a secret message from the input and spawns a Client that takes care of the secure message transfer: The client encrypts the given message and subsequently sends it via the network to the server. Note that there are multiple instances of the client thread as a new one is started in each iteration.

Fig. 8.

CFG structure of the multi-threaded server-client based message transfer.

Fig. 9.

Relevant parts of the multi-threaded encrypted message passing system with security annotations for JOANA.

Fig. 10.

JOANA analysing the e-voting source code.

There are two sources of secret (high) information: (1) the value of the parameter secret_bit (line 2) that decides about the content of the message; and (2) the private key of the encryption (line 30). Both are marked for JOANA with a @Source annotation, signalling an input statement (with a default security level of H). By Definition 14, (2) propagates to lines 39, 41, 5, and 9 which are also classified High. Likewise, (1) propagates to lines 19 and 22, which are thus High as well.

As information sent over network is visible to the attacker, calls to the method sendMessage (line 57f) are marked as a low @Sink, signalling an output statement (with a default security level of L). JOANA was started in “Giffhorn” mode, and – analysing the “ideal variant” – immediately guarantees that there are no explicit or implicit leaks. However the example contains two potential probabilistic leaks, which are both discovered by JOANA using Giffhorn’s criterion; one is later uncovered by RLSOD to be a false alarm.

To understand the first leak in detail, remember that this e-voting code spawns new threads in a loop. This will cause low-nondeterminism because the running times for the individual threads may vary and thus their relative execution order depends on scheduling. This low-nondeterminism is (context-sensitively) reachable from the high private-key initialization in line 39, hence criterion $2^{'} / 3^{'}$ will cause an alarm. Technically, we have $MHP (57, 57) \land ucl (57) = L$ ; that is, line 57 is low-nondeterministic with itself (because the same thread is spawned several times). Furthermore, $START \to_{CFG}^{*} 39 \to_{CFG}^{*} 57 \land ucl (39) = H$ . Thus criterion 3′ is violated: Giffhorn’s criterion (as well as classical LSOD) thinks there is a probabilistic leak.

Now let us apply RLSOD to this leak. The common dynamic ancestor for all the low-nondeterministic message sends in line 57 is located just before the loop header: $11 = cda (57, 57)$ .12

¹²

Note that we indeed need $cda$ instead of $cdom$ here, such that the static $cda$ lies before all dynamically possible spawns. JOANA handles such situations correctly, as well as handling interprocedural, context-sensitive dynamic ancestors.

Now it turns out that the initialisation of private keys lies before this common dynamic ancestor: lines 30, 39, 41, 5, 8, and 9 context-sensitively dominate line 11, and cannot happen parallel to it. Thus by RLSOD criterion

3^{″}

, this potential leak is uncovered to be a false alarm: the private key initialisation is in fact secure!

The second potential probabilistic leak comes from the potential high influence by secret_bit in line 19 to the low-nondeterministic message sends in line 63. Technically, we have the PDG High-chain $2 \to 19 \to 21 \to 53 \to 57$ , but $57$ is manually classified Low. However this second leak candidate is not eliminated by RLSOD, and indeed is a probabilistic leak: since the encrypt run time may depend on the message, the scheduler will statistically generate a specific “average” order of message send executions (remember the scheduler must be probabilistic). An attacker can thus watch this execution order, and deduce information about the secret messages. Technically, this subtle leak is discovered by RLSOD because the high operation which accesses the secret bit lies behind the common dynamic ancestor, but before the low-nondeterminism: $11 = cda (57, 57) \to_{CFG}^{*} 19 \to_{CFG}^{*} 57$ .

JOANA must and will report this probabilistic leak. The engineer might however decide that the leak is not dangerous. If the engineer can guarantee that the encrypt run time does not depend on msg, the leak may be ignored.

JOANA detects both potential probabilistic leaks in about 5 seconds on a standard PC (including PDG construction). A JOANA screenshot showing the analysis of the e-voting source code is given in Fig. 10; more details on the JOANA GUI can be found in [11]. After JOANA is set to RLSOD, one of the leaks disappears as described above. We consider the e-voting program a rather spectacular example how RLSOD improves precision. Note however that a systematic evaluation of RLSOD precision has not yet been tackled, as it is difficult to find realistic example programs with probabilistic leaks.

8. Evaluation

Table 1
PDG construction times (in milliseconds) for benchmark programs

#BC Instr. PDG time PDG time O-S

wallet 116 504 924

clientserver 601 204 298

battleship 937 408 1,078

corporatecard 1,186 427 821

safeappplet 1,295 376 1,332

hybrid 1,479 454 729

cloudstorage 1,972 563 1,030

j2mesafe 5,519 3,937 –

purse 10,807 6,004 13,165

barcode 11,406 1,307 –

onetimepass 13,034 48,729 –

bexplore 14,041 21,538 –

keepass 16,427 9,495 –

freecs 49,396 1,301,072 –

hsqldb 126,860 4,129,274 –

	#BC Instr.	PDG time	PDG time O-S
wallet	116	504	924
clientserver	601	204	298
battleship	937	408	1,078
corporatecard	1,186	427	821
safeappplet	1,295	376	1,332
hybrid	1,479	454	729
cloudstorage	1,972	563	1,030
j2mesafe	5,519	3,937	–
purse	10,807	6,004	13,165
barcode	11,406	1,307	–
onetimepass	13,034	48,729	–
bexplore	14,041	21,538	–
keepass	16,427	9,495	–
freecs	49,396	1,301,072	–
hsqldb	126,860	4,129,274	–

Table 1 presents PDG construction times for various programs. These times are taken from a recent JOANA scalability study provided by J. Graf in [9]. All measurements took place on a machine with a Core i7 processor, 32 GB RAM, with Java 8 64-Bit. For the 15 benchmark programs, program size in byte code instructions is given (without library functions), as well as PDG construction time in milliseconds. “PDG time O-S” is PDG construction time with object-sensitive points-to analysis; this variant is more expensive but much more precise. The largest program is “hsqldb” with 126860 byte code instructions, which corresponds to about 65kLOC source code.

[9] provides additional data on PDG size, summary edges, impact of points-to analysis details, and more. RLSOD time is not included in the PDG construction times. One observes that runtimes are strongly nonlinear, but moderate (1–2 hours/50kLOC). Memory is the limiting factor (7 of the programs cannot be analysed using object-sensitive points-to with 32 GB). Note that JOANA offers many analysis options, in particular choices for MHP and points-to precision [11].

Table 2 shows the runtimes of LSOD, Giffhorn’s criterion and RLSOD for a subset of the programs in Table 1, “BarrierBench” from the Java Grande Benchmark and the e-voting program from Section 7; on the same machine configuration as above. PDG construction time is not included. PDGs were built with object graphs and instance-based points-to precision (cmp. [9]). For each $n = 1, 5, 10$ we selected n sources and n sinks randomly from the PDG nodes. For each program, criterion and n we performed 10 measurements. The table shows the average runtime in milliseconds. For the top four programs, we used a more precise and more expensive MHP analysis. Since it does not scale for the last two programs, we used a simple MHP analysis there. Note that this choice only affects precision, not soundness. For the small programs, all (R)LSOD times are less than 100 msec; for the largest program (R)LSOD times are below 2 min. Interestingly, for the largest program and $n > 1$ , “Giffhorn” is a little faster than LSOD, and RLSOD is 4 times faster. The reason is that both the LSOD and Giffhorn implementations use multiple backward slices according to Definition 12 resp. conditions $2^{'} / 3^{'}$ , while RLSOD is based on Definition 14 and needs no backward slices. This also explains why RLSOD does not really depend on n.

Table 2

Performance of LSOD, Giffhorn’s criterion and RLSOD with different numbers of sources/sinks (in milliseconds)

Program	#BC Instr.	LSOD			Giffhorn			RLSOD

		1	5	10	1	5	10	1	5	10
barrierbench	416	38	31	32	38	31	34	93	63	55
battleship	937	11	17	24	13	17	21	25	17	14
evoting	1,106	13	9	11	13	10	12	37	23	21
barcode	11,406	20	21	25	25	23	28	58	37	36
freecs	49,396	23,945	34,502	50,427	23,622	32,072	45,160	54,280	53,042	56,111
hsqldb	126,860	16,427	70,740	133,777	17,288	62,581	119,767	31,885	30,333	30,333

9. Related work

Zdancewic’s work [41] was the starting point for us, once Giffhorn discovered that the Zdancewic LSOD criteria can naturally be checked using PDGs. Zdancewic uses an interesting definition of low-equivalent traces: low-equivalence is not demanded for traces, but only for every subtrace for every low variable (“location traces”). This renders more traces low-equivalent and thus increases precision. But location traces act contrary to flow-sensitivity (relative order of variable accesses is lost), and according to our experience flow-sensitivity is essential.

While strict LSOD guarantees probabilistic noninterference for any scheduler, it is too strict for multi-threaded programs. RLSOD considerably improves the precision of LSOD, while giving up on full scheduler-independence (by restricting RLSOD to truly probabilistic schedulers). This same tradeoff has been proposed by earlier authors. Smith [35] improves on PN based on probabilistic bisimulation, where the latter forbids the execution time of any thread to depend on secret input. Just as in our work, a probabilistic scheduler is assumed; the probability of any execution step is given by a markov chain. A secure program requires that the probability to go from one low-equivalence class of states A to another (after possibly remaining, or stuttering in A for some time) is independent of the specific state $a \in A$ . This approach is called weak probabilistic bisimulation, and allows the execution time of threads to depend on secret input, as long as it is not made observable by writing to public variables. The authors present a static check in form of a type system, and discuss an extension for thread creation. If the execution time up to the current point depends on secret input, their criterion allows to spawn new threads only if they do not alter public variables. In comparison, our $c cda (n, m)$ based check does allow two public operations to happen in parallel in newly spawned threads, even if the execution time up to c (i.e.: a point at which at most one of the two threads involved existed) depends on secret input.

Approaches for PN based on type systems benefit from compositionality, a good study of which is given in [29]. Again, a probabilistic scheduler is assumed. Scheduler-independent approaches can be found in, e.g., [25,30]. The authors each identify a natural class of “robust” resp. “noninterfering” schedulers, which include uniform and round-robin schedulers. They show that programs which satisfy specific possibilistic notions of bisimilarity (“FSI-security” resp. “possibilistically noninterferent”) remain probabilistically secure when run under such schedulers. Since programs like Fig. 7 left are not probabilistically secure under a round-robin scheduler, their possibilistic notion of bisimilarity require “lock-step” execution at least for threads with low-observable behaviour. Compared to RLSOD this is more restrictive for programs, but less restrictive on scheduling.

A completely different approach to noninterference and PN is the use of program logics and verification. For example the KeY system [1] has been used to verify noninterference and other nonfunctional security properties; KeY was also applied to Küster’s e-voting system (cmp. chapter 7) [20]. Recently, relational program logics have been proposed which allow to express probabilistic properties of programs, including PN [3]. Such verification systems are very powerful and allow to verify properties beyond PN, but are never automatic such as RLSOD and JOANA. We are thus exploring the combination KeY + JOANA: JOANA can, due to a programming interface, export relevant analysis results, such as points-to relations, PDG reachability, PN guarantees, or leak localizations. KeY can use JOANA as a black box to considerably simplify security verification [12].

9.1. Detailed comparison with type-system-based analysis for FSI

Fig. 11.

Security Type System FSI [25].

Fig. 12.

FSI-Variants of Fig. 2, left, and of Fig. 7, left.

In Fig. 11, the type system for FSI-Security from [25] for a concurrent $WHILE$ language is repeated verbatim. FSI-Security implies $S$ -Security for all robust schedulers $S$ . Both these notions require an explicit global classification $dom$ of all variables, implying a classification for all expressions. The attacker is assumed to observe the initial and final values of low variables. Intuitively, a judgment $⊢ com : (ass, stp)$ means that $com$ is secure, with a running time influenced only by input of level $stp$ or lower, and observable effects (specifically: writes to variables) only of level $ass$ or higher.

The observational model in our work differs slightly: we assume the attacker to observe not the final value of low variables, but instead the values of variables at observable nodes, i.e.: nodes n with $ucl (n) = L$ . The two FSI programs corresponding to Fig. 2, left, and to Fig. 7, left are shown in Fig. 12, assuming $dom (Hin) = H, dom (Lout) = L$ .

Comparing RLSOD with FSI, consider the example in Fig. 12, left; which contains simple explicit and implicit leaks. RLSOD requires $cl (2) ⊑ cl (3) ⊑ cl (4)$ via the PDG path $2 \to 3 \to 4$ and requirement (a) in Definition 14, violating $H = ucl (2) = cl (2)$ , $L = ucl (4) ⊒ cl (4)$ (via requirement (c)); and the leak is exposed. Likewise, FSI requires $\begin{array}{l} dom (H) \overset{IF}{⊑} {ass}_{4}, violating H = dom (Hin) \overset{ASS}{⊑} dom (H), {ass}_{4} \overset{ASS, SUB}{⊑} dom (Lout) = L . \end{array}$ where ${com}_{i}$ is the statement at line i, and ${ass}_{i}, {stp}_{i}$ are the security levels in judgements $⊢ {com}_{i} : ({ass}_{i}, {stp}_{i})$ appearing in candidate derivation trees for the hypothesis $⊢ main : (ass, stp)$ . ${ass}_{k_{1}, \dots, k_{n}}$ , ${stp}_{k_{1}, \dots, k_{n}}$ are the security levels in judgements $⊢ {com}_{k_{1}, \dots, k_{n}} : ({ass}_{k_{1}, \dots, k_{n}}, {stp}_{k_{1}, \dots, k_{n}})$ for sequentially composed statements ${com}_{k_{1}, \dots, k_{n}} = (\dots ({com}_{k_{1}}; {com}_{k_{2}}); \dots {com}_{k_{n}})$ . Thus FSI discovers the same leak.

But FSI does not use the “dominator trick”. To see the effect, consider Fig. 12, right, which is secure w.r.t. a probabilistic scheduler, but FSI-insecure as follows: Aside from $H = dom (Hin) \overset{ASS}{⊑} dom (H)$ , we have $dom (H) \overset{IF}{⊑} {stp}_{2}$ , and also ${ass}_{5} \overset{ASS, SUB}{⊑} dom (Lout) = L$ . But attempting to derive a type for ${com}_{2, 4} = {com}_{2}; spawn [Lout : = Lout + " 17 ", \dots]$ via rule $SEQ$ requires ${stp}_{2} ⊑ {ass}_{4} \overset{SPAWN, SUB}{⊑} {ass}_{5}$ . The latter is a contradiction, thus FSI is violated.

RLSOD, however, correctly classifies the corresponding program from Fig. 7 left secure w.r.t. a probabilistic scheduler, as witnessed by the classification

Specifically, this classification does not violate requirement (b) of Definition 14, since $4 cda (5, 9)$ , but for all nodes $c^{'}$ on paths $4 \to 5, 4 \to 9$ we have $cl (c^{'}) = L$ . The dominator avoids a false alarm.

9.2. Comparison with syntactic criteria for resumption based noninterference

In [29], the authors assume a uniform scheduler, and describe a lattice of security properties (Fig. 13) ordered by implication, the weakest of which being 01-bisimilarity ( $\approx_{01}$ ). 01-bisimilarity is not compositional w.r.t. every syntactic construct of the source language considered. Nevertheless, the authors derive syntactic criteria that, whenever a given construct is not compositional w.r.t. the security property, defer to a stronger property which is compositional w.r.t. this construct.

Instead of $spawn [{com}_{0}, \dots, {com}_{k - 1}]$ or $fork$ , their language assumes a parallel composition statement $par [{com}_{0}, \dots, {com}_{k - 1}]$ . For a direct comparison, the program corresponding to Fig. 7 left is shown in Fig. 13. Each line is annotated with its strongest security properties holding. For example, read(H) is self-isomorphic ( $siso$ ): if started in low-indistinguishable states (and: given low-indistinguishable inputs), executions take the same branches with the same probabilities. It also is discreet ( $discr$ ): during the computation, the states stay low-indistinguishable from the initial state, and no low output is made. Using the syntactic criteria, we can conclude that read(H); if (H) {skip} is $discr$ (but not: $siso$ ). Unfortunately, the syntactic criteria of [29] do not allow us to conclude that sequential composition of a $discr$ and a $siso$ command (like the $par []$ -Statement) are $\approx_{01}$ , and hence produce a false alarm.

Fig. 13.

Resumption Based Security: Security Properties [29], and the Program corresponding to Figure 7, left.

9.3. Compositionality

Fig. 14.

Typical problems of compositional analyses.

Compositionality is a useful property, but can be achieved only at the price of either losing precision, or losing automatic analysis. Let us explain this in more detail.

Typically, type systems are compositional because they use static classification. For example, in Fig. 14 left, the first two lines alone are secure, as well as the last two. A compositional IFC with static classification will discover the simple leak in this code piece once both fragments are composed, because there are conflicting (static) classifications for T. Unfortunately, static classification is very unprecise. In particular, it is not flow-sensitive and will produce a false alarm for the program in Fig. 14 middle: since the high value is overwritten in line 4, the program always outputs 0 and is secure. Note that there might be many more statements between the two writes to T (cmp. [14]).

For concurrent programs, compositionality is even more problematic. Consider the program in Fig. 14 right: it is sequential and always prints 0, and therefore fulfills PN for every scheduler. If this program is composed in parallel with the secure program print(1);, it however contains a probabilistic leak similar to Fig. 2 right. Therefore, a typical compositional analysis (e.g. [25,35]) will reject the isolated code piece in Fig. 14 right, because it conservatively assumes that it can be composed with arbitrary (unknown) threads. RLSOD in contrast is a whole-program analysis, and uses MHP information to exactly infer possible concurrency (cmp. Section 4.1). Thus it considers the isolated code piece secure – which it is. It should be noted that compromises between the two extreme positions “fully compositional” vs. “whole-program” have been attempted, e.g. [23,24].

Program logics as discussed above are also compositional, typically because they use Hoare triples. In contrast to type systems and RLSOD, program logics for PN can be made arbitrarily precise. But the price is high: program logics and verification are never fully automatic, and in practice require high manual effort for specification and verification. We thus believe that in practice, RLSOD is a good compromise: it is fully automatic yet very precise, and compositionality can be simulated by stubs.

10. Conclusion

We described a new algorithm for probabilistic noninterference, named RLSOD, which allows secure low-nondeterminism, while basically maintaining the low-deterministic security (LSOD) approach. RLSOD benefits from flow- and context-sensitive program analysis methods such as PDGs, points-to analysis, and dominators in multi-threaded programs. It turns out that RLSOD heavily reduces false alarms compared to LSOD, while a full soundness proof could be achieved. An Isabelle formalization of the soundness proof has already begun.

RLSOD is integrated into the JOANA IFC tool. JOANA can handle full Java with arbitrary threads, while being sound and scaling to 200k LOC. The decision to base PN in JOANA on low-deterministic security was made at a time when mainstream IFC research considered LSOD too restrictive. In the current paper we have shown that flow- and context-sensitive analysis, together with new techniques for allowing secure low-nondeterminism, has rehabilitated the LSOD idea.

References

Ahrendt,

Beckert,

Bubel,

Hähnle,

P.H.

Schmitt and

Ulbrich (eds), Deductive Software Verification – the Key Book – from Theory to Practice, Lecture Notes in Computer Science, Vol. 10001, Springer, 2016.

Askarov,

Hunt,

Sabelfeld and

Sands, Termination-insensitive noninterference leaks more than just a bit, in: Proc. ESORICS, LNCS, Vol. 5283, 2008, pp. 333–348.

Barthe,

Fournet,

Grégoire,

Strub,

Swamy and

S.Z.

Béguelin, Probabilistic relational verification for cryptographic implementations, in: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, Ca, Usa, January 20–21, 2014, 2014, pp. 193–206.

Breitner,

Graf,

Hecker,

Mohr and

Snelting, On improvements of low-deterministic security, in: Proc. Principles of Security and Trust (POST 2016), Lecture Notes in Computer Science, Vol. 9635, Springer Berlin Heidelberg, 2016, pp. 68–88. doi:10.1007/978-3-662-49635-0_4.

De Sutter,

Van Put and

De Bosschere, A practical interprocedural dominance algorithm, Acm Trans. Program. Lang. Syst. 29(4) (2007).

Giffhorn, Advanced chopping of sequential and concurrent programs, Software Quality Journal 19(2) (2011), 239–294. doi:10.1007/s11219-010-9114-7.

Giffhorn, Slicing of Concurrent Programs and its Application to Information Flow Control, PhD thesis, Karlsruher Institut für Technologie, Fakultät für Informatik, 2012.

Giffhorn and

Snelting, A new algorithm for low-deterministic security, International Journal of Information Security 14(3) (2015), 263–287. doi:10.1007/s10207-014-0257-6.

Graf, Information Flow Control with System Dependence Graphs — Improving Modularity, Scalability and Precision for Object Oriented Languages, PhD thesis, Karlsruher Institut für Technologie, Fakultät für Informatik, 2016.

10.

Graf,

Hecker,

Mohr and

Snelting, Checking applications using security APIs with JOANA, 2015, 8th International Workshop on Analysis of Security APIs.

11.

Graf,

Hecker,

Mohr and

Snelting, Tool demonstration: JOANA, in: Proc. Principles of Security and Trust (POST 2016), Lecture Notes in Computer Science, Vol. 9635, Springer Berlin Heidelberg, 2016, pp. 89–93. doi:10.1007/978-3-662-49635-0_5.

12.

Greiner,

Mohr and

Beckert, Modular verification of information flow security in component-based systems, in: Software Engineering and Formal Methods – 15th International Conference, SEFM 2017, Proceedings, Trento, Italy, September 4–8, 2017, 2017, pp. 300–315.

13.

Hammer, Experiences with PDG-based IFC, in: Proc. ESSoS’10,

Massacci,

Wallach and

Zannone, eds, LNCS, Vol. 5965, Springer-Verlag, 2010, pp. 44–60.

14.

Hammer and

Snelting, Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs, International Journal of Information Security 8(6) (2009), 399–422. doi:10.1007/s10207-009-0086-1.

15.

Horwitz,

Prins and

Reps, On the adequacy of program dependence graphs for representing programs, in: Proc. POPL ’88, ACM, New York, NY, USA, 1988, pp. 146–157. doi:10.1145/73560.73573.

16.

Huisman and

T.M.

Ngo, Scheduler-specific confidentiality for multi-threaded programs and its logic-based verification, in: Proc. Formal Verification of Object-Oriented Systems, 2011.

17.

Huisman,

Worah and

Sunesen, A temporal logic characterisation of observational determinism, in: Proc. 19th CSFW, IEEE, 2006, p. 3.

18.

Hunt and

Sands, On flow-sensitive security types, in: POPL ’06, ACM, 2006, pp. 79–90. doi:10.1145/1111037.1111045.

19.

Küsters,

Scapin,

Truderung and

Graf, Extending and applying a framework for the cryptographic verification of Java programs, in: Proc. POST 2014, LNCS 8424, Springer, 2014, pp. 220–239.

20.

Küsters,

Truderung,

Beckert,

Bruns,

Kirsten and

Mohr, A hybrid approach for proving noninterference of Java programs, in: IEEE 28th Computer Security Foundations Symposium, CSF 2015, Verona, Italy, 13–17 July, 2015, 2015, pp. 305–319.

21.

Küsters,

Truderung and

Graf, A framework for the cryptographic verification of Java-like programs, in: Computer Security Foundations Symposium (CSF), 2012 IEEE 25th, IEEE Computer Society, 2012.

22.

Li and

Verbrugge, A practical MHP information analysis for concurrent Java programs, in: Proc. LCPC’04, LNCS, Vol. 3602, Springer, 2004, pp. 194–208. doi:10.1007/11532378_15.

23.

Mantel,

Müller-Olm,

Perner and

Wenner, Using dynamic pushdown networks to automate a modular information-flow analysis, in: Pre-Proceedings of the 25th International Symposium on Logic Based Program Synthesis and Transformation (LOPSTR), 2015.

24.

Mantel,

Sands and

Sudbrock, Assumptions and guarantees for compositional noninterference, in: Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF), IEEE Computer Society, Cernay-la-Ville, France, 2011, pp. 218–232.

25.

Mantel and

Sudbrock, Flexible scheduler-independent security, in: Computer Security – ESORICS 2010,

Gritzalis,

Preneel and

Theoharidou, eds, Lecture Notes in Computer Science, Vol. 6345, Springer Berlin Heidelberg, 2010, pp. 116–133. ISBN 978-3-642-15496-6. doi:10.1007/978-3-642-15497-3_8.

26.

Mohr,

Graf and

Hecker, JoDroid: Adding Android support to a static information flow control tool, in: Gemeinsamer Tagungsband der Workshops der Tagung Software Engineering 2015, Dresden, Germany, 17.–18. März 2015, CEUR Workshop Proceedings, Vol. 1337, CEUR-WS.org, 2015, pp. 140–145.

27.

Naumovich and

G.S.

Avrunin, A conservative data flow algorithm for detecting all pairs of statements that may happen in parallel, in: Proceedings of the 6th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ACM, New York, NY, USA, 1998, pp. 24–34.

28.

T.M.

Ngo, Qualitative and quantitative information flow analysis for multi-threaded programs, PhD thesis, University of Enschede, 2014.

29.

Popescu,

Hölzl and

Nipkow, Formalizing probabilistic noninterference, in: Certified Programs and Proofs – Third International Conference, CPP 2013, Proceedings, Melbourne, VIC, Australia, December 11–13, 2013, 2013, pp. 259–275.

30.

Popescu,

Hölzl and

Nipkow, Noninterfering schedulers, in: Algebra and Coalgebra in Computer Science,

Heckel and

Milius, eds, Lecture Notes in Computer Science, Vol. 8089, Springer Berlin Heidelberg, 2013, pp. 236–252. doi:10.1007/978-3-642-40206-7_18.

31.

Reps,

Horwitz,

Sagiv and

Rosay, Speeding up slicing, in: Proc. FSE ’94, ACM, New York, NY, USA, 1994, pp. 11–20.

32.

A.W.

Roscoe,

Woodcock and

Wulf, Non-interference through determinism, in: ESORICS, LNCS, Vol. 875, 1994, pp. 33–53.

33.

Sabelfeld and

Myers, Language-based information-flow security, IEEE Journal on Selected Areas in Communications 21(1) (2003), 5–19. doi:10.1109/JSAC.2002.806121.

34.

Sabelfeld and

Sands, Probabilistic noninterference for multi-threaded programs, in: Proceedings of the 13th IEEE Computer Security Foundations Workshop, CSFW ’00 Cambridge, England, UK, July 3–5, 2000, 2000, pp. 200–214.

35.

Smith, Improved typings for probabilistic noninterference in a multi-threaded language, J. Comput. Secur. 14(6) (2006), 591–623. doi:10.3233/JCS-2006-14605.

36.

Smith and

Volpano, Secure information flow in a multi-threaded imperative language, in: Proc. POPL ’98, ACM, 1998, pp. 355–364. doi:10.1145/268946.268975.

37.

Snelting, Combining slicing and constraint solving for validation of measurement software, in: SAS ’96: Proceedings of the Third International Symposium on Static Analysis, Springer-Verlag, London, UK, 1996, pp. 332–348.

38.

Snelting,

Giffhorn,

Graf,

Hammer,

Hecker,

Mohr and

Wasserrab, Checking probabilistic noninterference using JOANA, It – Information Technology 56 (2014), 280–287. doi:10.1515/itit-2014-1051.

39.

Snelting,

Robschink and

Krinke, Efficient path conditions in dependence graphs for software safety analysis, ACM Trans. Softw. Eng. Methodol. 15(4) (2006), 410–457. doi:10.1145/1178625.1178628.

40.

Wasserrab,

Lohner and

Snelting, On PDG-based noninterference and its modular proof, in: Proc. PLAS ’09, ACM, 2009.

41.

Zdancewic and

A.C.

Myers, Observational determinism for concurrent program security, in: Proc. CSFW, IEEE, 2003, pp. 29–43.

Low-deterministic security for low-nondeterministic programs 1

Abstract

Keywords

1. Introduction

2 see joana.ipd.kit.edu. JOANA can analyse full Java with arbitrary threads, and was applied in various projects [10,19,21,26]. Usage of JOANA is described in [11].

2.1. Language assumptions

5 JOANA can also handle the Android Life cycle, see [26].

6 Note that this is less restrictive than a uniform scheduler, where that relative probability is always 1. A truly probabilistic scheduler on the other hand can assign priorities to statements, e.g. increase the priorities for all statements of a specific (syntactic) thread.

2.4. The role of flow- and context-sensitivity

3. Noninterference and LSOD

Definition 1 (Sequential noninterference).

3.2. Probabilistic noninterference

Definition 7 (Low-security observational determinism).

4.1. PDGs for IFC

5.1. Improving conditions 2 ′ and 3 ′

Definition 13 (Common dynamic ancestor).

9 Note that in programs with procedures and threads, immediate dynamic ancestors may not be unique due to context-sensitivity [5].

10 This formulation is used by JOANA; it also has the advantage that RLSOD can be used for an arbitrary security lattice. Note that our current soundness proof works only with the L / H lattice.

11 Note that due to this construction, at the encryption site there is no flow from the plaintext or key to the encrypted message.

9.1. Detailed comparison with type-system-based analysis for FSI

References

²
see joana.ipd.kit.edu. JOANA can analyse full Java with arbitrary threads, and was applied in various projects [10,19,21,26]. Usage of JOANA is described in [11].

⁵
JOANA can also handle the Android Life cycle, see [26].

⁶
Note that this is less restrictive than a uniform scheduler, where that relative probability is always 1. A truly probabilistic scheduler on the other hand can assign priorities to statements, e.g. increase the priorities for all statements of a specific (syntactic) thread.

5.1. Improving conditions $2^{'}$ and $3^{'}$

⁹
Note that in programs with procedures and threads, immediate dynamic ancestors may not be unique due to context-sensitivity [5].

¹⁰
This formulation is used by JOANA; it also has the advantage that RLSOD can be used for an arbitrary security lattice. Note that our current soundness proof works only with the $L / H$ lattice.

¹¹
Note that due to this construction, at the encryption site there is no flow from the plaintext or key to the encrypted message.