Secure multi-execution: Fine-grained,declassification-aware,and transparent

Abstract

Recently, much progress has been made on achieving information-flow security via secure multi-execution. Secure multi-execution ( $SME$ ) is an elegant way to enforce security by executing a given program multiple times, once for each security level, while carefully dispatching inputs and ensuring that an execution at a given level is responsible for producing outputs for information sinks at that level. Secure multi-execution guarantees noninterference, in the sense of no dependencies from secret inputs to public outputs, and transparency, in the sense that if a program is secure then its secure multi-execution does not disable any of its original behavior.

This paper pushes the boundary of what can be achieved with secure multi-execution. First, we lift the assumption from the original secure multi-execution work on the totality of the input environment (that there is always assumed to be input) and on cooperative scheduling. Second, we generalize secure multi-execution to distinguish between security levels of presence and content of messages. Third, we introduce a declassification model for secure multi-execution that allows expressing what information can be released and where it can be released. Fourth, we establish a full transparency result showing how secure multi-execution can preserve the original order of messages in secure programs. We demonstrate that full transparency is a key enabler for discovering attacks with secure multi-execution.

Keywords

Information flow dynamic enforcement secure multi-execution noninterference transparency

1. Introduction

As modern attacks are becoming more sophisticated, there is an increasing demand for protection measures more advanced than those offered by standard security practice. We demonstrate the problem with a motivating scenario from web application security, but note that the problem is of a general nature.

Motivation. In the context of the web, third-party script inclusion is pervasive. It drives the integration of advertisement and statistics services. As an indicative example, barackobama.com at the time of the 2012 US presidential campaign contained 76 different third-party tracking scripts [49]. The tracking was used for targeted political advertisement. Script inclusions extend the trusted computing base to the Internet domains of included scripts. This creates dangerous scenarios of trust-abuse. This can be done either by direct attacks from the included scripts or, perhaps more dangerously, by indirect attacks when a popular service is compromised and its scripts are replaced by the attacker. A recent empirical study [35] of script inclusion reports high reliance on third-party scripts. It outlines new attack vectors showing how easy it is to get code running in thousands of browsers simply by acquiring some stale or misspelled domains. A representative real-life example is the defacement of the Reuters site in June 2014 [50], attributed to “Syrian Electronic Army”, which compromised a third-party widget (Taboola). This shows that even established content delivery networks risk being compromised, and these risks immediately extend to all web sites that include scripts from such networks.

Access control mechanisms are of limited use because third-party scripts require access to sensitive information for their proper functionality. This is particularly important for statistics and context-aware advertisement services on the web. Similar scenarios arise in the setting of cloud computing where sharing the resources is desirable but without compromising confidentiality and integrity. This motivates the need for fine-grained information-flow control.

From static to dynamic information-flow control. Tracking information flow in programs is a popular area of research. Static analysis techniques have been extensively explored, leading to tools like Jif [34], FlowCaml [48], and SparkAda Examiner [10] that enhance compilers for Java, Caml, and Ada, respectively. Recently, dynamic monitoring techniques have received increased attention (cf. [5,6,23,27,28,45,47]), driven by the demand to analyze dynamic programming languages like JavaScript. While static analysis either accepts or rejects a given program before it is run, dynamic monitors perform checks at run time. There are known fundamental tensions [42] between static and dynamic analyses, implying that none is superior to the other. Although dynamic analysis might seem intuitively more permissive, it has to conservatively treat the paths that are not taken by the current execution.

Secure multi-execution ( $SME$ ). Recently, there has been much progress on $SME$ [7,11,12,18,20,24,25], a runtime enforcement mechanism for information flow. In contrast to the monitoring techniques, the goal is not to prevent insecurities but to “repair” them on the fly. This approach is secure by design: security is achieved by separation of computations at different security levels. The original program is run as many times as there are security levels, where outputs at a given security level are only allowed if the security level of the program is matched with the security level of the output channel. The handling of inputs is slightly more involved because inputs from less restrictive security levels are allowed to be used in computations at more restrictive levels. Secure multi-execution propagates inputs, once received, to the runs of the program that are responsible for the computation of outputs at more restrictive levels.

Fig. 1.

Original execution.

Typically, security levels are drawn from a lattice with the intuition that information from an input source at level ℓ may flow to an output sink at level $ℓ^{'}$ only if $ℓ ⊑ ℓ^{'}$ [19]. For simplicity, we will often use the two-level lattice with a secret (high) level and a public (low) level of confidentiality. Figure 1 shows program P with a pair of input sources, labeled high $H$ and low $L$ , and a similarly-labeled pair of sinks. The baseline policy of noninterference [22] demands that low outputs do not depend on high inputs.

Fig. 2.

$SME$ .

Figure 2 shows how secure multi-execution achieves noninterference. Program P is run twice, as $P_{H}$ at high and as $P_{L}$ at low levels. The high input is fed into the high run. The low input is fed into both the low and high run. Dummy default values are used whenever the low run asks for high input. High output is produced by the high run, and the low output is produced by the low run, while low output of the high run and high output of the low run are ignored. It is clear from the diagram that noninterference is enforced because the low run, the only producer of low output, never gets access to high input.

In contrast to the traditional dynamic analysis, there is no concern about executions not taken because the control flow of the low run cannot possibly be affected by high input. Further, secure multi-execution provides transparency, in the sense that if a program is secure then its secure multi-execution does not disable any of its original behavior.

Contributions. While secure multi-execution gains increased popularity, there are open challenges that need to be addressed before it can be applied widely. We overview the pros and cons of secure multi-executions compared to traditional information-flow control and, among other findings, point out that secure multi-execution (i) lacks support for fine-grained security levels for communication channels, (ii) relies on restrictive scheduling, (iii) lacks support for declassification, (iv) may reorder messages w.r.t. the original execution, and (v) lacks support for detecting attacks.

We push the boundary of what can be achieved with secure multi-execution. First, we lift the assumption from the original secure multi-execution work on the totality of the input environment (that there is always assumed to be input) and on cooperative scheduling. Second, we generalize secure multi-execution to distinguish between security levels of presence and content of messages. Third, we introduce a declassification model for secure multi-execution that allows expressing what information can be released and where it can be released. Fourth, we establish full transparency showing how secure multi-execution can preserve the original order of messages in secure programs by barrier synchronization. This enables the use of secure multi-execution to discover counterexamples to noninterference, i.e. attacks, on run time.

This journal paper extends and improves an earlier conference version [39]. The present journal version presents a complete overhaul of Section 5 on declassification in $SME$ , resulting in new results and substantial improvements. Notably, we give a critical evaluation, justification and motivation of our model of declassification. We clarify full release, our model of declassification to confine release to data of specified levels of sensitivity. This model was introduced in the conference version, and we now generalize it and develop theoretical results for it. Further, we show that our declassification model provides additional assurance: drawing on the knowledge-based gradual release [2,3] model, we demonstrate that information release may only take place at declassification points and nowhere else during the execution. We develop theoretical results for it, including a knowledge-based noninterference which we show is equivalent to the noninterference notion we use throughout the paper. We prove soundness for this model, establishing that our declassifying $SME$ only leaks information through declassification actions. This is the first such result for $SME$ . We generalize the declassification semantics to support multiple channels of declassification, enabling modeling of the semantics of a declassified value in the name of its declassification channel. For the remainder of the paper, we have improved readability by including corrections to the original paper and by revising notation and formatting. We have updated the related work section with work on $SME$ that has appeared since our original publication. Finally, we present the full proofs for all of our technical results.

2. Pros and cons of secure multi-execution

We overview the pros and cons of secure multi-execution with respect to direct information-flow enforcement. The overview has two goals: provide a general basis to decide which enforcement mechanism to pick in a particular case and identify the most pressing shortcomings, subject to improvements by this paper. For a more detailed account of the state of the art, we refer the reader to the related work section. We start by listing what we view as the pros of secure multi-execution.

Noninterference by design. A significant advantage of secure multi-execution is that it enforces noninterference in a straightforward manner by a simple access-control discipline: computation responsible for output at a given level never gets access to information at more restrictive or incomparable levels. This provides noninterference guarantees.

Language-independence. A major benefit is that secure multi-execution can be enforced in a blackbox, language-independent, fashion. The enforcement only concerns input and output operations allowing the rest of the language to be arbitrarily complex. This is particularly useful for dynamic languages like JavaScript that are hard to analyze.

Transparency for secure programs. If the original program is secure, there are transparency guarantees that limit ways in which semantics can be modified. The original work on secure multi-execution shows per-channel transparency (or precision in the terminology of Devriese and Piessens [20]). This means that if the original program is secure then, from the viewpoint of each channel, the sequence of I/O events in a given run of a program is the same in the original run and in the multi-executed run.

Transparency at top level. In addition, we note another transparency property which holds when e.g. the willingness of a program to consume low input is independent of high information: the high run in the secure multi-execution of a program performs the same inputs and outputs as the program does without being securely multi-executed. This property can be seen from Figs 1 and 2. Clearly, the original run of the program in Fig. 1 and the high run of the multi-executed program in Fig. 2 get the same inputs. Hence, the high output behaviors are the same no matter whether the original program is secure or not.

We now turn to the cons of secure multi-execution.

Coarse-grained labels for channels. In work on secure multi-execution so far, communication channels are provided with a single security label. This is often too coarse-grained: for example, the presence of a message might be public but the content is secret. This granularity might be useful for statistics services that might be counting different types of events without revealing their content. For example, Google Analytics is routinely used for various types of counting: how many clicks on the page, how many times a video is played, and how many visitors have viewed a page.

Devriese and Piessens [20] assume total input environments: that the input is always present. This does not allow modeling scenarios where the presence of secret input is secret (for example, whether or not the user visits a health web site). Bielova et al. [12] allow non-total environments but at the price of ignoring information leaks through termination behavior (targeting termination-insensitive noninterference [53]). This implies that the leaks as in the example with the health site are still ignored because the one bit of information of whether the user has visited a heath web site is allowed to be leaked.

This motivates the need for fine-grained secure multi-execution. We remove the assumption on total input environments and introduce fine-grained labels for communication channels, where the levels of presence and content of messages are distinguished.

Restrictive scheduling. With the exception of work by Kashyap et al. [25], secure multi-execution heavily relies on the low-priority scheduler that lets low computation run until completion before the high run gets a chance to run. The low-priority scheduler is both at the heart of the soundness results by Devriese and Piessens [20] and at the heart of FlowFox [18], an extension of Firefox to enforce secure information flow in JavaScript. The security theorem in the abstract setting of secure multi-execution [20] takes advantage of the low-priority scheduler and establishes timing-sensitive security. This is intuitive because the last access of low data occurs before any high data is accessed. Whenever the timing behavior is affected by secrets, there is no possibility for the attacker to inspect the difference.

However, the situation is different in the presence of event handlers, reactive program snippets that are triggered upon occurrence of events. The low-priority scheduler is fundamentally problematic because it is not possible to extend the low-priority discipline over multiple events – simply because it is not possible to run the low handlers that have not yet been triggered. As a compromise, FlowFox [18] multi-executes JavaScript with the low-priority scheduler on a per-event basis. However, as illustrated by a leak in Appendix A, this strategy is at the cost of timing-sensitive security. All we need to do is to set a low handler to execute after the high run of the main code has finished. Then the low handler can leak via the computation time taken by the high run. This is indeed what happens in the example program. Using setTimeout, the main code creates a new handler whose job is to report the time difference since the start of the program. Then the main code branches on a secret and performs a short or long computation depending on the secret. Upon the exit of the main thread, the handler is triggered to report the time difference to the attacker.

This motivates the need for flexible scheduling strategies and the need for (fair) interleaving of the runs at different levels, as pursued in this paper.

Declassification. Declassification is challenging because secure multi-execution is based on separating information at different security levels. Feeding secret information to a public run might introduce unintended leaks. Coming back to the example of tracking and statistics, we might want to track the popularity of items in a shopping cart or track various average values for transactions.

This motivates the need for declassification in secure multi-execution. The event of declassification should not leak information about the context (branching on a secret and declassifying in the body would leak the Boolean value of the secret). It turns out that the support for fine-grained communication channels provides us with a natural treatment of declassification. Indeed, declassification is about communicating a secret value from the high run to the low run, but without leaking through the presence of the communication event. Exactly this is provided by channels with high content and low presence! Hence, a declassification event corresponds to output on a high-content low-presence channel (in the view of the high run), and to input on a low-content low-presence channel (in the view of the low run).

Order of events modified. The transparency guarantees of secure multi-execution are per channel, allowing the order of events to be modified across different channels. This leads to unexpected results in an interactive setting.

This motivates the need for stronger transparency, where the behavior of secure programs is unmodified across the different levels. We show how to achieve this by careful scheduling of the runs at the different levels.

Silent failure. The behavior of secure and insecure programs is silently modified. As mentioned above, there are cases when the run at the top security level is immune to such modifications as it never gets dummy values. However, the behavior at less restrictive levels might be modified, leading to loss of important functionality. This directly connects to undiscovered attacks, addressed below.

Undiscovered attacks. Related to the silent failure point above, secure multi-execution “repairs” problematic executions on the fly, with no means to identify if there were any attempted attacks and what caused such attacks.

This motivates an enhancement of secure multi-execution that allows for detecting attacks. Intuitively, we introduce barrier synchronization of the runs at the different security levels and track the consistency of the values they produce. In the two-level lattice, we check if the low output produced by the low run matches the value produced by the high run (which is the same as the low output of the original program). If they are inconsistent, we have found an attack. Full transparency is the key for this result because it guarantees that secure programs must have exactly the same I/O behavior as their securely multi-executed versions.

Nondeterminism. While not required for soundness, the executions at different levels need to make the same nondeterministic choices for secure multi-execution to be transparent. Although this has not been explicitly handled in previous work, a natural possibility is to assign security levels to the source of nondeterminism [36] and propagate it to the relevant executions in a fashion similar to propagating inputs.

Dummy values. Dummy values are fed into executions that are not authorized to have access to sensitive input. An unfortunate choice of values might lead to the program crashing. Defensive programming is then needed to ensure that programs are stable under variation of allowed input.

Performance. Executing the program several times implies obvious performance overhead. At the same time, secure multi-execution benefits from multicore architectures, in particular when the number of executions is less than the number of cores [20]. Also, as we discuss in Section 7, optimizations are possible for simulating multiple executions by computing on enriched values [7].

3. Framework

We lay the foundation for our technical contributions outlined in the Introduction by presenting a framework for information-flow security of interactive programs [15,17,36–38].

3.1. Input–output labeled transition systems

Our model of computation is a labeled transition system ( $LTS$ ). An $LTS$ is a triple $(S, L, \overset{}{\to})$ , where S is a set (of states), L is a set (of labels), and $\overset{}{\to} \subseteq S \times L \times S$ (a labeled transition relation). Computation occurs in discrete steps (transitions), each taking a (unspecified) unit of time. We write $s \overset{l}{\to} s^{'}$ iff $(s, l, s^{'}) \in \overset{}{\to}$ , and $s \overset{l}{\to}$ iff $s \overset{l}{\to} s^{'}$ for some $s^{'}$ .

The systems we consider in this paper interact with their environment through channel-based message-passing. Such systems have three kinds of effects: (message-)input, output, and silence. The two latter effects are “productions”, referred to as output o, and the first effect is a “consumption”, referred to as input i. Collectively, these are actions a. $\begin{matrix} a : : = i ∣ o i : : = c ? v o : : = c! v ∣ ∙ \end{matrix}$ Here, $c ? v$ (resp. $c! v$ ) denotes a message received (resp. sent) on channel c carrying value v, and ∙ denotes a non-interaction. Let a, c and v range over the (nonempty) sets $A$ , $C$ and $V$ respectively. Actions are the only external interface to our systems; systems are “black boxes” in every other respect.

Definition 3.1.
An input–output $LTS$ ( ${LTS}_{IO}$ ) is an $LTS$ $(S, L, \overset{}{\to})$ , with L ranged by a.

Practical languages for which this model of computation is appropriate include Erlang and JavaScript. Bohannon et al. give the semantics of a JavaScript-like language as an ${LTS}_{IO}$ in [15] and Clark and Hunt give the semantics of an imperative language with I/O (used in our examples) as an ${LTS}_{IO}$ in [17]. Since all our results apply to any ${LTS}_{IO}$ state, our contributions are general.
3.2. Interactive programs

Definition 3.1 defines a general model of interaction that places no restrictions on how an ${LTS}_{IO}$ interacts with its environment. The interactive programs we consider in this paper are a class of ${LTS}_{IO}$ which interact with their environment in a particular way. We formalize this interaction pattern as three properties: input-neutral, input-blocking, and deterministic. An input-neutral ${LTS}_{IO}$ will, when it is ready to perform input on a channel, accept any value the environment provides on that channel. An input-blocking ${LTS}_{IO}$ will, when attempting to perform input on a channel, block until one is available. We formalize this as an input action with a distinguished value $⋆ \in V$ (blank); when $s \overset{c ? ⋆}{\to} s^{'}$ , then s has waited one time unit for an input on c without receiving one ( $c! ⋆$ has no specific meaning). A deterministic ${LTS}_{IO}$ can either only do a (unique) output, or only do input on a (unique) channel, and in both cases enter a state uniquely defined for the action it took. We require that these properties are preserved through execution, i.e., hold for all reachable states. In the following, let $S (s)$ be the set of states reachable from s. That is, $s \in S (s)$ , and for all $s^{'} \in S (s)$ we have for all a and $s^{″}$ for which $s^{'} \overset{a}{\to} s^{″}$ that $s^{″} \in S (s)$ .

Definition 3.2.
For all $s_{0}$ ,
$s_{0}$ is input-neutral iff $\forall s \in S (s_{0}) ․ \forall c ․ (\exists v ․ s \overset{c ? v}{\to}) ⟹ (\forall v ․ s \overset{c ? v}{\to})$ .

$s_{0}$ is input-blocking iff $\forall s \in S (s_{0}) ․ \forall s^{'}, c ․ s \overset{c ? ⋆}{\to} s^{'} ⟹ s^{'} = s$ .

$s_{0}$ is deterministic iff $\forall s \in S (s_{0}) ․$

$\forall a_{1}, a_{2} ․ s \overset{a_{1}}{\to} \land s \overset{a_{2}}{\to} \land a_{1} \neq a_{2} ⟹ \exists c, v_{1}, v_{2} ․ a_{1} = c ? v_{1} \land a_{2} = c ? v_{2}$ , and

$\forall s_{1}, s_{2}, a ․ s \overset{a}{\to} s_{1} \land s \overset{a}{\to} s_{2} ⟹ s_{1} = s_{2}$ .

Point (1) states that if s is ready to perform input on c, s is receptive to any v on c. Point (2) states that input is a blocking operation, by asserting that s does not change state while waiting for input. Point (3)(a) says if $s \overset{c ? v}{\to}$ , then $s \overset{a}{\to}$ iff $a \in {c ? v ∣ v \in V}$ (so s can be input-neutral), and implicitly, if $s \overset{o}{\to}$ , then $s \overset{a}{\to}$ iff $a = o$ . Point (3)(b) says s has no internal nondeterminism. Unless stated otherwise, any s we consider in this paper satisfies Points (1), (2) and (3). We discuss the assumption of Point (2) further in Section 4.
3.3. Traces

We will reason about the behavior or systems in terms of the sequences of actions the system can perform. We therefore formally define such sequences, and ways of comparing them, now. A trace is a (finite) list of actions, denoted $\bar{a}$ . We let ϵ denote the empty trace, “.” as the cons operator, and we usually omit ϵ in nonempty traces. We write $s \overset{\bar{a}}{\to} s_{n}$ if $s \overset{a_{1}}{\to} s_{1} \overset{a_{2}}{\to} \dots \overset{a_{n}}{\to} s_{n}$ for some $s_{1}, \dots, s_{n}$ and $\bar{a} = a_{1} . \dots . a_{n}$ . Let $\bar{a} ↾_{?}$ , $\bar{a} ↾_{!}$ and $\bar{a} ↾_{c}$ denote the projection of $\bar{a}$ to its input-, output- and c-messages, respectively. E.g., if $\bar{a} = c ? 1 . c^{'}! 2 . c^{'} ? ⋆ . c! 4$ , then $\bar{a} ↾_{?} = c ? 1 . c^{'} ? ⋆$ , $\bar{a} ↾_{!} = c^{'}! 2 . c! 4$ , and $\bar{a} ↾_{c} = c ? 1 . c! 4$ . $\bar{a} ↾_{c}$ extends to $\bar{a} ↾_{C}$ for $C \subseteq C$ in the obvious way. All of these, and other, projections used throughout the paper are given formally in Appendix B. We write $\bar{a} ↾_{x_{1}, \dots, x_{n}}$ as short for $\bar{a} ↾_{x_{1}} \dots ↾_{x_{n}}$ ; we refer to each $x_{j}$ as a projection predicate. With $\bar{a}$ defined as above, $\bar{a} ↾_{c, ?} = \bar{a} ↾_{c} ↾_{?} = c ? 1$ .

We write $\bar{a} ⩽ {\bar{a}}^{″}$ when, for some ${\bar{a}}^{'}$ , ${\bar{a}}^{″} = \bar{a} . {\bar{a}}^{'}$ . Here, $\bar{a} . {\bar{a}}^{'}$ is the concatenation of $\bar{a}$ and ${\bar{a}}^{'}$ . Throughout the paper, all the relations on traces that we use are defined as ⩽ or = after first applying projection functions in a particular order on both sides of the relation. To reduce notation, instead of using a new symbol for each such combination of relation and projection functions that we use, we develop a notation for applying projection functions in order to both sides of a relation. For a relation R, $\bar{a} R_{x_{1}, \dots, x_{n}} {\bar{a}}^{'}$ is short for $(\bar{a} ↾_{x_{1}, \dots, x_{n}}) R ({\bar{a}}^{'} ↾_{x_{1}, \dots, x_{n}})$ . Note that ${(R_{x_{1}, \dots, x_{n}})}_{x_{0}} = R_{x_{0}, \dots, x_{n}}$ . With $\bar{a}$ defined as above, $\bar{a} ⩽_{!, c} c ? 3 . c! 4 . c! 5$ .

3.4. Observables

The observables of our programs are its effects. The observability of a message is given by the security level associated with the channel carrying the message. As foreshadowed earlier, we assume a lattice $(L, ⊑)$ , with $L$ ranged by ℓ, of security levels which express levels of confidentiality. Each channel is labeled with two security levels; $π (c)$ is the level of the presence of a message on c, and $κ (c)$ is the level of the content or value of a message on c. We require for all c that $π (c) ⊑ κ (c)$ , the intuition being that an observer who can infer the value of a message can infer that there was a message carrying this value. In examples, we frequently represent a channel by its security labels; we then write $κ {(c)}^{π (c)}$ in place of c (in code, $κ (c) π (c)$ ). Note, however, that we do not assume that there is only one channel associated with each security level. A classic example is the two-level lattice $L_{L H} = {L, H}$ with $⊑ = {(L, L), (L, H), (H, H)}$ , $L$ for “low” confidentiality, $H$ for “high”. We let $H$ , $M$ , $L$ denote $H^{H}$ , $H^{L}$ and $L^{L}$ , resp. Since our results apply to any lattice, our contributions are general. In our technical results, we assume a fixed lattice.

Fig. 3.

Original execution with fine-grained security.

Figure 3 illustrates the flow of information in the case of $L_{L H}$ . Input on $M$ is depicted in-between the $H$ and $L$ input. The presence of such an input is $L$ (this dependency on $L$ is illustrated by the dashed line) while the content is $H$ (this dependency on $H$ is illustrated by the solid line). Similarly, output on $M$ is depicted in-between the $H$ and $L$ output. Its presence is observable at $L$ level (dashed arrow), and its value is observable at $H$ level (solid arrow).

The security labels express who can observe what. An observer is associated with a security level ℓ. An ℓ-observer is capable of observing the presence (resp. content) of a message on c iff $π (c) ⊑ ℓ$ (resp. $κ (c) ⊑ ℓ$ ). $\bar{a} ↾_{ℓ}$ removes ℓ-unobservable parts of actions in $\bar{a}$ . For $\bar{a} = ∙ . L ? 0 . H! 1 . M ? ⋆ . M! 2 . H ? ⋆ . ∙$ , $\bar{a} ↾_{L} = ∙ . L ? 0 . ∙ . M ? d . M! ⋆ . ∙ . ∙$ . Here, $H! 1$ got replaced with ∙ since communication on $H$ is unobservable to a $L$ -observer (thus looks like a ∙). $M! 2$ got replaced with $M! d$ (for a fixed $d \in V$ ), since a $L$ -observer only observes presence of messages on $M$ (all $a \in {M! v ∣ v \in V}$ look the same).

Timing and progress. Eventually we enforce a property stating that variations in unobservable inputs to a system do not cause an ℓ-observable difference in the traces the system can perform. Trace equivalence defines the class of attackers such a property guarantees security against. We consider two classes of attackers: timing- and progress-sensitive ones. Since each action takes a unit of time, these two attackers differ in whether or not they observe non-interaction. Since no message is passed when a system is blocking on input, we treat blank input as non-interaction. $\bar{a} ↾_{⋆}$ replaces all $c ? ⋆$ with ∙. With $\bar{a}$ defined as above, $\bar{a} ↾_{⋆} = ∙ . L ? 0 . H! 1 . ∙ . M! 2 . ∙ . ∙$ .

A timing-sensitive (e.g. [1,20]) attacker measures time between observables in a trace. $\bar{a} ↾_{\vec{∙}}$ removes trailing ∙ from $\bar{a}$ . E.g. $\bar{a} ↾_{\vec{∙}} = ∙ . L ? 0 . H! 1 . M ? ⋆ . M! 2 . H ? ⋆$ . Define timing-sensitive ℓ-equivalence $≃_{ℓ}$ as $=_{⋆, ℓ, \vec{∙}}$ (see Section 3.3 for a definition of $=_{⋆, ℓ, \vec{∙}}$ ). Let ${\bar{a}}_{1} = H ? ⋆ . H ? 1 . L! 0$ and ${\bar{a}}_{2} = H ? 1 . L! 0$ , and consider

Since this program can perform ${\bar{a}}_{1}$ and ${\bar{a}}_{2}$ , this program is not secure against a timing-sensitive $L$ -observer since ${\bar{a}}_{1} ↾_{⋆, L, \vec{∙}} = ∙ . ∙ . L! 0 \neq ∙ . L! 0 = {\bar{a}}_{2} ↾_{⋆, L, \vec{∙}}$ ( $L! 0$ is produced faster in the latter trace).

A progress-sensitive (e.g. [3,36,38]) attacker observes whether more observables are forthcoming. $\bar{a} ↾_{∙}$ removes all ∙ from $\bar{a}$ . With $\bar{a}$ as above, $\bar{a} ↾_{∙} = L ? 0 . H! 1 . M ? ⋆ . M! 2 . H ? ⋆$ . Define progress-sensitive ℓ-equivalence $\approx_{ℓ}$ as $=_{⋆, ℓ, ∙}$ . ${\bar{a}}_{1}$ and ${\bar{a}}_{2}$ are not evidence that the above program is insecure against progress-sensitive ℓ-observers; ${\bar{a}}_{1} ↾_{⋆, L, ∙} = L! 0 = {\bar{a}}_{2} ↾_{⋆, L, ∙}$ (in both traces, $L! 0$ eventually appears). A progress-sensitive timing-insensitive attacker is strictly weaker than a timing-sensitive one since $(≃_{ℓ}) ⊊ (\approx_{ℓ})$ .

3.5. Environments

Inputs to our systems come from the environment in which our systems run. Clark and Hunt [17] have demonstrated that when analyzing deterministic programs for security, an environment does not need to be adaptive to provoke a particular (leaking) behavior. Thus it is sufficient for our purposes to consider environments represented as a stream (infinite list) of inputs for each channel. So, an environment e is a mapping from input channels to the stream of inputs the environment provides on that channel. Since streams can contain blanks, our framework considers attacks driven by varying the timing of input.

The jth element in $e (c)$ represents what e provides on c in time unit j; if this element is $c ? v$ , then e provided value v on c in time unit j; if the element is $c ? ⋆$ , then e provided no value in time unit j. Since any program we consider can consume at most one input per computation step, we do not need to consider scenarios (or their security implications) where e provides input at a rate faster than the program can consume them. Since a program is not necessarily ready to receive an input when the environment provides it, we assume that the interface between e and the program manages a buffer for each input channel, and that the program draws input on a channel c from the c-buffer (in FIFO order), drawing a blank when the c-buffer is empty. We also assume that this interface never prevents a program from performing an output. The interaction between a program and its environment is therefore asynchronous.

We formalize this interaction using a relation that defines when a trace $\bar{a}$ is possible under a given environment e. Intuitively, $\bar{a}$ is possible under e if, for any c, (1) the c-inputs in $\bar{a}$ are (in value and order) as provided by e, (2) each c-input occurs no sooner in $\bar{a}$ than e could have provided it, and (3) a blank is drawn only when no c-input is buffered. Let $e_{c} = e (c)$ , and let $e_{c, n}$ denote the prefix of length n of $e_{c}$ . Formally, $\bar{a}$ is consistent with e, written $e ⊧ \bar{a}$ , iff for all c, we have for all $\forall {\bar{a}}^{'} ⩽ \bar{a}$ , with ${\bar{i}}^{'} = e_{c, | {\bar{a}}^{'} |}$ , that $\begin{array}{l} {\bar{a}}^{'} \neq ˍ . c ? ⋆ ⟹ {\bar{a}}^{'} ⩽_{?, c, ⋆, ∙} {\bar{i}}^{'}, and \\ {\bar{a}}^{'} = ˍ . c ? ⋆ ⟹ {\bar{a}}^{'} =_{?, c, ⋆, ∙} {\bar{i}}^{'} \land {\bar{i}}^{'} = ˍ . c ? ⋆ . \end{array}$ This states that for each prefix ${\bar{a}}^{'}$ of $\bar{a}$ and each c, the list of non-blank inputs in ${\bar{a}}^{'}$ must prefix the list of non-blank inputs in the same-length prefix ${\bar{i}}^{'}$ of $e (c)$ , and that ${\bar{a}}^{'}$ ends with a blank input on c only if all c-inputs provided by e up to this point are in ${\bar{a}}^{'}$ and e provided no new c-inputs in time unit $| {\bar{a}}^{'} |$ ( $ˍ$ is a wildcard). The quantification and definition of ${\bar{a}}^{'}$ and ${\bar{i}}^{'}$ formalizes (2), the trace equivalences formalize (1), and the ${\bar{a}}^{'} = ˍ . c ? ⋆$ case addresses (3). Since running s under e constrains the traces which s can perform, we obtain a definition of interaction as follows: s performs $\bar{a}$ under e, written $e ⊧ s \overset{\bar{a}}{\to}$ , iff $s \overset{\bar{a}}{\to}$ and $e ⊧ \bar{a}$ . Let s be the initial state of the following program.

Let ${e_{1}}_{c}, \dots, {e_{5}}_{c}$ be defined as on the left below. Then the judgments on the right hold. $\begin{array}{l} {e_{1}}_{c} = {(c ? ⋆)}^{\infty}, e_{1} ⊧ s \overset{{(c ? ⋆)}^{n}}{\to} for all n \in N, \\ {e_{2}}_{c} = c ? 0 . c ? 0 . {(c ? ⋆)}^{\infty}, e_{2} ⊧ s \overset{c ? 0 . ∙ . c ? 0}{\to}, \\ {e_{3}}_{c} = c ? 2 . c ? 0 . {(c ? ⋆)}^{\infty}, e_{3} ⊧ s \overset{c ? 2 . ∙ . ∙ . ∙ . ∙ . ∙ . c ? 0}{\to}, \\ {e_{4}}_{c} = c ? 0 . c ? ⋆ . c ? ⋆ . c ? ⋆ . c ? 0 . {(c ? ⋆)}^{\infty}, e_{4} ⊧ s \overset{c ? 0 . ∙ . c ? ⋆ . c ? ⋆ . c ? 0}{\to}, \\ {e_{5}}_{c} = c ? 2 . c ? ⋆ . c ? ⋆ . c ? ⋆ . c ? 0 . {(c ? ⋆)}^{\infty}, e_{5} ⊧ s \overset{c ? 2 . ∙ . ∙ . ∙ . ∙ . ∙ . c ? 0}{\to} . \end{array}$ These judgments hold regardless of how ${e_{k}}_{c^{'}}$ for $1 ⩽ k ⩽ 5$ and $c^{'} \neq c$ are defined (s only reads from c).

Equivalence. We compare the streams in the environments the same way we compare traces. So we define observational equivalence of environments as follows: $\begin{array}{l} e_{1} ≃_{ℓ} e_{2} iff \forall c ․ π (c) ⊑ ℓ ⟹ e_{1} (c) ≃_{ℓ} e_{2} (c), \\ e_{1} \approx_{ℓ} e_{2} iff \forall c ․ π (c) ⊑ ℓ ⟹ e_{1} (c) \approx_{ℓ} e_{2} (c) . \end{array}$

Totality. An environment is total if it always provides a system with input whenever the system needs it. In our framework, e is total if ⋆ does not occur in any $e_{c}$ . Previous work on security for interactive programs [17,36] assume environments are total. However, as we have demonstrated previously [37], this assumption limits (undesirably) the space of possible attacks on input-blocking interactive programs, since the presence of a message can depend on high data. Consider the program in Section 3.4. Let ${e_{1}}_{H} = H ? 0 . {(c ? ⋆)}^{\infty}$ and ${e_{2}}_{H} = {e_{1}}_{c} = {e_{2}}_{c} = {(c ? ⋆)}^{\infty}$ for all $c \neq H$ . While this program can perform $H ? 0 . L! 0$ under $e_{1}$ , the program cannot perform an $\approx_{L}$ -equivalent trace under $e_{2}$ . Since a program can encode a bit in the presence of a message, these attacks become crucial in an interactive setting. To emphasise the gravity of this, we give an example, from [37], of three interactive programs, each secure under total environments, which, when run in parallel (e.g. with the semantics in [37, Fig. 2]), leak the input on $H$ , bit by bit, on $L$ , by encoding the received value in the presence of $H_{0}$ and $H_{1}$ messages.

In summary, the lack (resp. delay) of input impedes on the progress (resp. timing) behavior of input-blocking interactive systems. To guarantee protection against attacks powered by varied input presence, nontotal environments (e.g. our e) must be considered. This in part motivates our fine-grained security levels; since no low observables are allowed to occur after a high input in deterministic input-blocking systems, the only way for such a system to input a high value before performing low observables is if the presence level of the input is low [37].

3.6. Noninterference

As mentioned earlier, our target policy is noninterference. The idea behind noninterference is the following. Assume an ℓ-observer observes all system effects which he is privileged to observe, i.e. all ℓ-observable actions. A system is noninterfering if, by observing ℓ-observable actions, the ℓ-observer learns nothing he is not privileged to learn, i.e., unobservable input does not interfere with observable behavior. Noninterfering systems are thereby not responsible for leaks. The formalization of this idea we use is that of possibilistic noninterference for interactive systems [17,36,37]. It states that, for any two ℓ-equivalent input environments, the respective sets of traces produced under either of them are ℓ-equivalent. Thus, an ℓ-observer, by observing ℓ-observables, cannot tell one input environment apart from any other input environment that differs only in ℓ-unobservable input. The following definition is a definition schema, parameterized by an security-level-indexed equivalence relation $R$ defined on traces and environments. We will later instantiate this schema with $≃_{}$ and $\approx_{}$ (both security-level-indexed equivalence relations on traces and environments) in place of $R$ .

Definition 3.3.
s is $R$ -noninterfering ( $s \in {NI}^{R}$ ) iff $\begin{matrix} \forall ℓ, e_{1}, e_{2} ․ e_{1} R_{ℓ} e_{2} ⟹ \forall {\bar{a}}_{1} ․ e_{1} ⊧ s \overset{{\bar{a}}_{1}}{\to} ⟹ \exists {\bar{a}}_{2} ․ e_{2} ⊧ s \overset{{\bar{a}}_{2}}{\to} \land {\bar{a}}_{1} R_{ℓ} {\bar{a}}_{2} . \end{matrix}$

Note that for nondeterministic programs, possibilistic noninterference is a somewhat weak notion of security, since it requires that a system can, by making the appropriate nondeterministic choices, match behavior. Since our systems are deterministic, however, the stream of actions a system can perform under a fixed e is unique. Possibilistic noninterference thus requires that, for any $e_{1} R_{ℓ} e_{2}$ , any prefix of the stream of actions s performs under $e_{1}$ must be matched by some prefix of the stream of actions s performs under $e_{2}$ , and vice versa, since $e_{2} R_{ℓ} e_{1}$ . Possibilistic noninterference (due to limited possibilities) is thus rather strong in our setting.

By instantiating this definition with the two ℓ-equivalence relations from Section 3.4, we get the two definitions of noninterference we will consider in this paper.
Definition 3.4.
s is timing-sensitive, progress sensitive noninterfering ( $s \in TSNI$ ) iff $s \in {NI}^{≃_{}}$ .
Definition 3.5.
s is timing-insensitive, progress sensitive noninterfering ( $s \in PSNI$ ) iff $s \in {NI}^{\approx_{}}$ .

For the system models under consideration in this paper, $PSNI$ is a weakening of $TSNI$ . The details of this, and all other proofs, are in Appendix C.
Theorem 3.6.
$\forall s ․ s \in TSNI ⟹ s \in PSNI$ .

Note that this result (and others) is sensitive to the assumptions we make in Definition 3.2. Consider a system s that times the arrival of an input on a $L$ input channel (by counting ⋆s), and outputs the time on a $L$ channel. Such a system is $TSNI$ -secure, and not input blocking. However, under $\approx_{L}$ -equivalent environments, the timing of $L$ input is allowed to differ; under such environments, s leaks the timing difference into a value in $L$ output, which a progress-sensitive observer can observe; a $PSNI$ -insecurity.
4. Fine-grained secure multi-execution

The opening series of our contributions develops a generalization of $SME$ [20] with respect to several dimensions. We lift the assumption on the totality of the input environment (i.e. that there is always assumed to be input) and on cooperative scheduling. Furthermore, we distinguish between security levels of presence and content of messages. In addition, we generalize $SME$ to arbitrary deterministic ${LTS}_{IO}$ and strengthen the guarantees $SME$ provides.

Fig. 4.

$SME$ with fine-grained security.

By design, our formalization of $SME$ ensures that the ℓ-observable part of the interaction on channels with ℓ presence depends only on ℓ-observable parts of input on channels with $⊑ ℓ$ presence, thus enforcing a noninterference policy. Figure 4 illustrates the intuition in our handling of the channels with fine-grained security levels for the two-level lattice. In addition to propagating low input to the high run (as in Fig. 2), we propagate to the high run the fact that an $M$ message has arrived to the low run. This allows consistent processing of the message. At the output, the presence of an $M$ message is observable at the low level (cf. dashed output arrow). On the other hand, the value of an $M$ output is produced by the high run (cf. solid output arrow).

Our $SME$ of s runs, concurrently, a copy of s for each level in the security lattice. The $SME$ of s can input on c iff the $π (c)$ -run can input on c. An ℓ-run which can consume a c-input with $π (c) ⋢ ℓ$ is fed a (constant, pre-determined, input-independent) default value, denoted $d$ , by $SME$ . An ℓ-run which can consume its nth c-input with $π (c) ⊏ ℓ$ gets a copy of the nth input consumed by the $π (c)$ -run, unless $π (c)$ is yet to consume n c-inputs, in which case the ℓ-run blocks until the $π (c)$ -run has done so. However, if $κ (c) ⋢ ℓ$ , then the ℓ-run is fed $d$ instead of the value in the nth c-input. The $SME$ of s can output on c iff the $π (c)$ -run can output on c. A c-output produced by a ℓ-run for which $π (c) \neq ℓ$ is discarded by $SME$ (as opposed to being sent to the environment). When an ℓ-run produces its nth c-output with $ℓ = π (c)$ , this output is sent straight to the environment, except when $π (c) \neq κ (c)$ ; in that case $SME$ first checks whether the $κ (c)$ -run has produced its nth c-output. If so, then the value of the nth c-output produced by the $SME$ of s becomes the value of the nth c-output produced by the $κ (c)$ -run. Otherwise, the value is $d$ .

4.1. Semantics

We now give a semantics for the $SME$ of an arbitrary s satisfying the assumptions in Definition 3.2, as an ${LTS}_{IO}$ state. Concurrent executions of ℓ-runs of s are scheduled by a scheduler. We consider schedulers which are autonomous and independent of input and of the behavior of ℓ-runs, since letting scheduling decisions depend on these can make $SME$ susceptible to subtle timing attacks (as demonstrated by Kashyap et al. [25], and discussed further in Section 4.2). Furthermore, to make $SME$ transparent, we require that schedulers are fair, in the sense that the scheduler schedules all ℓ-runs infinitely often, and deterministic, in the sense that the sequence of scheduling decisions the scheduler makes is unique.

Definition 4.1.
A scheduler $LTS$ , ${LTS}_{S}$ , is an $LTS$ with labels ranged by ℓ. A scheduler, σ, is a state of an ${LTS}_{S}$ . For all $σ_{0}$ ,
$σ_{0}$ is deterministic iff $\forall σ \in S (σ_{0}) ․$

$\forall ℓ, σ_{1}, σ_{2} ․ σ \overset{ℓ}{\to} σ_{1} \land σ \overset{ℓ}{\to} σ_{2} ⟹ σ_{1} = σ_{2}$ , and

$\forall ℓ, ℓ^{'} ․ σ \overset{ℓ}{\to} \land σ \overset{ℓ^{'}}{\to} ⟹ ℓ = ℓ^{'}$ .

$σ_{0}$ is fair iff $\forall σ \in S (σ_{0}) ․$

$\forall \bar{ℓ} ․ σ \overset{\bar{ℓ}}{\to} ⟹ \forall ℓ ․ \exists {\bar{ℓ}}^{'} ․ σ \overset{\bar{ℓ} . {\bar{ℓ}}^{'} . ℓ}{\to}$ .

Point (1)(a) states that the way future decisions is made is uniquely defined by the next choice, and Point (1)(b) stipulates that the choice of which ℓ-run to schedule next is unique. Point (2) states that no matter how many scheduling decisions have been made, each ℓ-run will eventually be scheduled. Unless stated otherwise, σ is deterministic and fair. Thus, since ℓ and $σ^{'}$ for which $σ \overset{ℓ}{\to} σ^{'}$ are unique and always exist, we use list and stream notation to represent and manipulate schedulers. An example of deterministic and fair schedulers is the round-robin schedulers. For instance, for $L_{L H}$ , ${(H . L)}^{\infty}$ and ${(L . H)}^{\infty}$ are deterministic fair schedulers (that repeat $H . L$ resp. $L . H$ , infinitely).

Fig. 5.
Semantics of $SME$ . (a) $SME$ ℓ-stepper. (b) $SME$ ℓ-chooser. (c) $SME$ history.

The semantics of $SME$ is an ${LTS}_{IO}$ of $SME$ -states. A $SME$ -state is a triple $(\bar{a}, σ, S)$ , where $\bar{a}$ is the list of actions which the $SME$ has performed so far, σ the state of the scheduler, and S contains the state of the ℓ-runs. S maps each security level ℓ to a pair $({\bar{a}}_{ℓ}, s_{ℓ})$ , where ${\bar{a}}_{ℓ}$ is the list of actions which the ℓ-run has performed so far, and $s_{ℓ}$ is the current state of the ℓ-run. For a given σ, the $SME$ of s, $SME (σ, s)$ , is defined as $SME (σ, s) = (ϵ, σ, λ ℓ \to (ϵ, s))$ . The transition relation for the ${LTS}_{IO}$ is given in Fig. 5. The transition relation is presented in three layers, in Fig. 5(c), Fig. 5(b) and Fig. 5(a) respectively. Each rule in each layer uses only rules in the layer directly above it. We start with the bottom-most layer, Fig. 5(c), and work our way upwards. The derivation of any $SME$ transition begins with the (history) rule (the judgment in the premise, which we will turn to momentarily, is defined in Fig. 5(b)). The purpose of (history) is to keep track of the interaction $\bar{a}$ which $SME (σ, s)$ has had with the environment. Note that $SME (σ, s) \overset{\bar{a}}{\to} ({\bar{a}}^{'}, σ^{'}, s^{'}) ⟹ \bar{a} = {\bar{a}}^{'}$ , so we sometimes omit the trace label on a $SME$ transition. We put $\bar{a}$ on the left side of “⊧” in the next layer of the semantics, Fig. 5(b), to show that this layer only reads $\bar{a}$ (we apply the same convention throughout the paper; this use of symbol “⊧” is not to be confused with the use of “⊧” in Section 3.5). The rules at the Fig. 5(b)-layer are responsible for, by use of σ, deciding which ℓ-run takes a step next, using the rules in the third (i.e. top) layer, Fig. 5(a). This third layer is responsible for hiding from the Fig. 5(b)-layer all the different ways which an ℓ-run can take a step without interacting with the environment ((dead), (silent), (o-old), (i-old)), and signaling to the Fig. 5(b)-layer when the ℓ-run requires I/O with the environment to proceed ((o-new), (i-new)). Each rule at the Fig. 5(a)-layer appends to the ℓ-run trace the action the ℓ-run performed during the step (which is not necessarily the same action as the one performed by the whole $SME$ -state). We equate a terminated ℓ-run with an infinitely silent one, as indicated by (dead) (not making terminated runs unschedulable excludes several timing attacks described by Kashyap et al. [25]). The Fig. 5(a)-layer stores output on channels with presence $\neq ℓ$ without forwarding it to the environment, as per (o-old). (i-old) covers multiple scenarios for the ℓ-run performing an input action on a channel which does not result in the $SME$ -state consuming input from the environment on c in this step. When $π (c) ⋢ ℓ$ , input $d$ . When $π (c) ⊑ ℓ$ , this rule is only applicable if the ℓ-run has not already read all the c-inputs which the $π (c)$ -run has read. When $κ (c) ⊑ ℓ$ , input the same value received from the environment when the $π (c)$ -run performed the corresponding input action. Otherwise, input $d$ instead. (i-new) indicates that the ℓ-run requires input to proceed, and for the value v received from the Fig. 5(b)-layer, indicated on the transition label, instead feeds $d$ to the ℓ-run iff $v \neq ⋆ \land κ (c) ⋢ ℓ$ ( $v_{ℓ}$ is a function of c, ℓ, and v). The previous layer has two rules for this scenario. When $π (c) ⊏ ℓ$ , then the ℓ-run blocks until the $π (c)$ -run reads on c, by (i-block). When $π (c)$ reads on c, the input is fed to every $⊒ π (c)$ -run blocking on c, by (i). (o-new) notifies the Fig. 5(b)-layer that the ℓ-run has a fresh output for the environment. Rule (o) in the previous layer handles this scenario, checking if the $κ (c)$ -run has already provided content for this output, and if so, replaces the value in the output with the value in the corresponding $κ (c)$ -run c-output.

When $κ (c) \neq π (c)$ , the output value is replaced by $d$ iff $κ (c)$ has not yet produced the corresponding value. Having the $π (c)$ -run instead wait for the $κ (c)$ -run to reach the corresponding c-output, or giving responsibility of producing the c-output to the $κ (c)$ -run, can introduce a leak:

Here the time it takes for the $H$ -run to produce the $M$ -output (for nonnegative h), and whether $H$ produces the output at all (for negative h), depends on h, in the $SME$ of this program.

While Fig. 5(b) indicates that $SME$ controls each step of each ℓ-run, in practice the responsibility of $SME$ can be distributed to the ℓ-runs, such that each ℓ-run is autonomous, as follows. Each ℓ-run is made responsible for environment I/O on all $c \in π^{- 1} (ℓ)$ , since $SME (s)$ performs I/O iff the ℓ-run of s performs it. Each ℓ-run makes input on each $c \in π^{- 1} (ℓ)$ and output on each $c \in κ^{- 1} (ℓ)$ available in a shared resource (e.g. memory) such that $⊐ ℓ$ -runs can obtain a copy of the input when they need it, and an $π (c)$ -run can obtain the actual value to output on c. Each ℓ-run processes (after sharing, when $ℓ = π (c)$ ) $d$ in place of the inputted value when $π (c) ⊑ ℓ$ and $κ (c) ⋢ ℓ$ , and outputs $d$ when the $κ (c)$ -run is yet to share the value to put into the output when $ℓ = π (c) ⊏ κ (c)$ . This approach is taken in a $SME$ benchmark by Devriese and Piessens [20]. Forcing ℓ-runs to diverge and recording full traces can be avoided [20,25]. This approach is sound as long as the ℓ-run threads cannot influence the scheduler.

While s is input-blocking, $SME (s)$ is not; varied presence of input on $c \in κ^{- 1} (ℓ)$ cannot impede progress or timing of $ℓ^{'}$ -runs where $ℓ ⋢ ℓ^{'}$ . This effect is achieved by $c ? ⋆$ actions; if $SME (s)$ is in a state where an ℓ-run wants input on c, and e does not have one ready (yet), the ℓ-run can do a $c ? ⋆$ -action, allowing $SME (s)$ to pass control to another $ℓ^{'}$ -run. In contrast, the formalization (as opposed to the benchmark implementation) of $SME$ by Devriese and Piessens [20] is input blocking; if an ℓ-run is scheduled before a $ℓ^{'}$ -run with $ℓ ⋢ ℓ^{'}$ , the nonpresence of input on $c \in π^{- 1} (ℓ)$ can interfere with the $ℓ^{'}$ -run. This hinders sound scheduling of runs for arbitrary nonlinear lattices.
4.2. Soundness

By design, $SME$ enforces timing-sensitive noninterference.

Theorem 4.2.
$\forall σ, s ․ SME (σ, s) \in TSNI$ .

We first highlight the implication of this result by contrasting it with similar results in related work. Afterwards, we give an intuition for why this theorem is true.

In contrast to Devriese and Piessens [20], who prove soundness for a cooperative scheduler for linear lattices, and to Kashyap et al. [25], who prove soundness for two round-robin schedulers (the “Multiplex-2” and “Lattice-based” approaches), we prove a more general result: soundness for arbitrary deterministic and fair schedulers. While Devriese and Piessens claim their scheduler, called ${select}_{lowprio}$ , which executes the ℓ-runs to completion in increasing order by ⊑, works for any linearization of a nonlinear lattice, Kashyap et al. have shown that ${select}_{lowprio}$ introduces a timing dependency between ℓ-runs at incomparable levels in nonlinear lattices. For instance, with $L = L_{AB} \overset{def}{=} {H, A, B, L}$ and ⊑ being the reflexive transitive closure of ${(L, A), (L, B), (A, H), (B, H)}$ , with linearization $L ⊑ A ⊑ B ⊑ H$ and $d = 0$ , the time it takes for $B^{B}! 1$ to emerge from the $SME$ of the following program is, under ${select}_{lowprio}$ , a function of the input on $A^{A}$ .

In the presence of nontotal environments, the situation is even worse; in the $SME$ of the following program under ${select}_{lowprio}$ , the presence of input on $A^{A}$ leaks to $B^{B}$ .

While swapping $A$ and $B$ in the linearization resolves the issue in the above program, the following program has no linearization of $L$ for which ${select}_{lowprio}$ schedules ℓ-runs soundly.

We show in Appendix A that assuming that any ℓ-run can run to completion of all of its inputs (necessary for ${select}_{lowprio}$ to schedule ℓ-runs soundly for linear lattices) is problematic when program input arrives arbitrarily in time.

The proof of Theorem 4.2 is a corollary of the following lemma, which can be obtained by removing the last two elements in the conjunction in the conclusion of the lemma, and comparing the result with Definition 3.4. We write $S_{1} =_{ℓ} S_{2}$ iff $\forall ℓ^{'} ⊑ ℓ ․ S_{1} (ℓ^{'}) = S_{2} (ℓ^{'})$ .
Lemma 4.3.
$\forall σ, s, ℓ, e_{1}, e_{2} ․ e_{1} ≃_{ℓ} e_{2} ⟹$ $\begin{matrix} \begin{matrix} \forall {\bar{a}}_{1}, σ_{1}, S_{1} ․ e_{1} ⊧ SME (σ, s) \overset{}{\to} ({\bar{a}}_{1}, σ_{1}, S_{1}) ⟹ \\ \exists {\bar{a}}_{2}, σ_{2}, S_{2} ․ e_{2} ⊧ SME (σ, s) \overset{}{\to} ({\bar{a}}_{2}, σ_{2}, S_{2}) \land {\bar{a}}_{1} =_{ℓ} {\bar{a}}_{2} \land S_{1} =_{ℓ} S_{2} \land σ_{1} = σ_{2} . \end{matrix} \end{matrix}$

Such a strong correspondence is achievable since, for each $ℓ^{'} ⊑ ℓ$ , the $ℓ^{'}$ -run of s, in $e_{1} ⊧ SME (σ, s)$ and $e_{2} ⊧ SME (σ, s)$ , behaves as $e ↾_{ℓ^{'}} ⊧ s$ , where $\begin{matrix} (e ↾_{ℓ^{'}}) (c) = \{\begin{matrix} {(c ? d)}^{\infty}, & if π (c) ⋢ ℓ^{'}, \\ e (c) ↾_{ℓ}, & otherwise. \end{matrix} \end{matrix}$ (While for $π (c) ⊑ ℓ^{'}$ , the number of $c ? ⋆$ preceding a $c ? v$ of an $ℓ^{'}$ -run in $e_{j} ⊧ SME (σ, s)$ compared to $e ↾_{ℓ^{'}} ⊧ s$ can differ due to σ, this number is the same in $e_{1} ⊧ SME (σ, s)$ compared to $e_{2} ⊧ SME (σ, s)$ . Since s is input-blocking, all three are in the same state at the time of the non-blank read, and consume the same input, by $e ↾_{ℓ^{'}}$ .) Thus, since $e_{1} ⊧ SME (σ, s)$ and $e_{2} ⊧ SME (σ, s)$ are both run under the same σ, we have that after any number of transitions, the $ℓ^{'}$ -runs will in both runs have performed the same number of actions, consumed the same inputs, produced the same outputs, and be in the same state.
4.3. Transparency

We show that $SME$ does not adversely modify the I/O behavior of a progress-sensitive noninterfering program (and therefore also a of timing-sensitive noninterfering program). Let $s \in PSNI$ , ℓ, e and σ be arbitrary. In s and $SME (σ, s)$ , the interaction on ℓ-presence channels is ℓ-equivalent.

Theorem 4.4.
$\forall σ, s \in PSNI, e, \bar{a} ․$
$e ⊧ s \overset{\bar{a}}{\to}$ $⟹ \exists {\bar{a}}^{'} ․ e ⊧ SME (σ, s) \overset{{\bar{a}}^{'}}{\to}$ $\land \forall ℓ ․ \bar{a} ⩽_{⋆, ℓ, π^{- 1} (ℓ), ∙} {\bar{a}}^{'}$ ,

$e ⊧ SME (σ, s) \overset{\bar{a}}{\to}$ $⟹ \exists {\bar{a}}^{'} ․ e ⊧ s \overset{{\bar{a}}^{'}}{\to}$ $\land \forall ℓ ․ \bar{a} ⩽_{⋆, ℓ, π^{- 1} (ℓ), ∙} {\bar{a}}^{'}$ .

When all ℓ-presence outputs also have ℓ-content, the ℓ-presence interaction in s and $SME (s)$ is the same. This is an improvement on Theorem 2 in [20] which establishes only the (a)-part of Theorem 4.4 for the interaction on each channel (as opposed to, for each ℓ, the interaction on all channels with presence level ℓ), and only for terminating runs of termination-sensitive s. Furthermore, under $L_{AB}$ and nontotal environments, ${select}_{lowprio}$ yields a nontransparent run for the following program, as no $B^{B}! 1$ occurs if no input on $A^{A}$ arrives.

However, when s outputs on c with $κ (c) ⊐ π (c)$ , $SME (σ, s)$ might replace the value in its corresponding output with $d$ . Thus, the timing behavior of $s \in PSNI$ can impede the ability of a σ to soundly schedule runs in $SME (σ, s)$ such that the $κ (c)$ -run reaches the output before the $π (c)$ -run does irrespective of previously inputted values. In $TSNI$ programs, however, all ℓ-runs for which $π (c) ⊑ ℓ$ will reach an output on c after the same number of reduction steps. This includes the $κ (c)$ -run, since $π (c) ⊑ κ (c)$ . Thus, if we ensure that any ℓ-run never “outruns” its parent-runs (in the sense that the ℓ-run has made more progress on its (nonblocking) actions than $ℓ ⊐$ -runs), we can ensure that the content-provider of an output reaches the output before its presence-provider does. It is, however, not sufficient to require, for instance, that at any given point, $H$ has been scheduled more often than $L$ , as the $H$ -run can waste its turns blocking on $L$ -presence input (we do not need to worry about a $H$ -run blocking on $H$ -presence input, because for a deterministic program to satisfy $PSNI$ (and therefore $TSNI$ ), it must be impossible for any $L$ effect to follow a $H$ -presence input [37]). For instance, the $SME$ of the following program under any σ satisfying $H . {(H)}^{n} . L . L ⩽ σ$ for any $n > 1$ is not transparent.

What we need is a schedule which ensures that when the $L$ -run reaches an action involving interaction on a $L$ -presence channel, $H$ is either already blocking on input on said channel (in case the $L$ -run is performing input on it), or has already moved past the output on said channel (in case the $L$ -run is performing output on it). We achieve this by making sure that, before scheduling $L$ , we have already scheduled $H$ since $L$ was last scheduled. The following predicate formalizes this; when invoked as $ϕ (ℓ_{H}, ℓ_{L}, 0, \bar{ℓ})$ , the predicate yields 1 when $ℓ_{L}$ and $ℓ_{H}$ have been scheduled in such a manner in $\bar{ℓ}$ , and 0 otherwise. $\begin{matrix} \begin{matrix} ϕ ( & ˍ & , ˍ & , ˍ & , ϵ) & = 1 \\ ϕ ( & ℓ_{H} & , ℓ_{L} & , b_{H seen} & , ℓ . \bar{ℓ}) & ∣ ℓ = ℓ_{H} & = ϕ (ℓ_{H}, ℓ_{L}, 1, \bar{ℓ}) \\ ∣ ℓ = ℓ_{L} \land b_{H seen} & = ϕ (ℓ_{H}, ℓ_{L}, 0, \bar{ℓ}) \\ ∣ ℓ = ℓ_{L} \land \neg b_{H seen} & = 0 \\ ∣ otherwise & = ϕ (ℓ_{H}, ℓ_{L}, b_{H seen}, \bar{ℓ}) \end{matrix} \end{matrix}$ This formalization achieves this effect by walking through $\bar{ℓ}$ , assigning a bit to 1 upon encountering a $ℓ_{H}$ (signifying that $ℓ_{H}$ has been scheduled since $ℓ_{L}$ was last scheduled), and assigning the bit to 0 upon encountering a $ℓ_{L}$ only if the bit is 1 (if it is 0, the schedule is rejected).

With this predicate, we can formalize schedulers which never allow runs to “outrun” their parent runs, for any lattice. We call these high-lead schedulers.
Definition 4.5.
σ is a high-lead scheduler ( $σ \in HLS$ ) iff $\begin{matrix} \forall \bar{ℓ} ․ σ \overset{\bar{ℓ}}{\to} ⟹ \forall ℓ_{L}, ℓ_{H} ․ ℓ_{L} ⊏ ℓ_{H} ⟹ ϕ (ℓ_{H}, ℓ_{L}, 0, \bar{ℓ}) . \end{matrix}$

An example of a high-lead scheduler is the round-robin scheduler which schedules levels in (increasing) order of maximal descendancy from top (ties broken arbitrarily). For instance, for $L = {H, A, B, C, L}$ and ⊑ being the reflexive transitive closure of ${(L, C), (L, A), (C, B), (A, H), (B, H)}$ , σ which infinitely repeats $H . B . A . C . L$ or $H . A . B . C . L$ is a high-lead scheduler. It is for these schedulers that, when $s \in TSNI$ , the interaction on ℓ-presence channels in and $SME (σ, s)$ is the same, for all ℓ.
Theorem 4.6.
$\forall σ \in HLS, s \in TSNI, e, \bar{a} ․$
$e ⊧ s \overset{\bar{a}}{\to}$ $⟹ \exists {\bar{a}}^{'} ․$ $e ⊧ SME (σ, s) \overset{{\bar{a}}^{'}}{\to}$ $\land \forall ℓ ․ \bar{a} ⩽_{⋆, π^{- 1} (ℓ), ∙} {\bar{a}}^{'}$ ,

$e ⊧ SME (σ, s) \overset{\bar{a}}{\to}$ $⟹ \exists {\bar{a}}^{'} ․$ $e ⊧ s \overset{{\bar{a}}^{'}}{\to}$ $\land \forall ℓ ․ \bar{a} ⩽_{⋆, π^{- 1} (ℓ), ∙} {\bar{a}}^{'}$ .

Thus, if $SME$ puts a $d$ in an $M$ output when run using $σ \in HLS$ , then this must have been done to prevent a (timing or progress) leak – a desired effect.
5. Declassification

Many systems intentionally leak information as part of their function [46]. For instance, systems with a login interface leak the (mis)match of a username–password pair through the success/failure of a login attempt, systems that release the average salary of workers for statistics purposes leak information about the salary of each worker, and displaying the popularity of an item in an online shop leaks information about the purchases of customers. The target properties of interest for such systems are ones which stipulate that all leaks (if any) are intentional. An intended leak is referred to as a release, and we refer to the act of releasing information as a declassification (note: while these words are typically synonymous in literature, we use them as prescribed here). Such properties, i.e. models of declassification, have proven to be highly scenario-specific; as of yet, there is no one model universally applicable. Exploring such models is an active area of research, the state of the art being a classification of models by declassification goals (called dimensions of declassification), and a set of principles which a model should follow [46].

As is, $SME$ enforces noninterference, which disallows all leaks, intentional or otherwise. When applied on a system with intentional leaks, $SME$ removes the leaks, thus removing a feature from the system. This makes $SME$ impractical for this broad class of systems. To remedy this, we present a variant of $SME$ , ${SME}_{D}$ , which supports declassification. A declassification model which would be a good fit for our scenario is one which requires that (1) declassification only takes place where the system needs it, and (2) what leaks are allowed must be defined outside the system (so they can be blackbox enforced by ${SME}_{D}$ ). These goals are primarily along the where (in the sense of where in the code the release may take place and where in the security lattice the affected information might be) and what (in the sense of what information may be released) dimensions of declassification [46], although the who dimension plays a role since attacker-controlled code and input must not affect which leaks are allowed. While models along the when dimension (which e.g. strive to delay release, release infrequently, or release only after a session has completed) provide useful guarantees, we find that facilitating them requires nontrivial extensions to our semantic and information-flow model for goals which are ultimately domain-specific.

While looking for a model matching the above goals, we discovered that none of the models we studied and their accompanying enforcements proved to be an ideal fit for our scenario. Whereas $SME$ is a blackbox dynamic enforcement operating on interactive systems, most models of declassification are designed for substantially different system models, and most enforcements are whitebox and static [46]. Furthermore, in many models of declassification, intended leaks are defined through annotations (e.g. $declassify$ ) in the program (and thereby assumed to be desired by principals); such an approach would not work in our scenario, since the systems $SME$ operates on are possibly-malicious black boxes.

To show that ${SME}_{D}$ enforces our desired goals, we prove it sound w.r.t. two models of declassification. One is gradual release [2], a where model which we have adapted to our scenario. Gradual release, along with an accompanying static enforcement, has previously been given for a semantic model for noninteractive imperative programs [2], and a generalization of gradual release with what goals with an accompanying hybrid enforcement, has previously been given for interactive programs [3]. In both cases, enforcements are whitebox, intended leaks are defined by the program, and the models were timing-insensitive. One reason for the above-mentioned generalization is that gradual release allows leaking arbitrary contextual information through a declassification action. Addressing the what dimension of declassification, we introduce a new model of release, full release, which is a blackbox what model that disallows leaking arbitrary contextual information through a declassification. Essentially, ${SME}_{D}$ satisfies full release by virtue of how $SME$ separates input at different security levels into independent runs. To this end, while being primarily a what condition, full release has aspects of where in the security lattice [46] since it limits the effects of declassification to the declared security levels.

Fig. 6.

$SME$ with declassification.

This very separation makes declassification in $SME$ nontrivial, since, by design, e.g. the $L$ run does not have $H$ information as part of its state when $H$ information is to be declassified to $L$ ; $L$ effects are controlled (only) by the $L$ run, and $H$ input is fed (only) to the $H$ run. To let $L$ effects depend on declassified $H$ information in ${SME}_{D}$ , we need to move (only) the declassified information from the $H$ run to the $L$ run in a controlled way, without breaking the kind of guarantee $SME$ was originally designed to provide. It turns out that the communication model from Section 4 is an excellent fit for secure communication between the runs at different levels. Recall that we wish to prevent the occurrence of declassification events from leaking information about the context while allowing intended release of the value to be declassified [46]. This is exactly the problem we needed to solve to properly handle channels with different security levels for presence and content! Conveniently, the same approach works here. The core idea is depicted in Fig. 6. Declassification corresponds to routing an $M$ output (containing the declassified value) from the $H$ run into the $L$ run. As with $M$ output in $SME$ , the occurrence of the declassification in the $H$ run in ${SME}_{D}$ is not leaked.

We begin this section with a brief departure from $SME$ to formalize our declassification goals in Sections 5.1 and 5.2. We then return to $SME$ in Sections 5.3–5.5 where we give a sound and transparent variant of $SME$ , ${SME}_{D}$ , that enforces these declassification goals, and discuss a variant ${SME}_{D}^{'}$ in Section 5.6.

5.1. Gradual release

One of our declassification goals is that information release only takes place where the system needs it. However, the systems we consider are black boxes which send and receive messages; at the point the system performs a declassification, the system is performing a noninteraction. When the effect of the declassification is then observed (much) later in the system-environment interaction, it is difficult to assess whether the observed leak was caused by the declassification or not. To address this issue, gradual release assumes that systems make declassifications an observable effect, thus providing the released information to its observer right where the declassification occurs. These effects form the interface the system uses to declare release intent to the gradual release property. The system then only leaks where needed if the system only leaks through these release actions, which is what gradual release stipulates.

We model s which make declassifications (i.e. the declarations of release intent) observable effects in our semantic model as follows. We use our channel abstraction to define release actions. Let $C_{R} \subseteq C$ be the set of release channels, ranged by $c_{R}$ , and let $A_{R} = {c_{R} ? v, c_{R}! v ∣ c_{R} \in C_{R} \land v \in V}$ be the set of release-actions, ranged by $a_{R}$ . A release action leaks information from one security level, to another. Let $φ (c_{R})$ denote the from-level, and $π (c_{R}) = κ (c_{R})$ denote the to-level of $c_{R}$ . The set of actions that release information to an ℓ-observer is then given as follows. $\begin{matrix} A_{R}^{ℓ} = {a_{R} \in A_{R} ∣ π (a_{R}) ⊑ ℓ \land φ (a_{R}) ⋢ ℓ} . \end{matrix}$ The following inference rule illustrates how the semantics of declassification, in a simple imperative language with I/O, can be given such that declassification becomes an effect. $\begin{matrix} \frac{(m, x : = t) \overset{∙}{\to} (m^{'}, skip) m^{'} (x) = v}{(m, x : = declassify (t, c_{R})) \overset{c_{R}! v}{\to} (m^{'}, skip)} \end{matrix}$ The action label $c_{R}! v$ on the transition signals, to gradual release, that the release is intended. This declassify construct is more fine-grained than the standard one as it specifies both the from level $φ (c_{R})$ and the to level $π (c_{R})$ of the declassification operation. Furthermore, the ability to support multiple channels releasing information from, say, $H$ to $L$ , enables us to encode the semantics of the value being released in the name of the channel; one channel could release age category, another could release gender, etc.

We say that s is releasing if it can perform a release action, and that s is release-compliant if all its release actions are output actions (s does not ask for permission to release; it just declares it; hence the release action must be an output).

Definition 5.1.
For all $s_{0}$ ,
$s_{0}$ is release-compliantiff $\forall s \in S (s_{0}) ․ \forall \bar{a}, i ․ s \overset{\bar{a} . i}{\to} ⟹ i \notin A_{R}$ .

$s_{0}$ is releasing ( $s \in {LTS}_{IO}^{_{R}}$ )iff $\exists \bar{a}, a_{R} ․ s \overset{\bar{a} . a_{R}}{\to}$ .

Unless stated otherwise, any s we consider in this paper is release-compliant.

Fig. 7.
Leaks through actions $a_{l_{1}}$ and $a_{l_{2}}$ reduce uncertainty about secrets.

Gradual release stipulates that an ℓ-observer only learns about ℓ-unobservables at points where the system performs a declassification. To formalize this, we first formalize what it means for the attacker to gain knowledge (cf. [2,3,9,21]). Recall the idea behind noninterference from Section 3.6. Assume the attacker knows the semantics of a system s and knows (or chooses) the ℓ-observables in the input environment e. From the attacker’s point of view, the input environment could be any one of ${e^{'} ∣ e R_{ℓ} e^{'}}$ . The goal of the attacker is to rule out elements of this set as possible input environments, by observing the ℓ-observable part of the interaction of s with e. If the attacker cannot, then s satisfies noninterference. If the attacker can rule out an environment $e^{'} R_{ℓ} e$ as a possible input environment, then the attacker obtains the knowledge that the ℓ-unobservables in e are not as defined by $e^{'}$ (thus learning things he is not privileged to learn). We define the knowledge of an ℓ-observer after observing a sequence of actions $\bar{a}$ performed by a system s under environment e as the set $k_{ℓ}^{R} (s, e, \bar{a})$ of input environments under which those observables were possible: $\begin{matrix} k_{ℓ}^{R} (s, e, \bar{a}) = {e^{'} ∣ e R_{ℓ} e^{'} \land \exists {\bar{a}}^{'} ․ e^{'} ⊧ s \overset{{\bar{a}}^{'}}{\to} \land \bar{a} R_{ℓ} {\bar{a}}^{'}} . \end{matrix}$ The smaller this set is, the less uncertainty there is about the input environment, and thus, the greater the knowledge of the ℓ-observer. This is depicted in Fig. 7. There, actions $a_{l_{1}}$ and $a_{l_{2}}$ , when observed by the ℓ-observer, reduce the uncertainty about the secrets in the input environment, and thus leak information to ℓ.

As more actions are observed, knowledge monotonely increases.
Lemma 5.2.
$\forall R \in {≃_{}, \approx_{}}$ , $ℓ, s, e, \bar{a}, a ․ k_{ℓ}^{R} (s, e, \bar{a}) \supseteq k_{ℓ}^{R} (s, e, \bar{a} . a)$ .

As hinted above, if an ℓ-observer never obtains knowledge about ℓ-unobservable input by observing ℓ-observable parts of the system-environment interaction, then the system satisfies noninterference.
Definition 5.3.
s is $R$ - ${noninterfering}_{k}$ ( $s \in {NI}_{k}^{R}$ ) iff $\begin{matrix} \forall ℓ, e, \bar{a}, a ․ e ⊧ s \overset{\bar{a} . a}{\to} ⟹ k_{ℓ}^{R} (s, e, \bar{a}) = k_{ℓ}^{R} (s, e, \bar{a} . a) . \end{matrix}$

As the name suggests, this knowledge-based formalization of noninterference is equivalent to the two-run formalization given in Section 3.6.
Theorem 5.4.
$\forall R \in {≃_{}, \approx_{}}$ , $s ․ s \in {NI}_{k}^{R} ⟺ s \in {NI}^{R}$ .

Gradual release states that an ℓ-observer can only gain knowledge by observing release actions. In terms of Fig. 7, gradual release requires that $a_{l_{1}}, a_{l_{2}} \in A_{R}^{ℓ}$ .
Definition 5.5.
s satisfies $R$ -gradual release ( $s \in {GR}^{R}$ ) iff $\begin{matrix} \forall ℓ, e, \bar{a}, a ․ e ⊧ s \overset{\bar{a} . a}{\to} ⟹ a \notin A_{R}^{ℓ} ⟹ k_{ℓ}^{R} (s, e, \bar{a}) = k_{ℓ}^{R} (s, e, \bar{a} . a) . \end{matrix}$

By comparing Definitions 5.5 and 5.3, it is apparent that ${GR}^{R}$ weakens ${NI}^{R}$ by strengthening the antecedent of the implication such that the consequent needs only hold for nonrelease actions. Thus, for the class of s which do not release information, gradual release and noninterference are equivalent. This is known as the conservativeness principle of declassification [46] that stipulates that for systems with no information release, the security condition is equivalent to noninterference.
Corollary 5.6.
$\forall R \in {≃_{}, \approx_{}}$ , $s \notin {LTS}_{IO}^{_{R}} ․ s \in {GR}^{R} ⟺ s \in {NI}^{R}$ .

To restore the typical semantics of declassification (which does not make declassification an effect) in an s, we simply place s in a wrapper which withholds release actions, as per $W (s)$ , given below. $\begin{matrix} \frac{s \overset{a}{\to} s^{'} a \in A_{R}}{W (s) \overset{∙}{\to} W (s^{'})}, \frac{s \overset{a}{\to} s^{'} a \notin A_{R}}{W (s) \overset{a}{\to} W (s^{'})} . \end{matrix}$ We let $W (ϵ) = ϵ$ , $W (a . \bar{a}) = ∙ . W (\bar{a})$ if $a \in A_{R}$ , and $W (a . \bar{a}) = a . W (\bar{a})$ otherwise. When a system satisfies gradual release, withholding its release actions can only reduce the amount of information it releases.
Corollary 5.7.
$\forall R \in {≃_{}, \approx_{}}, s ․ s \in {GR}^{R} ⟹ \forall ℓ, e, \bar{a} ․ k_{ℓ}^{R} (W (s), e, W (\bar{a})) \supseteq k_{ℓ}^{R} (s, e, \bar{a})$ .
5.2. Full release

Gradual release provides a natural way to formalize where goals in untrusted blackbox systems. However, on its own, gradual release does not satisfy our what declassification goal. To see why, first consider the following program $p_{d 1}$ , with from-level $φ (c_{R}) = B$ and presence-level $π (c_{R}) = L$ .

This program is not secure; it leaks contextual information a through the presence of release action $c_{R}! b$ . If a $L$ -observer does not observe $c_{R}! b$ (after a certain number of computation steps, or upon observing the $L$ output in the progress-sensitive timing-insensitive case), then the $L$ -observer can infer that a is even. Fortunately, gradual release rejects $p_{d 1}$ . However, the following variant $p_{d 2}$ does satisfy gradual release.

Let $o$ (resp. $e$ ) be a bijection between the integers and the odd (resp. even) integers. Then l is odd iff $a mod 2 = 1$ . While the presence of the release action is invariant of $L$ -unobservables, this program leaks the sensitive context, a, through the value of the release action. Being a pure where condition, gradual release abstracts away the fact that these are different declassification statements (occurring in different lexical contexts). This is easier to see if we modify the program again, to $p_{d 3}$ , where $φ ({c_{R}}_{A}) = A$ , $φ ({c_{R}}_{B}) = B$ and $π ({c_{R}}_{A}) = π ({c_{R}}_{B}) = L$ , which is likewise not secure but accepted by gradual release.

Our declassification goals require further restrictions in addition to gradual release to limit what can be released during a release action.

Fig. 8.

Permitted flows to $C$ given $ρ = {(A, X), (B, Y)}$ .

To address the what dimension, we introduce a new model of declassification: full release. Unlike gradual release, full release has no particular interface a system must make use of. Full release treats a system as a black box, operates only on its inputs and outputs, and stipulates that all leaks in a system are in accordance with a predefined release policy, which is external to the system. This is a good match for our what declassification goal, which states that permitted leaks must be (able to be) provided independently of the system, since systems are not trusted.

A release policy ρ is a set of pairs $(ℓ, ℓ^{'})$ for which $ℓ ⋢ ℓ^{'}$ . These pairs define exceptions to the standard only-upwards flows policy that noninterference stipulates. For instance, when $ρ = {(A, L)}$ in $L_{AB}$ , ρ permits the standard only-upwards flows of information that noninterference permits, but furthermore permits information to leak from $A$ to $L$ . A release policy is therefore similar to the intransitive downgrading relation ⇝ used in intransitive noninterference [30,31]. Let $(⊑^{ρ})$ be defined as the reflexive transitive closure of $(⊑) \cup ρ$ . This relation expresses which flow paths become permitted once the leaks in ρ are permitted. This is illustrated in Fig. 8. When $ρ = \emptyset$ , then the permitted flow paths become $(⊑^{ρ}) = (⊑)$ , same as for noninterference. Thus (only) information with security levels in the C-L rectangular region of the lattice is permitted to flow to $C$ . However, if information is permitted to leak from A to X and from B to Y, then $ρ = {(A, X), (B, Y)}$ . Since $X ⊑ B$ and $Y ⊑ c$ , information with a label anywhere in the gray region of the lattice is permitted to flow to C. Assuming an ℓ-observer observes all information which can travel along permitted flow paths to ℓ, this leads to the following new notion of equivalence of environments.

Definition 5.8.

$e_{1}$ and $e_{2}$ are ρ-ℓ- $R$ -equivalent ( $e_{1} R_{ℓ}^{ρ} e_{2}$ ) iff $\forall ℓ^{'} ․ ℓ^{'} ⊑^{ρ} ℓ ⟹ e_{1} R_{ℓ^{'}} e_{2}$ .

Observe that we already have $\forall R \in {≃_{}, \approx_{}}, ℓ, e_{1}, e_{2} ․ e_{1} R_{ℓ} e_{2} ⟹ \forall ℓ^{'} ․ ℓ^{'} ⊑ ℓ ⟹ e_{1} R_{ℓ^{'}} e_{2}$ . The minute, yet key, difference is the ρ on the ⊑, which requires $e_{1} R_{ℓ^{'}} e_{2}$ furthermore holds for $ℓ^{'} ⋢ ℓ$ for which $ℓ^{'} ⊑^{ρ} ℓ$ .

Corollary 5.9.

$\forall R \in {≃_{}, \approx_{}}, ℓ, e_{1}, e_{2} ․ e_{1} R_{ℓ}^{\emptyset} e_{2} ⟺ e_{1} R_{ℓ} e_{2}$ .

The more leaks that are allowed, the stronger ρ-ℓ- $R$ -equivalence becomes.

Corollary 5.10.

$\forall R \in {≃_{}, \approx_{}}, ℓ, ρ, ρ^{'} ․ (⊑^{ρ}) \subseteq (⊑^{ρ^{'}}) ⟹ \forall e_{1}, e_{2} ․ e_{1} R_{ℓ}^{ρ^{'}} e_{2} ⟹ e_{1} R_{ℓ}^{ρ} e_{2}$ .

Together, this gives that ρ-ℓ- $R$ -equivalence is most relaxed when no leaks are allowed.

Corollary 5.11.

$\forall R \in {≃_{}, \approx_{}}, ℓ, e_{1}, e_{2}, ρ ․ e_{1} R_{ℓ}^{ρ} e_{2} ⟹ e_{1} R_{ℓ} e_{2}$ .

Full release states that inputs which are not permitted to flow to an ℓ-observer must not interfere with ℓ-observables.

Definition 5.12.

s satisfies $R$ -ρ-full release ( $s \in {FR}_{ρ}^{R}$ ) iff $\begin{matrix} \forall ℓ, e_{1}, e_{2} ․ e_{1} R_{ℓ}^{ρ} e_{2} ⟹ \forall {\bar{a}}_{1} ․ e_{1} ⊧ s \overset{{\bar{a}}_{1}}{\to} ⟹ \exists {\bar{a}}_{2} ․ e_{2} ⊧ s \overset{{\bar{a}}_{2}}{\to} \land {\bar{a}}_{1} R_{ℓ} {\bar{a}}_{2} . \end{matrix}$

By comparing Definitions 5.12 and 3.3, it is apparent that ${FR}_{ρ}^{R}$ , for any ρ, weakens ${NI}^{R}$ by strengthening the antecedent of the leftmost implication such that its consequent needs to hold for fewer environment pairs. To make this conservativeness of declassification [46] result clearer, we need to make two observations. First, when $ρ = \emptyset$ , $(⊑^{ρ}) = (⊑)$ , so $(R_{ℓ}^{ρ}) = (R_{ℓ})$ , and thus, ∅-full release is just noninterference.

Corollary 5.13.

$\forall R \in {≃_{}, \approx_{}}, s ․ s \in {FR}_{\emptyset}^{R} ⟺ s \in {NI}^{R}$ .

Second, the more leaks are allowed, the weaker full release becomes. Full release is thus monotonely weakening in the size of $(⊑^{ρ})$ .

Corollary 5.14.

$\forall R \in {≃_{}, \approx_{}}, ℓ, ρ, ρ^{'} ․ (⊑^{ρ}) \subseteq (⊑^{ρ^{'}}) ⟹ \forall s ․ s \in {FR}_{ρ}^{R} ⟹ s \in {FR}_{ρ^{'}}^{R}$ .

Together this shows that full release follows the conservativeness principle of declassification, for any ρ.

Corollary 5.15.

$\forall R \in {≃_{}, \approx_{}}, s ․ s \in {NI}^{R} ⟹ \forall ρ ․ s \in {FR}_{ρ}^{R}$ .

We close this section with a few examples that contrast full release against gradual release, highlight the main shortcoming of full release (that it is coarse-grained) and show the way these declassification goals complement each other.

Full release stipulates what information is allowed to leak. Thus, when the release policy does not allow a leak from ℓ to $ℓ^{'}$ , then a system satisfying full release can by no means leak from ℓ to $ℓ^{'}$ . For instance, full release rejects $p_{d 1}$ and $p_{d 2}$ when $ρ = {(B, L)}$ (correctly identifying the implicit flow of $A$ -information, present in the context of the declassification, to $B$ ), and rejects $p_{d 3}$ when $ρ = {(A, L), (B, L)}$ . However, full release does not place demands or restrictions on how leaks are made, i.e. whether or not they only occur where the system declares intent by performing a declassification action. For instance, the following two programs $p_{d 4}$ and $p_{d 5}$ are treated exactly the same way by full release, both accepted if $H ⊑^{ρ} L$ , and both rejected otherwise (with $φ (c_{R}) = H$ and $π (c_{R}) = L$ ).

Since gradual release rejects the former program (which leaks without declaring intent), and accepts the latter (which declares intent), the two models of declassification complement each other to a large extent. However, full release is restrictive when it comes to systems that declare intent for some leaks from ℓ to $ℓ^{'}$ , but not for other such leaks. For instance, consider the following variant $p_{d 6}$ of programs $p_{d 1}$ to $p_{d 3}$ .

Program $p_{d 6}$ satisfies gradual release, despite the leak. However, there is no ρ which makes full release accept $p_{d 5}$ and reject $p_{d 6}$ ; full release will always accept both of them if $H ⊑^{ρ} L$ , and reject both otherwise. Full release is therefore coarse-grained, allowing leaks in an all-or-nothing manner. It is, however, necessarily so; since systems are black boxes, full release cannot tell whether or not a system that leaks intentionally from $H$ to $L$ is unintentionally (or maliciously) encoding all $H$ input in that one leak.

5.3. Semantics

We now return to $SME$ to formalize a variant $SME$ with declassification support, ${SME}_{D}$ , which, in addition to enforcing $TSNI$ , enforces the declassification goals developed in the previous sections. The main challenge in developing ${SME}_{D}$ is the fact that ℓ-runs are black boxes: Consider a system which must leak a function of some $H$ inputs as part of its function. The only interface $SME$ has to the system are its effects (i.e. action labels); since systems are black boxes, $SME$ as-is cannot tell the system apart from another system which leaks a different function of $H$ inputs as part of its function, or one that does not need to leak at all, and therefore cannot provide to the $L$ -run only the (parts of) $H$ input the system needs to perform its function. If $SME$ provides some $H$ input to the $L$ run, a leak may occur. If $SME$ provides no $H$ input to the $L$ run, system functionality may break.

Our approach is to add to $SME$ an interface which a wrapped system can utilize to ask for permission to declassify information. The semantics of ${SME}_{D}$ are obtained by adding rules to the semantics of $SME$ for managing this interface. The ${SME}_{D}$ declassification interface assumes that the wrapped system exposes a piece of its plumbing – the declassifications – as effects which describe the declassifications and allow the context (in our case, ${SME}_{D}$ ) to manipulate them. Any attempt by an ℓ-run to leak information that ${SME}_{D}$ has not explicitly allowed will fail, due to the way ${SME}_{D}$ , like $SME$ , separates input at different security levels into independent runs.

Analogous to our approach to define the release interface between a system and gradual release in Section 5.1, we turn to our channel abstraction to define the effects of the declassification interface. The similarity of the two formalizations is no accident; we will later build an interface to gradual release on top of our declassification interface. Let $C_{D} \subseteq C$ be the set of declassification channels, ranged by $c_{D}$ , and let $A_{D} = {c_{D} ? v, c_{D}! v ∣ c_{D} \in C_{D} \land v \in V}$ be the set of declassification actions, ranged by $a_{D}$ . A declassification leaks information from one security level, to another. Let $φ (c_{D})$ denote the from-level, and $π (c_{D}) = κ (c_{D})$ denote the to-level of $c_{D}$ (φ is defined on both release- and declassification channels) (we will return to the $π (c_{D}) = κ (c_{D})$ assumption in Section 5.5). A particular $c_{D}$ can represent something as general as “declassify some $H$ information to $L$ ”, in which case $φ (c_{D}) = H$ and $π (c_{D}) = L$ , or something as specific as “declassify the first character in Alice’s password to Bob”, in which case e.g. $φ (c_{D}) = A$ (Alice) and $π (c_{D}) = B$ (Bob).

The semantics of ${SME}_{D}$ requires that systems expose their declassification plumbing to the declassification interface through declassification actions as follows. To declassify a value v from ℓ to $ℓ^{'}$ , the system first performs output $c_{D}! v$ , where $c_{D}$ , for which $φ (c_{D}) = ℓ$ and $π (c_{D}) = ℓ^{'}$ , represents the information being declassified. The systems should then block on input from $c_{D}$ . The following inference rule illustrates how the semantics of declassification, in a simple imperative language with I/O, can be given in a manner satisfying this requirement. Again, this construct is more fine-grained than the standard one, for the same reasons as the declassification construct given in Section 5.1 is. $\begin{matrix} \frac{(m, out c_{D} t) \overset{c_{D}! v}{\to} (m, skip)}{(m, x : = declassify (t, c_{D})) \overset{c_{D}! v}{\to} (m, x : = in c_{D})} . \end{matrix}$ To restore the typical semantics of declassification (which does not make declassification an effect) in a system s satisfying the above requirement, we simply place s in a wrapper which makes communication on declassification channels a feedback, as per $F (s)$ , given below. $\begin{matrix} \frac{s \overset{c_{D}! v}{\to} s^{'}}{F (s) \overset{∙}{\to} F (c_{D} ? v, s^{'})}, \frac{s \overset{c_{D} ? v}{\to} s^{'}}{F (c_{D} ? v, s) \overset{∙}{\to} F (s^{'})}, \frac{s \overset{a}{\to} s^{'} a \notin A_{D}}{F (s) \overset{a}{\to} F (s^{'})} . \end{matrix}$ However, the point of this requirement is that the immediate context of s, in our case ${SME}_{D}$ , can control which value actually gets declassified by feeding any value $v^{'}$ back into s in place of v. To illustrate how ${SME}_{D}$ uses this feature to only release values which pass through this declassification interface and that ${SME}_{D}$ allows, let $φ (c_{D}) = A$ , $π (c_{D}) = B$ , and assume the $B$ -run has announced a $c_{D}$ -declassification by performing $c_{D}! v_{B}$ . If the $A$ -run has already performed a corresponding $c_{D}! v_{A}$ , and ${SME}_{D}$ allows this declassification, ${SME}_{D}$ has the $B$ -run perform $c_{D} ? v_{A}$ as its next action. Otherwise, ${SME}_{D}$ has the $B$ -run perform $c_{D} ? d$ as its next action. Thereby, the system only leaks at the point of declassification (since declassification is nonblocking), and by separation, only leaks information available to the $A$ -run to the $B$ -run (as opposed to leaking, say, arbitrary $H$ information from the lexical context of the declassification statement). We will discuss the rationale for ${SME}_{D}$ making declassification actions nonblocking in Section 5.6.

This approach, and $F$ , only have the desired effect if s adheres to our declassification interface, by first performing an output on a $c_{D}$ , and subsequently performing input on $c_{D}$ . We define this class of s now.

Definition 5.16.
For all $s_{0}$ ,
$s_{0}$ is declassification-compliant iff $\forall {\bar{a}}_{0}, s ․ s_{0} \overset{{\bar{a}}_{0}}{\to} s ⟹$

$\forall \bar{a}, c_{D}, v ․$ $s \overset{\bar{a} . c_{D}! v}{\to}$ $⟹ \exists v^{'} ․ s \overset{\bar{a} . c_{D}! v . c_{D} ? v^{'}}{\to}$ , and

$\forall \bar{a}, c_{D}, v ․$ $s \overset{\bar{a} . c_{D} ? v}{\to}$ $⟹ \exists v^{'}, {\bar{a}}^{'} ․ \bar{a} = {\bar{a}}^{'} . c_{D}! v^{'}$ .

$s_{0}$ is declassifying ( $s_{0} \in {LTS}_{IO}^{_{D}}$ ) iff $\exists \bar{a}, a_{D} ․ s_{0} \overset{\bar{a} . a_{D}}{\to}$ .

Unless stated otherwise, any s we consider in this paper is declassification-compliant. We parameterise ${SME}_{D}$ with a set $δ \subseteq C_{D}$ of desired declassifications, which ${SME}_{D}$ consults upon encountering a declassification announcement; if $c_{D} \notin δ$ , the declassification is turned into a feedback. Let $δ_{ℓ} = {c_{D} \in δ ∣ π (c_{D}) ⊑ ℓ \land φ (c_{D}) ⋢ ℓ}$ be the set of desired declassification channels which an ℓ-observer can observe the target, but not the source, of.

Fig. 9.
Semantics of ${SME}_{D}$ . (a) ${SME}_{D}$ ℓ-stepper. (b) ${SME}_{D}$ ℓ-chooser. (c) ${SME}_{D}$ history.

The semantics of ${SME}_{D}$ is given in Fig. 9. A ${SME}_{D}$ state is the same as a $SME$ state; the only new component, δ, is stateless, and used to instantiate the semantics of ${SME}_{D}$ . Note that ${SME}_{D} (σ, s, δ)$ interacts only on communication channels, that is, ${SME}_{D} (σ, s, δ) \notin {LTS}_{IO}^{_{D}}$ ; all declassification channel interaction is handled internally. By ( $D$ -no), any undesired declassification is a feedback. Furthermore, when an ℓ-run requests a declassification on $c_{D}$ which is desirable, but which ℓ is not a valid target of, the request is a feedback. By ( $D$ - ${yes}_{d}$ ), when a valid target ℓ-run of a declassification $c_{D}$ needs the declassified value before the source $φ (c_{D})$ -run produces it, $d$ is declassified instead. Otherwise, by ( $D$ -yes), if a valid target of a declassification has already received $d$ for the declassification in question, so does the ℓ-run (either every valid target of a declassification that requests it gets the value produced by $φ (c_{D})$ (if one was produced), or none of them do). This is to prevent the presence or timing of a $c_{D}$ -declassification from leaking through the declassification action, analogous to our treatment of $M$ -output in $SME$ . Otherwise, $φ (c_{D})$ has already produced the value to be declassified into the ℓ-run, and no other valid target has requested the value before it got produced, so a declassification is made by transferring the declassified value from the $φ (c_{D})$ -run to the ℓ-run.
5.4. Soundness

We now show how ${SME}_{D}$ fits into our declassification models. Recall that ${SME}_{D}$ takes as parameter the set δ of desired declassifications defining what can be leaked, and that ${SME}_{D}$ utilizes rule ( $D$ - ${yes}_{d}$ ) or ( $D$ -yes) in Fig. 9(b) where a declassification occurs. To intentionally leak information, a system utilizes the declassification interface of ${SME}_{D}$ . This provides ${SME}_{D}$ with the information it needs to circumvent ℓ-run separation and support intentional release as a system feature, while at the same time only releasing information between security levels as desired by δ, which is our desired what goal. Furthermore, ${SME}_{D}$ only declassifies information using rules ( $D$ - ${yes}_{d}$ ) or ( $D$ -yes). This provides us with the information we need to prove that ${SME}_{D}$ only releases information through declassification actions, which is our desired where goal. We do this by making actions derived with ( $D$ - ${yes}_{d}$ ) and ( $D$ -yes) release actions, to interface ${SME}_{D}$ with gradual release.

We start with the what results. Let $ρ (δ) = {(φ (c_{D}), π (c_{D})) ∣ c_{D} \in δ}$ be the reconciled releases of δ. As per the discussion on the coarseness of full release at the end of Section 5.2, since systems are (possibly malicious) black boxes, and since there therefore is no way to know or control what $φ (c_{D})$ -information a system leaks through $c_{D}$ , any leakage of $φ (c_{D})$ -information to $π (c_{D})$ the system makes must be reconciled. Fortunately, $ρ (δ)$ are the only leaks ${SME}_{D}$ can make. Let ${FR}_{ρ} = {FR}_{ρ}^{≃_{}}$ .

Theorem 5.17.
$\forall δ, σ, s ․ {SME}_{D} (σ, s, δ) \in {FR}_{ρ (δ)}$ .
The proof of this theorem follows a similar pattern as the proof of Theorem 4.2, utilizing a lemma which is nearly identical to Lemma 4.3.

If a system does not utilize the declassification interface, running the system in ${SME}_{D}$ causes no information to be released; the resulting execution is noninterfering. This is a corollary of Theorem 4.2, since no step in a trace from ${SME}_{D} (σ, s, ρ)$ is derived using any of the new rules from Fig. 9.
Corollary 5.18.
$\forall δ, σ, s \notin {LTS}_{IO}^{_{D}} ․ {SME}_{D} (σ, s, δ) \in TSNI$ .

To provide our where results, we need to interface ${SME}_{D}$ with gradual release. Before we do that, we show how to interface the systems ${SME}_{D}$ operates on (i.e. declassification-compliant ones) with gradual release. We do this my creating a mapping from declassification-channels to release channels, as follows: Let $ϱ : C_{D} \to C_{R}$ be an injective function associating a release channel with each declassification channel, in such a way that the from- and to-levels match, that is, $φ (ϱ (c_{D})) = φ (c_{D})$ and $π (ϱ (c_{D})) = π (c_{D})$ (assume $C_{D}$ and $C_{R}$ are disjoint). Then, for the declassification semantics in Section 5.3, wrapping a declassifying system in the following declassification feedback $F_{R}$ will likewise perform a release action iff the system performs a declassification. $\begin{matrix} \frac{s \overset{c_{D}! v}{\to} s^{'}}{F_{R} (s) \overset{∙}{\to} F_{R} (c_{D} ? v, s^{'})}, \frac{ϱ (c_{D}) = c_{R} s \overset{c_{D} ? v}{\to} s^{'}}{F_{R} (c_{D} ? v, s) \overset{c_{R}! v}{\to} F_{R} (s^{'})}, \frac{s \overset{a}{\to} s^{'} a \notin A_{D}}{F_{R} (s) \overset{a}{\to} F_{R} (s^{'})} . \end{matrix}$ In ${SME}_{D}$ , there are, for each declassification, (potentially) multiple ℓ-runs receiving it. Since not all receiving runs are necessarily ready to receive it at the time the value being declassified is produced by the from-level-run, the value cannot be fed to all of them at once. Indeed, the presence of a particular declassification action in those receiving ℓ-runs can vary, and each such (non)reception can leak different information to different observers. Furthermore, performing a release action when the from-level creates the value to be declassified leaks the presence of the declassification action in the from-level. Therefore, we make the reception of a declassified value, by each valid target of said declassification, a separate release action. We overload $ϱ : C_{D} \to L ↛ C_{R}$ to a partial injective function (↛ denotes partial function) such that $ϱ (c_{D}, ℓ)$ is defined iff $c_{D} \in δ_{ℓ}$ , and such that $φ (ϱ (c_{D}, ℓ)) = φ (c_{D})$ and $π (ϱ (c_{D}, ℓ)) = ℓ$ . Rules ( $D$ - ${yes}_{d}$ ) and ( $D$ -yes) in Fig. 9(b) are responsible for providing a declassified value to a valid target. By modifying the conclusion of these rules from the form $\begin{matrix} \bar{a} ⊧ (ℓ . σ, S) \overset{∙}{\to} (σ, S [ℓ \mapsto ({\bar{a}}_{ℓ} . c_{D} ? v, s)]), \end{matrix}$ to the form $\begin{matrix} \bar{a} ⊧ (ℓ . σ, S) \overset{ϱ (c_{D}, ℓ)! v}{\to} (σ, S [ℓ \mapsto ({\bar{a}}_{ℓ} . c_{D} ? v, s)]), \end{matrix}$ we obtain a variant ${SME}_{R}$ of ${SME}_{D}$ which performs a release action iff a declassified value is provided to a valid target run.

We are now ready to present the where result. The following technical lemma is in the style of Lemma 4.3. It states that ${SME}_{R} (σ, s, δ)$ can, under all the environments which an ℓ-observer knows could have caused $\bar{a}$ , not only match $\bar{a}$ , but do so in such a way that all $ℓ^{'}$ -runs, for $ℓ^{'} ⊑ ℓ$ , are in exactly the same state. Let $k_{ℓ} = k_{ℓ}^{≃_{}}$ .
Lemma 5.19.
$\forall δ, σ, s ․$ $\begin{matrix} \begin{matrix} \forall e_{1}, {\bar{a}}_{1}, σ_{1}, S_{1} ․ e_{1} ⊧ {SME}_{R} (σ, s, δ) \overset{}{\to} ({\bar{a}}_{1}, σ_{1}, S_{1}) ⟹ \forall ℓ, e_{2} ․ e_{2} \in k_{ℓ} ({SME}_{R} (σ, s, δ), e_{1}, {\bar{a}}_{1}) ⟹ \\ \exists {\bar{a}}_{2}, σ_{2}, S_{2} ․ e_{2} ⊧ {SME}_{R} (σ, s, δ) \overset{}{\to} ({\bar{a}}_{2}, σ_{2}, S_{2}) \land {\bar{a}}_{1} =_{ℓ}^{} {\bar{a}}_{2} \land σ_{1} = σ_{2} \land S_{1} =_{ℓ} S_{2} . \end{matrix} \end{matrix}$

We now have that ${SME}_{R}$ enforces gradual release, for any desired declassifications. Let $GR = {GR}^{≃_{}}$ .
Theorem 5.20.
$\forall δ, σ, s ․ {SME}_{R} (σ, s, δ) \in GR$ .

Thus, ${SME}_{D}$ only releases information through declassifications. Our instrumentation of ${SME}_{D}$ with release actions was done to provide the where guarantee we needed. In practice, however, release actions will not be present in the ${SME}_{D}$ of any system. To show that our instrumentation is nothing more than a tool to reason about where information leaks occur, we show that ${SME}_{D}$ leaks at most as much as ${SME}_{R}$ . First, for any list of actions ${SME}_{R}$ can perform, ${SME}_{D}$ can perform that same sequence of actions with release actions withheld. This follows from the definition of ${SME}_{R}$ .
Corollary 5.21.
$\forall δ, σ, s, e, \bar{a} ․$ $\begin{matrix} e ⊧ {SME}_{D} (σ, s, δ) \overset{\bar{a}}{\to} ⟹ \exists! {\bar{a}}^{'} ․ e ⊧ {SME}_{R} (σ, s, δ) \overset{{\bar{a}}^{'}}{\to} \land W ({\bar{a}}^{'}) = \bar{a} . \end{matrix}$

We refer to the ${\bar{a}}^{'}$ in the above corollary as $R (\bar{a})$ . The following result is what we are after. It follows from the above and Corollary 5.7.
Corollary 5.22.
$\forall δ, σ, s, e, \bar{a} ․$ $\begin{matrix} e ⊧ {SME}_{D} (σ, s, δ) \overset{\bar{a}}{\to} ⟹ k_{ℓ} ({SME}_{D} (σ, s, δ), e, \bar{a}) \subseteq k_{ℓ} ({SME}_{R} (σ, s, δ), e, R (\bar{a})) . \end{matrix}$

In summary, our full release soundness result states that the only leaks ${SME}_{D}$ can have are those declared as desired during instantiation of ${SME}_{D}$ , and our gradual release soundness result states that ${SME}_{D}$ only leaks through desired declassification actions. This, plus the way ${SME}_{D}$ otherwise separates information like $SME$ , ensures that ℓ-runs only leak information that has been declassified to them, and thus cannot leak arbitrary contextual information. For instance, in program $p_{d 1}$ , the ${SME}_{D}$ of $p_{d 1}$ allows the declassification but prevents the implicit flow of a at the same time! This is a fruitful byproduct of our what model of declassification and the separation of computation into ℓ-runs; the $B$ -run never obtains $A$ -information, and thus cannot leak it (not even implicitly). At last, ${SME}_{D}$ of the following program, with $δ = {c_{D}}$ , $π (c_{D}) = L$ and $φ (c_{D}) = H$ , allows the announced declassification, but stops the explicit flow. This follows from our where guarantee and $SME$ separation; the $L$ -run receives dummy values as input on $M$ , and only receives the right $h_{1}$ value where the declassification occurs.
5.5. Transparency

The new declassification features we added to $SME$ introduce new circumstances under which transparency is broken. If a system attempts a declassification which ${SME}_{D}$ does not reconcile, then ${SME}_{D}$ will deny the declassification by feeding $d$ to the to-run, thus breaking transparency. However, ${SME}_{D}$ can impede transparency even if all releases made by a system are reconciled. By Corollary 5.18, when s attempts to leak information without utilizing the declassification interface, the corresponding control in ${SME}_{D} (σ, s, δ)$ never receives the declassified value. For instance, with $δ = {c_{D} ∣ π (c_{D}) = L \land φ (c_{D}) = H}$ , consider the system s defined by program $p_{d 4}$ in Section 5.2. We have $s \in {FR}_{ρ (δ)}$ (i.e. if we reconcile all releases made by s, s is otherwise secure). However, the $L$ -run in ${SME}_{D} (σ, s, δ)$ never gets the $H$ -value in the $M$ -input, and thus, ${SME}_{D} (σ, s, δ)$ cannot be transparent. Thus $s \in {FR}_{ρ (δ)}$ is too weak an assumption to guarantee that ${SME}_{D} (σ, s, δ)$ is transparent. What is needed is a property stipulating that a system only releases information through its declassification interface. By design, this property is $TSNI$ ! Due to the assumption in Section 5.3 that $π (c_{D}) = κ (c_{D})$ for all $c_{D}$ , $TSNI$ assumes that an ℓ-observer who can observe the to-level of a declassification also observes the values being declassified. So for declassifying systems, $TSNI$ says that if we fix declassified values arbitrarily, no information is released. This implies that $TSNI$ systems do not release non-declassified values, i.e., for $TSNI$ systems, release is only possible through the declassification interface. However, even if we assume $TSNI$ , a similar problem arises when the $L$ -run reaches a declassification before the $H$ -run does; then the $L$ -run instead receives $d$ . This occurs in the ${SME}_{D}$ of $p_{d 5}$ from Section 5.2 ( $c_{R}$ replaced with $c_{D}$ ) if $L$ is scheduled too often before $H$ . Fortunately, we can rule out this scenario by assuming high-lead schedulers.

It turns out that these three scenarios – (1) ${SME}_{D}$ preventing undesired declassifications, (2) systems not utilizing the declassification interface to leak, and (3) the to-level of a release reaching the declassification action before the from-level does – are the only inhibitors for transparency. So by assuming high-lead scheding, that $s \in TSNI$ , and that all declassifications attempted by s are desired by ${SME}_{D}$ (that is, $δ = {c_{D} ∣ \exists \bar{a}, v ․ s \overset{\bar{a} . c_{D}! v}{\to}}$ ), we get transparency – that is, that the interaction on ℓ-presence channels, of s under ${SME}_{D}$ cf. s with declassification channels in feedback, is ℓ-equivalent.

Theorem 5.23.
$\forall σ \in HLS, s \in TSNI, e, \bar{a} ․$ , with $δ (s) = {c_{D} ∣ \exists \bar{a}, v ․ s \overset{\bar{a} . c_{D}! v}{\to}}$ ,
$e ⊧ F (s) \overset{\bar{a}}{\to}$ $⟹ \exists {\bar{a}}^{'} ․$ $e ⊧ {SME}_{D} (δ (s), σ, s) \overset{{\bar{a}}^{'}}{\to}$ $\land \forall ℓ ․ \bar{a} ⩽_{⋆, π^{- 1} (ℓ), ∙} {\bar{a}}^{'}$ ,

$e ⊧ {SME}_{D} (δ (s), σ, s) \overset{\bar{a}}{\to}$ $⟹ \exists {\bar{a}}^{'} ․$ $e ⊧ F (s) \overset{{\bar{a}}^{'}}{\to}$ $\land \forall ℓ ․ \bar{a} ⩽_{⋆, π^{- 1} (ℓ), ∙} {\bar{a}}^{'}$ .

Program $p_{d 5}$ satisfies $TSNI$ ; when $c_{D}$ input (which has $L$ presence and content) is fixed by the environment, changes in $H$ input do not affect the value declassified. Also, the presence of the declassification action does not depend on $L$ -unobservables. It is easy to see that if $σ \in HLS$ and $δ = {c_{D}}$ , then ${SME}_{D}$ of $p_{d 5}$ routes the value announced by the $H$ -run (which is the actual value received on $M$ ) to the $L$ -run in the desired way, thus yielding a transparent run. When $δ = \emptyset$ , ${SME}_{D}$ of $p_{d 5}$ stops the forbidden declassification to preserve soundness. Since $δ \neq δ (s)$ , our transparency result does not guarantee transparency. Indeed, transparency does not hold, since in ${SME}_{D}$ , the declassification is prevented.

To further clarify the scope of the above transparency result, it is worth noting that there are programs which, when declassification is a noninteraction, satisfy $TSNI$ , but when their declassification plumbing is pulled out to adhere to the ${SME}_{D}$ declassification interface, do not satisfy $TSNI$ ; the following modification $p_{d 7}$ of $p_{d 5}$ is such a program.

If $c_{D}$ is made into feedback, the result is a program which is not in ${LTS}_{IO}^{_{D}}$ and satisfies $TSNI$ (and thus has no leaks). However, without said feedback, since the program compares the value it received on $c_{D}$ with the value it sent on $c_{D}$ , the program fails to satisfy $TSNI$ , so ${SME}_{D}$ does not have to be transparent for it. Indeed, as it turns out, the ${SME}_{D}$ of this program attempts to leak whether the actual $M$ -input received by the ${SME}_{D}$ of $p_{d 7}$ equals $d$ or not (which δ then either permits or prevents), so ${SME}_{D}$ of $p_{d 7}$ , while sound for any δ, is not transparent. Thus, $TSNI$ for programs in ${LTS}_{IO}^{_{D}}$ requires that a program can, without causing further leaks, let an arbitrary value (provided by the environment, independent of program state) be the result of executing a declassify statement. This rules out programs that behave like $p_{d 7}$ . This is needed by ${SME}_{D}$ since ${SME}_{D}$ ensures that the $L$ -run never gets the $H$ input it needs to construct the correct value to be declassified, to ensure that the only $H$ values the $L$ -run gets are ones that have been declassified. Without this assumption on s, ${SME}_{D}$ can only guarantee soundness, not transparency. This explains why we did not assume $F (s) \in TSNI$ in our transparency result (which is otherwise more natural). On a related note, this approach seems to be one way of resolving the issues with the scrambling declassification semantics of (qualified) robustness [32] mentioned by Sabelfeld and Sands [46].
5.6. Blocking on declassification

We close this section with a justification for the part of the semantics of ${SME}_{D}$ which makes declassification actions performed by ℓ-runs nonblocking operations. Consider a variant ${SME}_{D}^{'}$ of ${SME}_{D}$ which does block the to-level-run of a declassification until the from-level-run has produced the value to be declassified. To keep the justification concrete, we consider only the $L_{L H}$ below, and note that the justifications generalize to arbitrary lattices.

It turns out that ${SME}_{D}^{'}$ is both transparent and sound. The transparency proof is the same as for ${SME}_{D}$ (since, as noted at the end of as noted in Section 3.5, no $L$ actions are permitted to follow a $H$ input in secure programs). The soundness proof applies if we have ${SME}_{D}^{'}$ produce a release action each time the $L$ -run is scheduled while blocking on a declassified value. The reason why this change to the soundness proof is needed – and the reason we chose to have ${SME}_{D}$ make declassifications nonblocking – is that the nonpresence of the declassification output from the $H$ -run can leak 1 bit about the state of the $H$ -run, each time the $L$ -run is scheduled, until the $H$ -run produces a value to be declassified. This bit could be all the information contained in the $H$ -run state, and this could be a different bit every time the $L$ -run is scheduled, as is the case in the below program, for scheduler ${(H . L)}^{\infty}$ (which we assume is known to the attacker).

In contrast, ${SME}_{D}$ leaks at most the whole state of the H-run once for each declassify action the L-run attempts (in the above example, one bit). We find that with the declassification semantics in ${SME}_{D}^{'}$ , it is harder to assess what and how much is leaked (e.g. when the program running under ${SME}_{D}^{'}$ is white-box), as the leak for a single declassify action can continue over time, forever. Hence we settled for ${SME}_{D}$ .

6. Full transparency

This section shows how to achieve full transparency for secure multi-execution by barrier synchronization. Full transparency, in contrast to per-channel or per-level transparency, guarantees that our $SME$ enforcement preserves the I/O behavior of secure programs, including the ordering of I/O messages. Thanks to such a strong property, we are able to deploy $SME$ to detect attacks.

Fig. 10.

$SME$ with barrier synchronization.

The core idea is pictorially summarized in Fig. 10. In contrast to Fig. 2, we are not ignoring the low output produced by the high run. Instead, we match it with the low output produced by the low run. If the program is secure, this approach guarantees that there will not be any deviation in this matching. Thus, if there is a deviation, it must be due to the insecurity of the original program. From this deviation, we can construct a counterexample to noninterference.

6.1. Semantics

A counterexample to $s \in {NI}^{R}$ is a proof of the logic negation of $s \in {NI}^{R}$ . That is, a level of observation ℓ, two $R_{ℓ}$ -equivalent environments, and a trace which s can perform under one of those environments, but cannot $R_{ℓ}$ -match under the other. We refer to such a counterexample as an $R$ -attack on s.

Definition 6.1.
An $R$ -attack α is a 4-tuple $(ℓ, e_{1}, e_{2}, {\bar{a}}_{1})$ with $e_{1} R_{ℓ} e_{2}$ and $e_{1} ⊧ {\bar{a}}_{1}$ . The attack is an $R$ -attack on s iff
$e_{1} ⊧ s \overset{{\bar{a}}_{1}}{\to}$ , and

$\forall {\bar{a}}_{2} ․ e_{2} ⊧ s \overset{{\bar{a}}_{2}}{\to} ⟹ \neg ({\bar{a}}_{2} R_{ℓ} {\bar{a}}_{1})$ .

We now formalize our variant of $SME$ , ${SME}_{T}$ , which can construct attacks on run-time. Its semantics for a two-point lattice is given in Fig. 11. ${SME}_{T}$ adds two new components to the $SME$ -state, ${\bar{α}}_{1}$ and ${\bar{α}}_{2}$ , which contain the list of (potential) attacks discovered so far, making the ${SME}_{T}$ -state a quintuple $(\bar{a}, σ, S, {\bar{α}}_{1}, {\bar{α}}_{2})$ . The semantics works as follows. While nothing inhibits the $H$ -run from performing non- $L$ -presence actions (by ( $H$ -a) and (∙)), a barrier forms when the $H$ -run reaches a $L$ -presence action (by ( $H$ -block)). The $H$ -run then only proceeds once the $L$ -run reaches a $L$ -presence action. When the $L$ -run reaches a $L$ -presence action, and the $H$ -run is yet to perform the corresponding action, a barrier forms (by ( $L$ -wait)). The $L$ -run then only proceeds once the $H$ -run has done one of two things. (1) reached an $L$ -observable action before advancing t steps beyond the $L$ -run (by ( $L$ -a)), or (2) advanced t steps without reaching a $L$ -observable action (by ( $L$ -timeout)). In (1), if the $H$ -run reached a $L$ -observably different action, we note the discrepancy in ${\bar{α}}_{1}$ . The $H$ -run will then be replaced by infinite silence (by (conflict)). In (2), we note the timeout in ${\bar{α}}_{2}$ . Input environments are constructed from traces using $E$ , defined as ${(E (\bar{a}))}_{c} = (\bar{a} ↾_{?, c}) . {(c ? ⋆)}^{\infty}$ .

Fig. 11.
Semantics of ${SME}_{T}$ . (a) ${SME}_{T} ℓ$ -stepper. (b) ${SME}_{T} ℓ$ -chooser. (c) ${SME}_{T}$ history.

Not every attack discovered by ${SME}_{T} (s)$ is an attack on s; we will establish when a discovered attack is an attack on s in Section 6.4.
6.2. Soundness

${SME}_{T}$ enforces $PSNI$ . This is easily seen by observing that the traces produced by $e ⊧ {SME}_{T} (s)$ and $e ↾_{L} ⊧ s$ are $\approx_{L}$ -equivalent. By allowing the $L$ -run to wait up to t steps for the $H$ -run to match an $L$ -observable, ${SME}_{T}$ $(s)$ introduces a timing leak into s when $t > 0$ , and thus does not enforce $TSNI$ .

Theorem 6.2.
$\forall s, σ ․ {SME}_{T} (σ, s) \in PSNI$ .

We note, however, that ${SME}_{T}$ does enforces $TSNI$ when $t = 0$ , and that the attacks discovered are $≃_{}$ -attacks. We find, however, that ${SME}_{T}$ becomes less practical with $t = 0$ , since ${SME}_{T}$ is much more likely to detect timeouts or discrepancies; when ${SME}_{T}$ detects these, ${SME}_{T}$ “freezes” the $H$ -run to avoid leaks, making the $H$ -run semantically equivalent to a program producing ∙ infinitely, by (conflict). A more practical version of ${SME}_{T}$ would instead have the $H$ -run behave like it would under $SME$ $(s)$ henceforth. We hypothesize (but do not prove) that this modification of ${SME}_{T}$ yields a sound enforcement. In any case, this weakening of the soundness guarantee compared to $SME$ is easily controlled by simply wrapping ${SME}_{T} (σ, s)$ in a blackbox timing leak mitigator [4].
6.3. Transparency

Modulo ∙, ${SME}_{T}$ $(s)$ and s produce the same sequence of I/O (up to discrepancy or timeout in ${SME}_{T}$ $(s)$ ). This holds even when s is not secure. Point (a) below states that ${SME}_{T}$ cannot break transparency without producing an attack on s, and Point (b) states that any trace that s can perform under ${SME}_{T}$ which does not produce an attack, can be matched by s not running under ${SME}_{T}$ .

Theorem 6.3.
$\forall σ, s, e, \bar{a} ․$
$e ⊧ s \overset{\bar{a}}{\to} ⟹ ∄ {\bar{a}}^{'} ․ e ⊧ {SME}_{T} (σ, s) \overset{}{\to} ({\bar{a}}^{'}, ˍ, ˍ, ϵ, ϵ) \land {\bar{a}}^{'} ≰_{⋆, ∙} \bar{a} \land \bar{a} ≰_{⋆, ∙} {\bar{a}}^{'}$ ,

$e ⊧ {SME}_{T} (σ, s) \overset{}{\to} (\bar{a}, ˍ, ˍ, ϵ, ϵ) ⟹ \exists {\bar{a}}^{'} ․ e ⊧ s \overset{{\bar{a}}^{'}}{\to} \land \bar{a} =_{⋆, ∙} {\bar{a}}^{'}$ .

A corollary of the above is that if $s \in TSNI$ , then s and ${SME}_{T} (σ, s)$ have the same (i.e. $=_{⋆, ∙}$ -equivalent) I/O behavior! This is because ${SME}_{T} (s)$ never generates attacks for $s \in TSNI$ . In contrast to e.g. Devriese and Piessens [20], who swap the order of outputs in the following two programs (for linearization $B ⊑ A$ ), we have full I/O correspondence between each program and its ${SME}_{T}$ .

However, the same I/O correspondence cannot hold in general if $s \in PSNI$ , since it is impossible (without solving the Turing halting problem) to determine whether the $H$ -run is taking forever, or just a very long time, to match the $L$ action by the $L$ -run. This can be demonstrated by the following $PSNI$ program; for any predetermined value of t, there is an input on $M$ for which ${SME}_{T}$ of the program times out while waiting for the $H$ -run to reach the $L$ output statement.
6.4. Attacks

It is important to note that even when s is not secure, running s under ${SME}_{T}$ does not guarantee attack discovery; the ${SME}_{T}$ of s might take branches of control in such a way that insecure states are never entered, and ${SME}_{T}$ only detects attacks along the control flow path that its ℓ-runs take. However, if ${SME}_{T}$ does detect a discrepancy between the $H$ -run and the $L$ -run on which $L$ -observable comes next (before a timeout has occurred), then ${SME}_{T}$ has indeed found a concrete proof that $s \notin PSNI$ .

Theorem 6.4.
$\forall s, σ, e ․ e ⊧ {SME}_{T} (σ, s) \overset{}{\to} (ˍ, ˍ, ˍ, α, ϵ) ⟹ α$ is an $\approx_{}$ -attack on s.

This theorem states that if the first attack discovered is a discrepancy, then the discrepancy is an $\approx_{}$ -attack on s. Further discrepancies discovered before timeouts are discovered are $\approx_{}$ -attack on s as well; we focused on the first attack in the above theorem since attacks discovered later may simply be extensions of the first attack. Unfortunately, as discussed above, we cannot infer in general that a timeout is an attack on s. Likewise, if a timeout is discovered before a discrepancy, we cannot conclude that the discrepancy is an attack on s, since the discrepancy might be the consequence of a timeout, which is not necessarily the basis of a leak in s.

We end this section with two $PSNI$ -insecure programs, and describe the attacks which ${SME}_{T}$ finds on them. Consider the following program.

With $d = 0$ , $t = 100$ and initial input 1, ${SME}_{T} (s)$ generates an $\approx_{}$ -attack $(L, e_{1}, e_{2}, M ? d . L! 0)$ on s in ${\bar{α}}_{1}$ , where $e_{1} (M) = M ? d . {(M ? ⋆)}^{\infty}$ , $e_{2} (M) = M ? 1 . {(M ? ⋆)}^{\infty}$ . Now consider the following program.

With $d = 0$ , $t = 100$ and initial input $- 1$ , ${SME}_{T} (s)$ generates an $\approx_{}$ -attack $(L, e_{1}, e_{2}, M ? d . ∙ . L! 0)$ on s in ${\bar{α}}_{2}$ , where $e_{1} (M) = M ? d . {(M ? ⋆)}^{\infty}$ , $e_{2} (M) = M ? - 1 . {(M ? ⋆)}^{\infty}$ . With initial input 5, no attack is generated. With initial input 500, however, an attack is generated which is not an attack on s (it merely took “too long” for the $H$ -run to match $L! 0$ ).
7. Related work

Referring the reader for general overviews on language-based information-flow security [43], on dynamic information-flow control [26], and on declassification [46], we focus on related work on multi-execution.

Li and Zdancewic [29] observe that “a noninterfering program $f (h, l)$ can usually be factored to a ‘high security’ part $f_{H} (h, l)$ and a ‘low security part’ $f_{L} (l)$ that does not use any of the high-level inputs h. As a result, noninterference can be proved by transforming the program into a special form that does not depend on the high-level input”. They propose relaxed noninterference that allows information release through a set of prescribed syntactic expressions. Their focus is on enforcing relaxed noninterference statically, by a security type system.

Russo et al. [40] sketch the idea of running multiple runs of a program, where each run corresponds to the computation of information at a security level. They discuss that by running the public computation ahead of the secret run, certain classes of timing attacks can be prevented.

Capizzi et al. [16] consider enforcement of secure information flow in the setting of an operating system. The enforcement is based on shadow executions as operating system processes for different security levels. They report on an implementation and an experimental study with benchmarks.

As discussed earlier, Devriese and Piessens [20] develop a general treatment of secure multi-execution at the application level and establish soundness and precision under the assumption of total environments (there is always new input), linear lattices and low priority scheduling.

Bielova et al. [12] investigate multi-execution in a reactive setting. Bielova et al.’s model multi-executes Featherweight Firefox [14], a formalization of a web browser as a reactive system. The environments of Bielova et al. are not necessarily total, but the security guarantee is weaker (than Devriese and Piessens’ [20]): termination-insensitive noninterference. The I/O model targets the browser setting, with handlers under cooperative scheduling. The full version [13] contains an informal discussion of what the authors call sub-input-event security policies, which corresponds to more flexible policies on input events (flexible policies on output events are not considered). These policies are defined by projections that describe how much is visible at each level. This mechanism is however not formalized. A formalization would require reasoning about policy consistency: for example, projections for less restrictive levels should not reveal more than projections for more restrictive levels.

Kashyap et al. [25] show that the low-priority scheduling might exhibit timing leaks for non-linear security lattices, and present several sound schedulers. We show (Appendix A) that in the presence of handlers, it is not necessary for the lattice to be non-linear to produce attacks on the low-priority scheduler. Timing leaks can freely occur in linear lattices, including the simple low-high lattice.

Jaskelioff and Russo [24] implement a monadic library for secure multi-execution in Haskell. Austin and Flanagan [7] introduce faceted values to simulate secure multi-execution by execution on enriched values. Faceted values can be projected to the different security levels. The projection theorem assures that a computation over faceted values faithfully simulates non-faceted computations. They show that faceted values guarantee termination-insensitive noninterference. Faceted values have been implemented in practical programming languages: for JavaScript by Austin and Flanagan, and for Jeeves [54] by Austin et al. [8]. Faceted values provide a viable alternative for an efficient implementation of our technique. Austin and Flanagan also show how to relax noninterference by facet declassification, based on robust declassification [33,56]. Robust declassification operates on both confidentiality and integrity labels, requiring the decision to declassify to be trusted. This leads to the introduction of integrity labels to model trust and integrity checks that the declassification operation is not influenced by untrusted data. This corresponds to the who dimension of declassification [46]. Compared to this approach, our declassification has aspects of what is declassified and where in the lattice and in the code information release may take place. We are able to capitalize on what secure multi-execution is best at: built-in security against implicit flows. No matter where in the code declassification occurs, it will not leak information about the context. There is no need to track the integrity of the code in our model.

Barthe et al. [11] present a “whitebox” approach to secure multi-execution. They devise a transformation that guarantees noninterference via secure multi-execution for programs in a language with communication and dynamic code evaluation primitives

De Groef et al. [18] implement secure multi-execution as an extension of the Firefox browser and report on experiments with browsing the web. Compared to the work by Bielova et al. [12] discussed above, De Groef et al. multi-execute the actual scripts in web pages rather than the entire browser. The main focus of their experiments is to confirm that the enforcement of simple policies does not modify the behavior of secure pages.

Compared to the work above, this paper enriches secure multi-execution with the following features: (i) channels with distinct presence and content security levels, (ii) the what dimension of declassification for secure multi-execution, (iii) full transparency results that preserve the order of messages, and (iv) show how secure multi-execution can be used to detect attacks. To the best of our knowledge, none of these features have been previously explored in the context of secure multi-execution.

This paper stands on the ground laid by our previous work [37] on the foundations of security for interactive programs. This earlier work presents a general framework for environments as strategies, lifts the assumptions of the total environment, and distinguishes between the security level of message presence and content in the general setting. While the previous work provides an excellent starting point for the present paper, it does not treat secure multi-execution.

Performance-wise, like Devriese and Piessens [20], the time complexity of our approach is linear in the size of the security lattice, since a process is created for each lattice element. That being said, when the size of the lattice is smaller than the number of CPU cores, the overhead of our approach is negligible, and can even yield an improvement since runs synchronize less with the environment. This is indicated by benchmarks performed by Devriese and Piessens, which are portable to our setting.

Unno et al. [51] focus on the problem of finding counterexamples against noninterference: pairs of input states that agree on the public parts and lead to paths that disagree on public outputs. Their technique combines type-based analysis and model checking to explore execution paths for programs that may cause insecure information flow. They show that this method is more efficient than model checking alone. In comparison, our attack-detection technique does not require program analysis and allows reasoning about the security of individual runs.

In an independent effort, Zanarini et al. [55] apply secure multi-execution for program monitoring in a reactive setting modeled by interaction trees. This work relates to our attack detection results, although it focuses on a more relaxed, progress-insensitive, security condition. Given a program, the goal is to construct a scheduler for secure multi-execution that mimics the execution of the original program. Whenever a deviation is detected, the execution is blocked to avoid leakage. This approach enforces progress-insensitive noninterference.

Most recently, Vanhoef et al. [52] have investigated an approach to declassification in secure multi-execution. This is accomplished through escape hatch [44] expressions, provided as policies for release, separately from code. Only through these expressions it is possible to declassify information to lower and incomparable security levels. This allows expressing what is released in a fine-grained fashion, but does not allow controlling where in the program the release may take place. Our approach is more coarse-grained for specifying what is released (per-level granularity rather than per-expression), yet it has the benefit of ensuring that information release takes place only at designated declassification points, thus also controlling where information can be declassified.

8. Conclusion

Secure multi-execution emerges as a promising technique for enforcing secure information flow. We have overviewed the pros and cons of secure multi-executions and identified most pressing challenges with it. This paper pushes the boundary of what can be achieved with secure multi-execution. First, we lift the assumption from the original secure multi-execution work on the totality of the input environment (that there is always assumed to be input) and on cooperative scheduling. Second, we generalize secure multi-execution to distinguish between security levels of presence and content of messages. Third, we introduce a declassification model for secure multi-execution that allows expressing what information can be released and where in the program the release can take place. We prove that declassification only affects the declared security levels and that our declassification mechanism restricts release to program points with declassification annotations. Fourth, we establish a full transparency result by barrier synchronization of the runs at different security levels. Full transparency guarantees that secure multi-execution preserves the original order of messages in secure programs. We demonstrate that full transparency is a key enabler for discovering attacks with secure multi-execution.

Representing reactive systems in our setting is an interesting topic of future work. In a reactive setting, an incoming input event determines which handler may be triggered. We can model this by tagging input values with a channel ID. The program can then pattern-match on the tag to dispatch the value to the handler associated with the channel.

Future work also includes implementation and case studies. We plan to experiment with modifying the Firefox browser to accommodate fine-grained, declassification-aware, and transparent secure multi-execution. The modification will allow us to multi-execute JavaScript code in an environment with preemptive scheduling of the runs at different levels.

Footnotes

Acknowledgments

Thanks are due to Frank Piessens for generous feedback, and to Daniel Hedin, and David Sands for the useful discussions. This work was funded by the European Community under the ProSecuToR and WebSand projects, by the Swedish research agencies SSF and VR, the US Naval Research award no. N000141310156 and NSF grant award no. CNS1320470.

FlowFox leak

The leak exploits the fact that FlowFox [18] multi-executes JavaScript with the low-priority scheduler on a per-event basis. Low priority implies that the low run is executed first and without preemption. The low-priority scheduler first applies to the main code. If the main code sets event handlers, they are processed after the multi-execution of the main code. Low handlers are multi-executed. High handlers are only run once, at the high level.

Note that the problem with low-priority scheduling is fundamental because it is not possible to extend the low-priority discipline over multiple events – simply because it is not possible to run the low handlers that have not yet been triggered.

The security theorem in the abstract setting of secure multi-execution [20] takes advantage of the low-priority scheduler and establishes timing-sensitive security. This is intuitive because the last access of the low data occurs before any high data is accessed. This implies that whenever the timing behavior is affected by secrets, there is no possibility for the attacker to inspect the difference.

We show that the situation is different in the presence of handlers. All we need to do is to set a low handler to execute after the high run for the main code has finished. Then the low handler can inspect the computation time taken by the high run. For a simple experiment, we consider the default example policy from the FlowFox distribution1

https://distrinet.cs.kuleuven.be/software/FlowFox/.

in Listing 1. The listing omits the non-customizable part of the policy, focusing on the sources and sinks. This policy defines same-origin domain as HIGH and cross-origin domains as LOW (line 16). In order to protect cookies, secret sources are defined by labeling document.cookie as HIGH (line 19). Lines 20 and 21 define the sinks that correspond to setting the source attributes of image and script HTML elements. These are labeled as HIGH for the same origin and LOW for the other origins. The intention is to prevent attacks that leak information about the cookie to third-party web sites (any sites other than the site of the web page origin).

Nevertheless, the code in the web page in Listing 2 leaks one bit of information about the cookie to the third-party web site attacker.com. Function getTime() of the $Date$ object returns the number of milliseconds since the midnight of January 1, 1970. First, information about the cookie flows via document.cookie into variable $h$ (line 8). Depending on the value of $h$ , the program might take longer time to execute (line 10). As foreshadowed below, all we need to do is to get a time stamp at the beginning of execution (line 4) and after the high run has finished. The difference in time reveals whether $h$ was zero. In order to bypass FlowFox’s multi-execution, we simply create a low handler (line 5) to perform the final time measurement (line 15). Running this page in FlowFox results in a request for an image with URL http://attacker.com?v=496 (repetitive runs show slight fluctuation around the value of 496). Running the code with line 7 uncommented and line 6 commented out, results in a request for an image with URL http://attacker.com?v=6 (repetitive runs fluctuate insignificantly around the value of 6). Hence, we can reliably leak one bit of secret information about the cookies. Clearly, the leak can be easily magnified to leak the entire cookie by walking through it bit-by-bit in a simple loop and sending the results for each bit to the attacker.

Note that changing the policy for getTime() to return HIGH result does not close the timing leak. The leak can be still achieved exploiting the difference in the internal timing behavior by a combination of low handlers [41].

While the leak outlined above is achieved by issuing a timeout event, other events (such as user-generated events and XMLHttpRequest) can be used to achieve the same effect.

The low-priority scheduler is both at the heart of the soundness results by Devriese and Piessens [20] and at the heart of FlowFox [18]. The experiment points to a fundamental problem with low-priority scheduling. The leak demonstrates that the low-priority scheduler breaks timing-sensitive security and motivates the need for (fair) interleaving of the runs at different levels, as pursued in this paper.

Projections

A projection applies as far left as possible (unless indicated otherwise with parentheses). For instance, $\bar{a} . {\bar{a}}^{'} ↾_{}$ means $(\bar{a} . {\bar{a}}^{'}) ↾_{}$ , not $\bar{a} . ({\bar{a}}^{'} ↾_{})$ . For all projections, $ϵ ↾_{} = ϵ$ . Let $ range over ? and !. The projection functions used throughout the paper and appendix are then as given in Fig. 12.

Proofs

In the following lemma, $S_{1} =_{ℓ} S_{2}$ iff $\forall ℓ^{'} ⊑^{ρ} ℓ ․ S_{1} (ℓ^{'}) = S_{2} (ℓ^{'})$ .

Let $B (e, s)$ behave like s except when s performs input on a declassification channel; that input is then drawn from e. In effect, B binds declassification channels internally. Let $B (e, s) = B (ϵ, e, s)$ . $\begin{array}{l} \frac{s \overset{o}{\to} s^{'} o \in A_{D}}{B (\bar{a}, e, s) \overset{∙}{\to} B (\bar{a} . o, e, s^{'})}, \frac{s \overset{i}{\to} s^{'} i \in A_{D} e ⊧ \bar{a} . i}{B (\bar{a}, e, s) \overset{∙}{\to} B (\bar{a} . i, e, s^{'})}, \frac{s \overset{a}{\to} s^{'} a \notin A_{D}}{B (\bar{a}, e, s) \overset{a}{\to} B (\bar{a} . a, e, s^{'})} . \end{array}$

References

[1]

Agat, Transforming out timing leaks, in: Proc. ACM Symp. on Principles of Programming Languages, 2000, pp. 40–53.

[2]

Askarov and

Sabelfeld, Gradual release: Unifying declassification, encryption and key release policies, in: Proc. IEEE Symp. on Security and Privacy, 2007, pp. 207–221.

[3]

Askarov and

Sabelfeld, Tight enforcement of information-release policies for dynamic languages, in: Proc. IEEE Computer Security Foundations Symposium, 2009.

[4]

Askarov,

Zhang and

A.C.

Myers, Predictive black-box mitigation of timing channels, in: CCS, 2010.

[5]

T.H.

Austin and

Flanagan, Efficient purely-dynamic information flow analysis, in: Proc. ACM Workshop on Programming Languages and Analysis for Security (PLAS), 2009.

[6]

T.H.

Austin and

Flanagan, Permissive dynamic information flow analysis, in: Proc. ACM Workshop on Programming Languages and Analysis for Security (PLAS), 2010.

[7]

T.H.

Austin and

Flanagan, Multiple facets for dynamic information flow, in: Proc. ACM Symp. on Principles of Programming Languages, 2012, pp. 165–178.

[8]

T.H.

Austin,

Yang,

Flanagan and

Solar-Lezama, Faceted execution of policy-agnostic programs, in: Proc. ACM Workshop on Programming Languages and Analysis for Security (PLAS), ACM, New York, NY, USA, 2013, pp. 15–26.

[9]

Banerjee,

Naumann and

Rosenberg, Expressive declassification policies and modular static enforcement, in: Proc. IEEE Symp. on Security and Privacy, 2008.

10.

[10]

Barnes, High Integrity Software: The SPARK Approach to Safety and Security, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 2003.

11.

[11]

Barthe,

J.M.

Crespo,

Devriese,

Piessens and

Rivas, Secure multi-execution through static program transformation, in: Formal Techniques for Distributed Systems (FMOODS/FORTE 2012), LNCS, Vol. 7273, 2012, pp. 186–202.

12.

[12]

Bielova,

Devriese,

Massacci and

Piessens, Reactive non-interference for a browser model, in: Proc. 5th International Conference on Network and System Security (NSS), 2011.

13.

[13]

Bielova,

Devriese,

Massacci and

Piessens, Reactive non-interference for the browser: Extended version, Technical Report CW602, CS Dept., K.U. Leuven, 2011.

14.

[14]

Bohannon and

B.C.

Pierce, Featherweight Firefox: Formalizing the core of a web browser, in: Proc. USENIX Conference on Web Application Development, 2010.

15.

[15]

Bohannon,

B.C.

Pierce,

Sjöberg,

Weirich and

Zdancewic, Reactive noninterference, in: ACM Conference on Computer and Communications Security, 2009, pp. 79–90.

16.

[16]

Capizzi,

Longo,

V.N.

Venkatakrishnan and

Prasad Sistla, Preventing information leaks through shadow executions, in: Annual Computer Security Applications Conference (ACSAC), 2008, pp. 322–331.

17.

[17]

Clark and

Hunt, Noninterference for deterministic interactive programs, in: Workshop on Formal Aspects in Security and Trust (FAST’08), 2008.

18.

[18]

De Groef,

Devriese,

Nikiforakis and

Piessens, FlowFox: A web browser with flexible and precise information flow control, in: ACM Conference on Computer and Communications Security, 2012.

19.

[19]

D.E.

Denning, A lattice model of secure information flow, Comm. of the ACM 19(5) (1976), 236–243.

20.

[20]

Devriese and

Piessens, Non-interference through secure multi-execution, in: Proc. IEEE Symp. on Security and Privacy, 2010.

21.

[21]

Dima,

Enea and

Gramatovici, Nondeterministic nointerference and deducible information flow, Technical Report 2006-01, LACL, University of Paris 12, 2006.

22.

[22]

J.A.

Goguen and

Meseguer, Security policies and security models, in: Proc. IEEE Symp. on Security and Privacy, 1982, pp. 11–20.

23.

[23]

Hedin and

Sabelfeld, Information-flow security for a core of Javascript, in: Proc. IEEE Computer Security Foundations Symposium, 2012, pp. 3–18.

24.

[24]

Jaskelioff and

Russo, Secure multi-execution in Haskell, in: Proc. Andrei Ershov International Conference on Perspectives of System Informatics, LNCS, Vol. 7162, Springer-Verlag, 2011, pp. 170–178.

25.

[25]

Kashyap,

Wiedermann and

Hardekopf, Timing- and termination-sensitive secure information flow: Exploring a new approach, in: Proc. IEEE Symp. on Security and Privacy, 2011.

26.

[26]

Le Guernic, Confidentiality enforcement using dynamic information flow analyses, PhD thesis, Kansas State University, 2007.

27.

[27]

Le Guernic, Automaton-based confidentiality monitoring of concurrent programs, in: Proc. IEEE Computer Security Foundations Symposium, 2007, pp. 218–232.

28.

[28]

Le Guernic,

Banerjee,

Jensen and

Schmidt, Automata-based confidentiality monitoring, in: Proc. Asian Computing Science Conference (ASIAN’06), LNCS, Vol. 4435, Springer-Verlag, 2006.

29.

[29]

Li and

Zdancewic, Downgrading policies and relaxed noninterference, in: Proc. ACM Symp. on Principles of Programming Languages, 2005, pp. 158–170.

30.

[30]

Mantel, Information flow control and applications – Bridging a gap, in: Proc. Formal Methods Europe, LNCS, Vol. 2021, Springer-Verlag, 2001, pp. 153–172.

31.

[31]

Mantel and

Sands, Controlled downgrading based on intransitive (non)interference, in: Proc. Asian Symp. on Programming Languages and Systems, LNCS, Vol. 3302, Springer-Verlag, 2004, pp. 129–145.

32.

[32]

A.C.

Myers,

Sabelfeld and

Zdancewic, Enforcing robust declassification, in: Proc. IEEE Computer Security Foundations Workshop, 2004, pp. 172–186.

33.

[33]

A.C.

Myers,

Sabelfeld and

Zdancewic, Enforcing robust declassification and qualified robustness, J. Computer Security 14(2) (2006), 157–196.

34.

[34]

A.C.

Myers,

Zheng,

Zdancewic,

Chong and

Nystrom, Jif: Java information flow. Software release, 2001, available at: http://www.cs.cornell.edu/jif.

35.

[35]

Nikiforakis,

Invernizzi,

Kapravelos,

Van Acker,

Joosen,

Kruegel,

Piessens and

Vigna, You are what you include: Large-scale evaluation of remote Javascript inclusions, in: ACM Conference on Computer and Communications Security, 2012, pp. 736–747.

36.

[36]

O’Neill,

Clarkson and

Chong, Information-flow security for interactive programs, in: Proc. IEEE Computer Security Foundations Workshop, 2006, pp. 190–201.

37.

[37]

Rafnsson,

Hedin and

Sabelfeld, Securing interactive programs, in: Proc. IEEE Computer Security Foundations Symposium, 2012.

38.

[38]

Rafnsson and

Sabelfeld, Limiting information leakage in event-based communication, in: Proc. ACM Workshop on Programming Languages and Analysis for Security (PLAS), 2011.

39.

[39]

Rafnsson and

Sabelfeld, Secure multi-execution: Fine-grained, declassification-aware, and transparent, in: Proc. IEEE Computer Security Foundations Symposium, 2013, pp. 3–18.

40.

[40]

Russo,

Hughes,

Naumann and

Sabelfeld, Closing internal timing channels by transformation, in: Proc. Asian Computing Science Conference (ASIAN’06), LNCS, Vol. 4435, Springer-Verlag, 2007.

41.

[41]

Russo and

Sabelfeld, Securing timeout instructions in web applications, in: Proc. IEEE Computer Security Foundations Symposium, 2009.

42.

[42]

Russo and

Sabelfeld, Dynamic vs. static flow-sensitive security analysis, in: Proc. IEEE Computer Security Foundations Symposium, 2010.

43.

[43]

Sabelfeld and

A.C.

Myers, Language-based information-flow security, IEEE J. Selected Areas in Communications 21(1) (2003), 5–19.

44.

[44]

Sabelfeld and

A.C.

Myers, A model for delimited information release, in: Proc. International Symp. on Software Security (ISSS’03), LNCS, Vol. 3233, Springer-Verlag, 2004, pp. 174–191.

45.

[45]

Sabelfeld and

Russo, From dynamic to static and back: Riding the roller coaster of information-flow control research, in: Proc. Andrei Ershov International Conference on Perspectives of System Informatics, LNCS, Vol. 5947, Springer-Verlag, 2009.

46.

[46]

Sabelfeld and

Sands, Declassification: Dimensions and principles, J. Computer Security 17(5) (2009), 517–548.

47.

[47]

Shroff,

Smith and

Thober, Dynamic dependency monitoring to secure information flow, in: Proc. IEEE Computer Security Foundations Symposium, 2007, pp. 203–217.

48.

[48]

Simonet, The Flow Caml system. Software release, 2003, available at: http://cristal.inria.fr/~simonet/soft/flowcaml.

49.

[49]

Singer and

Duhigg, Tracking voters’ clicks online to try to sway them, 2012, available at: http://www.nytimes.com/2012/10/28/us/politics/tracking-clicks-online-to-try-to-sway-voters.html.

50.

[50]Syrian Electronic Army uses Taboola ad to hack Reuters (again), available at: https://nakedsecurity.sophos.com/2014/06/23/syrian-electronic-army-uses-taboola-ad-to-hack-reuters-again/.

51.

[51]

Unno,

Kobayashi and

Yonezawa, Combining type-based analysis and model checking for finding counterexamples against non-interference, in: Proc. ACM Workshop on Programming Languages and Analysis for Security (PLAS), 2006, pp. 17–26.

52.

[52]

Vanhoef,

De Groef,

Devriese,

Piessens and

Rezk, Stateful declassification policies for event-driven programs, in: CSF, 2014.

53.

[53]

Volpano,

Smith and

Irvine, A sound type system for secure flow analysis, J. Computer Security 4(3) (1996), 167–187.

54.

[54]

Yang,

Yessenov and

Solar-Lezama, A language for automatically enforcing privacy policies, in: POPL, 2012, pp. 85–96.

55.

[55]

Zanarini,

Jaskelioff and

Russo, Precise enforcement of confidentiality for reactive system, in: Proc. IEEE Computer Security Foundations Symposium, 2013.

56.

[56]

Zdancewic and

A.C.

Myers, Robust declassification, in: Proc. IEEE Computer Security Foundations Workshop, 2001, pp. 15–23.