On the expressiveness and semantics of information flow types

1. Introduction

Information Flow Control (IFC) is a technique for tracking flows of information between different elements of a computer system. This is often used to prevent illicit flows with respect to a relevant security policy. In a language-based setting, IFC can be performed dynamically using runtime monitoring [5,6] or statically using type systems [1,8–10,15,19,20,22,27] for instance. In this paper, we focus only on the latter, i.e., on type-based approaches for IFC.

IFC type systems use security labels (elements of a security lattice) for tracking and prohibiting undesired flows of information. There are two significant aspects of security labels that govern the expressiveness of a sound type system, i.e., how many secure programs the type system can accept.1

The second aspect, which is the focus of this paper, is the granularity of labeling (which is different from the granularity of the label itself). It pertains to the extent to which labeling is used on a program. Under this classification, a fine-grained type system is one which labels every program value individually by including a label in every type. For instance, FlowCaml [22] is a fine-grained IFC type system for ML. Every type constructor in FlowCaml is annotated with a security label. For example, ( A H × B L ) L could be the type of low (public) pairs whose first component is high (secret) and second component is low. Here, H and L are standard labels used to denote high and low data respectively. For soundness, the label of a value must be an upper-bound on the labels of all the values that the value depends on. For instance, adding a low value to a high value must produce a high value. Therefore, a fine-grained type system must track such flows through all the operations in the language. These principles are embodied in several other type systems besides FlowCaml [9,15,20,27].

Coarse-grained type systems [1,8,10,19], on the other hand, are very different. They do not assign a label to every individual value. Instead, a label is associated with an entire sub-computation. Values in the scope of the sub-computation implicitly inherit the label of the sub-computation.2

Looking at these vastly contrasting type systems for enforcing information flow control, a natural question that arises is that of their relative expressiveness [23]. By this we mean whether all programs that can be expressed in a fine-grained type system can also be expressed in a coarse-grained type system (and vice versa)? Upfront, it seems that a fine-grained type system should be able to express every program that a coarse-grained type system can, as the former abstracts less flows than the later. But the reverse (expressing a fine-grained type system in a coarse-grained one) is not immediately obvious. However, then one wonders if by structuring programs as extremely small sub-computations in a coarse-grained type system one may recover the expressiveness of a fine-grained type system after all.

In this paper, we show that both these intuitions are actually correct. We do this constructively, by showing an embedding of a fine-grained type system in a coarse-grained type system and vice versa. We do this in the setting of a higher-order language with state, to which we assign a fine-grained and a coarse-grained type system. For the fine-grained type system, we choose a system which is very close to SLAM [15] and the exception-free fragment of FlowCaml [22]. We call this type system FG here. For the coarse-grained type system, we work with SLIO ∗ , a variant of SLIO mentioned above. We show that FG and SLIO ∗ are actually equi-expressive, by showing translations from FG to SLIO ∗ and from SLIO ∗ to FG.

While this is sufficient to prove the equi-expressiveness of fine-grained and coarse-grained IFC type systems, we note that the translation from FG to SLIO ∗ is quite complex, making essential use of label quantification and constraint types. Going further, we examine the cause of this complexity. We show that this complexity arises due to the use of the Hoare state monad for enforcing IFC in SLIO ∗ . To confirm this, we design a new coarse-grained type system, CG, which uses a monad different from that of SLIO ∗ . CG’s monad is also doubly indexed but does not interpret the two labels as precondition (input) and postcondition (output). This leads to a different proof theory for CG. A consequence of this change is that the translation from FG to CG is far simpler than that from FG to SLIO ∗ . Our translations between FG and CG show not only the equi-expressiveness of FG and CG but also CG and SLIO ∗ (indirectly through FG). Concretely, we present four translations in this paper: a) FG to SLIO ∗ b) SLIO ∗ to FG c) FG to CG and d) CG to FG. Taken separately, (a and b) or (c and d) suffices to show the equi-expressiveness of fine-grained and coarse-grained type systems. However, we use translations (b and c) and (d and a) to also show that SLIO ∗ and CG are equi-expressive, i.e., the change from SLIO ∗ to CG does not lead to any loss of expressiveness.

We believe that this resolves the question of the relative expressiveness of fine-grained and coarse-grained IFC type systems. A practical consequence of our theoretical results is that, since a coarse-grained type system involves less labeling annotations than a fine-grained one, a programmer can always choose to work with a coarse-grained type system without worrying about its expressiveness. In places where the precision of the fine-grained type system is really required, it can be simulated in the coarse-grained type system itself, following our (constructive) embedding of the fine-grained type system in the coarse-grained one.

As a second contribution of independent interest, we describe how to set up logical-relation based semantic models for the three type systems (FG, SLIO ∗ and CG) over calculi with higher-order state. While models of IFC types have been studied before [1,15,18,25], we do not know of any development that covers higher-order state. In fact, even in the absence of IFC, models of types with higher-order state are known to be difficult. We have the added complexity of dealing with information flow labels. Our models build on developments in the programming languages community in the past decade. Specifically, our models are based on step-indexed Kripke logical relations [2]. Like prior work on IFC types, our models are relational, i.e., they relate two runs of a program to each other. This is essential since we are interested in proving noninterference [14], the standard security property which says that public outputs of a program are not influenced by private inputs. This property is naturally defined using two runs. Using our models, we derive proofs of soundness of the fine-grained and both of the coarse-grained type systems.

We also use our logical relations to show that our translations are meaningful. Specifically, we set up cross-language logical relations to prove that our translations preserve program semantics, and from this, we derive a crucial result for each translation: Using the noninterference theorem of the target language as a lemma, we are able to re-prove the noninterference theorem for the source language directly. This implies that our translations preserve labels meaningfully [7]. Like all logical relations models, we expect that our models can be used for other purposes as well.

To summarize we make the following contributions through this work:

Accompanying appendix. Many technical details omitted from the paper to keep its length manageable are presented in an online appendix available from the authors’ homepages.

Differences from the conference version. This paper is an extended version of a paper that appeared in CSF 2018 [24]. The conference version showed only the translations from FG to CG (and vice versa), omitting the translations from FG to SLIO ∗ (and vice versa). This omitted material is covered in the completely new Section 3 of this paper. Accompanying this, Section 2.2 which recaps SLIO ∗ and presents its novel logical relations model, is also new. Compared to CG, which is a type system we designed ourselves for the purpose of exposition, SLIO ∗ is (very similar to) an existing type system and, hence, understanding its expressiveness relative to a fine-grained system is a more meaningful goal.

In this section, we describe the fine-grained type system and one of the two coarse-grained type systems we work with. Both these type systems are set up for higher-order stateful languages, but differ considerably in how they enforce IFC. The fine-grained type system, FG, works on a language with pervasive side-effects like ML, and associates a security label with every expression in the language. The coarse-grained type system, SLIO ∗ , works on a language that isolates state in a monad (like Haskell’s IO monad) and tracks flows coarsely at the granularity of a monadic computation, not on pure values within a monadic computation.

Both FG and SLIO ∗ use security labels (denoted by ℓ) drawn from an arbitrary security lattice ( L , ⊑ ). We denote the least and top element of the lattice by ⊥ and ⊤ respectively. As usual, the goal of the type systems is to ensure that outputs labeled ℓ depend only on inputs with security labels ℓ or lower. For drawing intuitions, we find it convenient to think of a confidentiality lattice (labels higher in the lattice represent higher confidentiality). However, nothing in our technical development is specific to a confidentiality lattice – the development works for any security lattice including an integrity lattice and a product lattice for confidentiality and integrity.

2.1. The fine-grained type system, FG

OPEN IN VIEWER

Fig. 1.

Language syntax and type system of FG (selected rules).

FG is based on the SLam calculus [15], but uses a presentation similar to Flow Caml, an IFC type system for ML [22]. It works on a call-by-value, eager language, which is a simplification of ML. The syntax of the language is shown at the top of Fig. 1. The language has the usual constructs for functions, pairs, sums, and mutable references (heap locations). Along with that the language also includes constructs for label quantification ( Λ e is the introduction form and e [ ] is the elimination form) and constraint types ( ν e is the introduction form and e ∙ is the elimination form). The expression ! e dereferences the location that e evaluates to, while e 1 : = e 2 assigns the value that e 2 evaluates to, to the location that e 1 evaluates to. The dynamic semantics of the language are defined by a “big-step” judgment ( H , e ) ⇓ j ( H ′ , v ) , which means that starting from heap H, expression e evaluates to value v, ending with heap H ′ . This evaluation takes j steps. The number of steps is important only for our logical relations models. The rules for the big-step judgment are standard, hence omitted here.

Every type τ in FG, including a type nested inside another, carries a security label. The security label represents the confidentiality level of the values the type ascribes. It is also convenient to define unlabeled types, denoted A , as shown in Fig. 1.

Typing rules. FG uses the typing judgment Σ ; Ψ ; Γ ⊢ pc e : τ . As usual, Γ maps free variables of e to their types, Σ is a set of a label variables and Ψ is a set of label constraints. The judgment basically says that, an expression e is of type τ under the assumptions specified by Σ (a set of a label variables), Ψ (a set of label constraints) and Γ (a mapping from a variable to its type). The annotation pc is also a label drawn from L , often called the “program counter” label. This label is a lower bound on the write effects of e. The type system ensures that any reference that e writes to is at a level pc or higher. This is necessary to prevent information leaks via the heap. A similar annotation, ℓ e , appears in the function type τ 1 → ℓ e τ 2 , type for label quantification ∀ α . ( ℓ e , τ ) and constraint type c ⇒ ℓ e τ . Here, ℓ e is a lower bound on the write effects of the body of the function.

FG’s typing rules are shown in Fig. 1. We describe some of the important rules. In the rule for case analysis (FG-case), if the case analyzed expression e has label ℓ, then both the case branches are typed in a pc that is joined with ℓ. This ensures that the branches do not have write effects below ℓ, which is necessary for IFC since the execution of the branches is control dependent on a value (the case condition) of confidentiality ℓ. Similarly, the type of the result of the case branches, τ, must have a top-level label at least ℓ. This is indicated by the premise τ ↘ ℓ and prevents implicit leaks via the result. The relation τ ↘ ℓ , read “τ protected at ℓ” [1], means that if τ = A ℓ ′ , then ℓ ⊑ ℓ ′ .

The rule for function application (FG-app) states if the function expression e 1 being applied has type ( τ 1 → ℓ e τ 2 ) ℓ , then ℓ must be below ℓ e and the result τ 2 must be protected at ℓ to prevent implicit leaks arising from the identity of the function that e 1 evaluates to. FG-FE and FG-CE are similar.

In the rule for assignment (FG-assign), if the expression e 1 being assigned has type ( ref τ ) ℓ , then τ must be protected at pc ⊔ ℓ to ensure that the written value (of type τ) has a label above pc and ℓ. The former enforces the meaning of the judgment’s pc , while the latter protects the identity of the reference that e 1 evaluates to.

OPEN IN VIEWER

Fig. 2.

FG subtyping.

All introduction rules such as those for λs, pairs and sums produce expressions labeled ⊥. This label can be weakened (increased) freely with the subtyping rule FGsub-label. The other subtyping rules (described in Fig. 2) are the expected ones, e.g., subtyping for unlabeled function types τ 1 → ℓ e τ 2 is co-variant in τ 2 and contra-variant in τ 1 and ℓ e (contra-variance in ℓ e is required since ℓ e is a lower bound on an effect). Subtyping for ref τ is invariant in τ, as usual.

The main meta-theorem of interest to us is soundness. This theorem says that every well-typed expression is noninterferent, i.e., the result of running an expression of a type labeled low is independent of substitutions used for its high-labeled free variables. This theorem is formalized below. Note that we work here with what is called termination-insensitive noninterference; we briefly discuss the termination-sensitive variant in Section 6.

Theorem 2.1 (Noninterference for FG).

Suppose (1) ℓ i ⋢ ℓ , (2) x : A ℓ i ⊢ pc e : bool ℓ , and (3) v 1 , v 2 : A ℓ i . If both e [ v 1 / x ] and e [ v 2 / x ] terminate, then they produce the same value (of type bool ).

By definition, noninterference, as stated above is a relational (binary) property, i.e., it relates two runs of a program. Next, we show how to build a semantic model of FG’s types that allows proving this property.

2.1.1. Semantic model of FG

OPEN IN VIEWER

Fig. 3.

Unary value, expression, and heap conformance relations for FG.

We now describe our new semantic model of FG’s types. We use this model to show that the type system is sound (Theorem 2.1) and later to prove the soundness of our translations. Our semantic model uses the technique of step-indexed Kripke logical relations [2] and is more directly based on a model of types in a different domain, namely, incremental computational complexity [11]. In particular, our model captures all the invariants necessary to prove noninterference.

The central idea behind our model is to interpret each type in two different ways – as a set of values (unary interpretation), and as a set of pairs of values (binary interpretation). The binary interpretation is used to relate low-labeled types in the two runs mentioned in the noninterference theorem, while the unary interpretation is used to interpret high-labeled types independently in the two runs (since high-labeled values may be unrelated across the two runs). What is high and what is low is determined by the level of the observer (adversary), which is a parameter to our binary interpretation. Remark.

Readers familiar with earlier models of IFC type systems [1,15,25] may wonder why we need a unary relation, when prior work did not. The reason is that we handle an effect (mutable state) in our model, which prior work did not. In the absence of effects, the unary model is unnecessary. In the presence of effects, the unary relation captures what is often called the “confinement lemma” in proofs of noninterference – we need to know that while the two runs are executing high branches independently, neither will modify low-labeled locations.

Unary interpretation. The unary interpretation of types is shown in Fig. 3. The interpretation is actually a Kripke model. It uses worlds, written θ, which specify the type for each valid (allocated) location in the heap. For example, θ ( a ) = bool H means that location a should hold a high boolean. The world can grow as the program executes and allocates more locations. A second important component used in the interpretation is a step-index, written m or n [3]. Step-indices are natural numbers, and are merely a technical device to break a non-well-foundedness issue in Kripke models of higher-order state, like this one. Our use of step-indices is standard and readers may ignore them.

The interpretation itself consists of three mutually inductive relations – a value relation for types (labeled and unlabeled), written ⌊ τ ⌋ V ; an expression relation for labeled types, written ⌊ τ ⌋ E pc ; and a heap conformance relation, written ( n , H ) ⊳ θ . These relations are well-founded by induction on the step indices n and types. This is the only role of step-indices in our model.

The value relation ⌊ τ ⌋ V defines, for each type, which values (at which worlds and step-indices) lie in that type. For base types b , this is straightforward: All syntactic values of type b (written ⟦ b ⟧ ) lie in ⌊ b ⌋ V at any world and any step index. For pairs, the relation is the intuitive one: ( v 1 , v 2 ) is in ⌊ τ 1 × τ 2 ⌋ V iff v 1 is in ⌊ τ 1 ⌋ V and v 2 is in ⌊ τ 2 ⌋ V . The function type τ 1 → ℓ e τ 2 contains a value λ x . e at world θ if in any world θ ′ that extends θ, if v is in ⌊ τ 1 ⌋ V , then ( λ x . e ) v or, equivalently, e [ v / x ] , is in the expression relation ⌊ τ 2 ⌋ E ℓ e . We describe this expression relation below. Importantly, we allow for the world θ to be extended to θ ′ since between the time that the function λ x . e was created and the time that the function is applied, new locations could be allocated. Value relation for label quantification ( ∀ α . ( ℓ e , τ ) ) and constraint type ( c ⇒ ℓ e τ ) follows intuition similar to the function type. The type ref τ contains all locations a whose type according to the world θ matches τ. Finally, security labels play no role in the unary interpretation, so ⌊ A ℓ ⌋ V = ⌊ A ⌋ V (in contrast, labels play a significant role in the binary interpretation).

The expression relation ⌊ τ ⌋ E pc defines, for each type, which expressions lie in the type (at each pc , each world θ and each step index n). The definition may look complex, but is relatively straightforward: e is in ⌊ τ ⌋ E pc if for any heap H that conforms to the world θ such that running e starting from H results in a value v ′ and a heap H ′ , there is a some extension θ ′ of θ to which H ′ conforms and at which v ′ is in ⌊ τ ⌋ V . Additionally, all writes performed during the execution (defined as the locations at which H and H ′ differ) must have labels above the program counter, pc . In simpler words, the definition simply says that e lies in ⌊ τ ⌋ E pc if its resulting value is in ⌊ τ ⌋ V , it preserves heap conformance with worlds and, importantly, its write effects are at labels above pc . (Readers familiar with proofs of noninterference should note that the condition on write effects is our model’s analogue of the so-called “confinement lemma”.)

OPEN IN VIEWER

Fig. 4.

Binary value, expression and heap conformance relations for FG.

The heap conformance relation ( n , H ) ⊳ θ defines when a heap H conforms to a world θ. The relation is simple; it holds when the heap H maps every location to a value in the semantic interpretation of the location’s type given by the world θ.

Binary interpretation. The binary interpretation of types is shown in Fig. 4. This interpretation relates two executions of a program with different inputs. Like the unary interpretation, this interpretation is also a Kripke model. Its worlds, written W, are different, though. Each world is a triple W = ( θ 1 , θ 2 , β ˆ ) . θ 1 and θ 2 are unary worlds that specify the types of locations allocated in the two executions. Since executions may proceed in sync on the two sides for a while, then diverge in a high-labeled branch, then possibly re-synchronize, and so on, some locations allocated on one side may have analogues on the other side, while other locations may be unique to either side. This is captured by β ˆ , which is a partial bijection between the domains of θ 1 and θ 2 . If ( a 1 , a 2 ) ∈ β ˆ , then location a 1 in the first run corresponds to location a 2 in the second run. Any location not in β ˆ has no analogue on the other side.

As before, the interpretation itself consists of three mutually inductive relations – a value relation for types (labeled and unlabeled), written ⌈ τ ⌉ V A ; an expression relation for labeled types, written ⌈ τ ⌉ E A ; and a heap conformance relation, written ( n , H 1 , H 2 ) ⊳ A W . These relations are all parameterized by the level of the observer (adversary), A , which is an element of L .

The value relation ⌈ τ ⌉ V A defines, for each type, which pairs of values from the two runs are related by that type (at each world, each step-index and each adversary). At base types, b , only identical values are related. For pairs, the relation is the intuitive one: ( v 1 , v 2 ) and ( v 1 ′ , v 2 ′ ) are related in ⌈ τ 1 × τ 2 ⌉ V A iff v i and v i ′ are related in ⌈ τ i ⌉ V A for i ∈ { 1 , 2 } . Two values are related at a sum type only if they are both left injections or both right injections. At the function type τ 1 → ℓ e τ 2 , two functions are related if they map values related at the argument type τ 1 to expressions related at the result type τ 2 . For technical reasons, we also need both the functions to satisfy the conditions of the unary relation. At a reference type ref τ , two locations a 1 and a 2 are related at world W = ( θ 1 , θ 2 , β ˆ ) only if they are related by β ˆ (i.e., they are correspondingly allocated locations) and their types as specified by θ 1 and θ 2 are equal to τ.

Finally, and most importantly, at a labeled type A ℓ , ⌈ A ℓ ⌉ V A relates values depending on the ordering between ℓ and the adversary A . When ℓ ⊑ A , the adversary can see values labeled ℓ, so ⌈ A ℓ ⌉ V A contains exactly the values related in ⌈ A ⌉ V A . When ℓ ⋢ A , values labeled ℓ are opaque to the adversary (in colloquial terms, they are “high”), so they can be arbitrary. In this case, ⌈ A ℓ ⌉ V A is the cross product of the unary interpretation of A with itself. This is the only place in our model where the binary and unary interpretations interact.

The expression relation ⌈ τ ⌉ E A defines, for each type, which pairs of expressions from the two executions lie in the type (at each world W, each step index n and each adversary  A ). The definition is similar to that in the unary case: e 1 and e 2 lie in ⌈ τ ⌉ E A if the values they produce are related in the value relation ⌈ τ ⌉ V A , and the expressions preserve heap conformance.

The heap conformance relation ( n , H 1 , H 2 ) ⊳ A W defines when a pair of heaps H 1 , H 2 conforms to a world W = ( θ 1 , θ 2 , β ˆ ) . The relation requires that any pair of locations related by β ˆ have the same types (according to θ 1 and θ 2 ), and that the values stored in H 1 and H 2 at these locations lie in the binary value relation of that common type.

Meta-theory. The primary meta-theoretic property of a logical relations model like ours is the so-called fundamental theorem. This theorem says that any expression syntactically in a type (as established via the type system) also lies in the semantic interpretation (the expression relation) of that type. Here, we have two such theorems – one for the unary interpretation and one for the binary interpretation.

To write these theorems, we define unary and binary interpretations of contexts, ⌊ Γ ⌋ V and ⌈ Γ ⌉ V A , respectively. These interpretations specify when unary and binary substitutions conform to Γ. A unary substitution δ maps each variable to a value whereas a binary substitution γ maps each variable to two values, one for each run. ⌊ Γ ⌋ V ≜ { ( θ , n , δ ) | dom ( Γ ) ⊆ dom ( δ ) ∧ ∀ x ∈ dom ( Γ ) . ( θ , n , δ ( x ) ) ∈ ⌊ Γ ( x ) ⌋ } ⌈ Γ ⌉ V A ≜ { ( W , n , γ ) | dom ( Γ ) ⊆ dom ( γ ) ∧ ∀ x ∈ dom ( Γ ) . ( W , n , π 1 ( γ ( x ) ) , π 2 ( γ ( x ) ) ) ∈ ⌈ Γ ( x ) ⌉ }

Theorem 2.2 (Unary fundamental theorem).

If Σ ; Ψ ; Γ ⊢ pc e : τ , L ⊧ Ψ σ and ( θ , n , δ ) ∈ ⌊ Γ σ ⌋ V then ( θ , n , e δ ) ∈ ⌊ τ σ ⌋ E pc .

Theorem 2.3 (Binary fundamental theorem).

If Σ ; Ψ ; Γ ⊢ pc e : τ , L ⊧ Ψ σ and ( W , n , γ ) ∈ ⌈ Γ ⌉ V A , then ( W , n , e ( γ ↓ 1 ) , e ( γ ↓ 2 ) ) ∈ ⌈ τ σ ⌉ E A , where γ ↓ 1 and γ ↓ 2 are the left and right projections of γ.

The proofs of these theorems proceed by induction on the given derivations of Γ ⊢ pc e : τ . The proofs are tedious, but not difficult or surprising. The primary difficulty, as with all logical relations models, is in setting up the model correctly, not in proving the fundamental theorems.

FG’s noninterference theorem (Theorem 2.1) is a simple corollary of these two theorems.

2.2. The coarse-grained type system, SLIO ∗

In this section, we describe our first coarse-grained type system, SLIO ∗ . It is a minor variant of SLIO – the static fragment of the hybrid type system HLIO considered in [10]. SLIO ∗ is defined for a call-by-value calculus.4

⁴

The choice of call-by-value evaluation is made to match the evaluation approach used for FG. The original SLIO [10] is defined for a language with call-by-name evaluation.

We introduce some changes relative to SLIO ∗ . First, SLIO ∗ does not include the label construct of SLIO. This is because the label construct is the same as the standard monadic ret construct specialized to the Labeled type, with an additional label check. This label check is not required for noninterference (our soundness criterion) and is only needed for containment [26]. Hence, we omit it from SLIO ∗ . Also, we introduce label quantification and constraints in SLIO ∗ as in FG. Label quantification and constraints are required to make the translation from FG to SLIO ∗ work, as we explain later.

Unlike FG, SLIO ∗ makes a clear separation between pure and impure types. On the pure side, SLIO ∗ includes types for an effect-free function, product, sum, label quantification and constraints. Both the intro and the elim forms for these types are completely free from IFC (label) checks. Additionally, SLIO ∗ has a type for specifying labeled expressions. This type is written Labeled ℓ τ , where ℓ specifies the confidentiality associated with the type τ. This represents the type of a labeled expression which is evaluated eagerly. References serve as sources and sinks for data and hence must have well-defined confidentiality associated with them. This is done by associating a label with the reference type, ref ℓ τ . The label ℓ represents the label of the value stored in the reference or, in other words, a well-typed reference of type ref ℓ τ will always contain a value of type Labeled ℓ τ . On the impure side, SLIO ∗ represents effectful computations with a monadic type, i.e., all computations which can cause effects must be isolated in a monad. Hence, pc (the lower-bound on the write effect) is only relevant inside a monad. This is reflected by modeling (effectful) computations using a state monad (at the type level) which carries the initial and final pc as the state. The monadic type is represented by SLIO ℓ i ℓ o τ . ℓ i and ℓ o describe the initial and the final pc , and τ is the type of the value returned by forcing the computation of this monadic type.5

⁵

We use the term forcing to mean execution of the computation of the monadic type.

It is an invariant of the SLIO ∗ type system that if e : SLIO ℓ i ℓ o τ then ℓ i ⊑ ℓ o . As in the FG type system, ℓ i is used as a lower-bound on the write-effects (as seen in the SLIO ∗ -ref and SLIO ∗ -assign rules explained later). In addition to that, SLIO ∗ also has as an explicit representation for an upper-bound on the read effects (the final pc ℓ o in the SLIO ℓ i ℓ o τ type). This is in tandem with the core operational philosophy of coarse-grained IFC – the context label must be an upper bound on the confidentiality of the secrets read so far.

OPEN IN VIEWER

Fig. 5.

Syntax and type system of SLIO ∗ (selected rules).

OPEN IN VIEWER

Fig. 6.

SLIO ∗ subtyping (selected rules).

Having explained the various types of the SLIO ∗ type system, we now describe some of its selected typing rules from Fig. 5 (note that we have omitted the type rules for pure expressions from Fig. 5 as they are completely standard and do not refer to labels at all). The typing judgment for the SLIO ∗ type system is given by Σ ; Ψ ; Γ ⊢ e : τ where Σ, Ψ and Γ represent the typing environment as in the FG type system. Notice that SLIO ∗ ’s typing judgment does not carry a global pc because effects in SLIO ∗ are localized to the monads only and are not pervasive unlike the FG system. We start with SLIO ∗ -ret (the intro form for the monadic type). ret ( e ) takes an expression of type τ and returns a computation of type SLIO ℓ i ℓ i τ causing no change to the starting pc (which is ℓ i ). The elim form, bind ( e 1 , x . e 2 ) , for the monadic type represents sequencing of two computations of types SLIO ℓ ℓ 1 τ and τ → SLIO ℓ 1 ℓ ′ τ ′ to obtain a computation of type SLIO ℓ ℓ ′ τ ′ . bind is the only locus of dependency tracking in this type system. This is reflected by typing the continuation ( e 2 ) in a starting pc which equals the ending pc of the first computation ( e 1 ). The SLIO ∗ -label type rule says that if an expression e has type τ then the expression Lb ( e ) has type Labeled ℓ τ .6

⁶

Note that the Lb construct does not carry any runtime label. This is because all the enforcement is static in the type system so carrying runtime labels would be redundant.

While Lb ( e ) represents a pure expression, its dual unlabel ( e ) represents a computation which when forced in a starting pc of ℓ i will end up with a ending pc of ℓ i ⊔ ℓ where ℓ is the label on the type of e.

All the rules related to references perform heap-related effects and thus all of them have monadic types. SLIO ∗ -ref and SLIO ∗ -assign ensure that the reference created and modified respectively both get values whose confidentiality is above the confidentiality of the starting pc (lower-bound on the write effect denoted by ℓ in the type rules). Everything we have explained up to now models the conventional coarse-grained tracking, where reading (unlabeling) a secret value by a computation must make the pc secret for its continuation. This can be a problem when the continuation wants to produce a low output which does not depend on the read secret as this leads to a label creep – a situation where the output has a label higher than it ought to – and reduces precision. To help the programmer circumvent such label creep, SLIO ∗ has a construct ( toLabeled ) which can prevent the pc from being raised at the cost of returning a labeled value. toLabeled ( e ) coerces an expression (e) of type SLIO ℓ i ℓ o τ to an expression of type SLIO ℓ i ℓ i ( Labeled ℓ o τ ) . As a result the continuation of toLabeled ( e ) is not forced to start in an elevated pc of ℓ o . Instead, it can start in ℓ i and only if the continuation actually unlabels the result of the first expression (now of type Labeled ℓ o τ ) will the pc be raised to ℓ o .

Selected subtyping rules for SLIO ∗ are described in Fig. 6. Labeled ℓ τ is co-variant in ℓ; and SLIO ℓ i ℓ o τ is contra-variant in ℓ i and co-variant in ℓ o . This is natural as ℓ i is a pre-condition and ℓ o is a post-condition.

We prove soundness for SLIO ∗ by showing that every well-typed expression satisfies noninterference. Due to the presence of monadic types, the soundness theorem takes a specific form (shown below), and refers to a forcing semantics. These semantics operate on monadic types and actually perform reads and writes on the heap (in contrast, the pure evaluation semantics simply return suspended computations for monadic types). The forcing semantics are the expected ones, so we defer their details to the appendix.

Theorem 2.4 (Noninterference for SLIO ∗ ).

Suppose (1) ℓ i ⋢ ℓ , (2) x : Labeled ℓ i τ ⊢ e : SLIO _ ℓ bool , and (3) v 1 , v 2 : Labeled ℓ i τ . If both e [ v 1 / x ] and e [ v 2 / x ] terminate when forced, then they produce the same value (of type bool ).

2.2.1. Semantic model of SLIO ∗

We build a new semantic model of SLIO ∗ ’s types. The model is very similar in structure to the model of FG’s types. We use two interpretations, unary and binary, and worlds exactly as in FG’s model. The difference is that since state effects are confined to a monad in SLIO ∗ , all the constraints on heap updates move from the expression relations to the value relations at the monadic types as described in Fig. 7 and Fig. 8. Due to the similarity in the structure with FG’s model, we defer the remaining details of the SLIO ∗ ’s model to the appendix.

3. Translations between FG and SLIO ∗

In this section, we describe our translations from FG to SLIO ∗ and vice-versa, thus showing that these two type systems are equally expressive. We start with the translation from FG to SLIO ∗ .

OPEN IN VIEWER

Fig. 7.

Unary logical relation for SLIO ∗ (a snippet).

OPEN IN VIEWER

Fig. 8.

Binary logical relation for SLIO ∗ (a snippet).

3.1. Translating FG to SLIO ∗

Translating FG to SLIO ∗ is surprisingly very difficult. A translation was attempted previously in [23] but it only works for a subset of FG. The key idea behind our FG to SLIO ∗ translation is to index the type translation function with a label α; the type translation takes the form ⦇ τ ⦈ α . The index α can be thought of as a label propagated from the outer context, i.e., an additional label that protects τ. This indexing enables us to appropriately propagate labels in the translated SLIO ∗ types.

We begin by looking at the translation of the typing judgment for FG, which is essentially the type preservation theorem that we would eventually like to prove. Here, ⦇ Γ ⦈ β ′ ‾ is the pointwise lifting of the type translation to FG contexts ( β ′ ‾ is a list of labels, of the same length as Γ).

Theorem 3.1.

Suppose Σ ; Ψ ; Γ ⊢ pc e : τ in FG. Then, there exists e ′ such that Σ ; Ψ ; Γ ⊢ pc e : τ ⇝ e ′ and for any α ′ , β ′ ‾ , γ ′ with β ′ ‾ ⊔ γ ′ ⊑ pc ⊓ α ′ , there is a derivation of Σ ; Ψ ; ⦇ Γ ⦈ β ′ ‾ ⊢ e ′ : SLIO γ ′ γ ′ ⦇ τ ⦈ α ′ in SLIO ∗ .

Theorem 3.1 basically states that every well-typed FG expression e can be translated into some SLIO ∗ expression e ′ s.t.  Σ ; Ψ ; ⦇ Γ ⦈ β ′ ‾ ⊢ e ′ : SLIO γ ′ γ ′ ⦇ τ ⦈ α ′ for every α ′ , β ′ ‾ , and γ ′ with β ′ ‾ ⊔ γ ′ ⊑ pc ⊓ α ′ .

The constraint β ′ ‾ ⊔ γ ′ ⊑ pc ⊓ α ′ is basically a succinct representation of the following four constraints: β ′ ‾ ⊑ pc , γ ′ ⊑ pc , β ′ ‾ ⊑ α ′ and γ ′ ⊑ α ′ . From the app rule of FG we know that the argument to the function can have a write effect of at least pc . We encode this using the β ′ ‾ ⊑ pc constraint. Similarly we know that in FG, pc represents a lower bound on the write effect. This is encoded using the γ ′ ⊑ pc constraint. The other two constraints are best explained by appealing to their need in the type preservation proof. The constraint β ′ ‾ ⊑ α ′ is required to type check the variable case: A variable of type ⦇ τ ⦈ β i in the context can be type checked at ⦇ τ ⦈ α for some α s.t.  β i ⊑ α (we prove this as a lemma in the appendix). The last constraint γ ′ ⊑ α is required for the type-preservation of elim forms of type constructors.

We describe the full type translation function in Fig. 9. The type translation function is indexed with a label ℓ. The interesting case is the translation of the function type. The constraints in the translation of this type are similar to the ones we have in the theorem above. Additionally, we have two more constraints – ℓ ⊑ α and ℓ ⊑ ℓ e . Both the constraints are required for technical reasons that show up in the proof of type preservation of the introduction rule for function types.

OPEN IN VIEWER

Fig. 9.

Type translation from FG to SLIO ∗ .

OPEN IN VIEWER

Fig. 10.

Expression translation for FG to SLIO ∗ (selected rules).

Given this translation of types, we next define a type derivation-directed translation of expressions. This translation is formalized by the judgment Σ ; Ψ ; Γ ⊢ pc e s : τ ⇝ e t . The judgment means that translating the source expression e s , which has the typing derivation Σ ; Ψ ; Γ ⊢ pc e s , yields the target expression e t . This judgment is functional: For each type derivation Γ ⊢ pc e s : τ , it yields exactly one e t . It is also easily implemented by induction on typing derivations. The rules for the judgment are shown in Fig. 10. The thing to keep in mind while reading the rules is that e t should have the type SLIO γ ′ γ ′ ⦇ τ ⦈ α ′ for any α ′ , β ′ ‾ , γ ′ s.t.  β ′ ‾ ⊔ γ ′ ⊑ pc ⊓ α ′ (as stated in Theorem 3.1).

Selected rules for the expression translation from FG (source) to SLIO ∗ (target) terms are described in Fig. 10. We illustrate how the translation works using one rule, FC-app. In this rule, inductively we obtain a translation of e 1 , i.e., e c 1 with the type SLIO γ ′ γ ′ ⦇ ( τ 1 → ℓ e τ 2 ) ℓ ⦈ β ′ ⊔ γ ′ , where β ′ = ⋃ β i ∈ β ′ ‾ β i which is equal to SLIO γ ′ γ ′ ( Labeled ( ( β ′ ⊔ γ ′ ) ⊔ ℓ ) ( ∀ α , β , γ . ( ( ( β ′ ⊔ γ ′ ) ⊔ ℓ ) ⊔ β ⊔ γ ⊑ α ⊓ ℓ e ) ⇒ ⦇ τ 1 ⦈ β → SLIO γ γ ⦇ τ 2 ⦈ α ) ) . Similarly, the translation of e 2 , i.e., e c 2 has type SLIO γ ′ γ ′ ⦇ τ 1 ⦈ β ′ ∪ γ ′ . We wish to construct a term of type SLIO γ ′ γ ′ ⦇ τ 2 ⦈ β ′ ∪ γ ′ .

To do this, we bind e c 1 to the variable a, which has the type Labeled ( ( β ′ ⊔ γ ′ ) ⊔ ℓ ) ( ∀ α , β , γ . ( ( ( β ′ ⊔ γ ′ ) ⊔ ℓ ) ⊔ β ⊔ γ ⊑ α ⊓ ℓ e ) ⇒ ⦇ τ 1 ⦈ β → SLIO γ γ ⦇ τ 2 ⦈ α ) . Similarly, we bind e c 2 to the variable b, which has the type ⦇ τ 1 ⦈ β ′ ∪ γ ′ . Next, we unlabel a and bind the result to variable c, which has the type ( ∀ α , β , γ . ( ( ( β ′ ⊔ γ ′ ) ⊔ ℓ ) ⊔ β ⊔ γ ⊑ α ⊓ ℓ e ) ⇒ ⦇ τ 1 ⦈ β → SLIO γ γ ⦇ τ 2 ⦈ α ) . However, due to the unlabeling, the taint label on whatever computation we sequence after this bind must be at least β ′ ⊔ γ ′ ⊔ ℓ . Next, we eliminate the quantifiers α with β ′ ⊔ γ ′ ⊔ ℓ , β with β ′ ⊔ γ ′ and γ with β ′ ⊔ γ ′ ⊔ ℓ . This gives us an expression of the type ( ( ( β ′ ⊔ γ ′ ) ⊔ ℓ ) ⊔ ( β ′ ⊔ γ ′ ) ⊔ ( β ′ ⊔ γ ′ ⊔ ℓ ) ⊑ ( ( β ′ ⊔ γ ′ ) ⊔ ℓ ) ⊓ ℓ e ) ⇒ ⦇ τ 1 ⦈ ( β ′ ⊔ γ ′ ) → SLIO ( β ′ ⊔ γ ′ ⊔ ℓ ) ( β ′ ⊔ γ ′ ⊔ ℓ ) ⦇ τ 2 ⦈ ( ( β ′ ⊔ γ ′ ) ⊔ ℓ ) . The constraint to the leftof ⇒ is satisfiable as ℓ ⊔ pc ⊑ ℓ e is given to us, so we eliminate the constraint type resulting in an expression c [ ] [ ] [ ] ∙ . Finally we apply c [ ] [ ] [ ] ∙ to b to obtain the final result of type SLIO ( γ ′ ) ( β ′ ⊔ γ ′ ⊔ ℓ ) ⦇ τ 2 ⦈ ( ( β ′ ⊔ γ ′ ) ⊔ ℓ ) which is the same as SLIO ( γ ′ ) ( β ′ ⊔ γ ′ ⊔ ℓ ) ( Labeled ( ℓ i ⊔ β ′ ⊔ γ ′ ⊔ ℓ ) ⦇ A ⦈ ( ℓ i ⊔ β ′ ⊔ γ ′ ⊔ ℓ ) ) , where τ 2 = A ℓ i . However, the desired type has the second index as γ ′ and subtyping can’t be used to achieve that because of the co-variance of the monadic type on the second label. So, to achieve the desired type we use the coerce _ taint function (described below) which has the type SLIO γ α c τ ′ → SLIO γ γ τ ′ , when τ has the form τ ′ = Labeled α c ′ τ with Σ , Ψ ⊧ α c ⊑ α c ′ . Here, α c is ( β ′ ⊔ γ ′ ⊔ ℓ ) and α c ′ is ( ℓ i ⊔ β ′ ⊔ γ ′ ⊔ ℓ ) . Since we are given that τ 2 ↘ ℓ , it follows that ℓ ⊑ ℓ i , and, hence, the required constraint is satisfied. This yields a term of type SLIO ( γ ′ ) ( γ ′ ) Labeled ( ℓ i ⊔ β ′ ⊔ γ ′ ⊔ ℓ ) ⦇ A ⦈ ( ℓ i ⊔ β ′ ⊔ γ ′ ⊔ ℓ ) , which is the same as SLIO ( γ ′ ) ( γ ′ ) ⦇ τ 2 ⦈ β ′ ∪ γ ′ , as desired.

Importantly, the function coerce _ taint uses toLabeled internally. The function is defined in Fig. 10. This pattern of using coerce _ taint , which internally contains toLabeled , to restrict the taint is used to translate all elimination forms (application, projection, case, etc.). Overall, our translation uses toLabeled judiciously to prevent taint from exploding in the translated expressions.

3.1.1. Soundness of the translation

Our translation satisfies type preservation (Theorem 3.1). Type preservation is a necessary but insufficient condition for the goal we are after – showing equi-expressiveness of FG and SLIO ∗ . In fact, one can obtain a trivial type-preserving translation from FG to SLIO ∗ by simply translating every type to unit and every expression to ( ) , but this translation would be useless as far as showing the equivalence of the two systems is concerned. Therefore, in this section we show that the translation from FG to SLIO ∗ described above also preserves the semantics and the security of the source program. To that end, we build a cross-language model (based on Kripke step-indexed logical relations) for the translation from FG to SLIO ∗ .

The cross-language relation (described in Fig. 11) relates a term of FG with a term of SLIO ∗ . The value relation is defined by induction on the FG type and the step-index. It is a predicate over a tuple consisting of a world (denoted by s θ ), which is a map from locations in the source language (FG) to their types, a step-index (denoted by m), a source value (of the FG type for which the relation is being defined) and a target value (of the corresponding translated type, obtained via the translation). Additionally, the relation is indexed by β ˆ , a partial bijection describing the related locations between the source FG term and the target SLIO ∗ term. The value relation for the arrow type, for instance, relates a FG λ-term to the corresponding translated term, if the given conditions are satisfied.

The expression relation embodies semantics preservation by stating that a FG’s expression ( e s ) is related to SLIO ∗ ’s expression ( e t ) if an execution in FG (starting with some given heap) can be simulated by an execution in SLIO ∗ (starting with a related heap) s.t. the resulting heaps and values are related by the heap well-formedness relation and the value relation, respectively. (We delegate the details of the heap well-formedness relation to the appendix.)

OPEN IN VIEWER

Fig. 11.

Cross language value and expression relation for FG to SLIO ∗ .

The logical relation can be extended to substitutions in a standard way. This enables us to state and prove the fundamental theorem.

Theorem 3.2 (Fundamental theorem).

∀ Σ , Ψ , Γ , τ , e s , e t , pc , L , δ s , δ t , σ , s θ , n , β ˆ .

Σ ; Ψ ; Γ ⊢ pc e s : τ ⇝ e t ∧ L ⊧ Ψ σ ∧ ( s θ , n , δ s , δ t ) ∈ ⌊ Γ σ ⌋ V β ˆ ⟹ ( s θ , n , e s δ s , e t δ t ) ∈ ⌊ τ σ ⌋ E β ˆ .

This theorem immediately implies that the FG to SLIO ∗ translation preserves semantics of terms. Moreover, combining this theorem with Theorem 3.1, we can re-derive the noninterference theorem of FG from that of SLIO ∗ . This means that the translation preserves the intents of security labels or, in other words, it is security-preserving.

3.2. Translating SLIO ∗ to FG

OPEN IN VIEWER

Fig. 12.

Expression translation SLIO ∗ to FG (selected rules only).

This section describes the translation in the other direction – from SLIO ∗ to FG. The overall structure of this translation is similar to that of the earlier FG to SLIO ∗ translation, given by a translation of types and a type-derivation-directed translation of terms. However, this translation is much simpler in the details, in particular, the type translation now does not require indexing with a label. Note that the superscript or subscript s (source) now marks elements of SLIO ∗ and t (target) marks elements of FG.

The key idea of the translation is to map a source ( SLIO ∗ ) expression e s satisfying ⊢ e s : τ to a target (FG) expression e t satisfying ⊢ ⊤ e t : ⟦ τ ⟧ . The type translation ⟦ τ ⟧ is defined below. The pc for the translated expression is ⊤ because, in SLIO ∗ , all effects are confined to a monad, so at the top-level, there are no effects. In particular, there are no write effects, so we can pick any pc ; we pick the most informative pc , ⊤.

The type translation, ⟦ τ ⟧ , is defined by induction on τ.

⟦ b ⟧ ≜ b ⊥ ⟦ τ 1 → τ 2 ⟧ ≜ ( ⟦ τ 1 ⟧ → ⊤ ⟦ τ 2 ⟧ ) ⊥ ⟦ τ 1 × τ 2 ⟧ ≜ ( ⟦ τ 1 ⟧ × ⟦ τ 2 ⟧ ) ⊥ ⟦ τ 1 + τ 2 ⟧ ≜ ( ⟦ τ 1 ⟧ + ⟦ τ 2 ⟧ ) ⊥ ⟦ ref ℓ τ ⟧ ≜ ( ref ( ⟦ τ ⟧ + unit ) ℓ ) ⊥ ⟦ SLIO ℓ 1 ℓ 2 τ ⟧ ≜ ( unit → ℓ 1 ( ⟦ τ ⟧ + unit ) ℓ 2 ) ⊥ ⟦ Labeled ℓ τ ⟧ ≜ ( ⟦ τ ⟧ + unit ) ℓ

The most interesting case of the translation is that for SLIO ℓ 1 ℓ 2 τ . Since a SLIO ∗ value of this type is a suspended computation, we map this type to a thunk – a suspended computation implemented as a function whose argument has type unit . The pc-label on the function matches the pc-label ℓ 1 of the source type. The taint label ℓ 2 is placed on the output type ⟦ τ ⟧ using a coding trick: ( ⟦ τ ⟧ + unit ) ℓ 2 . The expression translation of monadic expressions only ever produces values labeled inl , so the right type of the sum, unit , is never reached during the execution of a translated expression. The same coding trick is used to translate labeled and ref types. We could also have used a different coding in place of ( ⟦ τ ⟧ + unit ) ℓ 2 . For example, ( ⟦ τ ⟧ × unit ) ℓ 2 works equally well.

The expression translation is directed by source typing derivations and is defined by the judgment Σ ; Ψ ; Γ ⊢ e s : τ ⇝ e t , some of whose rules are shown in Fig. 12. The translation is fairly straightforward (given the type translation). The only noteworthy aspect is the use of the injection inl wherever an expression of the type form ( ⟦ τ ⟧ + unit ) ℓ needs to be constructed.

Properties. The translation preserves typing by construction, as formalized in the following theorem. The context translation ⟦ Γ ⟧ is defined pointwise on all types in Γ.

Again, a corollary of this theorem is that well-typed source programs translate to non-interfering target programs.

We further prove that the translation preserves the semantics of programs. Our approach is the same as that for the FG to SLIO ∗ translation – we set up a cross-language logical relation, this time indexed by SLIO ∗ types, and show the fundamental theorem. From this, we derive that the translation preserves the meanings of programs. Additionally, we derive the noninterference theorem for SLIO ∗ using the binary fundamental theorem of FG, thus gaining confidence that our translation maps security labels properly. Since this development mirrors that for our earlier translation, we defer the details to the appendix.

4. CG: A new coarse-grained type system

We explained in Section 2.2 that SLIO ∗ ’s monadic type SLIO ℓ i ℓ o τ is really a Hoare monad. The two labels ℓ i and ℓ o on the monadic type serve as input and output labels. For any well-typed program, they always satisfy the invariant that ℓ i ⊑ ℓ o . However, as it turns out, this constraint is really not necessary for the soundness of SLIO ∗ ’s type system. Accordingly, in this section, we develop a similar type system CG, but which does not force the ℓ i ⊑ ℓ o restriction. CG interprets ℓ i like a conventional pc and ℓ o as a label on the output of the result (the two do not have to be related, exactly as in FG). It further turns out that removing the restriction ℓ i ⊑ ℓ o really simplifies the translation from FG, by allowing more flexibility in the labels in the target. As we show later, a translation from FG to CG can be done without requiring any label quantification and constraints unlike the translation from FG to SLIO ∗ in Section 3.1. This suggests that a large part of the complexity in the translation of Section 3.1 in fact comes from the “Hoare” interpretation of the two labels on SLIO ∗ ’s monad.

CG is defined for the same language as SLIO ∗ , but it has a different type system. Specifically, CG differs from SLIO ∗ only in the rules for the monadic types (the impure part of the type system). These new rules are described in Fig. 13. CG’s monadic type is written C ℓ i ℓ o τ . As mentioned above, in CG, the first label ℓ i on the monadic type is like FG’s pc label: It is a lower bound on the write effects of the computation ascribed by the monadic type. The second label ℓ o can be thought of as the security label of the result and it is an upper bound on the read effects of the computation. No specific ordering relation is required or forced between the two labels.

OPEN IN VIEWER

Fig. 13.

CG’s type system (selected rules).

CG’s typing judgment is written Σ ; Ψ ; Γ ⊢ e : τ . Like SLIO ∗ , there is no need for a pc on the judgment since effects are confined to the monad. The construct ret ( e ) is the monadic return that immediately returns e, without any heap access. Consequently, it can be given the type C ⊤ ⊥ τ (rule CG-ret). The pc-label is ⊤ since the computation has no write effect, while the taint label is ⊥ since the computation has not analyzed any value.

The monadic construct bind ( e 1 , x . e 2 ) sequences the computation e 2 after e 1 , binding the return value of e 1 to x in e 2 . The typing rule for this construct, CG-bind, is important and interesting. The rule says that bind ( e 1 , x . e 2 ) can be given the type C ℓ ℓ 4 τ ′ if ( e 1 : C ℓ 1 ℓ 2 τ ) , ( e 2 : C ℓ 3 ℓ 4 τ ′ ) and four conditions hold. The conditions ℓ ⊑ ℓ 1 and ℓ ⊑ ℓ 3 check that the pc-label of bind ( e 1 , x . e 2 ) , which is ℓ, is below the pc-label of e 1 and e 2 , which are ℓ 1 and ℓ 3 , respectively. This ensures that the write effects of bind ( e 1 , x . e 2 ) are indeed above its pc-label, ℓ. The conditions ℓ 2 ⊑ ℓ 3 and ℓ 2 ⊑ ℓ 4 prevent leaking the output of e 1 via the write effects and the output of e 2 , respectively. Observe how these conditions together track labels at the level of entire computations, i.e., coarsely.

Next, we describe rules pertaining to the type Labeled ℓ τ . This type is introduced using the expression constructor Lb , as in rule CG-label. Dually, if e : Labeled ℓ τ , then the construct unlabel ( e ) eliminates this label. This construct has the monadic type C ⊤ ℓ τ . The taint label ℓ indicates that the computation has (internally) analyzed something labeled ℓ. The pc-label is ⊤ since nothing has been written.

Rule CG-deref says that dereferencing (reading) a location of type ref ℓ ′ τ produces a computation of type C ⊤ ⊥ ( Labeled ℓ ′ τ ) . The type is monadic because dereferencing accesses the heap. The value the computation returns is explicitly labeled at ℓ ′ . The pc-label is ⊤ since the computation does not write, while the taint label is ⊥ since the computation does not analyze the value it reads from the reference. (The taint label will change to ℓ ′ if the read value is subsequently unlabeled.) Dually, the rule CG-assign allows assigning a value labeled ℓ to a reference labeled ℓ. The result is a computation of type C ℓ ⊥ unit . The pc-label ℓ indicates a write effect at level ℓ.

The last typing rule we highlight pertains to the construct toLabeled ( e ) . This construct transforms e of monadic type C ℓ ℓ ′ τ to the type C ℓ ⊥ ( Labeled ℓ ′ τ ) . This is perfectly safe since the only way to observe the output of a monad is by binding its result and that result is explicitly labeled in the final type. The purpose of using this construct is to reduce the taint label of a computation to ⊥. This allows a subsequent computation, which will not analyze the output of the current computation, to avoid raising its own taint label to ℓ ′ . Hence, this construct limits the scope of the taint label to a single computation, and prevents over-tainting subsequent computations. We make extensive use of this construct in our translation from FG to CG.

We prove soundness for CG by showing that every well-typed expression satisfies noninterference (Theorem 4.1). The proof is done by developing logical relations of the kind we saw earlier for FG and SLIO ∗ . The logical relations for CG are exactly the same as that for SLIO ∗ , so we don’t describe them again.

5. Translations between FG and CG

In this section, we describe our translations from FG to CG and vice-versa. The purpose of describing these translations is two fold: 1) To show that these two type systems are equally expressive and, more importantly, to show that the translation from a fine-grained to a coarse-grained IFC type system does not have to be as complex as we saw in Section 3.1. We show the latter by describing a much simpler translation from FG to CG. 2) To show that CG and SLIO ∗ are also equi-expressive despite the differences in their proof theories. The translation from CG to FG is very similar to the translation from SLIO ∗ to FG. There are only minor differences in the proofs due to differences in the type system of the source. We omit this translation here as it adds no insight to what we already described in Section 3.2. Instead, we only describe the translation from FG to CG, which is substantially different from (and considerably simpler than) the translation from FG to SLIO ∗ .

5.1. Translating FG to CG

Our goal in translating FG to CG is to show how a fine-grained IFC type system can be simulated in a coarse-grained one in a very simple manner. This translation is directed by the type derivations in FG and preserves typing, semantics and security annotations. As before, we use the subscript or superscript s to indicate source (FG) elements, and t to indicate target (CG) elements.

The key idea of our translation is to map a source expression e s satisfying ⊢ pc e s : τ to a monadic target expression e t satisfying ⊢ e t : C pc ⊥ ⦇ τ ⦈ . The pc used to type the source expression is mapped as-is to the pc-label of the monadic computation. The type of the source expression, τ, is translated by the function ⦇ · ⦈ that is described below. However – and this is the crucial bit – the taint label on the translated monadic computation is ⊥. To get this ⊥ taint we use the toLabeled construct judiciously. Not setting the taint to ⊥ can cause a taint explosion in translated expressions, which would make it impossible to simulate the fine-grained dependence tracking of FG.

The function ⦇ · ⦈ defines how the types of source values are translated. This function is defined by induction on labeled and unlabeled source types.

⦇ b ⦈ ≜ b ⦇ unit ⦈ ≜ unit ⦇ τ 1 → ℓ e τ 2 ⦈ ≜ ⦇ τ 1 ⦈ → C ℓ e ⊥ ⦇ τ 2 ⦈ ⦇ ∀ α . ( ℓ e , τ ) ⦈ ≜ ∀ α . C ℓ e ⊥ ⦇ τ ⦈ ⦇ c ⇒ ℓ e τ ) ⦈ ≜ c ⇒ C ℓ e ⊥ ⦇ τ ⦈ ⦇ τ 1 × τ 2 ⦈ ≜ ⦇ τ 1 ⦈ × ⦇ τ 2 ⦈ ⦇ τ 1 + τ 2 ⦈ ≜ ⦇ τ 1 ⦈ + ⦇ τ 2 ⦈ ⦇ ref τ ⦈ ≜ ref ℓ ⦇ A ⦈ where τ = A ℓ ⦇ A ℓ ⦈ ≜ Labeled ℓ ⦇ A ⦈

The translation should be self-explanatory. The only nontrivial case is the translation of the function type τ 1 → ℓ e τ 2 . A source function of this type is mapped to a target function that takes an argument of type ⦇ τ 1 ⦈ and returns a monadic computation (the translation of the body of the source function) that has pc-label ℓ e and eventually returns a value of type ⦇ τ 2 ⦈ . It is instructive to contrast this type translation to the type translation from FG to SLIO ∗ . Now the translation of the function type does not need label quantification and constraints.

The expression translation uses ideas similar to that of the translation from FG to SLIO ∗ , but the translated terms are simpler. We don’t explain the term translation again, and only list some selected rules in Fig. 14.

Properties. Our translation preserves typing by construction. This is formalized in the following theorem. The context translation ⦇ Γ ⦈ is defined pointwise on all types in Γ. Notice the simplicity of this theorem in contrast with the type preservation for the FG to SLIO ∗ translation (Theorem 3.1).

OPEN IN VIEWER

Fig. 14.

Expression translation FG to CG (selected rules only).

Theorem 5.1 (Typing preservation).

If Γ ⊢ pc e s : τ in FG, then there is a unique e t such that Γ ⊢ pc e s : τ ⇝ e t and that e t satisfies ⦇ Γ ⦈ ⊢ e t : C pc ⊥ ⦇ τ ⦈ in CG.

An immediate corollary of this theorem is that well-typed source programs translate to non-interfering target programs (since target typing implies noninterference in the target).

Next, just like our previous translations we also show that this translation is semantics preserving by developing a cross-language relation between FG and CG terms. The cross-language relation is similar to (but not the same as) the cross-language relation we saw for the FG to SLIO ∗ translation. We defer its description to the appendix. As before, we also show that we are able to re-derive FG’s noninterference theorem from CG’s noninterference theorem and properties of the translation.

6. Discussion

Practical implications. Our results establish that a coarse-grained IFC type system that labels at the granularity of entire computations can be as expressive as a fine-grained IFC type system that labels every individual value, if the coarse-grained type system has a construct like toLabeled to limit the scope of taints. It is also usually the case that a coarse-grained type system burdens a programmer less with annotations as compared to a fine-grained type system. This leads to the conclusion that, in general, there is merit to preferring coarse-grained IFC type systems with taint-scope limiting constructs over fine-grained IFC type systems. In a coarse-grained type system, the programmer can benefit from the reduced annotation burden and simulate the fine-grained type system when the fine-grained labeling is absolutely necessary for verification. Since our embedding of the fine-grained type system in the coarse-grained type system is compositional, it can be easily implemented in the coarse-grained type system as a library of macros, one for each construct of the language of the fine-grained type system.

Full abstraction. Since our translations preserve typed-ness, they map well-typed source programs to non-interfering target programs. However, an open question is whether they preserve contextual equivalence, i.e., whether they are fully abstract. Establishing full abstraction will allow translated source expressions to be freely co-linked with target expressions. We haven’t attempted a proof of full abstraction yet, but it looks like an interesting next step. We note that since our dynamic semantics (big-step evaluation) are not cognizant of IFC (which is enforced completely statically), it may be sufficient to generalize our translations to simply-typed variants of FG and CG, and prove those fully abstract.

Other IFC properties. Our current setup is geared towards proving termination-insensitive noninterference, where the adversary cannot observe nontermination. We believe that the approach itself and the equivalence result should generalize to termination-sensitive noninterference, but will require nontrivial changes to our development. For example, we will have to change our binary logical relations to imply co-termination of related expressions and, additionally, modify the type systems to track nontermination as a separate effect.

Another relevant question in whether our equivalence result can be extended to type systems that support declassification and, more foundationally, whether our logical relations can handle declassification. This is a nuanced question, since it is unclear hitherto how declassification can be given a compositional semantic model. We are working on this problem currently.

7. Related work

We focus on related work directly connected to our contributions – logical relations for IFC type systems and language translations that care about IFC.

Logical relations for IFC type systems. Logical relations for IFC type systems have been studied before to a limited extent. Sabelfeld and Sands develop a general theory of models of information flow types based on partial-equivalence relations (PERs), the mathematical foundation of logical relations [25]. However, they do not use these models for proving any specific type system or translation sound. The pure fragment of the SLam calculus was proven sound (in the sense of noninterference) using a logical relations argument [15, Appendix A]. However, to the best of our knowledge, the relation and the proof were not extended to mutable state. The proof of noninterference for FlowCaml [22], which is very close to SLam, considers higher-order state (and exceptions), but the proof is syntactic, not based on logical relations. The dependency core calculus (DCC) [1] also has a logical relations model but, again, the calculus is pure. The DCC paper also includes a state-passing embedding from the IFC type system of Volpano, Irvine and Smith [27], but the state is first-order. Mantel et al. use a security criterion based on an indistinguishability relation that is a PER to prove the soundness of a flow-sensitive type system for a concurrent language [18]. Their proof is also semantic, but the language is first-order. In contrast to these prior pieces of work, our logical relations handle higher-order state, and this complicates the models substantially; we believe we are the first to do so in the context of IFC.

Our models are based on the now-standard step-indexed Kripke logical relations [2], which have been used extensively for showing the soundness of program verification logics. Our model for FG is directly inspired by Cicek et al.’s model for a pure calculus of incremental programs [11]. That calculus does not include state, but the model is structurally very similar to our model of FG in that it also uses a unary and a binary relation that interact at labeled types. Extending that model with state was a significant amount of work, since we had to introduce Kripke worlds. Our models for SLIO ∗ and CG have no direct predecessor; we developed them using ideas from our model of FG. (DCC is also coarse-grained and uses a labeled monad to track dependencies, but its model is quite different from ours in the treatment of the monadic type.)

Language translations that care about IFC. Language translations that preserve information flow properties appear in the DCC paper. The translations start from SLam’s pure fragment and the type system of Volpano, Irvine and Smith and go into DCC. The paper also shows how to recover the noninterference theorem of the source of a translation from properties of the target, a theorem we also prove for our translations. Barthe et al. [7] describe a compilation from a high-level imperative language to a low-level assembly-like language. They show that their compilation is type and semantics preserving. They also derive noninterference for the source from the noninterference of the target. Fournet and Rezk [13] describe a compilation from an IFC-typed language to a low-level language where confidentiality and integrity are enforced using cryptography. They prove that well-typed source programs compile to non-interfering target programs, where the target noninterference is defined in a computational sense. Algehed and Russo [4] define an embedding of DCC into Haskell. They also consider an extension of DCC with state but, to the best of our knowledge, they do not prove any formal properties of the translation.

8. Conclusion

This paper has examined the question of whether information flow type systems that label at fine granularity and those that label at coarse granularity are equally expressive. We answer this question in the affirmative, assuming that the coarse-grained type system has a construct to limit the scope of the taint label. We show this via cross-translations between a fine-grained type system, FG, and a coarse-grained type systems SLIO ∗ . The translation from FG to SLIO ∗ is quite complex due to the Hoare state monad implicitly used in SLIO ∗ . We come up with a new coarse-grained type system CG which is not only equi-expressive with SLIO ∗ , but also affords a much simpler translation from FG. A more foundational contribution of our work is a better understanding of semantic models of information flow types. To this end, we presented logical relations models of types for the fine-grained and both of the coarse-grained type systems presented in the paper.