|
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
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:
- conf_examples file that has some of the examples of a conference manager system
- conf_examples_abrv same as conf_examples but using global type and identifiers definitions
- simple_examples file that illustrates some of our system and type system features
- dropbox_examples file that illustrates a toy dropbox service example
- LambdaDIFT.jar jar file that contains our typechecker prototype
- z3_linux, z3_mac and z3_win binaries of Z3 SMT Solver, version 4.3.2
- dift (Unix) script file and dift.bat (Windows) script file to give execution permissions to Z3 binaries and execute the jar containing the typechecker
- Z3 dlls msvcp100.dll, msvcr100.dll and vcomp100.dll (required for Windows only)
- default_lattice file containing the description of a security lattice
Synopsis:
sh dift [-help] [-input ] [-output ] [-debug ] [-lattice ]
Executing the DIFT Typechecker prototype:
- 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
- Execute command '#exit' to exit the typechecker
To execute (an) example(s) from a file:
- 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;;
A series of simple examples, to illustrate the language syntax
and the basic type system features.
These illustrate security verified code for the conference manager
example described in the paper.
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