skip to main content
research-article

HLIO: mixing static and dynamic typing for information-flow control in Haskell

Published: 29 August 2015 Publication History

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.

References

[1]
A. Askarov and A. Sabelfeld. Tight enforcement of information-release policies for dynamic languages. In Proceedings of the 22nd IEEE Computer Security Foundations Symposium. IEEE Computer Society, 2009.
[2]
T. H. Austin and C. Flanagan. Efficient purely-dynamic information flow analysis. In Proc. ACM Workshop on Programming Languages and Analysis for Security (PLAS), June 2009.
[3]
N. Broberg, B. van Delft, and D. Sands. Paragon for practical programming with information-flow control. In APLAS, volume 8301 of Lecture Notes in Computer Science, pages 217–232. Springer, 2013.
[4]
P. Buiras and A. Russo. Lazy programs leak secrets. In Secure IT Systems - 18th Nordic Conference, NordSec 2013, Ilulissat, Greenland, October 18-21, 2013, Proceedings. Springer Verlag, 2013.
[5]
P. Buiras, A. Levy, D. Stefan, A. Russo, and D. Mazières. A library for removing cache-based attacks in concurrent information flow systems. In Trustworthy Global Computing - 8th International Symposium, TGC 2013, 2013.
[6]
P. Buiras, D. Stefan, and A. Russo. On flow-sensitive floating-label systems. In Proc. of 27th IEEE Computer Security Foundations Symp., July 2014.
[7]
P. Buiras, D. Vytiniotis, and A. Russo. HLIO: Mixing Static and Dynamic Typing for Information-Flow Control in Haskell (Extended version), 2015. URL http://www.cse.chalmers.se/ ~buiras/hlio/. T. Disney and C. Flanagan. Gradual information flow typing. In Workshop on Script-to-Program Evolution (STOP), 2011.
[8]
R. A. Eisenberg and S. Weirich. Dependently typed programming with singletons. In Proceedings of the 2012 Haskell Symposium, Haskell ’12, pages 117–130, New York, NY, USA, 2012. ACM. ISBN 978-1-4503- 1574-6. URL http://doi.acm.org/10.1145/2364506.2364522.
[9]
R. A. Eisenberg, D. Vytiniotis, S. Peyton Jones, and S. Weirich. Closed type families with overlapping equations. In Proc. of the 41st ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL ’14. ACM, 2014.
[10]
L. Fennell and P. Thiemann. Gradual security typing with references. In Proceedings of the IEEE 26th Computer Security Foundations Symposium, CSF ’13. IEEE Computer Society, 2013.
[11]
C. Flanagan. Hybrid type checking. In Proc. of the 33rd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL ’06. ACM, 2006.
[12]
D. B. Giffin, A. Levy, D. Stefan, D. Terei, D. Mazières, J. Mitchell, and A. Russo. Hails: Protecting data privacy in untrusted web applications. In 10th Symposium on Operating Systems Design and Implementation (OSDI), pages 47–60. USENIX, 2012.
[13]
S. T. Hochstadt and M. Felleisen. Interlanguage migration: from scripts to programs. In OOPSLA ’06: Companion to the 21st ACM SIGPLAN symposium on Object-oriented programming systems, languages, and applications. ACM, 2006.
[14]
J. Hughes. Generalising monads to arrows. Science of Computer Programming, 37(1–3):67–111, 2000.
[15]
M. Jaskelioff and A. Russo. Secure multi-execution in Haskell. In Perspectives of Systems Informatics - 8th International Andrei Ershov Memorial Conference, PSI, 2011.
[16]
G. Le Guernic. Automaton-based confidentiality monitoring of concurrent programs. In Computer Security Foundations Symposium, 2007. CSF ’07. 20th IEEE. IEEE Computer Society, 2007.
[17]
G. Le Guernic, A. Banerjee, T. Jensen, and D. A. Schmidt. Automatabased confidentiality monitoring. In Proc. of the 11th Asian Computing Science Conference on Advances in Computer Science: Secure Software and Related Issues, ASIAN’06. Springer-Verlag, 2007.
[18]
P. Li and S. Zdancewic. Encoding Information Flow in Haskell. In CSFW’06: Proc. of the 19th IEEE Workshop on Computer Security Foundations. IEEE Computer Society, 2006.
[19]
E. Meijer and P. Drayton. Static Typing Where Possible, Dynamic Typing When Needed. Revival of Dynamic Languages, 2005. URL \url{http://research.microsoft.com/\~emeijer/ Papers/RDL04Meijer.pdf}. S. Moore and S. Chong. Static analysis for efficient hybrid informationflow control. In Proc. of the 24th IEEE Computer Security Foundations Symposium. IEEE Press, June 2011.
[20]
A. C. Myers and B. Liskov. Protecting privacy using the decentralized label model. ACM Trans. on Computer Systems, 9(4):410–442, October 2000.
[21]
A. Nanevski, G. Morrisett, and L. Birkedal. Polymorphism and Separation in Hoare Type Theory. In Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming, ICFP ’06, pages 62–73, New York, NY, USA, 2006. ACM. ISBN 1-59593-309-3. URL http://doi.acm.org/10.1145/1159803.1159812.
[22]
D. Orchard and T. Schrijvers. Haskell type constraints unleashed. In Lecture Notes in Computer Science, pages 56–71. Springer, 2010.
[23]
. URL https://lirias.kuleuven.be/handle/123456789/259608.
[24]
A. Rastogi, N. Swamy, C. Fournet, G. Bierman, and P. Vekris. Safe and efficient gradual typing for typescript. In In Proc. of the ACM Conference on Principles of Programming Languages (POPL) 2015, Jan. 2015.
[25]
A. Russo and A. Sabelfeld. Dynamic vs. static flow-sensitive security analysis. In Proc. of the 2010 23rd IEEE Computer Security Foundations Symp., CSF ’10, pages 186–199. IEEE Computer Society, 2010.
[26]
A. Russo, K. Claessen, and J. Hughes. A library for light-weight information-flow security in Haskell. In Haskell ’08: Proc. of the first ACM SIGPLAN symposium on Haskell, pages 13–24, 2008.
[27]
A. Sabelfeld and A. C. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1), January 2003.
[28]
A. Sabelfeld and A. Russo. From dynamic to static and back: Riding the roller coaster of information-flow control research. In Proc. Andrei Ershov International Conference on Perspectives of System Informatics, Lecture Notes in Computer Science (LNCS). Springer Verlag, June 2009.
[29]
P. Shroff, S. Smith, and M. Thober. Dynamic Dependency Monitoring to Secure Information Flow. In Proceedings of the 20th IEEE Computer Security Foundations Symposium, CSF ’07. IEEE Computer Society, 2007.
[30]
J. G. Siek and W. Taha. Gradual typing for functional languages. In Proc. of Scheme and functional programming workshop. Technical Report. University of Chicago, 2006.
[31]
V. Simonet. The Flow Caml system. Software release. Located at http: //cristal.inria.fr/~simonet/soft/flowcaml/, July 2003.
[32]
A. Takikawa, T. S. Strickland, C. Dimoulas, S. Tobin-Hochstadt, and M. Felleisen. Gradual typing for first-class classes. In Proc. of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA ’12. ACM, 2012.
[33]
D. Terei, S. Marlow, S. P. Jones, and D. Mazières. Safe Haskell. In Proceedings of the 5th Symposium on Haskell, September 2012.
[34]
T. Tsai, A. Russo, and J. Hughes. A library for secure multi-threaded information flow in Haskell. In Computer Security Foundations Symp., 2007. CSF ’07. 20th IEEE, pages 187–202, July 2007.
[35]
S. VanDeBogart, P. Efstathopoulos, E. Kohler, M. Krohn, C. Frey, D. Ziegler, F. Kaashoek, R. Morris, and D. Mazières. Labels and event processes in the Asbestos operating system. ACM Trans. on Computer Systems, 25(4):11:1–43, December 2007. A version appeared in Proc. of the 20th ACM Symp. on Operating System Principles, 2005.
[36]
M. M. Vitousek, A. M. Kent, J. G. Siek, and J. Baker. Design and Evaluation of Gradual Typing for Python. In Proc. of the 10th ACM Symposium on Dynamic Languages, DLS ’14. ACM, 2014.
[37]
D. Volpano, C. Irvine, and G. Smith. A sound type system for secure flow analysis. Journal of Computer Security, 4(2-3):167–187, Jan. 1996.
[38]
D. Vytiniotis, S. Peyton Jones, and J. P. Magalh˜aes. Equality proofs and deferred type errors: A compiler pearl. In Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, ICFP ’12, pages 341–352, New York, NY, USA, 2012. ACM. ISBN 978- 1-4503-1054-3. URL http://doi.acm.org/10.1145/2364527.
[39]
[40]
P. Wadler and R. B. Findler. Well-typed programs can’t be blamed. In Proc. of the 18th European Symposium on Programming Languages and Systems: Held As Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, ESOP ’09. Springer-Verlag, 2009.
[41]
B. A. Yorgey, S. Weirich, J. Cretin, S. Peyton Jones, D. Vytiniotis, and J. P. Magalh˜aes. Giving Haskell a Promotion. In Proceedings of the 8th ACM SIGPLAN Workshop on Types in Language Design and Implementation, TLDI ’12, pages 53–66, New York, NY, USA, 2012. ACM. ISBN 978- 1-4503-1120-5. URL http://doi.acm.org/10.1145/2103786.
[42]
[43]
N. Zeldovich, S. Boyd-Wickizer, E. Kohler, and D. Mazières. Making information flow explicit in HiStar. In Proc. of the 7th Symp. on Operating Systems Design and Implementation, pages 263–278, Seattle, WA, November 2006.
[44]
L. Zheng and A. C. Myers. Dynamic security labels and static information flow. International Journal of Information Security, 6(2–3), 2007.

Cited By

View all
  • (2021)An axiomatic approach to detect information leaks in concurrent programsProceedings of the 43rd International Conference on Software Engineering: New Ideas and Emerging Results10.1109/ICSE-NIER52604.2021.00015(31-35)Online publication date: 25-May-2021
  • (2021)Dynamic IFC Theorems for Free!2021 IEEE 34th Computer Security Foundations Symposium (CSF)10.1109/CSF51468.2021.00005(1-14)Online publication date: Jun-2021
  • (2019)Compile-Time Security Certification of Imperative Programming LanguagesE-Business and Telecommunications10.1007/978-3-030-34866-3_8(159-182)Online publication date: 13-Nov-2019
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices
ACM SIGPLAN Notices  Volume 50, Issue 9
ICFP '15
September 2015
436 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2858949
  • Editor:
  • Andy Gill
Issue’s Table of Contents
  • cover image ACM Conferences
    ICFP 2015: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming
    August 2015
    436 pages
    ISBN:9781450336697
    DOI:10.1145/2784731
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 29 August 2015
Published in SIGPLAN Volume 50, Issue 9

Check for updates

Author Tags

  1. Information-flow control
  2. constraint kinds
  3. data kinds
  4. dynamic typing
  5. gradual typing
  6. hybrid typing
  7. singleton types

Qualifiers

  • Research-article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)27
  • Downloads (Last 6 weeks)3
Reflects downloads up to 20 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2021)An axiomatic approach to detect information leaks in concurrent programsProceedings of the 43rd International Conference on Software Engineering: New Ideas and Emerging Results10.1109/ICSE-NIER52604.2021.00015(31-35)Online publication date: 25-May-2021
  • (2021)Dynamic IFC Theorems for Free!2021 IEEE 34th Computer Security Foundations Symposium (CSF)10.1109/CSF51468.2021.00005(1-14)Online publication date: Jun-2021
  • (2019)Compile-Time Security Certification of Imperative Programming LanguagesE-Business and Telecommunications10.1007/978-3-030-34866-3_8(159-182)Online publication date: 13-Nov-2019
  • (2017)The Case for Writing a Kernel in RustProceedings of the 8th Asia-Pacific Workshop on Systems10.1145/3124680.3124717(1-7)Online publication date: 2-Sep-2017
  • (2024)Sesame: Practical End-to-End Privacy Compliance with Policy Containers and Privacy RegionsProceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles10.1145/3694715.3695984(709-725)Online publication date: 4-Nov-2024
  • (2024)Quest Complete: The Holy Grail of Gradual SecurityProceedings of the ACM on Programming Languages10.1145/36564428:PLDI(1609-1632)Online publication date: 20-Jun-2024
  • (2023)Information Flow Tracking for Heterogeneous Compartmentalized SoftwareProceedings of the 26th International Symposium on Research in Attacks, Intrusions and Defenses10.1145/3607199.3607235(564-579)Online publication date: 16-Oct-2023
  • (2022)Solo: a lightweight static analysis for differential privacyProceedings of the ACM on Programming Languages10.1145/35633136:OOPSLA2(699-728)Online publication date: 31-Oct-2022
  • (2022)Modular information flow through ownershipProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523445(1-14)Online publication date: 9-Jun-2022
  • (2022)SecWasm: Information Flow Control for WebAssemblyStatic Analysis10.1007/978-3-031-22308-2_5(74-103)Online publication date: 2-Dec-2022
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media