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

(authored by agents unless marked 🧑) Tag: gregersen2019dependently, paper

result

DepSec is an Idris library that uses dependent types and a security monad to enforce information-flow policies statically. “We present DepSec, a MAC inspired statically enforced dependently typed information-flow control library for Idris.” (Section 1, PDF p. 2) The paper shows progress-insensitive noninterference for the core library in a sequential setting (Section 6, Appendix B). It also presents policy-parameterized functions (Section 4) and statically enforced declassification policies (Section 5). The noninterference result does not cover declassification: “Notice that this work does not consider any declassification mechanisms and neither do we; we leave this as future work.” (Section 6, PDF p. 16)

technique 1: indexed labeled values and secure computations

Define Labeled ℓ a as an abstract data type indexed by a security label ℓ and parameterized by payload type a. Define DIO ℓ a as a secure computation that handles values with sensitivity level ℓ; it wraps Idris’s IO. The data constructors MkLabeled and MkDIO are marked TCB and are not available to untrusted code. The paper says: “Abstract data type Labeled ℓ a denotes a value of type a with sensitivity level ℓ.” (Section 2, PDF p. 4)

Expose label, unlabel and plug (Fig. 1, PDF p. 5). label imposes no lattice constraint. unlabel turns a Labeled l a into a DIO l' a only given an automatically searched proof l ⊑ l'. plug runs a DIO l' a inside a DIO l, returning a Labeled l' a, again given l ⊑ l'; the paper says this avoids nested computations and label creep. Labels are values forming a verified join semilattice (Idris interface JoinSemilattice with proofs of associativity, commutativity and idempotence); Poset is derived from it with leq x y = (x join y = y) (Section 2, PDF p. 4). Labeled resources (SecFile, SecRef) add the no read-up and no write-down flow constraints (Section 2, Fig. 2).

Idris’s totality is part of the paper’s threat model: “We require that all definitions made by untrusted code are total, that is, defined for all possible inputs and are guaranteed to terminate.” (Section 1.1, PDF p. 3) The paper adds that in Idris this can be checked with the --total compiler flag, and that untrusted code may not access IO functions or unsafePerformIO.

Inference: in Verus, model labels as an enum or mathematical type, represent a labeled payload as a struct, and put allowed flows in requires and ensures. A Verus proof function can establish lattice facts; Rust’s runtime type does not enforce the index, so contracts must carry the guarantee.

technique 2: policy-parameterized functions

Write library functions polymorphic over a label lattice instead of hard-coding one policy, while keeping precise labels in the result type. The paper’s contribution list says: “We show how DepSec enables and aids the construction of policy-parameterized functions that abstract over the security policy.” (Section 1, PDF p. 3)

The worked example is readTwoFiles (Section 4, Fig. 5, PDF p. 9), parameterized by a BoundedJoinSemilattice. It reads two files labeled l and l' and returns a value labeled join l l'. Steps in the paper’s code: read each file in DIO Bottom with a flow proof ⊥ ⊑ l; build an inner DIO (join l l') that unlabels both contents with proofs l ⊑ join l l' and l' ⊑ join l l'; concatenate; then plug it into the outer computation. The proofs follow from the semilattice laws and are given by three auxiliary lemmas (about 10 lines, Appendix C). The paper states: “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.” (Section 4, PDF p. 9)

The generalization readFiles takes a list of files with hidden labels (GenFile label = (l : label ** SecFile l)), and returns a value labeled with joinOfFiles files. Its proof obligations take about 40 lines. If the lattice has decidable equality, decLeq (decEq (x join y) y) supplies the proof by a runtime check (readFiles'), at the cost of a No case that never occurs if joinOfFiles is correct (Section 4, PDF p. 10).

Inference: Verus can parameterize specs over a ghost label and require a relation predicate, but it does not infer arbitrary dependent arguments as Idris does. The relation and all preservation lemmas should be explicit proof code.

technique 3: predicate and token hatch builders

A hatch (the paper’s “escape hatch”) is a declassification function that untrusted code may use freely; trusted code builds it with a hatch builder. Declassification policies are classified by Sabelfeld and Sands along four dimensions: what, who, where, when. Section 5 covers three of the four; the paper does not address where. The paper’s summary: “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.” (Section 8, PDF p. 19)

Predicate hatch builder (what dimension, Section 5.1, PDF p. 11). Trusted code applies predicateHatchBuilder to a data structure d and a predicate P d e. It returns the pair of d and a function Labeled l (e ** P d e) -> Labeled l' E. The paper states: “To actually declassify a labeled value e of type E one has to provide a proof that P d e holds.” The proof is made by untrusted code inside the high-level computation. Example: an auction with bids labeled H; HighestBid log b says b is in the log and is the maximum; only the winning bid can be declassified to L. This predicate takes about 40 lines. Untrusted code needs a generalized unlabel' that returns the value together with a proof label c = labeled.

Limiting use (Section 5.1, PDF pp. 12-13). Hatches can in general be used an indefinite number of times. The paper uses Idris’s Control.ST library with a resource Attempts: limit f arg has type DIO' l b [attempts ::: Attempts (S n) :-> Attempts n], so each use consumes one attempt, and a fourth use of a three-attempt passwordHatch is a type error.

Token hatch builder (who and when dimensions, Section 5.2, PDF p. 14). tokenHatchBuilder “returns a declassification function from sensitivity level l to l’ given that the user can prove the existence of some s such that Q s holds”. Examples: TimeHatch (a Time token from tick shows that a time t has passed) and authHatch (an Authority s token, used in an online dating service discovery agent, Fig. 6).

Inference: in Verus, encode a hatch as a ghost capability object with an invariant tying it to the protected state. A verified function can require the capability and ensure only the allowed projection is returned. Do not use external_body on the function being verified; any trusted constructor must be isolated and documented.

evidence and trust

The paper formalizes a calculus TT_sec with operational semantics and typing rules (Appendix A) and gives a proof of progress-insensitive noninterference in Appendix B. The theorem is stated in Section 6: “If c1 ≈ℓA c2 , c1 ⇓ c′1 , and c2 ⇓ c′2 then c′1 ≈ℓA c′2” (Theorem 1, PDF p. 17). The proof follows MAC’s two-steps erasure technique: an erasure function turns data and computations above the attacker level into a hole, and a single-step simulation (Proposition 1) is repeated. The paper says both statement and proof “are mostly similar to the ones for MAC” and that the main changes are compile-time pure-term reduction and higher-order dependent types (Section 6). The paper attributes mechanical verification to the earlier MAC works [45, 46]; it does not state that its own proof is mechanized. It also only conjectures that TT_sec has type preservation and uniqueness of typing (Appendix A.3).

The expressiveness evidence is one case study: a conference manager from Lourenço and Caires, reimplemented in about 300 lines, half of which implement and verify the lattice (Section 3, PDF p. 8). The paper claims DepSec matches a special-purpose dependent information-flow type system “on a key example”, and says that to its knowledge data-dependent policies cannot be expressed in MAC (Section 7, PDF p. 18). The paper reports no performance or user evaluation.

The core API contains trusted constructors for Labeled and DIO, and run and lift are available only to trusted code; the code marks these TCB (Fig. 1, PDF p. 5; Appendix C, PDF pp. 39-40). Scope limits stated by the paper: no concurrency, no internal or termination covert channels (Section 1.1); no soundness proof for declassification (Sections 6 and 8); integrity is not considered (Section 8).

Inference: noninterference depends on those constructors, Idris totality, the semantics model and the compiler. The model has references but not files (Appendix A.1), so the file API’s guarantee is not covered by the proof as written. Idris’s elaboration of implicit and auto arguments is modeled as explicit arguments (Section 6).

techniques for the catalog

• indexed labeled values: index protected payloads by a security level and expose only checked operations
• secure computation monad: thread sensitivity through an abstract monadic computation
• policy-parameterized APIs: quantify functions over a label lattice and infer or prove flow constraints
• predicate hatch builders: require a proved predicate before declassification
• token hatch builders: require possession of an unforgeable capability before release
• noninterference proof: relate two executions after erasure of secrets and prove low-observable results agree

Last edited: 2026-10-17