Foundations for Parallel Information Flow Control Runtime Systems

At a high level, the goal of an IFC system is to track and restrict the flow of information according to a security policy—almost always a form of non-interference [14]. Informally, this policy ensures confidentiality, i.e., secret data should not leak to public entities, and integrity, i.e., untrusted data should not affect trusted entities.

To this end, LIO tracks the flow of information at a coarse-granularity, by associating labels with threads. Implicitly, the thread label classifies all the values in its scope and reflects the sensitivity of the data that it has inspected. Indeed, LIO “raises” the label of a thread to accommodate for reading yet more sensitive data. For example, when a public thread reads secret data, its label is raised to secret—this reflects the fact that the rest of the thread computation may depend on sensitive data. Accordingly, LIO uses the thread’s current label or program counter label to restrict its communication. For example, a secret thread can only communicate with other secret threads.

In LIO, developers can express programs that manipulate data of varying sensitivity—for example programs that handle both public and secret data—by forking multiple threads, at run-time, as necessary. However, naively implementing concurrency in an IFC setting is dangerous: concurrency can amplify and internalize the termination covert channel [1, 58], for example, by allowing public threads to observe whether or not secret threads terminated. Moreover, concurrency often introduces internal timing covert channels wherein secret threads leak information by influencing the scheduling behavior of public threads. Both classes of covert channels are high-bandwidth and easy to exploit.

Stefan et al. [54] were careful to ensure that LIO does not expose these termination and timing covert channels internally. LIO ensures that even if secret threads terminate early, loop forever, or otherwise influence the runtime system scheduler, they cannot leak information to public threads. But, secret threads do affect public threads with those actions and thus expose timing covert channels externally—public threads just cannot detect it. In particular, LIO disallows public threads from (1) directly inspecting the return values (and thus timing and termination behavior) of secret threads, without first raising their program counter label, and (2) observing runtime system resource usage (e.g., elapsed time or memory availability) that would indirectly leak secrets.

LIO prevents public threads from measuring CPU-time usage directly—LIO does not expose a clock API—and indirectly—threads are scheduled fairly in a round-robin fashion [54]. Similarly, LIO prevents threads from measuring memory usage directly—LIO does not expose APIs for querying heap statistics—and indirectly, through garbage collection cycles (e.g., induced by secret threads) [46]—GHC’s stop-the-world GC stops all threads. Like other IFC systems, the security guarantees of LIO are weaker in practice because its formal model does not account for the GC and assumes memory to be infinite [54, 55].

Since secret threads can still influence public threads by abusing the scheduler and GC, LIO is vulnerable to external timing and termination attacks, i.e., attacks that leak information to external observers. To illustrate this, we craft several LIO programs consisting of two threads: a public thread p that writes to the external channel observed by the attacker and a secret thread s, which abuses the runtime to influence the throughput of the public thread. The secret thread can leak in many ways, for example, thread s can:

These attacks abuse the runtime’s automatic allocation and reclamation of shared resources, i.e., CPU time and memory. In particular, attack 1 hinges on the runtime allocating CPU time for the new secret threads, thus reducing the CPU time allotted to the public thread. Dually, attack 2 relies on it reclaiming the CPU time of terminated threads—it reassigns it to public threads. Similarly, attacks 3 and 4 force the runtime to allocate all the available memory and preemptively reassign CPU time to the GC, respectively.

These attacks are not surprising, but, with the exception of the GC-based attack [46], they are novel in the IFC context. Moreover these attacks are not exhaustive—there are other ways to exploit the runtime system—nor optimized—our implementation leaks sensitive data at a rate of roughly 2bits/second¹. Nevertheless, they are feasible and—because they abuse the runtime—they are effective against language-level external-timing mitigation techniques, including [54, 71]. The attacks are also feasible on other systems—similar attacks that abuse the GC have been demonstrated for both the V8 and JVM runtimes [46].

LIO, like almost all IFC systems, considers external timing out of scope for its attacker model. Unfortunately, when we run LIO threads on multiple cores, in parallel, the allocation and reclamation of resources on behalf of secret threads is indirectly observable by public threads. Unsurprisingly, some of the above external timing attacks manifest internally—a thread running on a parallel core acts as an “external” attacker. To demonstrate the feasibility of such attacks, we describe two variants of the aforementioned scheduler-based attacks which leak sensitive information internally to public threads.

Secret threads can leak information by relinquishing CPU time, which the runtime reclaims and unsafely redistributes to public threads running on the same core. Our attack program consists of three threads: two public threads—\(p_0\) and \(p_1\)—and a secret thread—\(s_0\). Figure 1 shows the pseudo-code for this attack. Note that the threads are secure in isolation, but leak the value of secret when executed in parallel, with a round robin scheduler. In particular, threads \(p_0\) and \(s_0\) run concurrently on core \(c_0\) using half of the CPU time each, while \(p_1\) runs in parallel alone on core \(c_1\) using all the CPU time. Both public threads repeatedly write their respective thread IDs to a public channel. The secret thread, on the other hand, loops forever or terminates depending on secret. Intuitively, when the secret thread terminates, the runtime system redirects its CPU time to \(p_0\), causing both \(p_1\) and \(p_0\) to write at the same rate. In converse, when the secret thread does not terminate early, \(p_0\) is scheduled in a round-robin fashion with \(s_0\) on the same core and can thus only write half as fast as \(p_1\). More specifically:

Secret LIO threads can also leak information by allocating many secret threads on a core with public threads—this reduces the CPU-time available to the public threads. For example, using the same setting with three threads from before, the secret thread forks a spinning thread on core \(c_1\) by replacing command terminate with command fork (forever skip) \(c_1\) in the code of thread \(s_0\) in Fig. 1. Intuitively, if secret is false, then \(p_1\) writes more often than \(p_0\) before, otherwise the write rate of \(p_1\) decreases—it shares core \(c_1\) with the child thread of \(s_0\)—and \(p_0\) writes as often as \(p_1\).

Not all external timing attacks can be internalized, however. In particular, GHC’s approach to reclaiming memory via a stop-the-world GC simultaneously stops all threads on all cores, thus the relative write rate of public threads remain constant. Interestingly, though, implementing LIO on runtimes (e.g., Node.js as proposed by Heule et al. [17]) with modern parallel garbage collectors that do not always stop the world would internalize the GC-based external timing attacks. Similarly, abusing GHC’s memory allocation to exhaust all memory crashes all the program threads and, even though it cannot be internalized, it still results in information leakage.

In this section, we extend LIO\(_{\mathrm {PAR}}\) with concurrency, which enables (i) interleaved execution of threads on a single core and (ii) simultaneous execution on \(\kappa \) cores. To protect against attacks that exploit the automatic management of shared finite resource (e.g., those in Sect. 2.3), LIO\(_{\mathrm {PAR}}\) maintains a resource budget for each running thread and updates it as threads allocate and reclaim resources. Since \(\kappa \) threads execute at the same time, those changes must be coordinated in order to preserve the consistency of the resource budgets and guarantee deterministic parallelism. For this reason, the hierarchical runtime system is split in two components: (i) the core scheduler, which executes threads on a single core, ensures that they respect their resource budgets and performs security checks, and (ii) the top-level parallel scheduler, which synchronizes the execution on multiple cores and reassigns resources by updating the resource budgets according to the instructions of the core schedulers. We now introduce the core scheduler and describe the top-level parallel scheduler in Sect. 4.3.

Syntax. Figure 3 presents the core scheduler, which has access to the global state \(\varSigma \mathrel {=}({T},{B}, H ,\theta ,\omega )\), consisting of a thread pool map \({T}\), which maps a thread id to the corresponding thread’s current state, the time budget map \({B}\), a memory budget map \( H \), core capabilities map \(\theta \), and the global clock \(\omega \). Using these maps, the core scheduler ensures that thread \( n \): (i) performs \({B}( n )\) uninterrupted steps until the next thread takes over, (ii) does not grow its heap above its maximum heap size \( H ( n )\), and (iii) has exclusive access to the free core capabilities \(\theta ( n )\). Furthermore, each thread id \( n \) records the initial current label when the thread was created (\( n . pc \)), its clearance (\( n . cl \)), and the core where it runs (\( n . k \)), so that the runtime system can enforce security. Notice that thread ids are opaque to threads—they cannot forge them nor access their fields.

Hierarchical Scheduling. The core scheduler performs deterministic and hierarchical scheduling—threads lower in the hierarchy are scheduled first, i.e., parent threads are scheduled before their children. The scheduler manages a core run queue \( Q \), which is structured as a binary tree with leaves storing thread ids and residual time budgets. The notation \( n ^ b \) indicates that thread \( n \) can run for \( b \) more steps before the next thread runs. When a new thread is spawned, the scheduler creates a subtree with the parent thread on the left and the child on the right. The scheduler can therefore find the thread with the highest priority by following the left spine of the tree and backtracking to the right if a thread has no residual budget.⁸ We write \( Q {[}\langle n ^ b \rangle {]}\) to mean the first thread encountered via this traversal is \( n \) with budget \( b \). As a result, given the slice \( Q {[}\langle n ^{\mathrm {1}\mathbin {+} b }\rangle {]}\), thread \( n \) is the next thread to run, and \( Q {[}\langle n ^{\mathrm {0}}\rangle {]}\) occurs only if all threads in the queue have zero residual budget. We overload this notation to represent tree updates: a rule \( Q {[}\langle n ^{\mathrm {1}\mathbin {+} b }\rangle {]}\rightarrow Q {[}\langle n ^{ b }\rangle {]}\) finds the next thread to run in queue \( Q \) and decreases its budget by one.

Semantics. Figure 3 formally defines the transition \( Q \;\xrightarrow {( n , s, e )}_{\varSigma }\; Q' \), which represents an execution step of the core scheduler that schedules thread \( n \) in core queue \( Q \), executes it with global state \(\varSigma \mathrel {=}({T},{B}, H ,\theta ,\omega )\) and updates the queue to \( Q' \). Additionally, the core scheduler informs the parallel scheduler of the final state \( s\) of the thread and requests on its behalf to update the global state by means of event message \( e \). In rule [Step], the scheduler retrieves the next thread in the schedule, i.e., \( Q {[}\langle n ^{\mathrm {1}\mathbin {+} b }\rangle {]}\) and its state in the thread pool from the global state, i.e., \(\varSigma .{T}( n )\mathrel {=} s\). Then, it executes the thread for one sequential step with its memory budget and clearance, i.e., with \(\mu \mathrel {=}( \varSigma .H ( n ), n . cl )\), sends the empty event \(\epsilon \) to the parallel scheduler, and decrements the thread’s residual budget in the final queue, i.e., \( Q {[}\langle n ^{ b }\rangle {]}\). In rule [Fork], thread \( n \) creates a new thread \( t \) with initial label and clearance , such that and . The child thread runs on the same core of the parent thread, i.e., \( n . k \), with fresh id \( n' \), which is then added to the set of children, i.e., . Since parent and child threads do not share memory, the core scheduler must copy the portion of the parent’s private heap reachable by the child’s thread, i.e., \(\varDelta '\); we do this by copying the bindings of the variables that are transitively reachable from \( t \), i.e., \(fv^{*}( t , \varDelta )\), from the parent’s heap \(\varDelta \). The parent thread gives \(h_{2}\) of its memory budget \( \varSigma .H ( n )\) to its child. The conditions \({\vert }\varDelta {\vert }\leqslant h_{1}\) and \({\vert }\varDelta '{\vert }\leqslant h_{2}\), ensure that the heaps do not overflow their new budgets. Similarly, the core scheduler splits the residual time budget of the parent into \( b _{1}\) and \( b _{2}\) and informs the parallel scheduler about the new thread and its resources with event \(\mathbf {fork}(\varDelta ', n' , t , b _{2},h_{2})\), and lastly updates the tree \( Q \) by replacing the leaf \(\langle n ^{\mathrm {1}\mathbin {+} b _{1}\mathbin {+} b _{2}}\rangle \) with the two-leaves tree , so that the child thread will be scheduled immediately after the parent has consumed its remaining budget \( b _{1}\), as explained above. Rule [Spawn] is similar to [Fork], but consumes core capability resources instead of time and memory. In this case, the core scheduler checks that the parent thread owns the core where the child is scheduled and the core capabilities assigned to the child, i.e., for some set \(K_2\), and informs the parallel scheduler with event \(\mathbf {spawn}(\varDelta ', n' , t ,K_1)\). Rule [Stuck] performs busy waiting by consuming the time budget of the scheduled thread, when it is stuck and cannot make any progress—the premises of the rule enumerate the conditions under which this can occur (see the extended version of this paper for details). Lastly, in rule [ContextSwitch] all the threads scheduled in the core queue have consumed their time budget, i.e., \( Q {[}\langle n ^{\mathrm {0}}\rangle {]}\) and the core scheduler resets their residual budget using the budget map \(\varSigma .{B}\). In the rule, the notation \( Q {[}\langle n _{i}^{ b }\rangle {]}\) selects the \(i\)-th leaf, where and \({\vert } Q {\vert }\) denotes the number of leaves of tree \( Q \) and symbol \(\circ \) denotes the thread identifier of the core scheduler, which updates a dummy thread that simply spins during a context-switch or whenever the core is unused.

The calculus presented so far enables threads to manage their time, memory and core capabilities hierarchically, but does not provide any primitive to reclaim their resources. This section rectifies this by introducing (i) a primitive to kill a thread and return its resources back to the owner and (ii) a primitive to elicit a garbage collection cycle and reclaim unused memory. Furthermore, we demonstrate that the runtime system presented in this paper is robust against timing attacks by exposing a timer API allowing threads to access a global clock.⁹ Intuitively, it is secure to expose this feature because LIO\(_{\mathrm {PAR}}\) ensures that the time spent executing high threads is fixed in advanced, so timing measurements of low threads remain unaffected. Lastly, since memory is hierarchically partitioned, each thread can securely query the current size of its private heap, enabling fine-grained control over the garbage collector.

Kill. A parent thread can reclaim the resources given to its child thread \( n' \), by executing \( kill \; n' \). If the child thread has itself forked or spawned other threads, they are transitively killed and their resources returned to the parent thread. The concurrent rule in Fig. 4 initiates this process, which is completed by the parallel scheduler via event \(\mathbf {kill}( n' )\). Note that the rule applies only when the thread killed is a direct child of the parent thread—that is when the parent’s children set has shape for some set \({N}\). Now that threads can unrestrictedly reclaim resources by killing their children, we must revise the primitive \( unlabel \), since the naive combination of \( kill \) and \( unlabel \) can result in information leakage. This will happen if a public thread forks another public thread, then reads a secret value (raising its label to secret), and based on that decides to kill the child. To close the leak, we modify the rule by adding the highlighted premise, causing the primitive \( unlabel \) to fail whenever the parent thread’s label would float above the initial current label of one of its children.

Garbage Collection. Rule [GC] extends LIO\(_{\mathrm {PAR}}\) with a time-sensitive hierarchical garbage collector via the primitive \( gc \; t \). The rule elicits a garbage collection cycle which drops entries that are no longer needed from the heap, and then evaluates \( t \). The sub-heap \(\varDelta '\) includes the portion of the current heap that is (transitively) reachable from the free variables in scope (i.e. those present in the term, \(fv^{*}( t , \varDelta )\) or on the stack \(fv^{*}( S , \varDelta )\)). After collection, the thread resumes and evaluates term \( t \) under compacted private heap \(\varDelta '\).¹⁰ In rule [App-GC], a collection is automatically triggered when the thread’s next memory allocation would overflow the heap.

Resource Observations. All threads in the system share a global fine-grained clock \(\omega \), which is incremented by the parallel scheduler at each cycle (see below). Rule [Time] gives all threads unrestricted access to the clock via monadic primitive \( time \).

This section extends LIO\(_{\mathrm {PAR}}\) with deterministic parallelism, which allows to execute \(\kappa \) threads simultaneously on as many cores. To this end, we introduce the top-level parallel scheduler, which coordinates simultaneous changes to the global state by updating the resource budgets of the threads in response core events (e.g., fork, spawn, and kill) and ticks the global clock.

Semantics. Figure 5 formalizes the operational semantics of the parallel scheduler, which reduces a configuration \( c \mathrel {=}\langle \varSigma ,\varPhi \rangle \) consisting of global state \(\varSigma \) and core map \(\varPhi \) mapping each core to its run queue, to configuration \( c' \) in one step, written \( c \hookrightarrow c' \), through rule [Parallel] only. The rule executes the threads scheduled on each of the \(\kappa \) cores, which all step at once according to the concurrent semantics presented in Sects. 4.1–4.2, with the same current global state \(\varSigma \). Since the execution of each thread can change \(\varSigma \) concurrently, the top-level parallel scheduler reconciles those actions by updating \(\varSigma \) sequentially and deterministically.¹¹ First, the scheduler updates the thread pool map \({T}\) and core map \(\varPhi \) with the final state obtained by running each thread in isolation, i.e., \( T' \mathrel {=}\varSigma .{T} [ n _{i} \mapsto s_{i} ]\) and \(\varPhi '\mathrel {=}\varPhi [ i \mapsto Q _{i} ]\) for . Then, it collects all concurrent events generated by the \(\kappa \) threads together with their thread id, sorts the events according to type, i.e., , and computes the updated configuration by processing the events in sequence.¹² In particular, new threads are created first (event \(\mathbf {spawn}(\cdot )\) and \(\mathbf {fork}(\cdot )\)), and then killed (event \(\mathbf {kill}(\cdot )\))—the ordering between events of the same type is arbitrary and assumed to be fixed. Trivial events (\(\epsilon \)) do not affect the configuration and thus their ordering is irrelevant. The function computes a final configuration by processing a list of events in order, accumulating configuration updates (\(next(\cdot )\) updates the current configuration by one event-step): . When no more events need processing, the configuration is returned .

Event Processing. Figure 5 defines function \(next( n , e , c )\), which takes a thread identifier \( n \), the event \( e \) that thread \( n \) generated, the current configuration and outputs the configuration obtained by performing the thread’s action. The empty event \(\epsilon \) is trivial and leaves the state unchanged. Event \(( n _{1},\mathbf {fork}(\varDelta , n _{2}, t , b ,h))\) indicates that thread \( n _{1}\) forks thread \( t \) with identifier \( n _{2}\), sub-heap \(\varDelta \), time budget \( b \) and maximum heap size \(h\). The scheduler deducts these resources from the parent’s budgets, i.e., \( B' \mathrel {=}{B} [ n _{1} \mapsto {B}( n _{1})\mathbin {-} b ]\) and \( H' \mathrel {=} H [ n _{1} \mapsto H ( n _{1})\mathbin {-}h ]\) and assigns them to the child, i.e., \( B' [ n _{2} \mapsto b ]\) and \( H' [ n _{2} \mapsto h ]\).¹³ The new child shares the core with the parent—it has no core capabilities i.e., \(\theta '\mathrel {=}\theta [ n _{2} \mapsto \varnothing ]\)—and so the core map is left unchanged. Lastly, the scheduler adds the child to the thread pool and initializes its state, i.e., . The scheduler handles event \(( n _{1},\mathbf {spawn}(\varDelta , n _{2}, t , K ))\) similarly. The new thread \( t \) gets scheduled on core \( n _{2}. k \), i.e., \(\varPhi [ n _{2}. k \mapsto \langle n _{2}^{{B}_{\mathrm {0}}}\rangle ]\), where the thread takes all the time and memory resources of the core, i.e., \({B} [ n _{2} \mapsto {B}_{\mathrm {0}} ]\) and \( H [ n _{2} \mapsto H _{\mathrm {0}} ]\), and extra core capabilities \( K \), i.e., \(\theta ' [ n _{2} \mapsto K ]\). For simplicity, we assume that all cores execute \({B}_{\mathrm {0}}\) steps per-cycle and feature a memory of size \( H _{\mathrm {0}}\). Event \(( n ,\mathbf {kill}( n' ))\) informs the scheduler that thread \( n \) wishes to kill thread \( n' \). The scheduler leaves the global state unchanged if the parent thread has already been killed by the time this event is handled, i.e., when the guard \( n \;\not \in \; Dom ({T})\) is true—the resources of the child \( n' \) will have been reclaimed by another ancestor. Otherwise, the scheduler collects the identifiers of the descendants of \( n' \) that are alive ( )—they must be killed (and reclaimed) transitively. The set \({N}\) is computed recursively by \(\llbracket {N}\rrbracket ^{{T}}\), using the thread pool \({T}\), i.e., \(\llbracket \varnothing \rrbracket ^{{T}}\mathrel {=}\varnothing \), and \(\llbracket {N}_{1}\,\cup \,{N}_{2}\rrbracket ^{{T}}\mathrel {=}\llbracket {N}_{1}\rrbracket ^{{T}}\,\cup \,\llbracket {N}_{2}\rrbracket ^{{T}}\). The scheduler then increases the time and memory budget of the parent with the sum of the budget of all its descendants scheduled on the same core, i.e., \(\sum _{i\;\in \;{N},i. k \mathrel {=} n . k }{{B}(i)}\) (resp. \(\sum _{i\;\in \;{N},i. k \mathrel {=} n . k }{ H (i)})\)—descendants running on other cores do not share those resources. The scheduler reassigns to the parent thread their core capabilities, which are split between capabilities explicitly assigned but not in use, i.e., \(\bigcup _{i\;\in \;{N}}\theta (i)\) and core capabilities assigned and in use by running threads, i.e., . Lastly, the scheduler removes the killed threads from each core, written \(\varPhi (i) \setminus {N}\), by pruning the leaves containing killed threads and reassigning their leftover time budget to their parent, see the extended version of this paper for details.

The term erasure technique relies on an erasure function, written , which rewrites secret data above the attacker’s level to special term \(\bullet \), in all the syntactic categories: values, terms, heaps, stacks, global states and configurations.¹⁴ Once the erasure function is defined, the core of the proof technique consists of proving an essential commutativity relationship between the erasure function and reduction steps: given a step \( c \hookrightarrow c' \), there must exist a reduction that simulates the original reduction between the erased configurations, i.e., . Intuitively, if the configuration \( c \) leaked secret data while stepping to \( c' \), that data would be classified as public in \( c' \) and thus would remain in — but such secret data would be erased by and the property would not hold. The erasure function leaves ground values, e.g., \(()\), unchanged and on most terms it acts homomorphically, e.g., . The interesting cases are for labeled values, thread configurations, and resource maps. The erasure function removes the content of secret labeled values, i.e., , and erases the content recursively otherwise, i.e., . The state of a thread is erased per-component, homomorphically if the program counter label is public, i.e., , and in full otherwise, i.e., .

Resource Erasure. Since LIO\(_{\mathrm {PAR}}\) manages resources explicitly, the simulation property above requires to define the erasure function for resources as well. The erasure function should preserve information about the resources (e.g., time, memory, and core capabilities) of public threads, since the attacker can explicitly assign resources (e.g., with \( fork \) and \( swap \)) and measure them (e.g., with \( size \)). But what about the resources of secret threads? One might think that such information is secret and thus it should be erased—intuitively, a thread might decide to assign, say, half of its time budget to its secret child depending on secret information. However, public threads can also assign (public) resources to a secret thread when forking: even though these resources currently belong to the secret child, they are temporary—the public parent might reclaim them later. Thus, we cannot associate the sensitivity of the resources of a thread with its program counter label when resources are managed hierarchically, as in LIO\(_{\mathrm {PAR}}\). Instead, we associate the security level of the resources of a secret thread with the sensitivity of its parent: the resources of a secret thread are public information whenever the program counter label of the parent is public and secret information otherwise. Furthermore, since resource reclamation is transitive, the erasure function cannot discard secret resources, but must rather redistribute them to the hierarchically closest set of public resources, as when killing them.

Time Budget. First, we project the identifiers of public threads from the thread pool , where notation indicates that the program counter label of thread \( n \) is public. Then, the set contains the identifiers of all the public threads and their immediate children.¹⁵ The resources of threads \( n \;\in \; P \) are public information. However, the program counter label of a thread \( n \;\in \; P \) is not necessarily public, as explained previously. Hence \( P \) can be disjointly partitioned by program counter label: , where and . Erasure of the budget map then proceeds on this partition, leaving the budget of the public threads untouched, and summing the budget of their secret children threads to the budgets of their descendants, which are instead omitted. In symbols, , where and .

Queue Erasure. The erasure of core queues follows the same intuition, preserving public and secret threads \( n \;\in \; P \) and trimming all other secret threads . Since queues annotate thread ids with their residual time budgets, the erasure function must reassign the budgets of all secret threads to their closest ancestor \( n \;\in \; P \) on the same core. The ancestor \( n \;\in \; P \) could be either (i) another secret thread on the same core, i.e., , or, (ii) the spinning thread of that core, \(\circ \;\in \; P \) if there is no other thread \( n \;\in \; P \) on that core—the difference between these two cases lies on whether the original thread \( n' \) was forked or spawned on that core. More formally, if the queue contains no thread \( n \;\in \; P \), then the function replaces the queue altogether with the spinning thread and returns the residual budgets of the threads to it, i.e., if \( n _{i}\;\not \in \; P \) and \({B}\mathrel {=}\sum _{}{ b _{i}}\), for each leaf \( Q {[}\langle n ^{ b _{i}}_{i}\rangle {]}\) where . Otherwise, the core contains at least a thread and the erasure function returns the residual time budget of its secret descendants, i.e., by combining the effects of the following mutually recursive functions:

The interesting case is , which reassigns the budget of the child (the right leaf ) to the parent (the left leaf ), by rewriting the subtree into .

The proof of progress- and timing-sensitive non-interference relies on two fundamental properties, i.e., determinacy and simulation of parallel reductions. Determinacy requires that the reduction relation is deterministic.

The equivalence in the statement denotes alpha-equivalence, i.e., up to the choice of variable names. We now show that the parallel scheduler preserves -equivalence of parallel configurations.

By combining determinism (Proposition 1) and parallel simulation (Proposition 2), we prove progress-insensitive non-interference, which assumes progress of both configurations.

In order to lift this result to be progress-sensitive, we first prove timing-sensitive progress. Intuitively, if a valid configuration steps then any low equivalent parallel configuration also steps.¹⁶

Using progress-insensitive non-interference, i.e., Proposition 3 and timing-sensitive progress, i.e., Proposition 4 in combination, we obtain a strong -bisimulation property between configurations and prove progress- and timing-sensitive non-interference.

The following corollary instantiates the non-interference security theorem from above for a given LIO\(_{\mathrm {PAR}}\) parallel program, that explicitly rules out leaks via timing channels. In the following, the notation \(\hookrightarrow _{ u }\) denotes \( u \) reduction steps of the parallel scheduler.

To conclude, we show that the timing-sensitive security guarantees of LIO\(_{\mathrm {PAR}}\) extend to concurrent single-core programs by instantiating Corollary 1 with \(\kappa \mathrel {=}\mathrm {1}\).