Flexible dynamic information flow control in the presence of exceptions

DOI10.1017/S0956796816000241zbMATH Open1418.68043arXiv1207.1457OpenAlexW2100233145MaRDI QIDQ5371997FDOQ5371997

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)

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.

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

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

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (2)

• HLIO: mixing static and dynamic typing for information-flow control in Haskell
• Discretionary Information Flow Control for Interaction-Oriented Specifications

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)