Information flow enforcement in monadic libraries

Dominique Devriese, Frank Piessens

Research output: Chapter in Book/Report/Conference proceedingConference paper

24 Citations (Scopus)

Abstract

In various scenarios, there is a need to expose a certain API to client programs which are not fully trusted. In cases where the client programs need access to sensitive data, confidentiality can be enforced using an information flow policy. This is a general and powerful type of policy that has been widely studied and implemented. Previous work has shown how information flow policy enforcement can be implemented in a lightweight fashion in the form of a library. However, these approaches all suffer from a number of limitations. Often, the policy and its enforcement are not cleanly separated from the underlying API, and the user of the API is exposed to a strongly and unnaturally modified interface. Some of the approaches are limited to functional APIs and have difficulty handling imperative features like I/O and mutable state variables. In addition, this previous work uses classic static information flow enforcement techniques, and does not consider more recent dynamic information flow enforcement techniques. In this paper, we show that information flow policies can be enforced on imperative-style monadic APIs in a modular and reasonably general way with only a minor impact on the interface provided to API users. The main idea of this paper is that we implement the policy enforcement in a monad transformer while the underlying monadic API remains unaware and unmodified. The policy is specified through the lifting of underlying monad operations. We show the generality of our approach by presenting implementations of three important information flow enforcement techniques, including a purely dynamic, a purely static and a hybrid technique. Two of the techniques require the use of a generalisation of the Monad type class, but impact on the API interface stays limited. We show that our technique lends itself to formal reasoning by sketching a proof that our implementation of the static technique is faithful to the original presentation. Finally, we discuss fundamental limitations of our approach and how it fits in general information flow enforcement theory.

Original languageEnglish
Title of host publicationTLDI'11 - Proceedings of the 7th ACM SIGPLAN Workshop on Types in Language Design and Implementation
Pages59-71
Number of pages13
DOIs
Publication statusPublished - 7 Mar 2011
Event7th ACM SIGPLAN Workshop on Types in Language Design and Implementation, TLDI'11 - Austin, TX, United States
Duration: 25 Jan 201125 Jan 2011

Conference

Conference7th ACM SIGPLAN Workshop on Types in Language Design and Implementation, TLDI'11
CountryUnited States
CityAustin, TX
Period25/01/1125/01/11

Keywords

  • Information flow enforcement
  • Monad transformer
  • Monads
  • Parameterised monads

Fingerprint

Dive into the research topics of 'Information flow enforcement in monadic libraries'. Together they form a unique fingerprint.

Cite this