Article

Secure multi-execution in haskell

Authors:

Mauro Jaskelioff,

Alejandro RussoAuthors Info & Claims

PSI'11: Proceedings of the 8th international conference on Perspectives of System Informatics

Pages 170 - 178

https://doi.org/10.1007/978-3-642-29709-0_16

Published: 27 June 2011 Publication History

Abstract

Language-based information-flow security has emerged as a promising technology to guarantee confidentiality in on-line systems, where enforcement mechanisms are typically presented as run-time monitors, code transformations, or type-systems. Recently, an alternative technique, called <em>secure multi-execution</em>, has been proposed. The main idea behind this novel approach consists on running a program multiple times, once for each security level, using special rules for I/O operations. Compared to run-time monitors and type-systems, secure multi-execution does not require to inspect the full code of the application (only its I/O actions). In this paper, we propose the core of a library to provide <em>non-interference</em> through secure-multi execution. We present the code of the library as well as a running example for Haskell. To the best of our knowledge, this paper is the first work to consider secure-multi execution in a functional setting and provide this technology as a library.

References

[1]

Andrews, M.: Guest Editor's Introduction: The State of Web Security. IEEE Security and Privacy 4(4), 14-15 (2006)

Digital Library

[2]

Chong, S., Liu, J., Myers, A.C., Qi, X., Vikram, K., Zheng, L., Zheng, X.: Secure web applications via automatic partitioning. In: Proc. ACM Symp. on Operating System Principles, pp. 31-44 (October 2007)

Digital Library

[3]

Cohen, E. S.: Information transmission in computational systems. ACM SIGOPS Operating Systems Review 11(5), 133-139 (1977)

Digital Library

[4]

Conti, J. J., Russo, A.: A taint mode for Python via a library. In: NordSec 2010. Selected paper by OWASP AppSec Research 2010 (2010)

Digital Library

[5]

Credit Research Foundation. Ratios and formulas in customer financial analysis (1999), http://www.crfonline.org/orc/cro/cro-16.html

[6]

Del Tedesco, F., Russo, A., Sands, D.: Implementing erasure policies using taint analysis. In: Aura, T. (ed.) The 15th Nordic Conf. in Secure IT Systems. Springer, Heidelberg (2010)

Digital Library

[7]

Devriese, D., Piessens, F.: Noninterference through secure multi-execution. In: Proc. of the 2010 IEEE Symposium on Security and Privacy, SP 2010, pp. 109-124. IEEE Computer Society, Washington, DC (2010)

Digital Library

[8]

Devriese, D., Piessens, F.: Information flow enforcement in monadic libraries. In: Proc. of the 7th ACM SIGPLAN Workshop on Types in Language Design and Implementation, TLDI 2011, pp. 59-72. ACM, New York (2011)

Digital Library

[9]

Federal Aviation Administration (US). Review of Web Applications Security and Intrusion Detection in Air Traffic Control Systems. Note: thousands of vulnerabilities were discovered (June 2009), http://www.oig.dot.gov/sites/dot/files/pdfdocs/ATC_Web_Report.pdf

[10]

Goguen, J. A., Meseguer, J.: Security policies and security models. In: Proc. IEEE Symp. on Security and Privacy, pp. 11-20 (April 1982)

[11]

Heintze, N., Riecke, J. G.: The SLam calculus: programming with secrecy and integrity. In: Proc. ACM Symp. on Principles of Programming Languages, pp. 365-377 (January 1998)

Digital Library

[12]

Jaskelioff, M.: Lifting of Operations in Modular Monadic Semantics. PhD thesis, University of Nottingham (2009)

[13]

Jaskelioff, M., Russo, A.: Secure multi-execution in Haskell. software release (2011), http://www.cse.chalmers.se/~russo/sme/

[14]

Li, P., Zdancewic, S.: Encoding Information Flow in Haskell. In: CSFW2006: Proc. of the 19th IEEE Workshop on Computer Security Foundations. IEEE Computer Society (2006)

Digital Library

[15]

Magazinius, J., Phung, P. H., Sands, D.: Safe wrappers and sane policies for self protecting JavaScript. In: Aura, T. (ed.) The 15th Nordic Conf. in Secure IT Systems. Springer, Heidelberg (2010)

Digital Library

[16]

Moggi, E.: An abstract view of programming languages. Technical Report ECS-LFCS-90- 113, Edinburgh University, Edinburgh, Scotland (1989)

[17]

Moggi, E.: Computational lambda-calculus and monads. In: Proc., Fourth Annual Symposium on Logic in Computer Science, pp. 14-23. IEEE Computer Society (1989)

Digital Library

[18]

Morgenstern, J., Licata, D. R.: Security-typed programming within dependently typed programming. In: Proc. of the 15th ACM SIGPLAN Int. Conf. on Funct. Prog., ICFP 2010, pp. 169-180. ACM, New York (2010)

Digital Library

[19]

Myers, A.C.: JFlow: Practical mostly-static information flow control. In: Proc. ACMSymp. on Principles of Programming Languages, pp. 228-241 (January 1999)

Digital Library

[20]

Myers, A.C., Zheng, L., Zdancewic, S., Chong, S., Nystrom, N.: Jif: Java information flow. Software release (July 2001), Located at http://www.cs.cornell.edu/jif

[21]

Peyton Jones, S., Gordon, A., Finne, S.: Concurrent haskell. In: POPL 1996: Proc. of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 295-308. ACM, New York (1996)

Digital Library

[22]

Peyton Jones, S. L., Wadler, P.: Imperative functional programming. In: Proc. of the ACM Conf. on Principles of Programming, pp. 71-84 (1993)

Digital Library

[23]

Phung, P. H., Sands, D., Chudnov, A.: Lightweight self-protecting javascript. In: Safavi-Naini, R., Varadharajan, V. (eds.) ACM Symposium on Information, Computer and Communications Security (ASIACCS 2009). ACM Press, Sydney (2009)

Digital Library

[24]

Pottier, F., Simonet, V.: Information flow inference for ML. In: Proc. ACM Symp. on Principles of Programming Languages, pp. 319-330 (January 2002)

Digital Library

[25]

Russo, A., Claessen, K., Hughes, J.: A library for light-weight information-flow security in Haskell. In: Haskell 2008: Proc. of the 1st ACM SIGPLAN Symp. on Haskell. ACM (2008)

Digital Library

[26]

Russo, A., Hughes, J., Naumann, J. D. A., Sabelfeld, A.: Closing Internal Timing Channels by Transformation. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 120-135. Springer, Heidelberg (2008)

Digital Library

[27]

Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Selected Areas in Communications 21(1), 5-19 (2003)

Digital Library

[28]

Sabelfeld, A., Sands, D.: Dimensions and principles of declassification. In: Proc. IEEE Computer Security Foundations Workshop, pp. 255-269 (June 2005)

Digital Library

[29]

Simonet, V.: Flow caml in a nutshell. In: Hutton, G. (ed.) Proc. of the First APPSEM-II Workshop, pp. 152-165 (March 2003)

[30]

Simonet, V.: The Flow Caml system. Software release (July 2003), http://cristal.inria.fr/~simonet/soft/flowcaml

[31]

Swierstra, W., Altenkirch, T.: Beauty in the beast. In: Proc. of the ACM SIGPLAN Workshop on Haskell, Haskell 2007, pp. 25-36. ACM, New York (2007)

Digital Library

[32]

Tsai, T.C., Russo, A., Hughes, J.: A library for secure multi-threaded information flow in Haskell. In: Proc. of the 20th IEEE Computer Security Foundations Symposium (July 2007)

Digital Library

[33]

Zdancewic, S.: Programming Languages for Information Security. PhD thesis, Cornell University (July 2002)

Digital Library

[34]

Zdancewic, S., Zheng, L., Nystrom, N., Myers, A.C.: Untrusted hosts and confidentiality: Secure program partitioning. In: Proc. ACM Symp. on Operating System Principles (2001)

Digital Library

Cited By

Chakraborty DHammer CBugiel SHung CPapadopoulos G(2019)Secure multi-execution in AndroidProceedings of the 34th ACM/SIGAPP Symposium on Applied Computing10.1145/3297280.3297469(1934-1943)Online publication date: 8-Apr-2019
https://dl.acm.org/doi/10.1145/3297280.3297469
Vassena MRusso AGarg DRajani VStefan D(2019)From fine- to coarse-grained dynamic information flow control and backProceedings of the ACM on Programming Languages10.1145/32903893:POPL(1-31)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290389
Schmitz TAlgehed MFlanagan CRusso ALie DMannan MBackes MWang X(2018)Faceted Secure Multi ExecutionProceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security10.1145/3243734.3243806(1617-1634)Online publication date: 15-Oct-2018
https://dl.acm.org/doi/10.1145/3243734.3243806
Show More Cited By

Recommendations

Secure Multi-execution: Fine-Grained, Declassification-Aware, and Transparent
CSF '13: Proceedings of the 2013 IEEE 26th Computer Security Foundations Symposium

Recently, much progress has been made on achieving information-flow security via secure multi-execution. Secure multi-execution (SME) is an elegant way to enforce security by executing a given program multiple times, once for each security level, while ...
A Library for Secure Multi-threaded Information Flow in Haskell
CSF '07: Proceedings of the 20th IEEE Computer Security Foundations Symposium

Li and Zdancewic have recently proposed an approach to provide information-flow security via a library rather than producing a new language from the scratch. They have shown how to implement such a library in Haskell by using arrow combinators. However, ...
Faceted Secure Multi Execution
CCS '18: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security

To enforce non-interference, both Secure Multi-Execution (SME) and Multiple Facets (MF) rely on the introduction of multi-executions. The attractiveness of these techniques is that they are precise: secure programs running under SME or MF do not change ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

PSI'11: Proceedings of the 8th international conference on Perspectives of System Informatics

June 2011

410 pages

ISBN:9783642297083

Editors:
Edmund Clarke
Computer Science Department, Carnegie Mellon University, 5000 Forbes Avenue, Pittsburgh, PA
,
Irina Virbitskaite
Computer Science Department, A.P. Ershov Institute of Informatics Systems Siberian Branch of the Russian Academy of Sciences, 6, Acad. Lavrentiev ave, 630090, PA, Russia
,
Andrei Voronkov
Computer Science Department, The University of Manchester, Oxford Road, Manchester, PA, UK

Sponsors

PlanetData: PlanetData
Google Inc.
Intel: Intel
RFBR: Russian Foundation for Basic Research
SESAME-S: SESAME-S

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 27 June 2011

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

16
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 27 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Chakraborty DHammer CBugiel SHung CPapadopoulos G(2019)Secure multi-execution in AndroidProceedings of the 34th ACM/SIGAPP Symposium on Applied Computing10.1145/3297280.3297469(1934-1943)Online publication date: 8-Apr-2019
https://dl.acm.org/doi/10.1145/3297280.3297469
Vassena MRusso AGarg DRajani VStefan D(2019)From fine- to coarse-grained dynamic information flow control and backProceedings of the ACM on Programming Languages10.1145/32903893:POPL(1-31)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290389
Schmitz TAlgehed MFlanagan CRusso ALie DMannan MBackes MWang X(2018)Faceted Secure Multi ExecutionProceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security10.1145/3243734.3243806(1617-1634)Online publication date: 15-Oct-2018
https://dl.acm.org/doi/10.1145/3243734.3243806
Ngo MBielova NFlanagan CRezk TRusso ASchmitz TChampin PGandon FMédini LLalmas MIpeirotis P(2018)A Better Facet of Dynamic Information Flow ControlCompanion Proceedings of the The Web Conference 201810.1145/3184558.3185979(731-739)Online publication date: 23-Apr-2018
https://dl.acm.org/doi/10.1145/3184558.3185979
Schmitz TRhodes DAustin TKnowles KFlanagan C(2016)Faceted Dynamic Information Flow via Control and Data MonadsProceedings of the 5th International Conference on Principles of Security and Trust - Volume 963510.5555/3089491.3089493(3-23)Online publication date: 2-Apr-2016
https://dl.acm.org/doi/10.5555/3089491.3089493
Vassena MRusso AMurray TStefan D(2016)On Formalizing Information-Flow Control LibrariesProceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security10.1145/2993600.2993608(15-28)Online publication date: 24-Oct-2016
https://dl.acm.org/doi/10.1145/2993600.2993608
Buiras PVytiniotis DRusso A(2015)HLIO: mixing static and dynamic typing for information-flow control in HaskellACM SIGPLAN Notices10.1145/2858949.278475850:9(289-301)Online publication date: 29-Aug-2015
https://dl.acm.org/doi/10.1145/2858949.2784758
Buiras PVytiniotis DRusso AFisher KReppy J(2015)HLIO: mixing static and dynamic typing for information-flow control in HaskellProceedings of the 20th ACM SIGPLAN International Conference on Functional Programming10.1145/2784731.2784758(289-301)Online publication date: 29-Aug-2015
https://dl.acm.org/doi/10.1145/2784731.2784758
Zanarini DJaskelioff MRusso ATripp O(2014)Monitoring Reactive Systems with Dynamic ChannelsProceedings of the Ninth Workshop on Programming Languages and Analysis for Security10.1145/2637113.2637120(66-78)Online publication date: 28-Jul-2014
https://dl.acm.org/doi/10.1145/2637113.2637120
Hassan DSabry ALazarus RKfoury ABeal J(2013)Encoding secure information flow with restricted delegation and revocation in HaskellProceedings of the 1st annual workshop on Functional programming concepts in domain-specific languages10.1145/2505351.2505354(11-18)Online publication date: 22-Sep-2013
https://dl.acm.org/doi/10.1145/2505351.2505354
Show More Cited By

View Options

View options

Figures

Tables

Media

View Table of Conten