Title: Dependent Information Flow Types
By: Luísa Lourenço (NovaLINCS / CITI / UNL)
More info: http://citi.di.fct.unl.pt/seminar/seminar.php?id=228
Abstract:
A critical issue in modern software development consists on finding trustworthy techniques to ensure confidentiality in the presence of multi-tenancy and container sharing. Many reported security leaks in globally used systems, such as email management or social network systems, turn out in many cases to result from programming errors that introduce insecure information flows in complex software layers.
In this talk, we present 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, allow the security level of a type, rather than just the structural type itself, to depend on values. We show how dependent function and dependent sum information flow types provide a direct, natural and elegant way to express and enforce rich and fine grained “row- level" security policies on computations on data structures in which the security level of a structure field may depend in general on values dynamically stored in various other fields, a pervasive challenge in realistic applications such as data-centric web apps.
We develop our framework on top of a minimal typed lambda-calculus with references and collections, and illustrate its expressiveness, showing how secure operations on relevant data manipulation scenarios can be modelled and analysed. Our main results are type-safety and a noninterference theorem ensuring that well-typed programs do not violate prescribed security policies.