HLIO: mixing static and dynamic typing for information-flow control in Haskell
- 29 August 2015
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM) in Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming
Abstract
Information-Flow Control (IFC) is a well-established approach for allowing untrusted code to manipulate sensitive data without disclosing it. IFC is typically enforced via type systems and static analyses or via dynamic execution monitors. The LIO Haskell library, originating in operating systems research, implements a purely dynamic monitor of the sensitivity level of a computation, particularly suitable when data sensitivity levels are only known at runtime. In this paper, we show how to give programmers the flexibility of deferring IFC checks to runtime (as in LIO), while also providing static guarantees---and the absence of runtime checks---for parts of their programs that can be statically verified (unlike LIO). We present the design and implementation of our approach, HLIO (Hybrid LIO), as an embedding in Haskell that uses a novel technique for deferring IFC checks based on singleton types and constraint polymorphism. We formalize HLIO, prove non-interference, and show how interesting IFC examples can be programmed. Although our motivation is IFC, our technique for deferring constraints goes well beyond and offers a methodology for programmer-controlled hybrid type checking in Haskell.Keywords
This publication has 35 references indexed in Scilit:
- Paragon for Practical Programming with Information-Flow ControlLecture Notes in Computer Science, 2013
- Lazy Programs Leak SecretsLecture Notes in Computer Science, 2013
- Secure Multi-execution in HaskellLecture Notes in Computer Science, 2012
- From Dynamic to Static and Back: Riding the Roller Coaster of Information-Flow Control ResearchLecture Notes in Computer Science, 2010
- Labels and event processes in the Asbestos operating systemACM Transactions on Computer Systems, 2007
- Dynamic security labels and static information flow controlInternational Journal of Information Security, 2007
- Automata-Based Confidentiality MonitoringLecture Notes in Computer Science, 2007
- Language-based information-flow securityIEEE Journal on Selected Areas in Communications, 2003
- Protecting privacy using the decentralized label modelACM Transactions on Software Engineering and Methodology, 2000
- Generalising monads to arrowsScience of Computer Programming, 2000