Permissive runtime information flow control in the presence of exceptions

Abstract

Information flow control (IFC) has been extensively studied as an approach to mitigate information leaks in applications. A vast majority of existing work in this area is based on static analysis. However, some applications, especially on the Web, are developed using dynamic languages like JavaScript where static analyses for IFC do not scale well. As a result, there has been a growing interest in recent years to develop dynamic or runtime information flow analysis techniques. In spite of the advances in the field, runtime information flow analysis has not been at the helm of information flow security, one of the reasons being that the analysis techniques and the security property related to them (non-interference) over-approximate information flows (particularly implicit flows), generating many false positives.

In this paper, we present a sound and precise approach for handling implicit leaks at runtime. In particular, we present an improvement and enhancement of the so-called permissive-upgrade strategy, which is widely used to tackle implicit leaks in dynamic information flow control. We improve the strategy’s permissiveness and generalize it. Building on top of it, we present an approach to handle implicit leaks when dealing with complex features like unstructured control flow and exceptions in higher-order languages. We explain how we address the challenge of handling unstructured control flow using immediate post-dominator analysis. We prove that our approach is sound and precise.

Keywords

Runtime information flow control permissive-upgrade control-flow graphs immediate post-dominator analysis exceptions

1. Introduction

Web applications rely extensively on third-party JavaScript to provide useful libraries, page analytics, advertisements and many other features [50]. In such a mashup model, wherein the hosting page and the included scripts share the page’s state (called the DOM), all included third-party scripts run with the same access privileges as the hosting page. While some third-party scripts are developed by large, well-known, trustworthy vendors, many other scripts are developed by small, domain-specific vendors whose commercial motives do not always align with those of the web-page providers and users. This leaves sensitive information such as passwords, credit card numbers, email addresses, click histories, cookies and location information vulnerable to inadvertent bugs and deliberate exfiltration by third-party scripts. In many cases, developers are fully aware that a third-party script accesses sensitive data to provide useful functionality, but they are unaware that the script also leaks that data on the side. In fact, this is a widespread problem [41].

The traditional browser security model is based on restricting scripts’ access to data, not on tracking how scripts use data. Existing web security standards like the same-origin policy [11] address this problem unsatisfactorily, favoring functionality over privacy. The same-origin policy (implemented in all major browsers) restricts a web-page and third-party scripts included in it to communicating with web servers from the including web-page’s domain only. However, broad exceptions are allowed. For instance, there is no restriction on request parameters in URLs that fetch images and, unsurprisingly, third-party scripts leak information by encoding it in image URLs. Content Security Policy [1], also implemented in most browsers, allows a page to white list scripts that may be included, but places no further restriction on scripts that have been white listed, thus not helping with the problem above.

Quite a few fine-grained access control techniques have also been proposed [18,26,27,32,45,47,63,69]. However, all these techniques enforce only access policies and cannot control what a script does with data it has been provided in good faith. That is, if a third-party script was allowed access to some data only for local computations, these techniques do not prevent the script from sending the data on the network. In fact, no mechanism based only on access control can solve the problem of information leakage in this setting.

The academic community has proposed solutions based on information flow control (IFC), which ensures the security of confidential information even in the presence of untrusted and buggy code. The idea is to track the flow of information through the program and prevent any undesired flows based on a security policy. Research has considered static methods such as type checking and program analysis, which verify the security policy at compile time [20,21,35,40,48,51,56,65], dynamic methods that track information flow at runtime [5,7–9,13,23,30,38,57,59,61,67], and gradual and hybrid approaches that combine both static and dynamic analyses to add precision to the analysis [12,14,19,25,28,29,34,36,43,49,55,62,64].

While runtime analysis has the drawback of introducing significant performance overheads, it can be more permissive than static analysis methods in certain cases [55]. Moreover, static analyses are mostly ineffective when working with dynamic languages like JavaScript, which is an indispensable part of the modern Web. The dynamic nature of JavaScript [53,54] with features like dynamic typing, runtime code generation (eval), scope-chains and prototype chains makes sound static analysis difficult. Thus, recent research has focused on dynamic analysis for enforcing information flow control especially in languages like JavaScript [7–9,14,23,38,59,61]. Even though research in runtime information flow control has made significant inroads in the last decade, the applicability of these techniques still remains bleak. The major challenge to the practicality of runtime information flow control is the conservative handling of implicit leaks, which affects the permissiveness of the approaches.

This paper proposes methods to improve the permissiveness of runtime information flow techniques by presenting mechanisms that enhance the precision of the analyses when handling implicit leaks. The two main contributions of the paper are as follows:

To improve the permissiveness of runtime information flow analysis, this paper presents the generalized permissive-upgrade strategy, a sound improvement and enhancement of the permissive-upgrade strategy (which is widely used to tackle implicit leaks when enforcing runtime information flow control [14,59]). The development improves the original strategy’s permissiveness and applicability by generalizing the approach to an arbitrary security lattice, in place of the two-point lattice considered in prior work.

Most of the existing work in runtime information flow control does not consider implicit leaks due to complex features like unstructured control flow and exceptions. The proposals that handle these features are too conservative and require additional annotations in the program. We present a sound and precise dynamic control scope analysis for handling these features building on top of the generalized permissive upgrade strategy and without requiring any additional annotations from the developer.

This paper extends a part of our conference paper [14] and our workshop paper [13]. In particular, we improve the permissiveness of the existing permissive-upgrade strategy (Section 3), and the formalism presented in the earlier workshop paper [13] to design a more permissive technique for enforcing runtime IFC with arbitrary lattices (Section 4.2). We use the generalized permissive-upgrade strategy to formalize runtime information flow control for a generic system where programs are represented using control-flow graphs and prove it sound (Section 6), and show the precision of our analysis technique (Section 5.3). Several proofs and details are covered in the appendix.

2. Background and overview

2.1. Information flow control

Information flow control (IFC) approaches control the flow of (confidential) information through a program based on a given security policy. Typically, pieces of information are classified into security labels and the policy is a lattice over labels. Information is only allowed to flow up the lattice. For illustration purposes often the smallest non-trivial lattice $L ⊏ H$ is used, which specifies that public (low, L) data must not be influenced by confidential (high, H) data. Information flow control can be used to provide confidentiality (or integrity) of secret (trusted) information; the work in this paper is, however, limited to confidentiality guarantees. Roughly, the idea behind information flow control is that an adversary can view all the public outputs of a program. By preventing private or sensitive data from flowing to public outputs, we prevent the adversary from obtaining any information about the private or sensitive data.

In general, information can flow along many channels. However, this paper considers two of the most important flows – explicit and implicit – in deterministic programs [20–22]. Covert channels like timing or resource usage are beyond the scope of this paper.

An explicit flow occurs as a result of direct assignment, e.g., the statement public = secret + 1 causes an explicit flow from secret to public. An implicit flow occurs due to the control structure of the program. For instance, consider the program in Listing 1. The final value of y is equal to the value of z even though there is no direct assignment from z to y. Leaking a bit like this can be magnified into leaking a bigger secret bit-by-bit [4].

Listing 1.

Implicit flow from z to y

The soundness of approaches enforcing information flow control is often stated in terms of a well-defined security property known as non-interference [31], which basically stipulates that high or secret inputs of a program must not influence its low or publicly observable outputs. While non-interference is too strong a property in practice, different variants of the definition are proven. One such variant of non-interference usually established for information flow control techniques is termination-insensitive non-interference [65]. Roughly, a program is termination-insensitive non-interferent if any two terminating runs of the program starting from low-equivalent heaps (i.e., heaps that look equivalent to the adversary assuming that an adversary can observe some part of the heap) end in low-equivalent heaps. In particular, this means that the parts of the initial heap that the adversary cannot see have no influence on the parts of the final heap that it can see.

2.2. Dynamic information flow control

Dynamic IFC usually works by tracking taints or labels on individual program values in the language runtime. A label represents a mandatory access policy on the value. A value v labeled ℓ is written $v^{ℓ}$ .

Dynamic IFC analysis propagates labels as data flows during program execution. Explicit flows are generally handled by carrying over the label of the computed value to the variable being assigned. For example, in the statement x = y + z, the result of computing y + z will have the label that is a join of the labels on y and z. This will also be the final label of x. So, if either of y or z is labeled H (confidential), then the final label of x is also H.1

¹
“x is labeled H” actually means “the value in x is labeled H”. This language convention is used consistently in the paper.

Implicit flows in a runtime IFC analysis are tracked by maintaining an additional taint, usually called the program counter taint or program context taint or $pc$ , which is an upper bound on the label of all the control dependencies that lead to the current instruction being executed. For example, in the program of Listing 1, the value in variable x at the end of line 3 depends on the value in z. If z is labeled H, then at line 3, $pc = H$ because of the branch in line 2 that depends on z. Thus, by tracking $pc$ , dynamic IFC can enforce that x has label H at the end of line 3, thus taking into account the control dependency.

However, simply tracking control flow dependencies via $pc$ is not enough to guarantee absence of information flows when labels are flow-sensitive, i.e., when the same variable may hold values with different labels depending on what program paths are executed. The program in Listing 1 is a classic counterexample, taken from [7]. Assume that z is labeled H and x and y are labeled L initially. The final value in y is computed as a function of the value in z. If z contains ${true}^{H}$ , then y ends with ${true}^{L}$ : The branch on line 2 is not taken, so x remains ${false}^{L}$ at line 4. Hence, the branch on line 4 is taken, but $pc = L$ at line 5 and y ends with ${true}^{L}$ . If z contains ${false}^{H}$ , then similar reasoning shows that y ends with ${false}^{L}$ . Consequently, in both cases y ends with label L and its value is exactly equal to the value in z. Hence, an adversary can deduce the value of z by observing y at the end (which is allowed because y ends with label L). So, this program leaks information about z despite correct use of $pc$ .

2.3. Basic IFC semantics

Fig. 1.

Syntax of the language.

Most of the technical development in this paper is based on the simple imperative language shown in Fig. 1. However, the key ideas are orthogonal to the choice of language and generalize to other languages easily. The use of a simpler language is to simplify non-essential technical details. Parts of the paper that require additional language features define those features in place. The language’s expressions include constants or values (n, b), variables ( $x$ ) and unspecified binary operators (⊙) to combine them. The set of variables is fixed upfront. Labels (ℓ) are drawn from a fixed security lattice with a partial order ⊑, join ⊔, meet ⊓, a least element ⊥ and a top element ⊤. Lattice elements are written $L, M, H, \dots$ . The meta-variables ℓ and $pc$ (program counter label) also ranges over lattice elements.

Fig. 2.

Semantics.

The rules in Fig. 2 define the big-step semantics of the language, including standard taint propagation for IFC: the evaluation relation $⟨ σ, e ⟩ ⇓ n^{k}$ for expressions, and the evaluation relation $⟨ σ, c ⟩ \underset{pc}{⇓} σ^{'}$ for commands. Here, σ denotes a store, a map from variables to labeled values of the form $n^{k}$ . b represents a Boolean constant. For now, labels $k : : = ℓ$ ; this is generalized later when “partially-leaked” taints are introduced in Section 2.5.

The evaluation relation for expressions evaluates an expression e and returns its value n and label k. The label k is the join of labels of all variables occurring in e (according to σ). The relation for commands executes a command c in the context of a store σ, and the current program counter label $pc$ , and yields a new store $σ^{'}$ . The function $Γ (σ (x))$ returns the label associated with the value in x in store σ: If $σ (x) = n^{k}$ , then $Γ (σ (x)) = k$ .

The sequencing rule (seq) evaluates the command $c_{1}$ under store σ and the current $pc$ label. This yields a new store $σ^{″}$ . It then evaluates the command $c_{2}$ under store $σ^{″}$ and the same $pc$ label, which yields the final store $σ^{'}$ . The if-else rule evaluates the branch condition e to a Boolean value b with label ℓ. Based on the value of b, one of the branches $c_{1}$ and $c_{2}$ is executed under a $pc$ obtained by joining the current $pc$ and the label ℓ of b. Similarly, the rules for while (while-t and while-f) evaluate the loop condition e and execute the loop command $c_{1}$ while e evaluates to true. The $pc$ for the loop’s body is obtained by joining the current $pc$ and the label ℓ of the result of evaluating e.

The rule for assignment statements are conspicuously missing from Fig. 2 because they depend on the strategy used to control implicit flows. We discuss different approaches to handle implicit leaks presented in prior work [7,8] next.

2.4. Dynamically handling implicit leaks using no-sensitive-upgrade check

Preventing leaks due to implicit flow in dynamic IFC requires coarse approximation because a dynamic monitor only sees program branches that are executed and does not know what assignments may happen in alternate branches in other executions. One such coarse approximation is the no-sensitive-upgrade (NSU) check proposed by Zdancewic [68]. In the program in Listing 1, x’s label is upgraded from L to H at line 3 in one of the two executions above, but not the other. Subsequently, information leaks in the other execution (where x’s label remains L) via the branch on line 4. The NSU check stops the leak by preventing the assignment on line 3. More generally, it stops a program whenever a public variable’s label is upgraded due to a high $pc$ . This check suffices to provide termination-insensitive non-interference, as shown by Austin and Flanagan [7].

Fig. 3.

Assignment rule for NSU.

The rule for assignment (assn-nsu) corresponding to the NSU check is shown in Fig. 3. The rule checks that the label l of the assigned variable x in the initial store σ is at least as high as $pc$ (premise $pc ⊑ l$ ). If this condition is not true, the program gets stuck.

2.4.1. Soundness the no-sensitive-upgrade check

For establishing and proving the security property of termination-insensitive non-interference (TINI), the observational power of the adversary needs to be defined. An adversary at level ℓ in the lattice is allowed to view all values that have a label less than or equal to ℓ. To prove the security property of non-interference, it is enough to show that when executing a program beginning with two different memory stores that are observationally equivalent to an adversary, the final memory stores are also observationally equivalent to the adversary. For this, the observational equivalence of two memory stores with respect to an adversary needs to be defined. Store equivalence is formalized as a relation $\sim_{ℓ}$ , indexed by lattice elements ℓ, representing the adversary.

Definition 1 (Value equivalence).

Two labeled values $n_{1}^{k}$ and $n_{2}^{m}$ are ℓ-equivalent, written $n_{1}^{k} \sim_{ℓ} n_{2}^{m}$ , iff either:

$(k = m) ⊑ ℓ$ and $n_{1} = n_{2}$ or

$k ⋢ ℓ$ and $m ⋢ ℓ$

This definition states that for an adversary at security level ℓ, two labeled values $n_{1}^{k}$ and $n_{2}^{m}$ are equivalent iff either ℓ can access both values, and $n_{1}$ and $n_{2}$ are equal, or it cannot access either value ( $k ⋢ ℓ$ and $m ⋢ ℓ$ ). Note that if $L ⊏ H$ , then any two values labeled L and H are distinguishable for the L-adversary.

Definition 2 (Store equivalence).

Two stores $σ_{1}$ and $σ_{2}$ are ℓ-equivalent, written $σ_{1} \sim_{ℓ} σ_{2}$ , iff for every variable x , $σ_{1} (x) \sim_{ℓ} σ_{2} (x)$ .

The following theorem states TINI for the NSU check. The theorem has been proved for various languages in the past.

Theorem 1 (TINI for NSU).

With the assignment rule assn-nsu from Fig. 3 , if $σ_{1} \sim_{ℓ} σ_{2}$ and $⟨ σ_{1}, c ⟩ \underset{pc}{⇓} σ_{1}^{'}$ and $⟨ σ_{2}, c ⟩ \underset{pc}{⇓} σ_{2}^{'}$ , then $σ_{1}^{'} \sim_{ℓ} σ_{2}^{'}$ .

Proof.
Standard, see e.g., [7]. □

2.5. Permissive-upgrade strategy for handling implicit leaks

The no-sensitive-upgrade (NSU) check described earlier provides the basic foundations for sound dynamic IFC. However, terminating a program preemptively because of the NSU check is quite restrictive in practice. For example, consider the program of Listing 2, where z is labeled H and y is labeled L. This program potentially upgrades variable x at line 3 under a high $pc$ , and then executes function f when y is true and executes function g otherwise. Suppose that f does not read x. Then, for $y \mapsto {true}^{L}$ , this program leaks no information, but the NSU check would terminate this program prematurely at line 3. (Note: g may read x, so x is not a dead variable at line 3.)

Listing 2.

Impermissiveness of the NSU strategy

To allow a dynamic IFC analysis to accept safe executions of programs with variable upgrades due to high $pc$ , Austin and Flanagan proposed a less restrictive strategy called the permissive-upgrade strategy [8]. They study this strategy for a two-point lattice $L ⊏ H$ and their strategy does not immediately generalize to arbitrary security lattices. Whereas NSU stops a program when a variable’s label is upgraded due to assignment in a high $pc$ , permissive-upgrade allows the assignment, but labels the variable as partially-leaked or P. The exact intuition behind the partially-leaked label P is the following:

The program must be stopped later if it tries to use or case-analyze the variable (in particular, branching on a partially-leaked Boolean variable is stopped). Permissive-upgrade also ensures termination-insensitive non-interference, but is strictly more permissive than NSU. For example, permissive-upgrade stops the leaky program of Listing 1 at line 4 when z contains ${false}^{H}$ , but it allows the program of Listing 2 to execute to completion when y contains ${true}^{L}$ .

In the revised syntax of labels, summarized in Fig. 4, the labels k, l, m on values can be either elements of the lattice (L, H) or P. The $pc$ can only be one of L, H because branching on partially-leaked values is prohibited. The join operation ⊔ is lifted to labels including P. Joining any label with P results in P. For brevity in definitions, the order is extended to $L ⊏ H ⊏ P$ . However, P is not a new “top” member of the lattice because it receives special treatment in the operational semantics.

Fig. 4.

Syntax of labels including the partially-leaked label P.

The rule for assignment with permissive-upgrade is $assn-pus \frac{l : = Γ (σ (x)) ⟨ σ, e ⟩ ⇓ n^{m}}{⟨ σ, x : = e ⟩ \underset{pc}{⇓} σ [x \mapsto n^{k}]}$ where k is defined as follows: $\begin{matrix} k = \{\begin{matrix} m & if pc = L \\ m ⊔ H & if pc = H and l = H \\ P & otherwise \end{matrix} \end{matrix}$

The first two conditions in the definition of k correspond to the NSU rule (Fig. 3). The third condition applies, in particular, when a variable whose initial label is L is assigned where $pc = H$ . The NSU check would stop this assignment. With permissive-upgrade, however, the updated variable is labeled P, consistent with the intuitive meaning of P. This allows more permissiveness by allowing the assignment to proceed in all cases. To compensate, any program (in particular, an adversarial program) is disallowed from case analyzing any value labeled P. Consequently, in the rules for if-then and while (Fig. 2), the label of the branch condition is of the form ℓ, which does not include P. Thus, assignments under high $pc$ succeed under the permissive-upgrade check but branching or case-analyzing a partially-leaked value is not permitted as that can also leak information.

The noninterference result obtained for NSU earlier can be extended to permissive-upgrade by changing the definition of store equivalence. Because no program can case-analyze a P-labeled value, such a value is equivalent to any other labeled value.

Definition 3.

Two labeled values $n_{1}^{k}$ and $n_{2}^{m}$ are equivalent to an adversary at level L, written $n_{1}^{k} \sim_{L} n_{2}^{m}$ , iff either:

$(k = m) = L$ and $n_{1} = n_{2}$ or

$k = H$ and $m = H$ or

$k = P$ or $m = P$

Definition 4.

Two stores $σ_{1}$ and $σ_{2}$ are L-equivalent, written $σ_{1} \sim_{L} σ_{2}$ , iff $\forall x . σ_{1} (x) \sim_{L} σ_{2} (x)$ .

Theorem 2 (TINI for permissive-upgrade with a two-point lattice).

With the assignment rule assn-PUS, if $σ_{1} \sim_{L} σ_{2}$ and $⟨ c, σ_{1} ⟩ ⇓_{pc} σ_{1}^{'}$ and $⟨ c, σ_{2} ⟩ ⇓_{pc} σ_{2}^{'}$ , then $σ_{1}^{'} \sim_{L} σ_{2}^{'}$ .

Proof.
See [8]. □
3. Improved permissive-upgrade strategy

The original permissive-upgrade strategy as described above lacks permissiveness in some cases. For example, it rejects the program of Listing 3, which is actually secure. Consider that x is labeled H and w, y are labeled L. With the original permissive-upgrade strategy, the label of z on line 3 would remain P and the execution would be terminated when branching on z on line 4.

Listing 3.

Impermissiveness of the permissive-upgrade strategy

Our improvement makes a small change to the definition of ⊔. We define: $\begin{matrix} H ⊔ P = H \end{matrix}$ Revisiting the example with this change, z would be labeled H on line 3, which would allow the execution to branch on line 4, thus taking the execution to completion. The idea behind the improvement is that an H-labeled value is never observable at L-level. Similarly, the result of any operation involving an H-labeled value is also never observable at L-level. Thus, the result of combining P-labeled value with a H-labeled value can safely be labeled H.

Following this change, we also redefine the label k in the assignment rule assn-pus. $\begin{matrix} k = \{\begin{matrix} m & if pc = L \\ H & if pc = H and l = H \\ P & otherwise \end{matrix} \end{matrix}$

The soundness results of the original permissive-upgrade strategy can be extended to show the soundness of the improved permissive-upgrade strategy. However, a significant difficulty in proving soundness with P is that the definition of ∼ is no longer transitive. In [8], the authors resolve this issue by defining a special relation called evolution. We follow a related but non-identical proof strategy for showing the improved permissive-upgrade strategy sound.

Lemma 1 (Expression evaluation).

If $⟨ σ_{1}, e ⟩ ⇓ n_{1}^{k_{1}}$ and $⟨ σ_{2}, e ⟩ ⇓ n_{2}^{k_{2}}$ and $σ_{1} \sim_{L} σ_{2}$ , then $n_{1}^{k_{1}} \sim_{L} n_{2}^{k_{2}}$ .

Proof.
By induction on e. □
Lemma 2 (Evolution).

If $pc = H$ and $⟨ σ, c ⟩ \underset{pc}{⇓} σ^{'}$ , then $\forall x . Γ (σ (x)) = P ⟹ Γ (σ^{'} (x)) = P$ .

Proof.
By induction on the derivation rules and case analysis on the last rule. □
Lemma 3 (Confinement for improved permissive-upgrade with a two-point lattice).

If $pc = H$ and $⟨ σ, c ⟩ \underset{pc}{⇓} σ^{'}$ , then $σ \sim_{L} σ^{'}$ .

Proof.
By induction on the given derivation. □
Theorem 3 (TINI for improved permissive-upgrade with a two-point lattice).

With the assignment rule assn-pus and the modifications above, if $σ_{1} \sim_{L} σ_{2}$ and $⟨ σ_{1}, c ⟩ \underset{pc}{⇓} σ_{1}^{'}$ and $⟨ σ_{2}, c ⟩ \underset{pc}{⇓} σ_{2}^{'}$ , then $σ_{1}^{'} \sim_{L} σ_{2}^{'}$ .

Proof.
By induction on c and case analysis on the last step. □

Detailed proofs of the above claims are in Appendix A.1. Note that the definitions and proofs presented in this section are specific to the two-point lattice and with respect to an adversary at level L.
4. Generalized permissive-upgrade strategy

Although the permissive-upgrade strategy as described above is useful, its development is incomplete so far: Austin and Flanagan’s original paper [8], and our improvement (Section 3), both develop permissive-upgrade for only a two-point security lattice, containing levels L and H with $L ⊏ H$ , and the new label P. A generalization to a pointwise product of such two-point lattices (and, hence, a powerset lattice) was suggested by Austin and Flanagan in the original paper, but not fully developed. As explained later in Section 4.1, this generalization works for the improved permissive-upgrade strategy and can be proven sound.

However, that still leaves open the question of generalizing permissive-upgrade to arbitrary lattices. It is not even clear hitherto that this generalization exists. This section shows by construction that a generalization of permissive-upgrade (with our improvement of Section 3) to arbitrary lattices does indeed exist and that it is, in fact, non-obvious. Specifically, the rule for adding partially-leaked labels and the definition of store (memory) equivalence needed to prove non-interference are reasonably involved.

4.1. Generalized improved permissive-upgrade strategy on powerset lattices

Austin and Flanagan point out that permissive-upgrade on a two-point lattice can be generalized to a pointwise product of such lattices. This generalization can also be extended to the improved permissive-upgrade strategy presented above. Specifically, let X be an index set – these indices are called principals (like Alice, Bob etc.) in [8]. Let a label l be a map of type $X \to {L, H, P}$ and let the subclass of pure labels contain maps ℓ, $pc$ of type $X \to {L, H}$ . The order ⊏ and the join operation ⊔ can be generalized pointwise to these labels. Finally, the rule assn-pus can be generalized pointwise by replacing it with the following rule: $assn-gpus \frac{l : = Γ (σ (x)) ⟨ σ, e ⟩ ⇓ n^{m}}{⟨ σ, x : = e ⟩ \underset{pc}{⇓} σ [x \mapsto n^{k}]}$ where k is defined as follows: $\begin{matrix} k (a) = \{\begin{matrix} m (a) & if pc (a) = L \\ H & if pc (a) = H and l (a) = H \\ P & otherwise \end{matrix} \end{matrix}$ In the definition above, a represents a principal like Alice from the set X. It can be shown that for any semantic derivation in this generalized system, projecting all labels to a given principal yields a valid semantic derivation in the system with a two-point lattice. This immediately implies non-interference for the generalized system, where observations are limited to individual principals.

Definition 5.
Two labeled values $n_{1}^{k}$ and $n_{2}^{m}$ are a-equivalent, written $n_{1}^{k} \approx^{a} n_{2}^{m}$ , iff either:
$k (a) = m (a) = L$ and $n_{1} = n_{2}$ or

$k (a) = m (a) = H$ or

$k (a) = P$ or $m (a) = P$

Definition 6 (Store equivalence).

Two stores $σ_{1}$ and $σ_{2}$ are ℓ-equivalent, written $σ_{1} \approx^{a} σ_{2}$ , iff for every variable x , $σ_{1} (x) \approx^{a} σ_{2} (x)$ .

Theorem 4 (TINI for permissive-upgrade with a product lattice).

With the assignment rule assn-gpus , if $σ_{1} \approx^{a} σ_{2}$ and $⟨ σ_{1}, c ⟩ \underset{pc}{⇓} σ_{1}^{'}$ and $⟨ σ_{2}, c ⟩ \underset{pc}{⇓} σ_{2}^{'}$ , then $σ_{1}^{'} \approx^{a} σ_{2}^{'}$ .

Proof.
The proof follows from Theorem 3 for every principal a. □

This generalization of the two-point lattice to a product of such lattices is interesting because a powerset lattice can be simulated using such a product. However, this still leaves open the question of constructing a generalization of permissive-upgrade to an arbitrary lattice (for instance, lattices like the one shown in Fig. 7). Such a generalization is developed next.
4.2. Generalized improved permissive-upgrade on arbitrary lattices

Fig. 5.

Labels and label operations.

This section shows by construction the generalization of the permissive-upgrade strategy to arbitrary security lattices. For every element ℓ of the lattice, a new label $ℓ^{⋆}$ is introduced which means “partially-leaked ℓ”, with the following intuition:

The syntax of labels is listed in Fig. 5. Labels k, l, m may be lattice elements ℓ or ⋆-ed lattice elements $ℓ^{⋆}$ . In examples, we continue to use suggestive lattice element names L, M, H (low, medium, high). Labels of the form ℓ are called ⋆-free or pure. Figure 5 also defines the join operation ⊔ on labels. This definition is based on the intuition above. When the two operands of ⊙ are labeled $ℓ_{1}$ and $ℓ_{2}^{⋆}$ , $ℓ_{1} ⊔ ℓ_{2}$ is a lower bound on the pure label of the resulting value in any execution (because $ℓ_{2}$ is a lower bound on the pure label of $ℓ_{2}^{⋆}$ in any run). Hence, $ℓ_{1} ⊔ ℓ_{2}^{⋆} = {(ℓ_{1} ⊔ ℓ_{2})}^{⋆}$ . The reason for the definition $ℓ_{1}^{⋆} ⊔ ℓ_{2}^{⋆} = {(ℓ_{1} ⊔ ℓ_{2})}^{⋆}$ is similar.

Fig. 6.

Assignment rules for the generalized permissive-upgrade.

The rules for assignment are shown in Fig. 6. They strictly generalize the rule assn-pus for the two-point lattice (where $P = L^{⋆}$ ). Rule assn-n applies when the existing label of the variable being assigned to is $ℓ_{x}$ or $ℓ_{x}^{⋆}$ and $pc ⊑ ℓ_{x}$ . The key intuition behind the rule is the following: If $pc ⊑ ℓ_{x}$ , then it is safe to overwrite the variable, because $ℓ_{x}$ is necessarily a lower bound on the (pure) label of $x$ in this and any alternate execution (see the above). Hence, overwriting the variable cannot cause an implicit flow. As expected, the label of the overwritten variable is $pc ⊔ m$ , where m is the label of the value assigned to $x$ .

Rule assn-s applies in the remaining case – when $pc ⋢ ℓ_{x}$ . In this case, there may be an implicit flow, so the final label on $x$ must have the form $ℓ^{⋆}$ for some ℓ. The question is which ℓ. Intuitively, it may seem that one could choose $ℓ = ℓ_{x}$ , the pure part of the original label of $x$ . The final label on $x$ would be $ℓ_{x}^{⋆}$ and this would satisfy the intuitive meaning of ⋆ written in the above. Indeed, this intuition suffices for the two-point lattice of Section 2.5 and 3. However, for a more general lattice, this intuition is unsound, as illustrated with an example below. The correct label is ${((pc ⊔ m) ⊓ ℓ_{x})}^{⋆}$ .

Fig. 7.

Lattice explaining rule assn-s.

Listing 4.

Example explaining rule assn-s

Example. We illustrate the need for the label $k : = {((pc ⊔ m) ⊓ ℓ_{x})}^{⋆}$ instead of $k : = ℓ_{x}^{⋆}$ in the rule assn-s. Consider the lattice of Fig. 7 and the program of Listing 4. Assume that, initially, the variables $z$ , $w$ , $x_{1}$ , $x^{'}$ , $x_{2}$ , $y_{1}$ and $y_{2}$ have labels H, $L_{1}$ , $L_{1}$ , $L^{'}$ , $L_{2}$ , $M_{1}$ and $M_{2}$ , respectively. Fix the attacker at level $L_{1}$ . Fix the value of $x_{1}$ at ${true}^{L_{1}}$ , so that the branch on line 5 is always taken and line 6 is always executed. Set $y_{1} \mapsto {false}^{M_{1}}$ , $y_{2} \mapsto {true}^{M_{2}}$ , $w \mapsto {false}^{L_{1}}$ initially. The initial value of $z$ is irrelevant. Consider two executions of the program starting from two stores $σ_{1}$ with $x^{'} \mapsto {true}^{L^{'}}$ , $x_{2} \mapsto {true}^{L_{2}}$ and $σ_{2}$ with $x^{'} \mapsto {false}^{L^{'}}$ , $x_{2} \mapsto {false}^{L_{2}}$ . Note that as $L^{'}$ and $L_{2}$ are incomparable to $L_{1}$ in the lattice, $σ_{1}$ and $σ_{2}$ are equivalent for $L_{1}$ .

Table 1

Execution steps in two runs of the program from Listing 4, with two variants of the rule assn-s

	$w = {false}^{L_{1}}$ , $x_{1} = {true}^{L_{1}}$ , $y_{1} = {false}^{M_{1}}$ , $y_{2} = {true}^{M_{2}}$

	$x^{'} = {true}^{L^{'}}$	$x^{'} = {false}^{L^{'}}$
	$x_{2} = {true}^{L_{2}}$	$x_{2} = {false}^{L_{2}}$

		$k : = ℓ_{x}^{⋆}$	$k : = {((pc ⊔ m) ⊓ ℓ_{x})}^{⋆}$
if ( $x^{'}$ )	$pc = L^{'}$
$z = y_{1}$	$z = {false}^{M_{1}}$
else		$pc = L^{'}$	$pc = L^{'}$
$z = y_{2}$		$z = {true}^{M_{2}}$	$z = {true}^{M_{2}}$
if ( $x_{1}$ )	$pc = L_{1}$	$pc = L_{1}$	$pc = L_{1}$
$z = x_{1}$	$z = {true}^{L_{1}}$	$z = {true}^{M_{2}^{⋆}}$	$z = {true}^{L^{⋆}}$
if ( $not (x_{2})$ )	branch not taken	$pc = L_{2}$	$pc = L_{2}$
$z = x_{2}$		$z = {false}^{L_{2}}$	$z = {false}^{L^{⋆}}$
if ( $z$ )	$pc = L_{1}$	branch not taken	execution halted
$w = z$	$w = {true}^{L_{1}}$
Result	$w = {true}^{L_{1}}$	$w = {false}^{L_{1}}$ (leak)	no leak

Requiring $k : = ℓ_{x}^{⋆}$ in rule assn-s causes an implicit flow that is observable for $L_{1}$ . The intermediate values and labels of the variables for executions starting from $σ_{1}$ and $σ_{2}$ are shown in the second and third columns of Table 1. Starting with $σ_{1}$ , line 2 is executed, but line 4 is not, so $z$ ends with ${false}^{M_{1}}$ at line 5 (rule assn-n applies at line 2). At line 6, $z$ contains ${true}^{L_{1}}$ (again by rule assn-n) and line 8 is not executed. Thus, the branch on line 9 is taken and $w$ ends with ${true}^{L_{1}}$ at line 10. Starting with $σ_{2}$ , line 2 is not executed, but line 4 is, so $z$ becomes ${true}^{M_{2}}$ at line 5 (rule assn-n applies at line 4). At line 6, rule assn-s applies, but because $k : = ℓ_{x}^{⋆}$ is assumed in that rule, $z$ now contains the value ${true}^{M_{2}^{⋆}}$ . As the branch on line 7 is taken, at line 8, $z$ becomes ${false}^{L_{2}}$ by rule assn-n because $L_{2} ⊑ M_{2}$ . Thus, the branch on line 9 is not taken and $w$ ends with ${false}^{L_{1}}$ in this execution. Hence, $w$ ends with ${true}^{L_{1}}$ and ${false}^{L_{1}}$ in the two executions, respectively. The attacker at level $L_{1}$ can distinguish these two results and, hence, the program leaks the value of $x^{'}$ and $x_{2}$ to $L_{1}$ .

With the correct assn-s rule in place, this leak is avoided (last column of Table 1). In that case, after the assignment on line 6 in the second execution, $z$ has label ${((L_{1} ⊔ L_{1}) ⊓ M_{2})}^{⋆} = L^{⋆}$ . Subsequently, after line 8, $z$ gets the label $L^{⋆}$ . As case analysis on a ⋆-ed value is not allowed, the execution is halted on line 9. This guarantees termination-insensitive non-interference with respect to the attacker at level $L_{1}$ .

4.3. Termination-insensitive non-interference (TINI)

To prove non-interference for the generalized permissive-upgrade, equivalence of labeled values relative to an adversary at arbitrary lattice level ℓ needs to be defined. The definition is shown below (Definition 7). Note that clauses (3)–(5) here refine clause (3) of Definition 5 for the two-point lattice. The obvious generalization of clause (3) of Definition 5 – $n_{1}^{k} \sim_{ℓ} n_{2}^{m}$ whenever either k or m is ⋆-ed – is too coarse to prove non-interference inductively. For the degenerate case of the two-point lattice, this definition also degenerates to Definition 5 (there, ℓ is fixed at L, $P = L^{⋆}$ and only L may be ⋆-ed).

Definition 7.
Two values $n_{1}^{k}$ and $n_{2}^{m}$ are ℓ-equivalent, written $n_{1}^{k} \sim_{ℓ} n_{2}^{m}$ , iff either
$k = m = ℓ^{'} ⊑ ℓ$ and $n_{1} = n_{2}$ , or

$k = ℓ^{'} ⋢ ℓ$ and $m = ℓ^{″} ⋢ ℓ$ , or

$k = ℓ_{1}^{⋆}$ and $m = ℓ_{2}^{⋆}$ , or

$k = ℓ_{1}^{⋆}$ and $m = ℓ_{2}$ and ( $ℓ_{2} ⋢ ℓ$ or $ℓ_{1} ⊑ ℓ_{2}$ ), or

$k = ℓ_{1}$ and $m = ℓ_{2}^{⋆}$ and ( $ℓ_{1} ⋢ ℓ$ or $ℓ_{2} ⊑ ℓ_{1}$ )

Definition 8.
Two stores $σ_{1}$ and $σ_{2}$ are ℓ-equivalent, written $σ_{1} \sim_{ℓ} σ_{2}$ , iff for every variable x , $σ_{1} (x) \sim_{ℓ} σ_{2} (x)$ .

This definition is obtained by constructing (through examples) an extensive transition graph of pairs of labels that may be assigned to a single variable at corresponding program points in two executions of the same program. The starting point is label-pairs of the form $(ℓ, ℓ)$ . This characterization of equivalence is both sufficient and necessary. It is sufficient in the sense that it allows us to prove TINI inductively. It is necessary in the sense that example programs can be constructed that end in states exercising every possible clause of this definition. Appendix A.2 lists these examples.

Using the above definition of equivalence of labeled values, TINI can be proven for the generalized permissive-upgrade strategy presented above. As before, a significant difficulty in proving the theorem is that the definition of $\sim_{ℓ}$ is not transitive. Detailed proofs of all the lemmas and the theorems are presented in Appendix A.3.
Lemma 4 (Expression evaluation).

If $⟨ σ_{1}, e ⟩ ⇓ n_{1}^{k_{1}}$ and $⟨ σ_{2}, e ⟩ ⇓ n_{2}^{k_{2}}$ and $σ_{1} \sim_{ℓ} σ_{2}$ , then $n_{1}^{k_{1}} \sim_{ℓ} n_{2}^{k_{2}}$ .

Proof.
By induction on e. □
Lemma 5 (⋆-preservation).

If $⟨ σ, c ⟩ \underset{pc}{⇓} σ^{'}$ and $Γ (σ (x)) = ℓ^{⋆}$ and $pc ⋢ ℓ$ , then $Γ (σ^{'} (x)) = ℓ^{' ⋆}$ and $ℓ^{'} ⊑ ℓ$ .

Proof.
By induction on the given derivation. □
Corollary 1.
If $⟨ σ, c ⟩ \underset{pc}{⇓} σ^{'}$ and $Γ (σ (x)) = ℓ^{⋆}$ and $Γ (σ^{'} (x)) = ℓ^{'}$ , then $pc ⊑ ℓ$ .
Proof.
Immediate from Lemma 5. □
Lemma 6 ( $pc$ -lemma).

If $⟨ σ, c ⟩ \underset{pc}{⇓} σ^{'}$ and $Γ (σ^{'} (x)) = ℓ$ , then $σ (x) = σ^{'} (x)$ or $pc ⊑ ℓ$ .

Proof.
By induction on the given derivation. □
Corollary 2.
If $⟨ σ, c ⟩ \underset{pc}{⇓} σ^{'}$ and $Γ (σ (x)) = ℓ^{⋆}$ and $Γ (σ^{'} (x)) = ℓ^{'}$ , then $pc ⊑ ℓ^{'}$ .
Proof.
Immediate from Lemma 6. □

Using these lemmas, the standard confinement lemma and non-interference can be proven. Lemma 7 (Confinement lemma).

If $pc ⋢ ℓ$ and $⟨ σ, c ⟩ \underset{pc}{⇓} σ^{'}$ , then $σ \sim_{ℓ} σ^{'}$ .

Proof.
By induction on the given derivation. □
Theorem 5 (TINI for generalized permissive-upgrade for arbitrary lattices).

If $σ_{1} \sim_{ℓ} σ_{2}$ and $⟨ σ_{1}, c ⟩ \underset{pc}{⇓} σ_{1}^{'}$ and $⟨ σ_{2}, c ⟩ \underset{pc}{⇓} σ_{2}^{'}$ , then $σ_{1}^{'} \sim_{ℓ} σ_{2}^{'}$ .

Proof.
By induction on c. □

4.4. Comparison of the generalization of Section 4.2 with the generalization of Section 4.1

Two distinct and sound generalizations of the permissive-upgrade strategy for the two-point lattice have now been described: The generalization of the improved permissive-upgrade to pointwise products of two-point lattices or, equivalently, to powerset lattices as described in Section 4.1, and the generalization to arbitrary lattices described in Section 4.2. Since both the generalizations apply to powerset lattices, an obvious question is whether one is more permissive than the other on such lattices. The generalization of permissive-upgrade to pointwise lattices described in Section 4.1 can be more permissive than the generalization described in Section 4.2 for powerset lattices in certain cases as shown by the example below. The reason for this permissiveness is that the generalization of permissive-upgrade to pointwise lattices tracks finer taints, i.e., it tracks partial leaks for each principal separately.

Fig. 8.

A powerset/product lattice.

Listing 5.

Example where generalization of permissive-upgrade to pointwise lattices is more permissive than the generalization to arbitrary lattices

Example. We use the powerset lattice of Fig. 8. This lattice is the pointwise lifting of the order $L ⊏ H$ to the set $S = {L, H} \times {L, H}$ . For brevity, this lattice’s elements are written as $LL$ , $LH$ , etc. When generalization from Section 4.1 is applied to this lattice, labels are drawn from the set ${L, H, P} \times {L, H, P}$ . These labels are concisely written as $LP$ , $HL$ , etc. For the generalization from Section 4.2 to arbitrary lattices, labels are drawn from the set $S \cup S^{⋆}$ . These labels are written $LH$ , ${LH}^{⋆}$ , etc. Note that ${LH}^{⋆}$ parses as ${(LH)}^{⋆}$ , not $L (H^{⋆})$ (the latter is not a valid label in the generalization applied to this lattice). Consider the program in Listing 5. Assume that $x$ , $y$ and $z$ have initial labels $LL$ , $HL$ and $LH$ , respectively and that the initial store contains $y \mapsto {true}^{HL}$ , $z \mapsto {true}^{LH}$ , so the branches on lines 1 and 3 are both taken. The initial value in $x$ is irrelevant but its label is important. Under the generalization from Section 4.1, $x$ obtains label ${(((HL) ⊔ (LH)) ⊓ (LL))}^{⋆} = {LL}^{⋆}$ at line 2 by rule assn-s. At line 4, the same rule applies but the label of $x$ remains ${LL}^{⋆}$ . When the program tries to branch on $x$ at line 5, it is stopped. In contrast, under generalization of permissive-upgrade to pointwise lattices, this program executes to completion. At line 2, the label of $x$ changes to $PH$ by rule assn-gpus. At line 4, the label changes to $LH$ because $pc$ and the label of $z$ are both $LH$ . Since this new label has no P, line 5 executes without halting. Hence, for this example, generalization of permissive-upgrade to pointwise lattices is more permissive than the generalization to arbitrary lattices presented in Section 4.2.

We could not find an example for which the generalization of permissive-upgrade to arbitrary lattices is more permissive than generalization to pointwise lattices in the case of powerset lattices. But the generalization presented in Section 4.2 is more general than the product construction (Section 4.1) when applied to arbitrary lattices (and hence, applicable to a broader set of lattices) as it is unclear whether or how the results of Section 4.1 apply to arbitrary lattices.

5. Handling implicit leaks with complex features

Implicit flows correspond to control dependence in program analysis, where branch conditions govern which program path is executed and leak information through the control flow of the program. For sound analysis and to avoid over-approximation in certain cases, the generalized permissive upgrade strategy presented earlier works by determining when the influence of a control construct has ended. This is necessary to lower the $pc$ label for subsequent program statements, thus preventing overtainting.

For block-structured control flow limited to if and while commands, it is straightforward to determine where the influence of a control construct ends as this is obvious syntactically. For example, in the program $\begin{matrix} if (h) {l = 1;} l = 2 \end{matrix}$ h influences the control flow at l = 1 but not at l = 2. In a big-step operational semantics, lowering the $pc$ after the influence of a control construct ends is very straightforward since the $pc$ is raised exactly for the syntactic scope of the control construct. In a small-step semantics, a bit more is required, but the overall setup is still straightforward: One maintains a stack of $pc$ labels [68]; the effective $pc$ is the top one. When entering a control flow construct like if or while, a new $pc$ label, equal to the join of labels of all values on which the construct’s guard depends with the previous effective $pc$ , is pushed. When exiting the construct, the label is popped.

Unfortunately, it is unclear how to extend this simple strategy (with both big-step and small-step semantics) to non-block-structured control flow constructs such as break, continue and return-in-the-middle for functions, all of which occur in imperative high-level languages. For example, consider the program $\begin{matrix} l = 1; while (1) {... if (h) {break;}; l = 0; break;} \end{matrix}$ with h labeled H. This program leaks the value of h into l, but no assignment to l appears in a syntactic block-scope guarded by h. Indeed, the lexical scoping strategy just described is ineffective for this program. Tracking information flow in the presence of such unstructured control flows is non-trivial as the control breaks out of block structures.

Exceptions are even more difficult to handle as they allow for non-local control transfer. Consider, for instance, the program snippet shown below: $\begin{matrix} function f() = { & function g() = { \\ l = 0; & if (h) {throw 9;} \\ try { g(); } catch(e) { l = 1; } & return 7; \\ return l; & } \\ } \end{matrix}$

The function f() calls the function g(), which throws an exception that is caught by the exception handler in f() if the value of h is not false. The exception handler modifies the value of the public variable l, which the function returns. When f is invoked with $pc = L$ , the two functions together leak the value of h, which is assumed to have a label H, into the return value of f.

To solve this issue of handling implicit leaks with complex features, we present a precise dynamic analysis approach building on top of the generalized permissive upgrade strategy using post-dominator analysis [22,42].

5.1. Control flow graphs and post-dominator analysis

Our approach is based on an on-the-fly post-dominator analysis at runtime to handle implicit flows. A control flow graph (CFG), which is a directed graph, is constructed for every new function before it is executed with every instruction being represented as a node and whose edges represent the possible control flows. For every branch node, its immediate post-dominator (IPD) is computed [14,22,42]. A stack of $pc$ labels is maintained. When executing a branch node, a new $pc$ label is pushed on the stack along with the node’s IPD. When the IPD is actually reached, the $pc$ label along with the IPD is popped from the stack. In prior work [46,66], it is proved that the IPD marks the end of the scope of an operation and hence the security context of the operation, so our strategy is sound. The IPD-based solution works for all forms of unstructured control flow like break, continue, return-in-the-middle, and exceptions. Multiple return statements in a function can be represented as a single return node.

Maintaining a precise CFG for post-dominator analysis at runtime in the presence of exceptions is expensive. As the CFG of a function is constructed on-the-fly when compiling the function at runtime, an exception-throwing node in a function that does not catch that exception should have an outgoing control flow edge to the next related exception handler in the runtime call-stack. This means that the CFG is, in general, inter-procedural, and edges going out of a function depend on its calling context, so IPDs of nodes in the function must be computed every time the function is called (the IPDs change based on the earlier functions in the call-stack that called the particular function where the exception occurs). Moreover, in the case of recursive functions, the nodes must be replicated for every call. This is rather expensive. Ideally, the function’s CFG should be built only once when the function is compiled and work intra-procedurally.

5.2. Synthetic exit nodes

In our approach, every function that may throw an unhandled exception and has an exception handler present earlier in the call-stack (which is assumed to be known at runtime through additional data structures in the system) has a special synthetic exit node ( $SEN$ ), which is placed after the regular return node of the function in the CFG. Every exception-throwing node, whose exception will not be caught within the function, has an outgoing edge to the $SEN$ . In essence, the $SEN$ is treated as the IPD for nodes whose actual IPDs lie outside of the function. By doing this, all cross-function edges are eliminated and the CFGs become intra-procedural. This allows the computation of the CFGs just once as compared to the inter-procedural case. For every exception-throwing instruction that has an associated handler, its context is maintained during dynamic information flow analysis until the handler is reached.

Thus, function calls and all potential exception-throwing instructions are represented as nodes with multiple edges (branches) and push a node on the $pc$ -stack. However, a new node is not pushed on the $pc$ -stack if the IPD of the current node is the same as the IPD on the top of the $pc$ -stack or if the IPD of the current node is the $SEN$ , as in this case the real IPD, which is outside of this method, should already be on the $pc$ -stack.

In summary, these semantics emulate the effect of having cross-function edges. For illustration, consider the two functions f and g from before. The ◇ at the end of g denotes its $SEN$ . Note that there is an edge from throw 9 to ◇ because throw 9 is not handled within g. □ denotes the IPD of the function call g() and handler catch(e). $\begin{matrix} function f() = { & function g() = { \\ l = 0; & if (h) {throw 9;} \\ try { g(); } catch(e) { l = 1; } & return 7; \\ □ return l; & } ◇ \\ } \end{matrix}$

When calling g, the current $pc$ and IPD $(L, □)$ are pushed on the $pc$ -stack. When executing the condition if (h) a new node is not pushed again, but the top element is merely updated to $(H, □)$ as its IPD is the $SEN$ ◇. If h is false, control reaches the return statement but with $pc = H$ . At □, $pc$ is lowered to L, so f ends with the return value 0 and public label L. If h is true, control reaches the handler, which is in f and invokes it with the same $pc$ as at the point of exception, i.e., H. Consequently, the generalized permissive-upgrade strategy marks the assignment in the catch block as partially-leaked and prevents the implicit information leak in this case.

5.3. Precision proofs

We show that the approach presented above where we pop the $pc$ -stack at the IPD of a node is precise. In other words, the IPD of a node is the most precise node where the influence of $pc$ ends, and the top of the $pc$ -stack can be safely popped. Theorem 6 shows this result. For proving Theorem 6, we formally define a control flow graph, paths on the control flow graph, branch-points and post-dominators.

Definition 9 (Control flow graph).

A control flow graph is a directed graph $G = (N, E, n_{s}, n_{e}, L)$ . $N$ is the set of nodes. $E$ is the set of control flow edges $(n_{1}, n_{2}) \in E$ , where $n_{i} \in N$ . $(n_{1}, n_{2})$ represents $n_{2}$ may immediately execute after $n_{1}$ . The nodes $n_{s}, n_{e} \in N$ are special nodes representing the start and the end point of $G$ , respectively. The function $L$ maps the edges in $E$ to labels.

Definition 10 (Path).

A path in a CFG $G$ is a sequence of nodes $(n_{1}, n_{2}, \dots, n_{m})$ such that $(n_{i}, n_{i + 1}) \in E$ , written as $n_{1} \to_{p} n_{m}$ . A node n that lies on the path $n_{1} \to_{p} n_{m}$ is written as $n \in n_{1} \to_{p} n_{m}$ . The notation $n_{1} < n_{2}$ with respect to two nodes $n_{1}$ and $n_{2}$ in a CFG $G$ indicates that $n_{2}$ lies on a path $n_{1} \to_{p} n_{e}$ .

Definition 11 (Branch-point).

A branch-point b is a node in a CFG $G$ that has more than one successor, i.e., $outdegree (b) > 1$ .

Definition 12 (Post-dominator).

In a CFG $G$ , a node $n_{d}$ is said to be the post-dominator of a node n if all paths from n to the end-node pass through $n_{d}$ , i.e., $\forall p . n \to_{p} n_{e} ⟹ n_{d} \in p$ . The notation $n_{d} pd n$ indicates that $n_{d}$ is a post-dominator of n.

Definition 13 (Immediate post-dominator).

A node i is the immediate post-dominator of the node n, denoted as $IPD (n)$ , iff:

$i pd n$ and

$∄ n_{o} \in N . ((n_{o} pd n) \land (n_{o} < i))$ or

$\forall n_{o} \in N . ((n_{o} \neq n) ⟹ (n_{o} pd n ⟹ n_{o} pd i))$ .

Theorem 6 (Precision).

Choosing any node other than the IPD to lower the $pc$ -label will either give unsound results or be less precise.

Proof.
Consider a branch-point $b \in N$ with IPD $IPD (b) = i \in N$ .

Assume that $(n \in N) \neq i$ is the node where the context of the predicate expression in b is removed. Thus, either:
$b < n < i$ : Then, $\exists p . n \notin b \to_{p} n_{e}$ . Thus, if n performs an action that should not have been performed in the context of the predicate expression in b, it might leak information about the predicate expression in b.

$b < i < n$ : Then, for any $n^{'} \in N$ such that $i < n^{'} < n$ performing an operation that should not be performed in the context of b would be reported illicit as $n^{'}$ would be executed in the context of b.

If $n^{'} pd b$ , then $\forall p . n^{'} \in b \to_{p} n_{e}$ . Hence, the statement $n^{'}$ executes irrespective of whether the branch at b is taken or not and hence, does not depend on the predicate expression in b, i.e., there is no implicit flow from the predicate expression in b to $n^{'}$ , but still the program might be rejected.

If $n^{'}$ is a statement executing under the context of another branch-point $b^{'}$ , such that $b^{'} pd b$ , then as $b^{'}$ does not have any implicit flow from the predicate expression in b, any statement executing under the context of the predicate expression in $b^{'}$ should not be influenced by the context of the predicate expression in b. Hence, the program might be rejected even though there is no information leak.

$i < > n$ : $\forall p . n \notin i \to_{p} n_{e}$ or $\forall p . n \notin b \to_{p} n_{e}$ , n will never be reached. Thus, the context of b shall not be removed until $n_{e}$ such that $b < i < n_{e}$ . Similar reasoning as in the second case with $n = n_{e}$ .
Hence, the most precise node where one can safely remove the context of b is $n = IPD (b) = i$ . □

We also show that our design decision to not push the $SEN$ on the $pc$ -stack if the IPD of a node is $SEN$ is correct. In fact, the actual IPD of a node having $SEN$ as its IPD is the node that is currently on the top of the stack. This result is shown in Theorem 7. Theorem 7.
The actual IPD of a node having $SEN$ as its IPD is the node that is currently on the top of the pc-stack.
Proof.
Assume two functions F and G given by the CFGs $G = (N, E, n_{s}, n_{e}, L)$ and $G^{'} = (N^{'}, E^{'}, n_{s}^{'}, n_{e}^{'}, L^{'})$ , respectively. The program’s start and exit node are given by $N_{s}$ and $N_{e}$ , respectively. Consider a branch-point $b^{'} \in N^{'}$ having $SEN$ as its IPD. Assume a branch-point $b \in N$ such that $b < b^{'} < (i = IPD (b))$ , $(i \in N) \neq SEN$ , b is the last executed branch-point and top of the pc-stack contains i.

$\forall p . i \in b \to_{p} n_{e}$ . Thus, $i pd b^{'}$ such that $b < b^{'} < i$ .

T.S. $∄ n \in b^{'} \to_{p} i | (n pd b^{'}) \land (b^{'} < n < i)$ .

Proof by contradiction: Assume $\exists n . n pd b^{'} | b^{'} < n < i$ . Then the node n either lies in the function F or G or in another function H given by the CFG $G^{″} = (N^{″}, E^{″}, n_{s}^{″}, n_{e}^{″}, L^{″})$ , such that F calls H and H calls G.
$n \in N^{'}$ : As $IPD (b^{'}) = SEN$ and $SEN$ is the last node in a function( $G^{'}$ ), $\exists p . n \notin b \to_{p} n_{e}$ .

$n \in N^{″}$ : As $\forall p . n \in b^{'} \to_{p} N_{e}$ and $G () < b^{'}$ , thus, $\forall p . n \in G () \to_{p} N_{e}$ , which means $IPD (G ()) \neq SEN$ . Hence, the top of the pc-stack then would have $IPD (G ()) = (n^{″} \in N^{″}) ⩽ n$ and not i.

$n \in N$ : When the call to G or any other function H is made, it would push i, IPD of the branch-point on the top of the pc-stack.
Thus, $∄ n \in b^{'} \to_{p} i | (n pd b^{'}) \land (b^{'} < n < i)$ . Hence, the top of the $pc$ -stack, i is the actual IPD of any node $b^{'}$ having $SEN$ as its intra-procedural IPD. □

6. Formal model

We consider a language with unstructured control flow and exceptions, and give it an operational semantics with IFC using the generalized permissive-upgrade check. The language is an extension of that in Fig. 1 with unstructured control flow constructs like break, continue, return and exceptions. A program is a collection of functions (without parameter-passing). The control flow analysis is performed on a function before it is executed and is abstractly represented as a CFG. This involves a translation from the language of Fig. 1 extended with unstructured control flow and exceptions into a formal language of CFGs, the syntax of whose nodes is shown in Fig. 9.

Fig. 9.

Language syntax (extends Fig. 1).

A program in the CFG language is modeled as a huge control flow graph ( $G$ ). IPDs are computed using the algorithm by Lengauer and Tarjan [44] when the CFG is created. For new functions added at runtime, the CFG is constructed only once. For a non-branching node $ι \in G$ , $Succ (ι)$ denotes ι’s unique successor. For a conditional branching node ι, $Left (ι)$ and $Right (ι)$ denote successors when the condition is true and false, respectively.

The command if e then $c_{1}$ else $c_{2}$ is represented as the node branch e with $Left (G, ι) = c_{1}$ and $Right (G, ι) = c_{2}$ . Similarly, while e do c is represented as branch e with $Left (ι) = c$ and $Right (ι)$ being the command following while in the program. A jmp node is added as $Succ (c)$ with the successor $Succ (ι)$ set to the branch instruction to jump to the predicate. A jmp node in the CFG also corresponds to break and continue with $Succ (ι)$ pointing to the next node in the CFG according to the operation. It is also assumed that a function always ends with a return statement and thus a CFG normally ends with the return node. (Multiple return statements in a function are represented using a single return node.) When ι is a $return$ node, $Succ (ι)$ is the node to return to in the previous CFG. Here “previous” refers to the previous function in the call stack (the caller). The return value is saved in a global variable that can be accessed by the program later on. Every node in the program’s CFG is uniquely identifiable.

In general, every function has an associated exception table that maps each potentially exception-throwing instruction in the function to the appropriate exception handler within the function. This is represented by adding a $Right$ edge in the CFG from the instruction’s node to the handler’s node. throw has only one outgoing edge. It is conservatively assumed that any unknown code may throw an exception, so function call is exception-throwing for this purpose. If a function contains unhandled exceptions, the corresponding edges in the CFG point to the $SEN$ of the CFG. The $SEN$ is only created if one of the previous functions in the call-stack has an appropriate exception handler for the unhandled exceptions in the current function. When an $SEN$ node is created, an edge is added from the $SEN$ of the CFG to a node in the previous CFG, which is either the catch node or the $SEN$ of that CFG. $Succ$ denotes one of these edges. If there are no appropriate handlers in the call-stack, the exception-throwing nodes have an edge to the end node of the program CFG. For simplicity of exposition, it is assumed here that all exceptions belong to a single class – for different types of exceptions, the exception class would also be matched for determining the appropriate exception handler.

Program configurations for commands (nodes) are represented as $⟨ σ, ι, ρ ⟩$ , where σ represents the memory store as before, ι represents the currently executing node, and ρ is the $pc$ -stack. The configuration for expressions is the same as before: $⟨ σ, e ⟩$ .

Each entry of the $pc$ -stack ρ is a pair $(ℓ, ι)$ , where ℓ is a security label and ι is a node in the CFG. When a new control context is entered, the new $pc$ -label, which is a join of the current context label and the existing $pc$ -label (the label on the top of the stack), is pushed together with the IPD ι of the entry point of the control context. This IPD ι uniquely identifies where the control of the context ends. In the semantics, the meta-function $isIPD$ pops the stack. It takes the current instruction and the current $pc$ -stack, and returns a new $pc$ -stack. $! ρ$ returns the top frame of the $pc$ -stack. $Γ (! ρ)$ returns the current context label, also represented as $pc$ in the semantics. $\begin{matrix} isIPD (ι, ρ) : = \{\begin{matrix} ρ . pop () & if! ρ = (_, ι) \\ ρ & otherwise \end{matrix} \end{matrix}$ As explained in Section 5.2, a new node $(ℓ, ι)$ is pushed onto ρ only when ι (the IPD) differs from the corresponding entry on the top of the stack or it is not $SEN$ (Theorem 7). Otherwise, ℓ is joined with the label on the top of the stack. This is formally represented using the function $ρ . push (ℓ, ι)$ .

Fig. 10.

Semantics.

The rules in Fig. 10 define small-step semantics of CFGs. The rules for expressions are the same as in Fig. 2. The rules are informally explained above. The soundness of the analysis including unstructured control flow and exceptions is proved below.

To state the theorem formally, the equivalence of different data structures with respect to the adversary needs to be defined. We reuse value and memory equivalences from Definitions 7 and 8. We prove termination-insensitive non-interference using the generalized permissive-upgrade strategy, for which we formalize some additional definitions and define auxiliary lemmas. The detailed proofs, definitions and other lemmas can be found in Appendix B.

Definition 14 (

pc

-stack equivalence).

For two $pc$ -stacks $ρ_{1}$ , $ρ_{2}$ , $ρ_{1} \sim_{ℓ} ρ_{2}$ iff the corresponding nodes of $ρ_{1}$ and $ρ_{2}$ having labels less than or equal to ℓ are equal.

Definition 15 (State equivalence).

Two states $s_{1} = ⟨ σ_{1}, ι_{1}, ρ_{1} ⟩$ and $s_{2} = ⟨ σ_{2}, ι_{2}, ρ_{2} ⟩$ are equivalent, written as $s_{1} \sim_{ℓ} s_{2}$ , iff $σ_{1} \sim_{ℓ} σ_{2}$ , $ι_{1} = ι_{2}$ , and $ρ_{1} \sim_{ℓ} ρ_{2}$ .

Lemma 8 (Confinement lemma).

If $⟨ σ, ι, ρ ⟩ \to ⟨ σ^{'}, ι^{'}, ρ^{'} ⟩$ and $Γ (! ρ) ⋢ ℓ$ , then $σ \sim_{ℓ} σ^{'}$ , and $ρ \sim_{ℓ} ρ^{'}$ .

Theorem 8.
Suppose:
$⟨ σ_{1}, ι_{1}, ρ_{1} ⟩ \sim_{ℓ} ⟨ σ_{2}, ι_{2}, ρ_{2} ⟩$

$⟨ σ_{1}, ι_{1}, ρ_{1} ⟩ \to^{} ⟨ σ_{1}^{'}, end, [] ⟩$

$⟨ σ_{2}, ι_{2}, ρ_{2} ⟩ \to^{} ⟨ σ_{2}^{'}, end, [] ⟩$
Then, $σ_{1}^{'} \sim_{ℓ} σ_{2}^{'}$ .
7. Related work

7.1. Permissive IFC

Secure multi-execution [23] is another approach for enforcing non-interference at runtime, where one executes multiple copies of the program with different values of sensitive data. Conceptually, the same code is executed once for each security level (like low and high) with a few constraints. High inputs in the low execution are replaced by default values, i.e., the low execution of the program does not see the actual value of the high data but a pre-determined default value. Additionally, outputs on an ℓ-labeled channel are permitted only in the ℓ-level execution of the program. This ensures noninterference and precision (the semantics of a secure program are not altered). However, executing a program multiple times can be prohibitive for a security lattice with many levels [2,9]. The runtime overhead incurred can be reduced if the executions are done in parallel but this requires more hardware resources. In addition to this, secure multi-execution makes declassification complicated as it requires synchronization between different executions [52].

To tackle the issue of permissiveness with the no-sensitive-upgrade strategy and the permissive-upgrade strategy, Austin and Flanagan proposed the idea of faceted execution [9], which is the most permissive of the three. Faceted execution simulates multiple executions simultaneously within a single runtime. They introduce the concept of faceted values that are pairs of values, one each for low and high observers. When branching on a faceted value, multiple executions are simulated for the two values in the facet. To achieve better precision and security guarantees, researchers have proposed techniques that combine faceted execution and secure multi-execution on an as-needed basis [3,58]. However, the runtime overheads of faceted execution is also prohibitive for multiple security levels [2]. This paper, thus, considers only the permissive-upgrade strategy, which is more permissive than the no-sensitive-upgrade strategy and much less performance-intensive than faceted execution.

Birgisson et al. [15] describe a testing-based approach that adds variable upgrade annotations to avoid halting on the NSU check in an implementation of dynamic IFC for JavaScript [38]. A different way of handling the problem of implicit flows through flow-sensitive labels is to assign a (fixed) label to each label; this approach has been examined by Buiras et al. in the context of a language with a dedicated monad for tracking information flows [16]. The precise connection between that approach and permissive-upgrade remains unclear, although Buiras et al. sketch a technique related to permissive-upgrade in their system, while also noting that generalizing permissive-upgrade to arbitrary lattices is non-obvious. This paper confirms the latter and shows how it can be done.

7.2. IFC with error handling

Much work on error handling for IFC has been in the context of static analysis [6,48]. Work on IFC for dynamic languages has mostly ignored exceptions and other unstructured control flow constructs [7,8,17,24,33]. Just et al. [42] present dynamic IFC for JavaScript bytecode with static analysis to determine implicit flows precisely but ignore implicit flows due to exceptions. Hedin and Sabelfeld propose a dynamic IFC approach for a language modeling the core features of JavaScript [38] but ignore unstructured control flow constructs like break, continue and return-in-the-middle for functions. For handling exceptions, they introduce annotations and an additional class of labels. An extension introduces similar annotations to deal with unstructured control flow [37]. These labels are more restrictive than needed, e.g., the code indicated by dots in the snippet: $l = 1; while (1) {... if (h) {break;}; l = 0; break;}$ , is executed irrespective of the condition h in the first iteration, and thus there is no need to raise the $pc$ before checking that condition.

Stefan et al. [60] use special constructs to catch exceptions and convert them into normal values for enforcing IFC in Haskell. Hritcu et al. [39] propose the propagation of exception values as NaNs, and delay normal and IFC exceptions, changing the semantics of exception handling. Austin et al. [10] extend faceted execution to work with exceptions by including additional constructs to raise and catch exceptions. They use big-step semantics to define exception handling while our formalism uses small-step semantics. Our formalism also supports unstructured control flow, which is not considered in their semantics.

8. Conclusion

We have presented the design of a sound improvement and generalization of the permissive-upgrade strategy for dynamic information flow analysis. The development improves the original strategy’s permissiveness by relaxing the rules for handling partially-leaked data while retaining soundness. Additionally, the original strategy’s enforcement was limited to a two-point security lattice; we generalize that to an arbitrary lattice.

We also present a sound approach for improving the precision of runtime information flow analysis when handling unstructured control flow and exceptions. Existing approaches to handle these constructs are more conservative and often require additional annotations by the developer. In contrast, the methodology presented here performs a sound and precise runtime information flow analysis using post-dominator analysis to handle these features without requiring any additional annotations from the developer.

Footnotes

Proofs for improved and generalized permissive upgrade

Proofs for IFC with unstructured control flow and exceptions

References

Content Security Policy 1.0, http://www.w3.org/TR/CSP/.

Algehed and

Flanagan, Transparent IFC enforcement: Possibility and (in)efficiency results, in: 2020 IEEE 33rd Computer Security Foundations Symposium (CSF), 2020, pp. 65–78. doi:10.1109/CSF49147.2020.00013.

Algehed,

Russo and

Flanagan, Optimising faceted secure multi-execution, in: 2019 IEEE 32nd Computer Security Foundations Symposium (CSF), 2019, pp. 1–16.

Askarov,

Hunt,

Sabelfeld and

Sands, Termination-insensitive noninterference leaks more than just a bit, in: Proc. European Symposium on Research in Computer Security, 2008, pp. 333–348.

Askarov and

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

Askarov and

Sabelfeld, Catch me if you can: Permissive yet secure error handling, in: Proc. ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security, 2009, pp. 45–57. ISBN 978-1-60558-645-8. doi:10.1145/1554339.1554346.

T.H.

Austin and

Flanagan, Efficient purely-dynamic information flow analysis, in: Proc. ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security, 2009, pp. 113–124. ISBN 978-1-60558-645-8. doi:10.1145/1554339.1554353.

T.H.

Austin and

Flanagan, Permissive dynamic information flow analysis, in: Proc. 5th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, 2010, pp. 3:1–3:12. ISBN 978-1-60558-827-8. doi:10.1145/1814217.1814220.

T.H.

Austin and

Flanagan, Multiple facets for dynamic information flow, in: Proc. 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012, pp. 165–178. ISBN 978-1-4503-1083-3. doi:10.1145/2103656.2103677.

10.

T.H.

Austin,

Schmitz and

Flanagan, Multiple facets for dynamic information flow with exceptions, ACM Trans. Program. Lang. Syst. 39(3) (2017). doi:10.1145/3024086.

11.

Barth, The web origin concept, http://tools.ietf.org/html/rfc6454.

12.

Bedford,

Chong,

Desharnais,

Kozyri and

Tawbi, A progress-sensitive flow-sensitive inlined information-flow control monitor, Computers & Security 71 (2017), 114–131. doi:10.1016/j.cose.2017.04.001.

13.

Bichhawat,

Rajani,

Garg and

Hammer, Generalizing permissive-upgrade in dynamic information flow analysis, in: Proc. Workshop on Programming Languages and Analysis for Security, 2014, pp. 15–24. doi:10.1145/2637113.2637116.

14.

Bichhawat,

Rajani,

Garg and

Hammer, Information flow control in WebKit’s JavaScript bytecode, in: Proc. Principles of Security and Trust, 2014, pp. 159–178. doi:10.1007/978-3-642-54792-8_9.

15.

Birgisson,

Hedin and

Sabelfeld, Boosting the permissiveness of dynamic information-flow tracking by testing, in: Computer Security – ESORICS 2012, LNCS, Vol. 7459, Springer, Berlin Heidelberg, 2012, pp. 55–72. ISBN 978-3-642-33166-4. doi:10.1007/978-3-642-33167-1_4.

16.

Buiras,

Stefan and

Russo, On dynamic flow-sensitive floating-label systems, in: Proc. 2014 IEEE 27th Computer Security Foundations Symposium, CSF’14, IEEE Computer Society, 2014, pp. 65–79. doi:10.1109/CSF.2014.13.

17.

Chugh,

J.A.

Meister,

Jhala and

Lerner, Staged information flow for JavaScript, in: Proc. 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2009, pp. 50–62. doi:10.1145/1542476.1542483.

18.

Crockford, ADSafe, http://adsafe.org/.

19.

A.A.

de Amorim,

Fredrikson and

Jia, Reconciling noninterference and gradual typing, in: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’20, Association for Computing Machinery, New York, NY, USA, 2020, pp. 116–129. ISBN 9781450371049. doi:10.1145/3373718.3394778.

20.

D.E.

Denning, A lattice model of secure information flow, Commun. ACM 19(5) (1976), 236–243. doi:10.1145/360051.360056.

21.

D.E.

Denning and

P.J.

Denning, Certification of programs for secure information flow, Commun. ACM 20(7) (1977), 504–513. doi:10.1145/359636.359712.

22.

D.E.R.

Denning, Cryptography and Data Security, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1982. ISBN 0-201-10150-5.

23.

Devriese and

Piessens, Noninterference through secure multi-execution, in: Proc. 2010 IEEE Symposium on Security and Privacy, 2010, pp. 109–124. ISBN 978-0-7695-4035-1. doi:10.1109/SP.2010.15.

24.

Dhawan and

Ganapathy, Analyzing information flow in JavaScript-based browser extensions, in: Proc. 2009 Annual Computer Security Applications Conference, ACSAC’09, 2009, pp. 382–391. ISBN 978-0-7695-3919-5. doi:10.1109/ACSAC.2009.43.

25.

Disney and

Flanagan, Gradual information flow typing, in: Proceedings of the 2nd International Workshop on Scripts to Programs Evolution, STOP’11, 2011.

26.

Dong,

Chen,

Siadati,

Tople,

Saxena and

Liang, Protecting sensitive web content from client-side vulnerabilities with CRYPTONS, in: Proc. 2013 ACM SIGSAC Conference on Computer and Communications Security, 2013, pp. 1311–1324.

27.

Facebook. FBJS, https://developers.facebook.com/docs/javascript.

28.

Fennell and

Thiemann, Gradual security typing with references, in: Proceedings of the 2013 IEEE 26th Computer Security Foundations Symposium, CSF’13, IEEE Computer Society, Washington, DC, USA, 2013, pp. 224–239. ISBN 978-0-7695-5031-2. doi:10.1109/CSF.2013.22.

29.

Fennell and

Thiemann, LJGS: Gradual security types for object-oriented languages, in: 30th European Conference on Object-Oriented Programming, ECOOP, 2016, 2016, pp. 9:1–9:26.

30.

J.S.

Fenton, Memoryless subsystems, The Computer Journal 17(2) (1974), 143. doi:10.1093/comjnl/17.2.143.

31.

J.A.

Goguen and

Meseguer, Security policies and security models, in: Proc. 1982 IEEE Symposium on Security and Privacy, 1982, pp. 11–20. doi:10.1109/SP.1982.10014.

32.

Google Caja – A source-to-source translator for securing JavaScript-based web content, Online; accessed 25-Apr-2017.

33.

Guarnieri,

Pistoia,

Tripp,

Dolby,

Teilhet and

Berg, Saving the world wide web from vulnerable JavaScript, in: Proc. 2011 International Symposium on Software Testing and Analysis, ISSTA’11, 2011, pp. 177–187. ISBN 978-1-4503-0562-4. doi:10.1145/2001420.2001442.

34.

G.L.

Guernic,

Banerjee,

Jensen and

D.A.

Schmidt, Automata-based confidentiality monitoring, in: Proc. Asian Computing Science Conference on Secure Software, 2006, pp. 75–89.

35.

Hammer and

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

36.

Hedin,

Bello and

Sabelfeld, Value-sensitive hybrid information flow control for a JavaScript-like language, in: Proc. 2015 IEEE 28th Computer Security Foundations Symposium, CSF’15, 2015, pp. 351–365. doi:10.1109/CSF.2015.31.

37.

Hedin,

Birgisson,

Bello and

Sabelfeld, JSFlow: Tracking information flow in JavaScript and its APIs, in: Proc. ACM Symposium on Applied Computing, 2014, pp. 1663–1671. doi:10.1145/2554850.2554909.

38.

Hedin and

Sabelfeld, Information-flow security for a core of JavaScript, in: Proc. 25th IEEE Computer Security Foundations Symposium, 2012, pp. 3–18. ISBN 978-0-7695-4718-3. doi:10.1109/CSF.2012.19.

39.

Hritcu,

Greenberg,

Karel,

B.C.

Pierce and

Morrisett, All your IFCException are belong to us, in: Proceedings of the 2013 IEEE Symposium on Security and Privacy, SP’13, IEEE Computer Society, USA, 2013, pp. 3–17. ISBN 9780769549774. doi:10.1109/SP.2013.10.

40.

Hunt and

Sands, On flow-sensitive security types, in: Proc. ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2006, pp. 79–90.

41.

Jang,

Jhala,

Lerner and

Shacham, An empirical study of privacy-violating information flows in JavaScript web applications, in: Proc. 17th ACM Conference on Computer and Communications Security, 2010, pp. 270–283.

42.

Just,

Cleary,

Shirley and

Hammer, Information flow analysis for JavaScript, in: Proc. 1st ACM SIGPLAN International Workshop on Programming Language and Systems Technologies for Internet Clients, 2011, pp. 9–18. ISBN 978-1-4503-1171-7. doi:10.1145/2093328.2093331.

43.

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

44.

Lengauer and

R.E.

Tarjan, A fast algorithm for finding dominators in a flowgraph, ACM Trans. Program. Lang. Syst. 1(1) (1979), 121–141. doi:10.1145/357062.357071.

45.

M.T.

Louw,

K.T.

Ganesh and

V.N.

Venkatakrishnan, AdJail: Practical enforcement of confidentiality and integrity policies on web advertisements, in: Proc. 19th USENIX Conference on Security, 2010, pp. 24–24.

46.

Masri and

Podgurski, Algorithms and tool support for dynamic information flow analysis, Information & Software Technology 51(2) (2009), 385–404. doi:10.1016/j.infsof.2008.05.008.

47.

L.A.

Meyerovich and

Livshits, ConScript: Specifying and enforcing fine-grained security policies for JavaScript in the browser, in: Proc. 2010 IEEE Symposium on Security and Privacy, 2010, pp. 481–496. doi:10.1109/SP.2010.36.

48.

A.C.

Myers, JFlow: Practical mostly-static information flow control, in: Proc. 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’99, 1999, pp. 228–241.

49.

Nentwich,

Jovanovic,

Kirda,

Kruegel and

Vigna, Cross-site scripting prevention with dynamic data tainting and static analysis, in: Proc. Network and Distributed System Security Symposium, 2007.

50.

Nikiforakis,

Invernizzi,

Kapravelos,

Van Acker,

Joosen,

Kruegel,

Piessens and

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

51.

Pottier and

Simonet, Information flow inference for ML, ACM Trans. Program. Lang. Syst. 25(1) (2003), 117–158. doi:10.1145/596980.596983.

52.

Rafnsson and

Sabelfeld, Secure multi-execution: Fine-grained, declassification-aware, and transparent, in: Proc. 2013 IEEE 26th Computer Security Foundations Symposium, 2013, pp. 33–48. doi:10.1109/CSF.2013.10.

53.

Richards,

Hammer,

Burg and

Vitek, The eval that men do – a large-scale study of the use of eval in JavaScript applications, in: ECOOP’11,

Mezzini, ed., LNCS, Vol. 6813, 2011, pp. 52–78. ISBN 978-3-642-22654-0.

54.

Richards,

Hammer,

Zappa Nardelli,

Jagannathan and

Vitek, Flexible access control for Javascript, in: Proc. 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA’13, 2013, pp. 305–322. ISBN 978-1-4503-2374-1. doi:10.1145/2509136.2509542.

55.

Russo and

Sabelfeld, Dynamic vs. static flow-sensitive security analysis, in: Proc. 2010 IEEE 23rd Computer Security Foundations Symposium, 2010, pp. 186–199. doi:10.1109/CSF.2010.20.

56.

Sabelfeld and

A.C.

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

57.

Sabelfeld and

Russo, From dynamic to static and back: Riding the roller coaster of information-flow control research, in: Proc. Perspectives of Systems Informatics, 2010, pp. 352–365. doi:10.1007/978-3-642-11486-1_30.

58.

Schmitz,

Algehed,

Flanagan and

Russo, Faceted secure multi execution, in: ACM CCS, 2018, pp. 1617–1634. ISBN 9781450356930. doi:10.1145/3243734.3243806.

59.

A.L.

Scull Pupo,

Christophe,

Nicolay,

de Roover and

Gonzalez, Boix, Practical Information Flow Control for Web Applications,

Verification,

Colombo and

Leucker, eds, Springer International Publishing, Cham, 2018, pp. 372–388. ISBN 978-3-030-03769-7.

60.

Stefan,

Mazières,

J.C.

Mitchell and

Russo, Flexible dynamic information flow control in the presence of exceptions, J. Funct. Program. 27 (2017), e5. doi:10.1017/S0956796816000241.

61.

Stefan,

E.Z.

Yang,

Marchenko,

Russo,

Herman,

Karp and

Mazières, Protecting users by confining JavaScript with COWL, in: Proc. USENIX Symposium on Operating Systems Design and Implementation, 2014, pp. 131–146.

62.

Toro,

Garcia and

Tanter, Type-driven gradual security with references, ACM Trans. Program. Lang. Syst. 40(4) (2018), 16:1–16:55. doi:10.1145/3229061.

63.

Van Acker,

De Ryck,

Desmet,

Piessens and

Joosen, WebJail: Least-privilege integration of third-party components in web mashups, in: Proc. 27th Annual Computer Security Applications Conference, 2011, pp. 307–316.

64.

Vogt,

Nentwich,

Jovanovic,

Kirda,

Krügel and

Vigna, Cross site scripting prevention with dynamic data tainting and static analysis, in: Proceeding of the Network and Distributed System Security Symposium, 2007, https://www.isoc.org/isoc/conferences/ndss/07/papers/cross-site-scripting_prevention.pdf .

65.

Volpano,

Irvine and

Smith, A sound type system for secure flow analysis, J. Comput. Secur. 4(2–3) (1996), 167–187. doi:10.3233/JCS-1996-42-304.

66.

Xin and

Zhang, Efficient online detection of dynamic control dependence, in: Proc. 2007 International Symposium on Software Testing and Analysis, 2007, pp. 185–195. ISBN 978-1-59593-734-6. doi:10.1145/1273463.1273489.

67.

Yang,

Yessenov and

Solar-Lezama, A language for automatically enforcing privacy policies, in: Proc. 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’12, 2012, pp. 85–96.

68.

S.A.

Zdancewic, Programming Languages for Information Security, PhD thesis, Cornell University, 2002.

69.

Zhou and

Evans, Protecting private web content from embedded scripts, in: Proc. 16th European Conference on Research in Computer Security, 2011, pp. 60–79.

Permissive runtime information flow control in the presence of exceptions

Abstract

Keywords

1. Introduction

2. Background and overview

2.1. Information flow control

1 “x is labeled H” actually means “the value in x is labeled H”. This language convention is used consistently in the paper.

Definition 1 (Value equivalence).

Definition 2 (Store equivalence).

Theorem 1 (TINI for NSU).

Proof. Standard, see e.g., [7]. □ 2.5. Permissive-upgrade strategy for handling implicit leaks

Proof. See [8]. □ 3. Improved permissive-upgrade strategy

Proof. By induction on e. □ Lemma 2 (Evolution).

Proof. By induction on the derivation rules and case analysis on the last rule. □ Lemma 3 (Confinement for improved permissive-upgrade with a two-point lattice).

Proof. By induction on the given derivation. □ Theorem 3 (TINI for improved permissive-upgrade with a two-point lattice).

4.1. Generalized improved permissive-upgrade strategy on powerset lattices

Definition 5. Two labeled values n 1 k and n 2 m are a-equivalent, written n 1 k ≈ a n 2 m , iff either: k ( a ) = m ( a ) = L and n 1 = n 2 or k ( a ) = m ( a ) = H or k ( a ) = P or m ( a ) = P Definition 6 (Store equivalence).

Theorem 4 (TINI for permissive-upgrade with a product lattice).

Proof. By induction on e. □ Lemma 5 (⋆-preservation).

Proof. By induction on the given derivation. □ Corollary 1. If ⟨ σ , c ⟩ ⇓ pc σ ′ and Γ ( σ ( x ) ) = ℓ ⋆ and Γ ( σ ′ ( x ) ) = ℓ ′ , then pc ⊑ ℓ . Proof. Immediate from Lemma 5. □ Lemma 6 ( pc -lemma).

Proof. By induction on the given derivation. □ Theorem 5 (TINI for generalized permissive-upgrade for arbitrary lattices).

Proof. By induction on c. □ 4.4. Comparison of the generalization of Section 4.2 with the generalization of Section 4.1

5.1. Control flow graphs and post-dominator analysis

5.2. Synthetic exit nodes

5.3. Precision proofs

Definition 9 (Control flow graph).

Definition 10 (Path).

Definition 11 (Branch-point).

Definition 12 (Post-dominator).

Definition 13 (Immediate post-dominator).

Theorem 6 (Precision).

Definition 15 (State equivalence).

Lemma 8 (Confinement lemma).

Theorem 8. Suppose: ⟨ σ 1 , ι 1 , ρ 1 ⟩ ∼ ℓ ⟨ σ 2 , ι 2 , ρ 2 ⟩ ⟨ σ 1 , ι 1 , ρ 1 ⟩ → ∗ ⟨ σ 1 ′ , end , [ ] ⟩ ⟨ σ 2 , ι 2 , ρ 2 ⟩ → ∗ ⟨ σ 2 ′ , end , [ ] ⟩ Then, σ 1 ′ ∼ ℓ σ 2 ′ . 7. Related work

7.1. Permissive IFC

7.2. IFC with error handling

8. Conclusion

Footnotes

Proofs for improved and generalized permissive upgrade

Proofs for IFC with unstructured control flow and exceptions

References

¹
“x is labeled H” actually means “the value in x is labeled H”. This language convention is used consistently in the paper.

Proof.
Standard, see e.g., [7]. □

2.5. Permissive-upgrade strategy for handling implicit leaks

Proof.
See [8]. □
3. Improved permissive-upgrade strategy

Proof.
By induction on e. □
Lemma 2 (Evolution).

Proof.
By induction on the derivation rules and case analysis on the last rule. □
Lemma 3 (Confinement for improved permissive-upgrade with a two-point lattice).

Proof.
By induction on the given derivation. □
Theorem 3 (TINI for improved permissive-upgrade with a two-point lattice).

Definition 5.
Two labeled values $n_{1}^{k}$ and $n_{2}^{m}$ are a-equivalent, written $n_{1}^{k} \approx^{a} n_{2}^{m}$ , iff either:
$k (a) = m (a) = L$ and $n_{1} = n_{2}$ or

$k (a) = m (a) = H$ or

$k (a) = P$ or $m (a) = P$

Definition 6 (Store equivalence).

Proof.
By induction on e. □
Lemma 5 (⋆-preservation).

Proof.
By induction on the given derivation. □
Corollary 1.
If $⟨ σ, c ⟩ \underset{pc}{⇓} σ^{'}$ and $Γ (σ (x)) = ℓ^{⋆}$ and $Γ (σ^{'} (x)) = ℓ^{'}$ , then $pc ⊑ ℓ$ .
Proof.
Immediate from Lemma 5. □
Lemma 6 ( $pc$ -lemma).

Proof.
By induction on the given derivation. □
Theorem 5 (TINI for generalized permissive-upgrade for arbitrary lattices).

Proof.
By induction on c. □

4.4. Comparison of the generalization of Section 4.2 with the generalization of Section 4.1

Theorem 8.
Suppose:
$⟨ σ_{1}, ι_{1}, ρ_{1} ⟩ \sim_{ℓ} ⟨ σ_{2}, ι_{2}, ρ_{2} ⟩$

$⟨ σ_{1}, ι_{1}, ρ_{1} ⟩ \to^{} ⟨ σ_{1}^{'}, end, [] ⟩$

$⟨ σ_{2}, ι_{2}, ρ_{2} ⟩ \to^{} ⟨ σ_{2}^{'}, end, [] ⟩$
Then, $σ_{1}^{'} \sim_{ℓ} σ_{2}^{'}$ .
7. Related work