research-article

On Formalizing Information-Flow Control Libraries

Authors:

Alejandro RussoAuthors Info & Claims

PLAS '16: Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security

Pages 15 - 28

https://doi.org/10.1145/2993600.2993608

Published: 24 October 2016 Publication History

Abstract

Many state-of-the-art IFC libraries support a variety of advanced features like mutuable data structures, exceptions, and concurrency, whose subtle interaction makes verification of security guarantees challenging. In this paper, we present a full-fledged, mechanically-verified model of MAC---a statically enforced IFC library. We describe three main insights gained during the formalization process. As previous libraries (e.g., LIO and HLIO), we utilize term erasure as the proof technique to show non-interference. This technique essentially states that the same public output should be produced if secrets are erased before or after program execution. Our first insight identifies challenges when the sensitivity of terms may depend on the context where they are used, thus affecting how they will be erased. This situation is not uncommon in MAC as well as other IFC libraries---in fact, we spot problems in the proofs of previous work. To deal with such complicated situations, we propose a novel erasure technique that performs erasure by additional evaluation rules, triggered by special-purpose constructs. Furthermore, we simplify reasoning about exception-aware primitives by removing sensitive exceptions from programs where secrets have been erased. We show progress insensitive non-interference for our sequential calculus and pinpoint sufficient requirements on the scheduler to prove progress-sensitive non-interference for our concurrent calculus. We prove that MAC is secure under a round-robin scheduler by simply instantiating our main scheduler-parametric theorem.

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.

Digital Library

[2]

Anindya Banerjee and David A. Naumann. Secure information flow and pointer confinement in a java-like language. In Proceedings of the 15th IEEE Workshop on Computer Security Foundations, CSFW '02. IEEE Computer Society, 2002.

Digital Library

[3]

G. Barthe, T. Rezk, A. Russo, and A. Sabelfeld. Security of multithreaded programs by compilation. Special issue of ACM Transactions on Information and System Security (TISSEC), August 2009.

Digital Library

[4]

David E. Bell and L. La Padula. Secure computer system: Unified exposition and multics interpretation. Technical Report MTR-2997, Rev. 1, MITRE Corporation, Bedford, MA, 1976.

[5]

K. J. Biba. Integrity considerations for secure computer systems. ESD-TR-76--372, 1977.

[6]

Abhishek Bichhawat, Vineet Rajani, Deepak Garg, and Christian Hammer. Information Flow Control in WebKit's JavaScript Bytecode, pages 159--178. Springer Berlin Heidelberg, Berlin, Heidelberg, 2014. ISBN 978--3--642--54792--8. 10.1007/978--3--642--54792--8_9. URL http://dx.doi.org/10.1007/978--3--642--54792--8_9.

[7]

P. Buiras, D. Vytiniotis, and A. Russo. HLIO: Mixing static and dynamic typing for information-flow control in Haskell. In Proc. of the ACM SIGPLAN International Conference on Functional Programming (ICFP '15). ACM, 2015.

Digital Library

[8]

Pablo Buiras, Deian Stefan, and Alejandro Russo. On dynamic flow-sensitive floating-label systems. In Proc. of the IEEE Computer Security Foundations Symposium, CSF '14. IEEE Computer Society, 2014.

Digital Library

[9]

D. Devriese and F. Piessens. Information flow enforcement in monadic libraries. In Proc. of the ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI '11). ACM, 2011.

Digital Library

[10]

Petros Efstathopoulos, Maxwell Krohn, Steve VanDeBogart, Cliff Frey, David Ziegler, Eddie Kohler, David Mazières, Frans Kaashoek, and Robert Morris. Labels and event processes in the asbestos operating system. In phProc. of the twentieth ACM symp. on Operating systems principles, SOSP '05. ACM, 2005.

Digital Library

[11]

s, Mitchell, and Russo}Giffin:2012Daniel B. Giffin, Amit Levy, Deian Stefan, David Terei, David Mazières, John C. Mitchell, and Alejandro Russo. Hails: Protecting data privacy in untrusted web applications. In Proceedings of the 10th USENIX Conference on Operating Systems Design and Implementation, OSDI'12. USENIX Association, 2012.

Digital Library

[12]

J. A. Goguen and J. Meseguer. Unwinding and inference control. In Security and Privacy, 1984 IEEE Symposium on, April 1984.

[13]

J.A. Goguen and J. Meseguer. Security policies and security models. In Proc of IEEE Symposium on Security and Privacy. IEEE Computer Society, 1982.

[14]

Stefan Heule, Deian Stefan, Edward Z. Yang, John C. Mitchell, and Alejandro Russo. IFC inside: Retrofitting languages with dynamic information flow control. In Conference on Principles of Security and Trust (POST). Springer, April 2015.

Digital Library

[15]

Kohei Honda and Nobuko Yoshida. A uniform type structure for secure information flow. ACM Trans. Program. Lang. Syst., October 2007.

Digital Library

[16]

Kohei Honda, Vasco Thudichum Vasconcelos, and Nobuko Yoshida. Secure Information Flow as Typed Process Behaviour. In Proc. of the 9th European Symposium on Programming Languages and Systems. Springer-Verlag, 2000.

Digital Library

[17]

C. Hritcu, M. Greenberg, B. Karel, B. C. Peirce, and G. Morrisett. All your IFCexception are belong to us. In Proc. of the IEEE Symposium on Security and Privacy. IEEE Computer Society, 2013.

Digital Library

[18]

M. Jaskelioff and A. Russo. Secure multi-execution in Haskell. In Proc. Andrei Ershov International Conference on Perspectives of System Informatics, LNCS. Springer-Verlag, June 2011.

Digital Library

[19]

Naoki Kobayashi. Type-based information flow analysis for the π-calculus. Acta Inf., 42 (4), December 2005.

Digital Library

[20]

Maxwell Krohn, Alexander Yip, Micah Brodsky, Natan Cliffer, M. Frans Kaashoek, Eddie Kohler, and Robert Morris. Information flow control for standard os abstractions. In Proceedings of ACM SIGOPS Symposium on Operating Systems Principles, SOSP '07. ACM, 2007.

Digital Library

[21]

P. Li and S. Zdancewic. Encoding information flow in Haskell. In Proc. of the IEEE Workshop on Computer Security Foundations (CSFW '06). IEEE Computer Society, 2006.

Digital Library

[22]

P. Li and S. Zdancewic. Arrows for secure information flow. Theoretical Computer Science, 411 (19): 1974--1994, 2010.

Digital Library

[23]

Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao, and Gerwin Klein. sel4: From general purpose to a proof of information flow enforcement. 2012 IEEE Symposium on Security and Privacy, 0, 2013.

Digital Library

[24]

François Pottier. A Simple View of Type-Secure Information Flow in the π-Calculus. In In Proc. of the 15th IEEE Computer Security Foundations Workshop, pages 320--330, 2002.

Digital Library

[25]

A. Russo and A. Sabelfeld. Securing Interaction between Threads and the Scheduler. In Proc. IEEE Computer Sec. Foundations Workshop, pages 177--189, July 2006.

Digital Library

[26]

A. Russo, K. Claessen, and J. Hughes. A library for light-weight information-flow security in Haskell. In Proc. ACM SIGPLAN symposium on Haskell (HASKELL '08). ACM, September 2008.

Digital Library

[27]

Alejandro Russo. Functional Pearl: Two Can Keep a Secret, if One of Them Uses Haskell. In Proc. of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015. ACM, 2015.

Digital Library

[28]

Thomas Schmitz, Dustin Rhodes, Thomas H. Austin, Kenneth Knowles, and Cormac Flanagan. Faceted dynamic information flow via control and data monads. In Frank Piessens and Luca Viganò, editors, POST, volume 9635 of phLecture Notes in Computer Science. Springer, 2016.

[29]

G. Smith and D. Volpano. Secure information flow in a multi-threaded imperative language. In phProc. ACM symposium on Principles of Programming Languages (POPL '98), 1998.

Digital Library

[30]

D. Stefan, A. Russo, P. Buiras, A. Levy, J. C. Mitchell, and D. Maziéres. Addressing covert termination and timing channels in concurrent information flow systems. In Proc. of the ACM SIGPLAN International Conference on Functional Programming (ICFP '12). ACM, 2012.

Digital Library

[31]

D. Stefan, A. Russo, J. C. Mitchell, and D. Mazières. Flexible dynamic information flow control in the presence of exceptions. Arxiv preprint arXiv:1207.1457, to appear in Journal of Functional Programming, Cambridge University Press, 2012.

[32]

Deian Stefan, Alejandro Russo, John C. Mitchell, and David Mazières. Flexible Dynamic Information Flow Control in Haskell. In Proceedings of the 4th ACM symposium on Haskell, pages 95--106, New York, NY, USA, 2011. ACM.

Digital Library

[33]

T. C. Tsai, A. Russo, and J. Hughes. A library for secure multi-threaded information flow in Haskell. In Proc. IEEE Computer Security Foundations Symposium (CSF '07), July 2007.

Digital Library

[34]

Marco Vassena, Pablo Buiras, Lucas Waye, and Alejandro Russo. Flexible manipulation of labeled values for information-flow control libraries. In Proceedings of the 12th European Symposium On Research In Computer Security. Springer, September 2016.

[35]

Nickolai Zeldovich, Silas Boyd-Wickizer, Eddie Kohler, and David Mazières. Making information flow explicit in HiStar. In Proc. of the 7th USENIX Symp. on Operating Systems Design and Implementation. USENIX, 2006.

Digital Library

Cited By

Cortinas CVassena MRusso A(2020)Securing Asynchronous Exceptions2020 IEEE 33rd Computer Security Foundations Symposium (CSF)10.1109/CSF49147.2020.00023(214-229)Online publication date: Jun-2020
https://doi.org/10.1109/CSF49147.2020.00023
Algehed MBernardy J(2019)Simple noninterference from parametricityProceedings of the ACM on Programming Languages10.1145/33416933:ICFP(1-22)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341693
Tomé Cortiñas CValliappan NMardziel PVazou N(2019)Simple Noninterference by NormalizationProceedings of the 14th ACM SIGSAC Workshop on Programming Languages and Analysis for Security10.1145/3338504.3357342(61-72)Online publication date: 15-Nov-2019
https://dl.acm.org/doi/10.1145/3338504.3357342
Show More Cited By

Index Terms

On Formalizing Information-Flow Control Libraries
1. Security and privacy
  1. Systems security
    1. Information flow control
2. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Functional languages
  2. Software organization and properties
    1. Software functional properties
      1. Correctness

Recommendations

Cryptographically sound implementations for typed information-flow security
POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

In language-based security, confidentiality and integrity policies conveniently specify the permitted flows of information between different parts of a program with diverse levels of trust. These policies enable a simple treatment of security, and they ...
Information-flow types for homomorphic encryptions
CCS '11: Proceedings of the 18th ACM conference on Computer and communications security

We develop a flexible information-flow type system for a range of encryption primitives, precisely reflecting their diverse functional and security features. Our rules enable encryption, blinding, homomorphic computation, and decryption, with selective ...
Cryptographically sound implementations for typed information-flow security
POPL '08

In language-based security, confidentiality and integrity policies conveniently specify the permitted flows of information between different parts of a program with diverse levels of trust. These policies enable a simple treatment of security, and they ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLAS '16: Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security

October 2016

116 pages

ISBN:9781450345743

DOI:10.1145/2993600

Program Chairs:
Toby Murray
University of Melbourne and Data61
,
Deian Stefan
UC San Diego and Intrinsic

Copyright © 2016 ACM.

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].

Sponsors

SIGSAC: ACM Special Interest Group on Security, Audit, and Control

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 24 October 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Vetenskapsrådet (VR)

Conference

CCS'16

Sponsor:

SIGSAC

CCS'16: 2016 ACM SIGSAC Conference on Computer and Communications Security

October 24, 2016

Vienna, Austria

Acceptance Rates

PLAS '16 Paper Acceptance Rate 6 of 11 submissions, 55%;

Overall Acceptance Rate 43 of 77 submissions, 56%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
139
Total Downloads

Downloads (Last 12 months)8
Downloads (Last 6 weeks)1

Reflects downloads up to 23 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Cortinas CVassena MRusso A(2020)Securing Asynchronous Exceptions2020 IEEE 33rd Computer Security Foundations Symposium (CSF)10.1109/CSF49147.2020.00023(214-229)Online publication date: Jun-2020
https://doi.org/10.1109/CSF49147.2020.00023
Algehed MBernardy J(2019)Simple noninterference from parametricityProceedings of the ACM on Programming Languages10.1145/33416933:ICFP(1-22)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341693
Tomé Cortiñas CValliappan NMardziel PVazou N(2019)Simple Noninterference by NormalizationProceedings of the 14th ACM SIGSAC Workshop on Programming Languages and Analysis for Security10.1145/3338504.3357342(61-72)Online publication date: 15-Nov-2019
https://dl.acm.org/doi/10.1145/3338504.3357342
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
Parker JVazou NHicks M(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
https://dl.acm.org/doi/10.1145/3290388
Gregersen SThomsen SAskarov A(2019)A Dependently Typed Library for Static Information-Flow Control in IdrisUrbanization and Its Impact in Contemporary China10.1007/978-3-030-17138-4_3(51-75)Online publication date: 3-Apr-2019
https://doi.org/10.1007/978-3-030-17138-4_3
Vassena MSoeller GAmidon PChan MRenner JStefan D(2019)Foundations for Parallel Information Flow Control Runtime SystemsUrbanization and Its Impact in Contemporary China10.1007/978-3-030-17138-4_1(1-28)Online publication date: 3-Apr-2019
https://doi.org/10.1007/978-3-030-17138-4_1
Vassena MBreitner JRusso A(2017)Securing Concurrent Lazy Programs Against Information Leakage2017 IEEE 30th Computer Security Foundations Symposium (CSF)10.1109/CSF.2017.39(37-52)Online publication date: Aug-2017
https://doi.org/10.1109/CSF.2017.39

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents