2012/07/05 by Deian Stefan, Stefan, Deian, Alejandro Russo +5 · 1 citation
Computer Science · Social Sciences · #Access Control and Trust #Cloud Data Security Solutions #Cryptography and Security (cs.CR) #D.1.1 #D.3.3 #D.4.6 #FOS: Computer and information sciences #Programming Languages (cs.PL) #Security and Verification in Computing #cs.CR #cs.PL
paper · pdf · doi:10.48550/arxiv.1207.1457
arxiv created 2012/07/05 · openalex publication_date 2012/07/05 · arxiv updated 2015/03/20 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 λ-calculus and provide an implementation in Haskell.