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

3.1. Input–output labeled transition systems

Our model of computation is a labeled transition system ( LTS ). An LTS is a triple ( S , L , → ) , where S is a set (of states), L is a set (of labels), and → ⊆ S × L × S (a labeled transition relation). Computation occurs in discrete steps (transitions), each taking a (unspecified) unit of time. We write s → l s ′ iff ( s , l , s ′ ) ∈ → , and s → l iff s → l 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. a : : = i ∣ o i : : = c ? v o : : = c ! v ∣ ∙ 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.

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.

OPEN IN VIEWER

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 ) ⊑ ℓ ). a ¯ ↾ ℓ removes ℓ-unobservable parts of actions in a ¯ . For a ¯ = ∙ . L ? 0 . H ! 1 . M ? ⋆ . M ! 2 . H ? ⋆ . ∙ , 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 ∈ V ), since a L -observer only observes presence of messages on M (all a ∈ { M ! v ∣ v ∈ 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. a ¯ ↾ ⋆ replaces all c ? ⋆ with ∙. With a ¯ defined as above, a ¯ ↾ ⋆ = ∙ . L ? 0 . H ! 1 . ∙ . M ! 2 . ∙ . ∙ .

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

Since this program can perform a ¯ 1 and a ¯ 2 , this program is not secure against a timing-sensitive L -observer since a ¯ 1 ↾ ⋆ , L , ∙ → = ∙ . ∙ . L ! 0 ≠ ∙ . L ! 0 = a ¯ 2 ↾ ⋆ , L , ∙ → ( L ! 0 is produced faster in the latter trace).

A progress-sensitive (e.g. [3,36,38]) attacker observes whether more observables are forthcoming. a ¯ ↾ ∙ removes all ∙ from a ¯ . With a ¯ as above, a ¯ ↾ ∙ = L ? 0 . H ! 1 . M ? ⋆ . M ! 2 . H ? ⋆ . Define progress-sensitive ℓ-equivalence ≈ ℓ as = ⋆ , ℓ , ∙ . a ¯ 1 and a ¯ 2 are not evidence that the above program is insecure against progress-sensitive ℓ-observers; a ¯ 1 ↾ ⋆ , L , ∙ = L ! 0 = 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 ( ≃ ℓ ) ⊊ ( ≈ ℓ ) .

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 a ¯ is possible under a given environment e. Intuitively, a ¯ is possible under e if, for any c, (1) the c-inputs in a ¯ are (in value and order) as provided by e, (2) each c-input occurs no sooner in 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, a ¯ is consistent with e, written e ⊧ a ¯ , iff for all c, we have for all ∀ a ¯ ′ ⩽ a ¯ , with i ¯ ′ = e c , | a ¯ ′ | , that a ¯ ′ ≠ ˍ . c ? ⋆ ⟹ a ¯ ′ ⩽ ? , c , ⋆ , ∙ i ¯ ′ , and a ¯ ′ = ˍ . c ? ⋆ ⟹ a ¯ ′ = ? , c , ⋆ , ∙ i ¯ ′ ∧ i ¯ ′ = ˍ . c ? ⋆ . This states that for each prefix a ¯ ′ of a ¯ and each c, the list of non-blank inputs in a ¯ ′ must prefix the list of non-blank inputs in the same-length prefix i ¯ ′ of e ( c ) , and that a ¯ ′ ends with a blank input on c only if all c-inputs provided by e up to this point are in a ¯ ′ and e provided no new c-inputs in time unit | a ¯ ′ | ( ˍ is a wildcard). The quantification and definition of a ¯ ′ and i ¯ ′ formalizes (2), the trace equivalences formalize (1), and the 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 a ¯ under e, written e ⊧ s → a ¯ , iff s → a ¯ and e ⊧ a ¯ . Let s be the initial state of the following program.

Let e 1 c , … , e 5 c be defined as on the left below. Then the judgments on the right hold. e 1 c = ( c ? ⋆ ) ∞ , e 1 ⊧ s → ( c ? ⋆ ) n for all n ∈ N , e 2 c = c ? 0 . c ? 0 . ( c ? ⋆ ) ∞ , e 2 ⊧ s → c ? 0 . ∙ . c ? 0 , e 3 c = c ? 2 . c ? 0 . ( c ? ⋆ ) ∞ , e 3 ⊧ s → c ? 2 . ∙ . ∙ . ∙ . ∙ . ∙ . c ? 0 , e 4 c = c ? 0 . c ? ⋆ . c ? ⋆ . c ? ⋆ . c ? 0 . ( c ? ⋆ ) ∞ , e 4 ⊧ s → c ? 0 . ∙ . c ? ⋆ . c ? ⋆ . c ? 0 , e 5 c = c ? 2 . c ? ⋆ . c ? ⋆ . c ? ⋆ . c ? 0 . ( c ? ⋆ ) ∞ , e 5 ⊧ s → c ? 2 . ∙ . ∙ . ∙ . ∙ . ∙ . c ? 0 . These judgments hold regardless of how e k c ′ for 1 ⩽ k ⩽ 5 and c ′ ≠ 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: e 1 ≃ ℓ e 2 iff ∀ c ․ π ( c ) ⊑ ℓ ⟹ e 1 ( c ) ≃ ℓ e 2 ( c ) , e 1 ≈ ℓ e 2 iff ∀ c ․ π ( c ) ⊑ ℓ ⟹ e 1 ( c ) ≈ ℓ e 2 ( c ) .

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 ? ⋆ ) ∞ and e 2 H = e 1 c = e 2 c = ( c ? ⋆ ) ∞ for all c ≠ H . While this program can perform H ? 0 . L ! 0 under e 1 , the program cannot perform an ≈ 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 ≈ (both security-level-indexed equivalence relations on traces and environments) in place of R .

Definition 3.3.

s is R -noninterfering ( s ∈ NI R ) iff ∀ ℓ , e 1 , e 2 ․ e 1 R ℓ e 2 ⟹ ∀ a ¯ 1 ․ e 1 ⊧ s → a ¯ 1 ⟹ ∃ a ¯ 2 ․ e 2 ⊧ s → a ¯ 2 ∧ a ¯ 1 R ℓ a ¯ 2 .

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 ∈ TSNI ) iff s ∈ NI ≃ .

Definition 3.5.

s is timing-insensitive, progress sensitive noninterfering ( s ∈ PSNI ) iff s ∈ NI ≈ .

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.

∀ s ․ s ∈ TSNI ⟹ s ∈ 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 ≈ 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.

OPEN IN VIEWER

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 ) ≠ ℓ 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 ) ≠ κ ( 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 ∀ σ ∈ S ( σ 0 ) ․

∀ ℓ , σ 1 , σ 2 ․ σ → ℓ σ 1 ∧ σ → ℓ σ 2 ⟹ σ 1 = σ 2 , and

∀ ℓ , ℓ ′ ․ σ → ℓ ∧ σ → ℓ ′ ⟹ ℓ = ℓ ′ .

σ 0 is fair iff ∀ σ ∈ S ( σ 0 ) ․

∀ ℓ ¯ ․ σ → ℓ ¯ ⟹ ∀ ℓ ․ ∃ ℓ ¯ ′ ․ σ → ℓ ¯ . ℓ ¯ ′ . ℓ .

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 σ → ℓ σ ′ 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 ) ∞ and ( L . H ) ∞ are deterministic fair schedulers (that repeat H . L resp. L . H , infinitely).

OPEN IN VIEWER

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 ( a ¯ , σ , S ) , where 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 ( a ¯ ℓ , s ℓ ) , where 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 ) = ( ϵ , σ , λ ℓ → ( ϵ , 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 a ¯ which SME ( σ , s ) has had with the environment. Note that SME ( σ , s ) → a ¯ ( a ¯ ′ , σ ′ , s ′ ) ⟹ a ¯ = a ¯ ′ , so we sometimes omit the trace label on a SME transition. We put a ¯ on the left side of “⊧” in the next layer of the semantics, Fig. 5(b), to show that this layer only reads 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 ≠ ℓ 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 ≠ ⋆ ∧ κ ( 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 ) ≠ π ( 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 ∈ π − 1 ( ℓ ) , since SME ( s ) performs I/O iff the ℓ-run of s performs it. Each ℓ-run makes input on each c ∈ π − 1 ( ℓ ) and output on each c ∈ κ − 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 ∈ κ − 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 ∈ π − 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.

∀ σ , s ․ SME ( σ , s ) ∈ 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 = 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 ∀ ℓ ′ ⊑ ℓ ․ S 1 ( ℓ ′ ) = S 2 ( ℓ ′ ) .

Lemma 4.3.

∀ σ , s , ℓ , e 1 , e 2 ․ e 1 ≃ ℓ e 2 ⟹ ∀ a ¯ 1 , σ 1 , S 1 ․ e 1 ⊧ SME ( σ , s ) → ( a ¯ 1 , σ 1 , S 1 ) ⟹ ∃ a ¯ 2 , σ 2 , S 2 ․ e 2 ⊧ SME ( σ , s ) → ( a ¯ 2 , σ 2 , S 2 ) ∧ a ¯ 1 = ℓ a ¯ 2 ∧ S 1 = ℓ S 2 ∧ σ 1 = σ 2 .

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 ( e ↾ ℓ ′ ) ( c ) = ( c ? d ) ∞ , if π ( c ) ⋢ ℓ ′ , e ( c ) ↾ ℓ , otherwise. (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 ∈ PSNI , ℓ, e and σ be arbitrary. In s and SME ( σ , s ) , the interaction on ℓ-presence channels is ℓ-equivalent.

Theorem 4.4.

∀ σ , s ∈ PSNI , e , a ¯ ․

e ⊧ s → a ¯ ⟹ ∃ a ¯ ′ ․ e ⊧ SME ( σ , s ) → a ¯ ′ ∧ ∀ ℓ ․ a ¯ ⩽ ⋆ , ℓ , π − 1 ( ℓ ) , ∙ a ¯ ′ ,

e ⊧ SME ( σ , s ) → a ¯ ⟹ ∃ a ¯ ′ ․ e ⊧ s → a ¯ ′ ∧ ∀ ℓ ․ a ¯ ⩽ ⋆ , ℓ , π − 1 ( ℓ ) , ∙ 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 ∈ 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 , ℓ ¯ ) , the predicate yields 1 when ℓ L and ℓ H have been scheduled in such a manner in ℓ ¯ , and 0 otherwise. ϕ ( ˍ , ˍ , ˍ , ϵ ) = 1 ϕ ( ℓ H , ℓ L , b H seen , ℓ . ℓ ¯ ) ∣ ℓ = ℓ H = ϕ ( ℓ H , ℓ L , 1 , ℓ ¯ ) ∣ ℓ = ℓ L ∧ b H seen = ϕ ( ℓ H , ℓ L , 0 , ℓ ¯ ) ∣ ℓ = ℓ L ∧ ¬ b H seen = 0 ∣ otherwise = ϕ ( ℓ H , ℓ L , b H seen , ℓ ¯ ) This formalization achieves this effect by walking through ℓ ¯ , 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 ( σ ∈ HLS ) iff ∀ ℓ ¯ ․ σ → ℓ ¯ ⟹ ∀ ℓ L , ℓ H ․ ℓ L ⊏ ℓ H ⟹ ϕ ( ℓ H , ℓ L , 0 , ℓ ¯ ) .

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 ∈ TSNI , the interaction on ℓ-presence channels in and SME ( σ , s ) is the same, for all ℓ.

Theorem 4.6.

∀ σ ∈ HLS , s ∈ TSNI , e , a ¯ ․

e ⊧ s → a ¯ ⟹ ∃ a ¯ ′ ․ e ⊧ SME ( σ , s ) → a ¯ ′ ∧ ∀ ℓ ․ a ¯ ⩽ ⋆ , π − 1 ( ℓ ) , ∙ a ¯ ′ ,

e ⊧ SME ( σ , s ) → a ¯ ⟹ ∃ a ¯ ′ ․ e ⊧ s → a ¯ ′ ∧ ∀ ℓ ․ a ¯ ⩽ ⋆ , π − 1 ( ℓ ) , ∙ a ¯ ′ .

Thus, if SME puts a d in an M output when run using σ ∈ 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.

OPEN IN VIEWER

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 ⊆ C be the set of release channels, ranged by c R , and let A R = { c R ? v , c R ! v ∣ c R ∈ C R ∧ v ∈ 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. A R ℓ = { a R ∈ A R ∣ π ( a R ) ⊑ ℓ ∧ φ ( a R ) ⋢ ℓ } . 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. ( m , x : = t ) → ∙ ( m ′ , skip ) m ′ ( x ) = v ( m , x : = declassify ( t , c R ) ) → c R ! v ( m ′ , skip ) 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 ∀ s ∈ S ( s 0 ) ․ ∀ a ¯ , i ․ s → a ¯ . i ⟹ i ∉ A R .

s 0 is releasing ( s ∈ LTS IO R )iff ∃ a ¯ , a R ․ s → a ¯ . a R .

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

OPEN IN VIEWER

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 a ¯ performed by a system s under environment e as the set k ℓ R ( s , e , a ¯ ) of input environments under which those observables were possible: k ℓ R ( s , e , a ¯ ) = { e ′ ∣ e R ℓ e ′ ∧ ∃ a ¯ ′ ․ e ′ ⊧ s → a ¯ ′ ∧ a ¯ R ℓ a ¯ ′ } . 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.

∀ R ∈ { ≃ , ≈ } , ℓ , s , e , a ¯ , a ․ k ℓ R ( s , e , a ¯ ) ⊇ k ℓ R ( s , e , 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 ∈ NI k R ) iff ∀ ℓ , e , a ¯ , a ․ e ⊧ s → a ¯ . a ⟹ k ℓ R ( s , e , a ¯ ) = k ℓ R ( s , e , a ¯ . a ) .

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.

∀ R ∈ { ≃ , ≈ } , s ․ s ∈ NI k R ⟺ s ∈ 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 ∈ A R ℓ .

Definition 5.5.

s satisfies R -gradual release ( s ∈ GR R ) iff ∀ ℓ , e , a ¯ , a ․ e ⊧ s → a ¯ . a ⟹ a ∉ A R ℓ ⟹ k ℓ R ( s , e , a ¯ ) = k ℓ R ( s , e , a ¯ . a ) .

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.

∀ R ∈ { ≃ , ≈ } , s ∉ LTS IO R ․ s ∈ GR R ⟺ s ∈ 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. s → a s ′ a ∈ A R W ( s ) → ∙ W ( s ′ ) , s → a s ′ a ∉ A R W ( s ) → a W ( s ′ ) . We let W ( ϵ ) = ϵ , W ( a . a ¯ ) = ∙ . W ( a ¯ ) if a ∈ A R , and W ( a . a ¯ ) = a . W ( a ¯ ) otherwise. When a system satisfies gradual release, withholding its release actions can only reduce the amount of information it releases.

Corollary 5.7.

∀ R ∈ { ≃ , ≈ } , s ․ s ∈ GR R ⟹ ∀ ℓ , e , a ¯ ․ k ℓ R ( W ( s ) , e , W ( a ¯ ) ) ⊇ k ℓ R ( s , e , 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.

OPEN IN VIEWER

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 ( ⊑ ) ∪ ρ . This relation expresses which flow paths become permitted once the leaks in ρ are permitted. This is illustrated in Fig. 8. When ρ = ∅ , 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 ∀ ℓ ′ ․ ℓ ′ ⊑ ρ ℓ ⟹ e 1 R ℓ ′ e 2 .

Observe that we already have ∀ R ∈ { ≃ , ≈ } , ℓ , e 1 , e 2 ․ e 1 R ℓ e 2 ⟹ ∀ ℓ ′ ․ ℓ ′ ⊑ ℓ ⟹ 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.

∀ R ∈ { ≃ , ≈ } , ℓ , e 1 , e 2 ․ e 1 R ℓ ∅ e 2 ⟺ e 1 R ℓ e 2 .

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

Corollary 5.10.

∀ R ∈ { ≃ , ≈ } , ℓ , ρ , ρ ′ ․ ( ⊑ ρ ) ⊆ ( ⊑ ρ ′ ) ⟹ ∀ 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.

∀ R ∈ { ≃ , ≈ } , ℓ , 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 ∈ FR ρ R ) iff ∀ ℓ , e 1 , e 2 ․ e 1 R ℓ ρ e 2 ⟹ ∀ a ¯ 1 ․ e 1 ⊧ s → a ¯ 1 ⟹ ∃ a ¯ 2 ․ e 2 ⊧ s → a ¯ 2 ∧ a ¯ 1 R ℓ a ¯ 2 .

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 ρ = ∅ , ( ⊑ ρ ) = ( ⊑ ) , so ( R ℓ ρ ) = ( R ℓ ) , and thus, ∅-full release is just noninterference.

Corollary 5.13.

∀ R ∈ { ≃ , ≈ } , s ․ s ∈ FR ∅ R ⟺ s ∈ 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.

∀ R ∈ { ≃ , ≈ } , ℓ , ρ , ρ ′ ․ ( ⊑ ρ ) ⊆ ( ⊑ ρ ′ ) ⟹ ∀ s ․ s ∈ FR ρ R ⟹ s ∈ FR ρ ′ R .

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

Corollary 5.15.

∀ R ∈ { ≃ , ≈ } , s ․ s ∈ NI R ⟹ ∀ ρ ․ s ∈ 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 ⊆ C be the set of declassification channels, ranged by c D , and let A D = { c D ? v , c D ! v ∣ c D ∈ C D ∧ v ∈ 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. ( m , out c D t ) → c D ! v ( m , skip ) ( m , x : = declassify ( t , c D ) ) → c D ! v ( m , x : = in c D ) . 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. s → c D ! v s ′ F ( s ) → ∙ F ( c D ? v , s ′ ) , s → c D ? v s ′ F ( c D ? v , s ) → ∙ F ( s ′ ) , s → a s ′ a ∉ A D F ( s ) → a F ( s ′ ) . 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 ∀ a ¯ 0 , s ․ s 0 → a ¯ 0 s ⟹

∀ a ¯ , c D , v ․ s → a ¯ . c D ! v ⟹ ∃ v ′ ․ s → a ¯ . c D ! v . c D ? v ′ , and

∀ a ¯ , c D , v ․ s → a ¯ . c D ? v ⟹ ∃ v ′ , a ¯ ′ ․ a ¯ = a ¯ ′ . c D ! v ′ .

s 0 is declassifying ( s 0 ∈ LTS IO D ) iff ∃ a ¯ , a D ․ s 0 → a ¯ . a D .

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

OPEN IN VIEWER

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 , δ ) ∉ 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 ∈ δ } 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.

∀ δ , σ , s ․ SME D ( σ , s , δ ) ∈ 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.

∀ δ , σ , s ∉ LTS IO D ․ SME D ( σ , s , δ ) ∈ 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 → 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. s → c D ! v s ′ F R ( s ) → ∙ F R ( c D ? v , s ′ ) , ϱ ( c D ) = c R s → c D ? v s ′ F R ( c D ? v , s ) → c R ! v F R ( s ′ ) , s → a s ′ a ∉ A D F R ( s ) → a F R ( s ′ ) . 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 → L ↛ C R to a partial injective function (↛ denotes partial function) such that ϱ ( c D , ℓ ) is defined iff c D ∈ δ ℓ , 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 a ¯ ⊧ ( ℓ . σ , S ) → ∙ ( σ , S [ ℓ ↦ ( a ¯ ℓ . c D ? v , s ) ] ) , to the form a ¯ ⊧ ( ℓ . σ , S ) → ϱ ( c D , ℓ ) ! v ( σ , S [ ℓ ↦ ( a ¯ ℓ . c D ? v , s ) ] ) , 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 a ¯ , not only match a ¯ , but do so in such a way that all ℓ ′ -runs, for ℓ ′ ⊑ ℓ , are in exactly the same state. Let k ℓ = k ℓ ≃ .

Lemma 5.19.

∀ δ , σ , s ․ ∀ e 1 , a ¯ 1 , σ 1 , S 1 ․ e 1 ⊧ SME R ( σ , s , δ ) → ( a ¯ 1 , σ 1 , S 1 ) ⟹ ∀ ℓ , e 2 ․ e 2 ∈ k ℓ ( SME R ( σ , s , δ ) , e 1 , a ¯ 1 ) ⟹ ∃ a ¯ 2 , σ 2 , S 2 ․ e 2 ⊧ SME R ( σ , s , δ ) → ( a ¯ 2 , σ 2 , S 2 ) ∧ a ¯ 1 = ℓ a ¯ 2 ∧ σ 1 = σ 2 ∧ S 1 = ℓ S 2 .

We now have that SME R enforces gradual release, for any desired declassifications. Let GR = GR ≃ .

Theorem 5.20.

∀ δ , σ , s ․ SME R ( σ , s , δ ) ∈ 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.

∀ δ , σ , s , e , a ¯ ․ e ⊧ SME D ( σ , s , δ ) → a ¯ ⟹ ∃ ! a ¯ ′ ․ e ⊧ SME R ( σ , s , δ ) → a ¯ ′ ∧ W ( a ¯ ′ ) = a ¯ .

We refer to the a ¯ ′ in the above corollary as R ( a ¯ ) . The following result is what we are after. It follows from the above and Corollary 5.7.

Corollary 5.22.

∀ δ , σ , s , e , a ¯ ․ e ⊧ SME D ( σ , s , δ ) → a ¯ ⟹ k ℓ ( SME D ( σ , s , δ ) , e , a ¯ ) ⊆ k ℓ ( SME R ( σ , s , δ ) , e , R ( a ¯ ) ) .

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 ∧ φ ( c D ) = H } , consider the system s defined by program p d 4 in Section 5.2. We have s ∈ 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 ∈ 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 ∈ TSNI , and that all declassifications attempted by s are desired by SME D (that is, δ = { c D ∣ ∃ a ¯ , v ․ s → a ¯ . c D ! v } ), 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.

∀ σ ∈ HLS , s ∈ TSNI , e , a ¯ ․ , with δ ( s ) = { c D ∣ ∃ a ¯ , v ․ s → a ¯ . c D ! v } ,

e ⊧ F ( s ) → a ¯ ⟹ ∃ a ¯ ′ ․   e ⊧ SME D ( δ ( s ) , σ , s ) → a ¯ ′ ∧ ∀ ℓ ․ a ¯ ⩽ ⋆ , π − 1 ( ℓ ) , ∙ a ¯ ′ ,

e ⊧ SME D ( δ ( s ) , σ , s ) → a ¯ ⟹ ∃ a ¯ ′ ․   e ⊧ F ( s ) → a ¯ ′ ∧ ∀ ℓ ․ a ¯ ⩽ ⋆ , π − 1 ( ℓ ) , ∙ 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 σ ∈ 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 δ = ∅ , SME D of p d 5 stops the forbidden declassification to preserve soundness. Since δ ≠ δ ( 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 ) ∈ 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 ) ∞ (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.

OPEN IN VIEWER

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 ∈ NI R is a proof of the logic negation of s ∈ 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 , a ¯ 1 ) with e 1 R ℓ e 2 and e 1 ⊧ a ¯ 1 . The attack is an R -attack on s iff

e 1 ⊧ s → a ¯ 1 , and

∀ a ¯ 2 ․ e 2 ⊧ s → a ¯ 2 ⟹ ¬ ( a ¯ 2 R ℓ 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, α ¯ 1 and α ¯ 2 , which contain the list of (potential) attacks discovered so far, making the SME T -state a quintuple ( a ¯ , σ , S , α ¯ 1 , α ¯ 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 α ¯ 1 . The H -run will then be replaced by infinite silence (by (conflict)). In (2), we note the timeout in α ¯ 2 . Input environments are constructed from traces using E , defined as ( E ( a ¯ ) ) c = ( a ¯ ↾ ? , c ) . ( c ? ⋆ ) ∞ .

OPEN IN VIEWER

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 ≈ 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.

∀ s , σ ․ SME T ( σ , s ) ∈ 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.

∀ σ , s , e , a ¯ ․

e ⊧ s → a ¯ ⟹ ∄ a ¯ ′ ․ e ⊧ SME T ( σ , s ) → ( a ¯ ′ , ˍ , ˍ , ϵ , ϵ ) ∧ a ¯ ′ ≰ ⋆ , ∙ a ¯ ∧ a ¯ ≰ ⋆ , ∙ a ¯ ′ ,

e ⊧ SME T ( σ , s ) → ( a ¯ , ˍ , ˍ , ϵ , ϵ ) ⟹ ∃ a ¯ ′ ․ e ⊧ s → a ¯ ′ ∧ a ¯ = ⋆ , ∙ a ¯ ′ .

A corollary of the above is that if s ∈ 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 ∈ 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 ∈ 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 ∉ PSNI .

Theorem 6.4.

∀ s , σ , e ․ e ⊧ SME T ( σ , s ) → ( ˍ , ˍ , ˍ , α , ϵ ) ⟹ α is an ≈ -attack on s.

This theorem states that if the first attack discovered is a discrepancy, then the discrepancy is an ≈ -attack on s. Further discrepancies discovered before timeouts are discovered are ≈ -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 ≈ -attack ( L , e 1 , e 2 , M ? d . L ! 0 ) on s in α ¯ 1 , where e 1 ( M ) = M ? d . ( M ? ⋆ ) ∞ , e 2 ( M ) = M ? 1 . ( M ? ⋆ ) ∞ . Now consider the following program.

With d = 0 , t = 100 and initial input − 1 , SME T ( s ) generates an ≈ -attack ( L , e 1 , e 2 , M ? d . ∙ . L ! 0 ) on s in α ¯ 2 , where e 1 ( M ) = M ? d . ( M ? ⋆ ) ∞ , e 2 ( M ) = M ? − 1 . ( M ? ⋆ ) ∞ . 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.