Gradual Information Flow Control

Presented as part of the 2016 HCSS conference.

ABSTRACT
Information-flow control (IFC) is a cornerstone of language-based security. A typical IFC policy rules out the flow of information from classified sources to public sinks. The technical property aimed for is noninterference: changes in a classified source do not influence the public sinks. Noninterference comes in different flavors depending on the observational capabilities of an attacker.

Static IFC may take the form of a security type system, which guarantees noninterference for well-typed programs. Dynamic IFC attaches run-time security labels to values, propagates them along with the values, and checks them at appropriate points during program execution, which can be expensive. Hybrid systems enhance the precision of dynamic IFC with additional static analysis to detect implicit flows.

We investigate gradual security type systems that enable mixing static and dynamic (hybrid) IFC in the same program. Our systems guarantee secure information flow for sequential programs with mutable objects and virtual method calls. A program is composed of fragments that are checked either statically or dynamically. Statically checked fragments adhere to a security type system so that they incur no run-time penalty whereas dynamically checked fragments rely on passing and processing run-time security labels. The programmer marks the boundaries between static and dynamic checking with casts so that it is always clear whether a program fragment requires run-time checks.

Our system relies on security annotations on fields and methods. A field annotation either specifies a fixed static security level or it prescribes dynamic checking. A method annotation is a constrained polymorphic security signature. The types of local variables in method bodies are analyzed flow-sensitively and require no annotation. The dynamic checking of fields can be improved by relying on an optional static pointer analysis to approximate implicit flows.

The system is sound and guarantees termination-insensitive noninterference. We sketch the design of a run-time system, the steps needed to extend to a full OO-language like Java, and a path to integrate legacy code.

BIO
Peter Thiemann obtained his diploma in computer science in 1987 at the Technical University of Aachen, Germany. He graduated in 1991 at the University of Tubingen, Germany, where worked as a research and teaching assistant until 1997. In 1998, he was a lecturer in Computer Science at the University of Nottingham, England. Since 1999 he is a professor at the computer science department of the University of Freiburg, Germany, where he leads the programming languages group.

His research interests comprise theory and practice of modern programming languages, in particular program analysis, compiler construction, and program specialization for functional programming languages. The focus of his current research is static and dynamic program analysis for scripting languages.