Flexible dynamic information flow control in the presence of exceptions

DOI10.1017/S0956796816000241MaRDI QIDQ5371997zbMATH OpenOpenAlexFDO

Authors Deian Stefan, David Folkman Mazières, John Mitchell, Alejandro Russo

Publication date 23 October 2017

Published in Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1207.1457

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Abstract: We describe a new, dynamic, floating-label approach to language-based information flow control. A labeled IO monad, LIO, keeps track of a current label and permits restricted access to IO functionality. The current label floats to exceed the labels of all data observed and restricts what can be modified. Unlike other language-based work, LIO also bounds the current label with a current clearance that provides a form of discretionary access control. Computations may encapsulate and pass around the results of computations with different labels. In addition, the LIO monad offers a simple form of labeled mutable references and exception handling. We give precise semantics and prove confidentiality and integrity properties of a call-by-name lambda-calculus and provide an implementation in Haskell.

Recommendations

• HLIO: mixing static and dynamic typing for information-flow control in Haskell
• Flexible manipulation of labeled values for information-flow control libraries
• Programming Languages and Systems
• Information Flow Tracking for Side-Effectful Libraries
• A Logical System for Modular Information Flow Verification

Cites work

• scientific article; zbMATH DE number 439891 (Why is no real title available?)
• A lattice model of secure information flow
• A monadic analysis of information flow security with mutable state
• Addressing covert termination and timing channels in concurrent information flow systems
• Arrows for secure information flow
• Certification of programs for secure information flow
• Generalising monads to arrows
• Information flow inference for ML
• Laminar
• Parameterised notions of computation
• Security-typed programming within dependently typed programming
• Tackling the awkward squad: Monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell
• Transforming out timing leaks
• Understanding functional dependencies via constraint handling rules

Cited in

(3)

• Discretionary Information Flow Control for Interaction-Oriented Specifications
• HLIO: mixing static and dynamic typing for information-flow control in Haskell
• Flexible manipulation of labeled values for information-flow control libraries

Describes a project that uses

Uses Software

• Haskell
• Aglet
• Laminar

This page was built for publication: Flexible dynamic information flow control in the presence of exceptions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5371997)