Team for Research in
Ubiquitous Secure Technology

Citation
Delan Stefan, Alejandro Russo, John C. Mitchell, David Mazières. "Flexible dynamic information flow control in Haskell". Proceedings of the 4th ACM symposium on Haskell, 2011.

Abstract
We describe a new, dynamic, floating-label approach to language-based information flow control, and present an implementation in Haskell. A labeled IO monad, LIO, keeps track of a current label and permits restricted access to IO functionality, while ensuring that the current label exceeds 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. In addition, programs may encapsulate and pass around the results of computations with different labels. We give precise semantics and prove confidentiality and integrity properties of the system.

Electronic downloads

• http://dl.acm.org/citation.cfm?doid=2096148.2034688

• HTML

  Delan Stefan, Alejandro Russo, John C. Mitchell, David
  Mazières. <a
  href="http://www.truststc.org/pubs/889.html"
  >Flexible dynamic information flow control in
  Haskell</a>, Proceedings of the 4th ACM symposium on
  Haskell, 2011.

• Plain text

  Delan Stefan, Alejandro Russo, John C. Mitchell, David
  Mazières. "Flexible dynamic information
  flow control in Haskell". Proceedings of the 4th ACM
  symposium on Haskell, 2011.

• BibTeX

  @inproceedings{StefanRussoMitchellMazires11_FlexibleDynamicInformationFlowControlInHaskell,
      author = {Delan Stefan and Alejandro Russo and John C.
                Mitchell and David Mazières},
      title = {Flexible dynamic information flow control in
                Haskell},
      booktitle = {Proceedings of the 4th ACM symposium on Haskell},
      year = {2011},
      abstract = {We describe a new, dynamic, floating-label
                approach to language-based information flow
                control, and present an implementation in Haskell.
                A labeled IO monad, LIO, keeps track of a current
                label and permits restricted access to IO
                functionality, while ensuring that the current
                label exceeds 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. In addition,
                programs may encapsulate and pass around the
                results of computations with different labels. We
                give precise semantics and prove confidentiality
                and integrity properties of the system.},
      URL = {http://www.truststc.org/pubs/889.html}
  }
  

Posted by Mary Stewart on 4 Apr 2012.
For additional information, see the Publications FAQ or contact webmaster at www truststc org.