An Agda model of MAC

Information Flow Control (IFC) is a language-based security mechanism that tracks where data flows within a program and prevents leakage of sensitive data. IFC has been embedded in pure functional languages such as Haskell, in the form of a library, thus reducing the implementation and maintenance effort and fostering a secure-by-construction programming-model.

MAC is a state-of-the-art IFC Haskell library that detects leaks statically and that supports many advanced programming features, such as exceptions, mutable references and concurrency. While MAC is an elegant functional pearl (Two can keep a secret, if one of them uses Haskell) and is implemented concisely in less than 200 lines of code, it does not provide any formal security guarantee.

This project fills that gap, by studying the formal security guarantees of MAC. In particular, the code in this repository models the MAC library as a simply-typed call-by-name lambda-calculus extended with MAC primitives and proves that the language satisfies non-interference. These proofs support the theorems of the manuscript MAC A Verified Static Information-Flow Control Library.

The mechanized model and the proofs are developed in Agda. The code has been typechecked with Agda version 2.5.3, stdlib version 0.14, and --rewriting flag.

What to trust

Agda is a dependently typed functional programming language and a proof assistant based on intuitionistic type theory, a foundational system for constructive mathematics developed by the Swedish logician Per Martin-Lof. Intuitively, under the Curry-Howard Correspondence, theorems correspond to type-signatures and proofs to well-typed programs. Note that the correctness of the proofs developed in this repository rely upon the correctness of Agda's type-checker and termination-checker. In the code, we use unicode characters extensively in order to follow closely the notation used in the manuscript. As a result, it should be easy to relate the rules and theorems listed there, with the data-types and type-signatures in the code in this repository.

Where to start

The main modules of the (sequential) model are the following:

  • Sequential.Calculus (syntax)
  • Sequential.Semantics (operational semantics)
  • Sequential.Determinism (determinancy)
  • Sequential.Security.Erasure (erasure function)
  • Sequential.Security.Simulation (simulation property)

Modules are names likewise in the directory Concurrent. Module MAC instantiates the main security theorems, which are parametric in the lattice and in the scheduler, with the two point lattice and with the Round Robin scheduler used by GHC. The security theorems proved are progress-insensitive noninterference (Sequential.Security.PINI) for the sequential calculus and progress-sensitive noninterference (Concurrent.PSNI) for the concurrent calculus.

What is verified

Note that there is a gap between the model formalized here and the actual library. For example, the run-time system of the language is not part of the model and can be misused to leak secrets via covert channels. The presence of multiple cores, the garbage collector and lazy evaluation itself are examples of those channels, which must be addressed specifically, since they cannot be controlled by a library. (For instance the paper Securing Concurrent Lazy Programs Against Information Leakage and the accompying code lazy-mac, address lazy-evaluation.