A Dependently Typed Library for Static Information-Flow Control in Idris

Modern software applications are increasingly built using libraries and code from multiple third parties. At the same time, protecting confidentiality of information manipulated by such applications is a growing, yet long-standing problem. Third-party libraries could in general have been written by anyone and they are usually run with the same privileges as the main application. While powerful, such privileges open up for abuse.

Traditionally, access control [7] and encryption have been the main means for preventing data dissemination and leakage, however, such mechanisms fall short when third-party code needs access to sensitive information to provide its functionality. The key observation is that these mechanisms only place restrictions on the access to information but not its propagation. Once information is accessed, the accessor is free to improperly transmit or leak the information in some form, either by intention or error.

Language-based Information-Flow Control [36] is a promising technique for enforcing information security. Traditional enforcement techniques analyze how information at different security levels flows within a program ensuring that information flows only to appropriate places, suppressing illegal flows. To achieve this, most information-flow control tools require the design of new languages, compilers, or interpreters (e.g. [12, 17, 22, 23, 26, 29, 39]). Despite a large, growing body of work on language-based information-flow security, there has been little adoption of the proposed techniques. For information-flow policies to be enforced in such systems, the whole system has to be written in new languages – an inherently expensive and time-consuming process for large software systems. Moreover, in practice, it might very well be that only small parts of an application are governed by information-flow policies.

Pure functional programming languages, like Haskell, have something to offer with respect to information security as they strictly separate side-effect free and side-effectful code. This makes it possible to enforce lightweight information-flow control through libraries [11, 20, 34, 35, 42] by constructing an embedded domain-specific security sub-language. Such libraries enforce a secure-by-construction programming model as any program written against the library interface is not capable of leaking secrets. This construction forces the programmer to write security-critical code in the sub-language but otherwise allows them to freely interact and integrate with non-security critical code written in the full language. In particular, static enforcement libraries like MAC [34] are appealing as no run-time checks are needed and code that exhibits illegal flows is rejected by the type checker at compile-time. Naturally, the expressiveness of Haskell’s type system sets the limitation on which programs can be deemed secure and which information flow policies can be guaranteed.

Dependent type theories [24, 31] are implemented in many programming languages such as Coq [13], Agda [32], Idris [8], and F\(^{*}\) [44]. Programming languages that implement such theories allow types to dependent on values. This enables programmers to give programs a very precise type and increased confidence in its correctness.

In this paper, we show that dependent types provide a direct and natural way of expressing precise data-dependent security policies. Dependent types can be used to represent rich security policies in environments like databases and data-centric web applications where, for example, new classes of users and new kinds of data are encountered at run-time and the security level depends on the manipulated data itself [23]. Such dependencies are not expressible in less expressive systems like MAC. Among other things, with dependent types, we can construct functions where the security level of the output depends on an argument:

Given a user name , retrieves the corresponding password and classifies it at the security level of . As such, we can express much more precise security policies that can depend on the manipulated data.

Idris is a general-purpose functional programming language with full-spectrum dependent types, that is, there is no restrictions on which values may appear in types. The language is strongly influenced by Haskell and has, among others, inherited its strict encapsulation of side-effects. Idris essentially asks the question: “What if Haskell had full dependent types?” [9]. This work, essentially, asks:

“What if MAC had full dependent types?”

We address this question using Idris because of its positioning as a general-purpose language rather than a proof assistant. All ideas should be portable to equally expressive systems with full dependent types and strict monadic encapsulation of side-effects.

In summary, the contributions of this paper are as follows.

Outline. The rest of the paper proceeds through a presentation of the DepSec library (Sect. 2); a conference manager case study (Sect. 3) and the introduction of policy-parameterized functions (Sect. 4) both showcasing the expressiveness of DepSec; means to specify statically-ensured declassification policies (Sect. 5); soundness of the core library (Sect. 6); and related work (Sect. 7).

All code snippets presented in the following are extracts from the source code. All source code is implemented in Idris 1.3.1. and available at

https://​github.​com/​simongregersen/​DepSec.

In information-flow control, labels are used to model the sensitivity of data. Such labels usually form a security lattice [14] where the induced partial ordering \(\sqsubseteq \) specifies allowed flows of information and hence the security policy. For example, \(\ell _{1} \sqsubseteq \ell _{2}\) specifies that data with label \(\ell _{1}\) is allowed to flow to entities with label \(\ell _{2}\). In DepSec, labels are represented by values that form a verified join semilattice implemented as Idris interfaces¹. That is, we require proofs of the lattice properties when defining an instance of .

Dependent function types (often referred to as \({\varPi }\) types) in Idris can express such requirements. If is a type and is a type indexed by a value of type then is the type of functions that map arguments of type to values of type .

A lattice induces a partial ordering, which gives a direct way to express flow constraints. We introduce a verified partial ordering together with an implementation of this for . That is, to define an instance of the interface we require a concrete instance of an associated data type as well as proofs of necessary algebraic properties of .

This definition allows for generic functions to impose as few restrictions as possible on the user while being able to exploit the algebraic structure in proofs, as will become evident in Sects. 3 and 4. For the sake of the following case studies, we also have a definition of a requiring a least element of an instance of and a proof of the element being the unit.

The Core API. Figure 1 presents the type signature of DepSec’s core API. Notice that names beginning with a lower case letter that appear as a parameter or index in a type declaration will be automatically bound as an implicit argument in Idris, and the annotation on implicit arguments means that Idris will attempt to fill in the implicit argument by searching the calling context for an appropriate value.

Abstract data type denotes a value of type a with sensitivity level \(\ell \). We say that is indexed by and parameterized by . Abstract data type denotes a secure computation that handles values with sensitivity level and results in a value of type a. It is internally represented as a wrapper around the regular monad that, similar to the one in Haskell, can be thought of as a state monad where the state is the entire world. Notice that both data constructors and are not available to untrusted code as this would allow pattern matching and uncontrolled unwrapping of protected entities. As a consequence, we introduce functions and for labeling and unlabeling values. Like Rajani and Garg [33], but unlike MAC, the type signature of imposes no lattice constraints on the computation context. This does not leak information as, if \(l \sqsubseteq l'\) and a computation c has type for any type V, then there is no way for the labeled return value of c to escape the computation context with label \(l'\).

As in MAC, the API contains a function that safely integrates sensitive computations into less sensitive ones. This avoids the need for nested computations and label creep, that is, the raising of the current label to a point where the computation can no longer perform useful tasks [34, 47]. Finally, we also have functions and that are only available to trusted code for unwrapping of the monad and lifting of the monad into the monad.

Labeled Resources. Data type is used to denote a labeled Idris value with type a. This is an example of a labeled resource [34]. By itself, the core library does not allow untrusted code to perform any side effects but we can safely incorporate, for example, file access and mutable references as other labeled resources. Figure 2 presents type signatures for files indexed by security levels used for secure file handling while mutable references are available in the accompanying source code. Abstract data type  \(\ell \) denotes a secure file with sensitivity level \(\ell \). As for , the data constructor is not available to untrusted code.

The function takes as input a secure file and returns a computation with sensitivity level that returns a labeled value with sensitivity level Notice that the flow constraint is required to enforce the no read-up policy [7]. That is, the result of the computation returned by only involves data with sensitivity at most . The function takes as input a secure file and a labeled value of sensitivity level , and it returns a computation with sensitivity level that returns a labeled value with sensitivity level . Notice that both the and flow constraints are required, essentially enforcing the no write-down policy [7], that is, the file never receives data more sensitive than its sensitivity level.

Finally, notice that the standard library functions for reading and writing files in Idris used to implement the functions in Fig. 2 do not raise exceptions. Rather, both functions return an instance of the sum type . We stay consistent with Idris’ choice for this instead of adding exception handling as done in MAC.

This case study showcases the expressiveness of DepSec by reimplementing a conference manager system with a fine-grained data-dependent security policy introduced by Lourenço and Caires [23]. Lourenço and Caires base their development on a minimal \(\lambda \)-calculus with references and collections and they show how secure operations on relevant scenarios can be modelled and analysed using dependent information flow types. Our reimplementation demonstrates how DepSec matches the expressiveness of such a special-purpose built dependent type system on a key example.

In this scenario, a user is either a regular user, an author user, or a program committee (PC) member. The conference manager contains information about the users, their submissions, and submission reviews. This data is stored in lists of references to records, and the goal is to statically ensure, by typing, the confidentiality of the data stored in the conference manager system. As such, the security policy is:

To achieve this security policy, Lourenço and Caires make use of indexed security labels [22]. The security level \( U \) is partitioned into a number of security compartments such that \( U ( uid ) \) represents the compartment of the registered user with id \( uid \). Similarly, the security level \( A \) is indexed such that \( A ( uid , sid ) \) stands for the compartment of data belonging to author \( uid \) and their submission \( sid \), and \( PC \) is indexed such that \( PC ( uid , sid ) \) stands for data belonging to the PC member with user id \( uid \) assigned to review the submission with id \( sid \). Furthermore, levels \(\top \) and \(\bot \) are introduced such that, for example, \( U ( \bot ) \sqsubseteq U ( uid ) \sqsubseteq U ( \top ) \). Now, the security lattice is defined using two equations: Lourenço and Caires are able to type a list of submissions with a dependent sum type that assigns the content of the paper the security level \( A ( uid , sid ) \), where \( uid \) and \( sid \) are fields of the record. For example, if a concrete submission with identifier 2 was made by the user with identifier 1, the content of the paper gets classified at security level \( A ( 1 , 2 ) \). In consequence, \( A ( 1 , 2 ) \sqsubseteq PC ( n , 2 ) \) for any \( uid \) n and the content of the paper is only observable by its assigned reviewers. Similar types are given for the list of user information and the list of submission reviews, enforcing the security policy described in the above.

To express this policy in DepSec, we introduce abstract data types and (cf. Fig. 3) followed by an implementation of the interface that satisfies Eqs. (1) and (2).

Using the above, the required dependent sum types can easily be encoded with DepSec in Idris as presented in Fig. 4. With these typings in place, implementing the examples from Lourenço and Caires [23] is straightforward. For example, the function takes as input a list of submissions and a user identifier from which it returns a computation that returns a list of submissions authored by the user with identifier . Notice that denotes the automatically generated record projection function that retrieves the field of the record, and that is notation for a dependent pair (often referred to as a \({\varSigma }\) type) where and are types and may depend on  .

The operation is used by the PC members to add comments to the submissions. The function takes as input a list of reviews, a user identifier of a PC member, a submission identifier, and a comment with label . It returns a computation that updates the field in the review of the paper with identifier .

Notice that to implement this specific type signature, up-classification is necessary to assign the comment with type to a field with type . This can be achieved soundly with the primitive introduced by Vassena et al. [47] as . We include this primitive in the accompanying source code together with several other examples. The entire case study amounts to about 300 lines of code where half of the lines implement and verify the lattice.

A consequence of using a dependently typed language, and the design of DepSec, is that functions can be defined such that they abstract over the security policy while retaining precise security levels. This makes it possible to reuse code across different applications and write other libraries on top of DepSec. We can exploit the existence of a lattice , the induced poset, and their verified algebraic properties to write such functions.

Figure 5 presents the function that is parameterized by a bounded join semilattice. It takes two secure files with labels and as input and returns a computation that concatenates the contents of the two files labeled with the join of and . To implement this, we make use of the and primitives from Figs. 1 and 2, respectively. This computation unlabels the contents of the files and returns the concatenation of the contents if no file error occurred. Notice that is the Idris function for monadic return, corresponding to the function in Haskell. Finally, this computation is plugged into the surrounding computation. Notice how the usage of and introduces several proof obligations, namely \(\bot \sqsubseteq \)  , , and , . When working on a concrete lattice these obligations are usually fulfilled by Idris’ automatic proof search but, currently, such proofs need to be given manually in the general case. All obligations follow immediately from the algebraic properties of the bounded semilattice and are given in three auxiliary lemmas , , and available in the accompanying source code (amounting to 10 lines of code).

Writing functions operating on a fixed number of resources is limiting. However, the function in Fig. 5 can easily be generalized to a function working on an arbitrary data structure containing files with different labels from an arbitrary lattice. Similar to the approach taken by Buiras et al. [11] that hide the label of a labeled value using a data type definition, we hide the label of a secure file with a dependent pair

that abstracts away the concrete sensitivity level of the file. Moreover, we introduce a specialized join function

that folds the function over a list of file sensitivity labels. Now, it is possible to implement a function that takes as input a list of files, reads the files, and returns a computation that concatenates all their contents (if no file error occurred) where the return value is labeled with the join of all their sensitivity labels.

When implementing this, one has to satisfy non-trivial proof obligations as, for example, that \(l \sqsubseteq \)  for all secure files where the label of f is l. While provable (in 40 lines of code in our development), if equality is decidable for elements of the concrete lattice we can postpone such proof obligations to a point in time where it can be solved by reflexivity of equality. By defining a decidable lattice order

we can get such a proof “for free” by inserting a dynamic check of whether the flow is allowed. With this, a function with the exact same functionality as the original function can be implemented with minimum effort. In the below, is the proof that the label of may flow to .

The downside of this is the introduction of a negative case, the -case, that needs handling even though it will never occur if is implemented correctly.

In combination with , can be used to implement several other interesting examples. For instance, a function that reads all files with a sensitivity label below a certain label to a string labeled with that label. The accompanying source code showcases multiple such examples that exploit decidable equality.

In DepSec, trusted code may declassify secret information without adhering to any security policy as trusted code has access to both the and data constructors. However, only giving trusted code the power of declassification is limiting as we want to allow the use of third-party code as much as possible. The main challenge we address is how to grant untrusted code the right amount of power such that declassification is only possible in the intended way.

Sabelfeld and Sands [38] identify four dimensions of declassification: what, who, where, and when. In this section, we present novel and powerful means for static declassification with respect to three of the four dimensions and illustrate these with several examples. To statically enforce different declassification policies we take the approach of Sabelfeld and Myers [37] and use escape hatches, a special kind of functions. In particular, we introduce the notion of a hatch builder; a function that creates an escape hatch for a particular resource and which can only be used when a certain condition is met. Such an escape hatch can therefore be used freely by untrusted code.

Recent works [46, 47] present a mechanically-verified model of MAC and show progress-insensitive noninterference (PINI) for a sequential calculus. We use this work as a starting point and discuss necessary modification in the following. Notice that this work does not consider any declassification mechanisms and neither do we; we leave this as future work.

The proof relies on the two-steps erasure technique, an extension of the term erasure [21] technique that ensures that the same public output is produced if secrets are erased before or after program execution. The technique relies on a type-driven erasure function \(\varepsilon _{\ell _{A}}\) on terms and configurations where \(\ell _{A}\) denotes the attacker security level. A configuration consists of an \(\ell \)-indexed compartmentalized store \({\varSigma }\) and a term t. A configuration \(\langle {\varSigma }, t \rangle \) is erased by erasing t and by erasing \({\varSigma }\) pointwise, i.e. \(\varepsilon _{\ell _{A}}({\varSigma }) = \lambda \ell . \varepsilon _{\ell _{A}}({\varSigma }(\ell ))\). On terms, the function essentially rewrites data and computations above \(\ell _{A}\) to a special \(\bullet \) value. The full definition of the erasure function is available in the full version of this paper [15]. From this definition, the definition of low-equivalence of configurations follows.

The main theorem follows by repeated applications of Proposition 1.

Both the statement and the proof of noninterference for DepSec are mostly similar to the ones for MAC and available in the full version of this paper [15]. Nevertheless, one has to be aware of a few subtleties.

First, one has to realize that even though dependent types in a language like Idris may depend on data, the data itself is not a part of a value of a dependent type. Recall the type of vectors of length with components of type and consider the following program.

This example may lead one to believe that it is possible to extract data from a dependent type. This is not the case. Both and are implicit arguments to the function that the compiler is able to infer. The actual type is

As a high-level dependently typed functional programming language, Idris is elaborated to a low-level core language based on dependent type theory [9]. In the elaboration process, such implicit arguments are made explicit when functions are defined and inferred when functions are invoked. This means that in the underlying core language, only explicit arguments are given. Our modeling given in the full version of this paper reflects this fact soundly.

Second, to model the extended expressiveness of DepSec, we extend both the semantics and the type system with compile-time pure-term reduction and higher-order dependent types. These definitions are standard (defined for Idris by Brady [9]) and available in the full version of our paper. Moreover, as types now become first-class terms, the definition of \(\varepsilon _{\ell _{A}}\) has to be extended to cover the new kinds of terms. As before, primitive types are unaffected by the erasure function, but dependent and indexed types, such as the type , have to be erased homomorphically, e.g., . The intuition of why this is sensible comes from the observation that indexed dependent types considered as terms may contain values that will have to be erased. This is purely a technicality of the proof. If defined otherwise, the erasure function would not commute with capture-avoiding substitution on terms, \(\varepsilon _{\ell _{A}}(t[v/x]) = \varepsilon _{\ell _{A}}(t)[\varepsilon _{\ell _{A}}(v)/x\)], which is vital for the remaining proof.

Security Libraries. The pioneering and formative work by Li and Zdancewic [20] shows how arrows [18], a generalization of monads, can provide information-flow control without runtime checks as a library in Haskell. Tsai et al. [45] further extend this work to handle side-effects, concurrency, and heterogeneous labels. Russo et al. [35] eliminate the need for arrows and implement the security library SecLib in Haskell based solely on monads. Rather than labeled values, this work introduces a monad which statically label side-effect free values. Furthermore, it presents combinators to dynamically specify and enforce declassification policies that bear a resemblance to the policies that DepSec are able to enforce statically.

The security library LIO [41, 42] dynamically enforces information-flow control in both sequential and concurrent settings. Stefan et al. [40] extend the security guarantees of this work to also cover exceptions. Similar to this work, Stefan et al. [42] present a simple API for implementing secure conference reviewing systems in LIO with support for data-dependent security policies.

Inspired by the design of SecLib and LIO, Russo [34] introduces the security library MAC. The library statically enforces information-flow control in the presence of advanced features like exceptions, concurrency, and mutable data structures by exploiting Haskell’s type system to impose flow constraints. Vassena and Russo [46], Vassena et al. [47] show progress-insensitive noninterference for MAC in a sequential setting and progress-sensitive noninterference in a concurrent setting, both using the two-steps erasure technique.

The flow constraints enforcing confidentiality of read and write operations in DepSec are identical to those of MAC. This means that the examples from MAC that do not involve concurrency can be ported directly to DepSec. To the best of our knowledge, data-dependent security policies like the one presented in Sect. 3 cannot be expressed and enforced in MAC, unlike LIO that allows such policies to be enforced dynamically. DepSec allows for such security policies to be enforced statically. Moreover, Russo [34] does not consider declassification. To address the static limitations of MAC, HLIO [11] takes a hybrid approach by exploiting advanced features in Haskell’s type-system like singleton types and constraint polymorphism. Buiras et al. [11] are able to statically enforce information-flow control while allowing selected security checks to be deferred until run-time.

Dependent Types for Security. Several works have considered the use of dependent types to capture the nature of data-dependent security policies. Zheng and Myers [51, 52] proposed the first dependent security type system for dealing with dynamic changes to runtime security labels in the context of Jif [29], a full-fledged IFC-aware compiler for Java programs, where similar to our work, operations on labels are modeled at the level of types. Zhang et al. [50] use dependent types in a similar fashion for the design of a hardware description language for timing-sensitive information-flow security.

A number of functional languages have been developed with dependent type systems and used to encode value-dependent information flow properties, e.g. Fine [43]. These approaches require the adoption of entirely new languages and compilers where DepSec is embedded in an already existing language. Morgenstern and Licata [25] encode an authorization and IFC-aware programming language in Agda. However, their encoding does not consider side-effects. Nanevski et al. [30] use dependent types to verify information flow and access control policies in an interactive manner.

Lourenço and Caires [23] introduce the notion of dependent information-flow types and propose a fine-grained type system; every value and function have an associated security level. Their approach is different to the coarse-grained approach taken in our work where only some computations and values have associated security labels. Rajani and Garg [33] show that both approaches are equally expressive for static IFC techniques and Vassena et al. [48] show the same for dynamic IFC techniques.

Principles for Information Flow. Bastys et al. [6] put forward a set of informal principles for information flow security definitions and enforcement mechanisms: attacker-driven security, trust-aware enforcement, separation of policy annotations and code, language-independence, justified abstraction, and permissiveness.

Declassification Enforcement. Our hatch builders are reminiscent of downgrading policies of Li and Zdancewic [19]. For example, similar to them, DepSec’s declassification policies naturally express the idea of delimited release [36] that provides explicit characterization of the declassifying computation. Here, DepSec’s policies can express a broad range of policies that can be expressed through predicates, an improvement over simple expression-based enforcement mechanisms for delimited release [4, 5, 36].

An interesting point in the design of declassification policies is robust declassification [49] that demands that untrusted components must not affect information release. Qualified robustness [2, 28] generalizes this notion by giving untrusted code a limited ability to affect information release through the introduction of an explicit endorsement operation. Our approach is orthogonal to both notions of robustness as the intent is to let the untrusted components declassify information but only under very controlled circumstances while adhering to the security policy.

In this paper, we have presented DepSec – a library for statically enforced information-flow control in Idris. Through several case studies, we have showcased how the DepSec primitives increase the expressiveness of state-of-the-art information-flow control libraries and how DepSec matches the expressiveness of a special-purpose dependent information-flow type system on a key example. Moreover, the library allows programmers to implement policy-parameterized functions that abstract over the security policy while retaining precise security levels.

By taking ideas from the literature and by exploiting dependent types, we have shown powerful means of specifying statically enforced declassification policies related to what, who, and when information is released. Specifically, we have introduced the notion of predicate hatch builders and token hatch builders that rely on the fulfillment of predicates and possession of tokens for declassification. We have also shown how the monad [10] can be used to limit hatch usage statically.

Future Work. There are several avenues for further work. Integrity is vital in many security policies and is not considered in MAC nor DepSec. It will be interesting to take integrity and the presence of concurrency into the dependently typed setting and consider internal and termination covert channels as well. It also remains to prove our declassification mechanisms sound. Here, attacker-centric epistemic security conditions [3, 16] that intuitively express many declassification policies may be a good starting point.