Special issue on verified information flow security

1.Foreword

Information flow security has remained an active topic of research since the seminal work of Denning [4], Goguen and Meseguer [5] and their contemporaries. The past few years have seen the seeds of formal information flow security sown in the preceding three decades bear practical fruit. A number of real-world systems with formally verified guarantees of information flow security now exist. These systems serve as exemplars of verified security that span hardware [1], operating system microkernels [11] and virtualisation platforms [6], programming languages [7], mobile operating systems [9], web browsers [2,8], web applications [3,10] and distributed systems. The time is ripe to mark this success with this special issue of the Journal of Computer Security that presents a collection of papers that synthesise the major results from a range of exemplar projects.

This issue contains three papers that represent the state-of-the-art in distributed systems and programming languages for information flow control. An additional two articles were commissioned for this special issue that do the same for specialist hardware architectures and virtualisation platforms, and appeared in Volume 24, Issue 6, of this journal.

Each paper was specially solicited by approaching authors of major papers on verified information flow security that had recently appeared in the top conference venues. We carefully selected work that focused on practicality, and presented feature-rich systems or platforms with strong information flow guarantees, that have remained under active development, while ensuring we covered the broadest portion of the traditional hardware/software stack (hardware, operating system, programming language, distributed system). Thus the running theme of this special issue is very much on the kinds of practical security guarantees that can be obtained, and secure systems that can be constructed, by system- and platform-enforced information flow control.

Hardware. Azevedo de Amorim et al. [1] (in Volume 24, Issue 6 of this journal) present a clean slate hardware architecture that provides special facilities for enforcing strong security properties, and the verification of operating system software that uses these facilities to enforce a strong information flow control property. This work demonstrates the kinds of verified guarantees that can be provided by deploying specialist software atop a clean-slate hardware platform.

Virtualisation software. Guanciale et al. [6] (in Volume 24, Issue 6 of this journal) present a verified virtualisation solution for ARM, which runs entire Linux operating systems while enforcing strong isolation to allow security sensitive applications to run alongside. They deploy the solution in the context of a security monitor running alongside Linux to prevent code injection attacks against the latter. This work demonstrates the kinds of guarantees that can be obtained by deploying verified, minimal virtualisation solutions to confine large legacy, untrustworthy components.

Programming languages. Broberg et al. (in this issue) present the design of the Paragon programming language for programming applications with strong, dynamic information flow guarantees. Paragon provides a set of minimal, yet highly expressive, constructs for defining dynamic, stateful, information flow control policies that are enforced via sophisticated static checking, in an extension of the Java language. Their paper focuses heavily on the design rationale of Paragon and the mechanics of its static policy enforcement. It demonstrates the kinds of guarantees that can be obtained by static checking in the context of careful extensions to mainstream programming languages.

Distributed systems. Liu et al. and Griffin et al. (both in this issue) each present the design of distributed systems, namely Fabric and Hails respectively, for enforcing strong, decentralised information flow policies. Each enables programming distributed applications composing mutually suspicious components accessing persistent data, with strong information flow control applied to how data may be accessed and transmitted through the system. Each is built as an extension of an existing information flow control (IFC) programming language: Liu et al.’s Fabric is an extension of Jif, which is itself an IFC extension of Java; and Griffin et al.’s Hails is an extension of LIO, which adds IFC to Haskell. Hails focuses on supporting distributed web applications, programmed in an extension to the traditional Model-View-Controller paradigm that incorporates security policy enforcement as a first class activity. Fabric is more along the lines of a traditional distributed system, incorporating support for distributed transactions and secure mobile code. Each represents one view on how to apply IFC languages to build platforms for implementing secure distributed systems with strong information flow control.