Dependent Information Flow Types


Paper

Dependent Information Flow Types, Luisa Lourenšo and Luis Caires, TR 2014/6 DI FCT UNL.

Abstract. In this paper, we develop a novel notion of dependent information flow types. Dependent information flow types fit within the standard framework of dependent type theory, but, unlike usual dependent types, crucially allow the security level of a type, rather than just the structural data type itself, to depend on runtime values. Our dependent function and dependent sum information flow types provide a direct, natural and elegant way to express and enforce fine grained security policies on programs, including programs that manipulate structured data types in which the security level of a structure field may depend on values dynamically stored in other fields, still considered a challenge to security enforcement in software systems such as data-centric web-based applications. We base our development on the very general setting of a minimal lambda-calculus with references and collections. We illustrate its expressiveness, showing how secure operations on relevant scenarios can be modelled and analysed using our dependent information flow type system, which is also shown to be amenable to algorithmic type checking. Our main results include type-safety and non-interference theorems ensuring that well-typed programs do not violate prescribed security policies.


Accepted paper version (preprint as accepted at POPL'15)

Download

Short Prototype Manual 1.10

Minimum requirements: jre 1.6

Online version (rise4fun)


Prototype Type Checker

Our current type checker implementation (version 1.10), based on the algorithm described in the paper above, is still under development (check for updates), but already covers all features of the language and type system. It is downloadable as a zip archive, including the main java jar file (the system is written in Scala), the (required) Z3 SMT solver, and sample security lattice definition file. If you find issues or bugs, please let us know, we would appreciate, the development is continuing.

Instructions:

.zip file includes: Synopsis:
 sh dift [-help] [-input ] [-output ] [-debug ] [-lattice ] 
Executing the DIFT Typechecker prototype:
  1. Run sh dift (Unix system) or dift.bat(Windows) to execute the typechecker with the default options, that is using security lattice defined in default_lattice
  2. Execute command '#exit' to exit the typechecker
To execute (an) example(s) from a file:
  1. Run sh dift -input filename (Unix system) or dift.bat -input filename(Windows) to execute the typechecker with the default lattice, using the examples from file filename. For e.g., sh dift -input simples_examples will execute the examples in file simple_examples.
Programs always terminate with ';;', so a file can contain multiple programs separated by ';;'.

A typical example

Operations on a mutable password "file" with heterogeneous dynamic security conpartments.
typedef usr_type = Sigma[uid: int^BOT,pwd: int^U(uid)]^BOT in
typedef usr_file_type = { ref (usr_type)^BOT } in
typedef pwd_list_type = { int^U(TOP) } in

let get_pwd = 
      fun u:int^BOT, f:usr_file_type => 
         foreach (urec in f) with s = 0 do
            let r = !urec in
              if (r.uid == u) then r.pwd else s 
in
let list_pwds =
      fun f:usr_file_type => [ { int^U(TOP) } ]
         ( foreach (urec in f) with s = {}:pwd_list_type do
            let r = !urec in r.pwd :: s )
in 
let updt_pwd = 
      fun f:usr_file_type, u:int^BOT, pw:int^U(u) => 
         foreach (urec in f) with s = skip do
            let r = !urec in
              if (r.uid == u) then
               urec := [ uid:int^BOT=r.uid, pwd:int^U(uid) = pw ] 
              else skip
in updt_pwd;;

Simple examples

A series of simple examples, to illustrate the language syntax and the basic type system features.

Examples from the paper above

These illustrate security verified code for the conference manager example described in the paper.

Toy multi-tenant dropbox service

A toy drop box service, featuring disjoint dynamically generated security compartments over a mutable object store (objects encoded using records of closures).
last update 20-March-2015