skip to main content
10.1145/1411286.1411289acmconferencesArticle/Chapter ViewAbstractPublication PagesicfpConference Proceedingsconference-collections
research-article

A library for light-weight information-flow security in haskell

Published: 25 September 2008 Publication History

Abstract

Protecting confidentiality of data has become increasingly important for computing systems. Information-flow techniques have been developed over the years to achieve that purpose, leading to special-purpose languages that guarantee information-flow security in programs. However, rather than producing a new language from scratch, information-flow security can also be provided as a library. This has been done previously in Haskell using the arrow framework. In this paper, we show that arrows are not necessary to design such libraries and that a less general notion, namely monads, is sufficient to achieve the same goals. We present a monadic library to provide information-flow security for Haskell programs. The library introduces mechanisms to protect confidentiality of data for pure computations, that we then easily, and modularly, extend to include dealing with side-effects. We also present combinators to dynamically enforce different declassification policies when release of information is required in a controlled manner. It is possible to enforce policies related to what, by whom, and when information is released or a combination of them. The well-known concept of monads together with the light-weight characteristic of our approach makes the library suitable to build applications where confidentiality of data is an issue.

Supplementary Material

JPG File (1411289.jpg)
Audio only (1411289.mp3)
Video (1411289.mp4)

References

[1]
M. Abadi, A. Banerjee, N. Heintze, and J. Riecke. A core calculus of dependency. In Proc. ACM Symp. on Principles of Programming Languages, pages 147--160, January 1999.
[2]
A. Askarov and A. Sabelfeld. Localized delimited release: combining the what and where dimensions of information release. In PLAS '07: Proceedings of the 2007 workshop on Programming languages and analysis for security, pages 53--60, New York, NY, USA, 2007. ACM.
[3]
N. Broberg and D. Sands. Flow locks: Towards a core calculus for dynamic flow policies. In Peter Sestoft, editor, Proc. European Symp. on Programming, volume 3924 of Lecture Notes in Computer Science, pages 180--196. Springer, 2006.
[4]
S. Chong and A. C. Myers. Security policies for downgrading. In ACM Conference on Computer and Communications Security, pages 198--209, October 2004.
[5]
D. Clark, S. Hunt, and P. Malacaria. Quantitative analysis of the leakage of confidential data. In QAPL'01, Proc. Quantitative Aspects of Programming Languages, volume 59 of ENTCS. Elsevier, 2002.
[6]
E. S. Cohen. Information transmission in sequential programs. In R. A. DeMillo, D. P. Dobkin, A. K. Jones, and R. J. Lipton, editors, Foundations of Secure Computation, pages 297--335. Academic Press, 1978.
[7]
K. Crary, A. Kliger, and F. Pfenning. A monadic analysis of information flow security with mutable state, 2003.
[8]
D. E. Denning. A lattice model of secure information flow. Comm. of the ACM, 19(5):236--243, May 1976.
[9]
D. E. Denning and P. J. Denning. Certification of programs for secure information flow. Comm. of the ACM, 20(7):504--513, July 1977.
[10]
J. A. Goguen and J. Meseguer. Security policies and security models. In Proc. IEEE Symp. on Security and Privacy, pages 11--20, April 1982.
[11]
G. Le Guernic, A. Banerjee, T. Jensen, and D. Schmidt. Automata-based confidentiality monitoring. In Proc. Annual Asian Computing Science Conference, volume 4435 of LNCS, pages 75--89. Springer-Verlag, December 2006.
[12]
W. L. Harrison and J. Hook. Achieving information flow security through precise control of effects. In CSFW '05: Proceedings of the 18th IEEE workshop on Computer Security Foundations, pages 16--30,Washington, DC, USA, 2005. IEEE Computer Society.
[13]
N. Heintze and J. G. Riecke. The SLam calculus: programming with secrecy and integrity. In Proc. ACM Symp. on Principles of Programming Languages, pages 365--377, January 1998.
[14]
J. Hughes. Generalising monads to arrows. Science of Computer Programming, 37(1-3):67--111, 2000.
[15]
M. H. Jackson. Linux shadow password howto. Available at http://tldp.org/HOWTO/Shadow-Password-HOWTO.html, 1996.
[16]
J. R. Lewis, J. Launchbury, E. Meijer, and M. B. Shields. Implicit parameters: dynamic scoping with static types. In POPL '00: Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 108--118, New York, NY, USA, 2000. ACM.
[17]
P. Li and S. Zdancewic. Encoding Information Flow in Haskell. In CSFW '06: Proceedings of the 19th IEEE Workshop on Computer Security Foundations. IEEE Computer Society, 2006.
[18]
P. Li and S. Zdancewic. Arrows for secure information flow. Available at http://www.seas.upenn.edu/~lipeng/homepage/lz06tcs.pdf, 2007.
[19]
Local Root Exploit. Linux kernel 2.6 local root exploit. Available at http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=465246, February 2008.
[20]
H. Mantel and A. Reinhard. Controlling the what and where of declassification in language-based security. In Rocco De Nicola, editor, European Symposium on Programming (ESOP), volume 4421 of LNCS, pages 141--156. Springer, 2007. ISBN 978-3-540-71314-2.
[21]
A. C. Myers and B. Liskov. A decentralized model for information flow control. In Proc. ACM Symp. on Operating System Principles, pages 129--142, October 1997.
[22]
A. C. Myers and B. Liskov. Complete, safe information flow with decentralized labels. In Proc. IEEE Symp. on Security and Privacy, pages 186--197, May 1998.
[23]
A. C. Myers and B. Liskov. Protecting privacy using the decentralized label model. ACM Transactions on Software Engineering and Methodology, 9(4):410--442, 2000.
[24]
S. K. Nair, P. N. D. Simpson, B. Crispo, and A. S. Tanenbaum. A virtual machine based information flow control system for policy enforcement. The First International Workshop on Run Time Enforcement for Mobile and Distributed Systems (REM 2007), September 2007.
[25]
A. Narayanan and V. Shmatikov. Fast dictionary attacks on passwords using time-space tradeoff. In CCS '05: Proceedings of the 12th ACM conference on Computer and communications security, pages 364--372, New York, NY, USA, 2005. ACM.
[26]
B. C. Pierce. Advanced Topics In Types And Programming Languages. MIT Press, November 2004. ISBN 0262162288.
[27]
F. Pottier and V. Simonet. Information flow inference for ML. In Proc. ACM Symp. on Principles of Programming Languages, pages 319--330, January 2002.
[28]
A. Russo, K. Claessen, and J. Hughes. A library for light-weight information-flow security in Haskell. Software release and documentation. Available at http://www.cs.chalmers.se/~russo/seclib.htm, 2008a.
[29]
A. Russo, K. Claessen, and J. Hughes. A library for light-weight information-flow security in Haskell. Technical Report. Chalmers University of Technology. To appear., October 2008b.
[30]
A. Sabelfeld and A. C. Myers. A model for delimited information release. In Proc. International Symp. on Software Security (ISSS'03), volume 3233 of LNCS, pages 174--191. Springer-Verlag, October 2004.
[31]
A. Sabelfeld and D. Sands. Dimensions and principles of declassification. In CSFW '05: Proceedings of the 18th IEEE Computer Security Foundations Workshop (CSFW'05), pages 255--269. IEEE Computer Society, 2005.
[32]
P. Shroff, S. Smith, and M. Thober. Dynamic dependency monitoring to secure information flow. Computer Security Foundations Symposium, 2007. CSF '07. 20th IEEE, pages 203--217, 2007.
[33]
V. Simonet. Flow caml in a nutshell. In Graham Hutton, editor, Proceedings of the first APPSEM-II workshop, pages 152--165, March 2003.
[34]
A. S. Tanenbaum. Modern Operating Systems. Prentice Hall PTR, Upper Saddle River, NJ, USA, 2001. ISBN 0130313580.
[35]
T. C. Tsai, A. Russo, and J. Hughes. A library for secure multi-threaded information flow in Haskell. In Proc. of the 20th IEEE Computer Security Foundations Symposium, July 2007.
[36]
S. Tse and S. Zdancewic. Translating dependency into parametricity. In ICFP '04: Proceedings of the ninth ACM SIGPLAN international conference on Functional programming, pages 115--125, New York, NY, USA, 2004. ACM.
[37]
D. Volpano and G. Smith. A type-based approach to program security. In Proc. TAPSOFT'97, volume 1214 of LNCS, pages 607--621. Springer-Verlag, April 1997.
[38]
D. Volpano, G. Smith, and C. Irvine. A sound type system for secure flow analysis. J. Computer Security, 4(3):167--187, 1996.
[39]
P.Wadler. Monads for functional programming. In Marktoberdorf Summer School on Program Design Calculi, August 1992.

Cited By

View all
  • (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
  • (2021)Practical normalization by evaluation for EDSLsProceedings of the 14th ACM SIGPLAN International Symposium on Haskell10.1145/3471874.3472983(56-70)Online publication date: 18-Aug-2021
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
Haskell '08: Proceedings of the first ACM SIGPLAN symposium on Haskell
September 2008
134 pages
ISBN:9781605580647
DOI:10.1145/1411286
  • Program Chair:
  • Andy Gill
  • cover image ACM SIGPLAN Notices
    ACM SIGPLAN Notices  Volume 44, Issue 2
    HASKELL '08
    February 2009
    126 pages
    ISSN:0362-1340
    EISSN:1558-1160
    DOI:10.1145/1543134
    Issue’s Table of Contents
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 ACM 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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 September 2008

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. declassification
  2. information-flow
  3. library
  4. monad

Qualifiers

  • Research-article

Conference

ICFP08
Sponsor:

Acceptance Rates

Haskell '08 Paper Acceptance Rate 13 of 28 submissions, 46%;
Overall Acceptance Rate 57 of 143 submissions, 40%

Upcoming Conference

ICFP '25
ACM SIGPLAN International Conference on Functional Programming
October 12 - 18, 2025
Singapore , Singapore

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

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

Other Metrics

Citations

Cited By

View all
  • (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
  • (2021)Practical normalization by evaluation for EDSLsProceedings of the 14th ACM SIGPLAN International Symposium on Haskell10.1145/3471874.3472983(56-70)Online publication date: 18-Aug-2021
  • (2021)Scooter & Sidecar: a domain-specific approach to writing secure database migrationsProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454072(710-724)Online publication date: 19-Jun-2021
  • (2021)Giving semantics to program-counter labels via secure effectsProceedings of the ACM on Programming Languages10.1145/34343165:POPL(1-29)Online publication date: 4-Jan-2021
  • (2021)Mechanized logical relations for termination-insensitive noninterferenceProceedings of the ACM on Programming Languages10.1145/34342915:POPL(1-29)Online publication date: 4-Jan-2021
  • (2020)Liquid information flow controlProceedings of the ACM on Programming Languages10.1145/34089874:ICFP(1-30)Online publication date: 3-Aug-2020
  • (2020)A Programming Framework for Differential Privacy with Accuracy Concentration Bounds2020 IEEE Symposium on Security and Privacy (SP)10.1109/SP40000.2020.00086(411-428)Online publication date: May-2020
  • (2020)Securing Asynchronous Exceptions2020 IEEE 33rd Computer Security Foundations Symposium (CSF)10.1109/CSF49147.2020.00023(214-229)Online publication date: Jun-2020
  • (2019)LWeb: information flow security for multi-tier web applicationsProceedings of the ACM on Programming Languages10.1145/32903883:POPL(1-30)Online publication date: 2-Jan-2019
  • 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