Type-based gradual enforcement of security policies for concurrent programs

Funded by DFG as part of the priority programme 1496 "Reliably Secure Software Systems RS³"

Summary

Sequential programming is no longer adequate to tap the full potential of today's computing systems. They require concurrent programming models because they contain multi-core processors and regularly access networked, distributed services. Message-passing concurrency with channel-based communication is a promising programming paradigm for these systems.

As concurrent, distributed programs cannot be considered in isolation, enforcing access control and guaranteeing data integrity and confidentiality is of utmost importance. However, the complexity of such programs makes the statement and enforcement of consistent security policies challenging.

The overall goal of this project is to establish a framework for stating and enforcing user-configurable security policies on object-oriented programs with message-passing concurrency. This framework centralizes the concerns for access control and information flow and relies on static and dynamic analysis to enforce the respective policies. It also supports the gradual introduction of security policies into an existing code base.

The framework will be based on hierarchical policies specified by session types and contracts, corresponding to a role hierarchy. The policies considered range from simple safety properties to noninterference assertions that manage secure information flow. The compilation of hierarchical policies into staged monitoring and its efficient realization is a central component of the framework. Practical applicability will be demonstrated with a browser-based implementation for the JavaScript language.

Gradual Security Typing with References

Luminous Fennell and Peter Thiemann

in Proceedings: Computer Security Foundations Symposium 2013

Type systems for information-flow control (IFC) are often inflexible and too conservative. On the other hand, dynamic run-time monitoring of information flow is flexible and permissive but it is difficult to guarantee robust behavior of a program. Gradual typing for IFC enables the programmer to choose between permissive dynamic checking and a predictable, conservative static type system, where needed.

We propose ML-GS, a monomorphic ML core language with references and higher-order functions that implements gradual typing for IFC. This language contains security casts, which enable the programmer to transition back and forth between static and dynamic checking.

In particular, ML-GS enables non-trivial casts on reference types so that a reference can be safely used everywhere in a program regardless of whether it was created in a dynamically or statically checked part of the program. The reference can be shared between dynamically and statically checked parts.

The Blame Theorem for a Linear Lambda Calculus with Type Dynamic

Luminous Fennell and Peter Thiemann

in Proceedings: Symposium on Trends of Functional Programming 2012 (LNCS 7829)

Scripting languages have renewed the interest in languages with dynamic types. For various reasons, realistic programs comprise dynamically typed components as well as statically typed ones. Safe and seamless interaction between these components is achieved by equipping the statically typed language with a type Dynamic and coercions that map between ordinary types and Dynamic. In such a gradual type system, coercions that map from Dynamic are checked at run time, throwing a blame exception on failure.

This paper enlightens a new facet of this interaction by considering a gradual type system for a linear lambda calculus with recursion and a simple kind of subtyping. Our main result is that linearity is orthogonal to gradual typing. The blame theorem, stating that the type coercions always blame the dynamically typed components, holds in a version analogous to the one proposed by Wadler and Findler, also the operational semantics of the calculus is given in a quite different way. The significance of our result comes from the observation that similar results for other calculi, e.g., affine lambda calculus, standard call-by-value and call-by-name lambda calculus, are straightforward to obtain from our results, either by simple modification of the proof for the affine case, or, for the latter two, by encoding them in the linear calculus.

• Full version with proofs

Last modified: Thu May 31 2012