skip to main content
research-article

Dependent Information Flow Types

Published: 14 January 2015 Publication History

Abstract

In this paper, we develop a novel notion of dependent information flow types. Dependent information flow types fit within the standard framework of dependent type theory, but, unlike usual dependent types, crucially allow the security level of a type, rather than just the structural data type itself, to depend on runtime values.
Our dependent function and dependent sum information flow types provide a direct, natural and elegant way to express and enforce fine grained security policies on programs, including programs that manipulate structured data types in which the security level of a structure field may depend on values dynamically stored in other fields, still considered a challenge to security enforcement in software systems such as data-centric web-based applications.
We base our development on the very general setting of a minimal lambda-calculus with references and collections. We illustrate its expressiveness, showing how secure operations on relevant scenarios can be modelled and analysed using our dependent information flow type system, which is also shown to be amenable to algorithmic type checking. Our main results include type-safety and non-interference theorems ensuring that well-typed programs do not violate prescribed security policies.

Supplementary Material

MPG File (p317-sidebyside.mpg)

References

[1]
M. Abadi, A. Banerjee, N. Heintze, and J. G. Riecke:. A Core Calculus of Dependency. In POPL 1999.
[2]
O. Arden, M. D. George, J. Liu, K. Vikram, A. Askarov, and A. C. Myers. Sharing mobile code securely with information flow control. In IEEE SSP 2012.
[3]
G. M. Bierman, A. D. Gordon, C. Hritcu, and D. E. Langworthy. Semantic Subtyping with an SMT Solver. J. Funct. Program., 2012.
[4]
A. Chlipala. Static Checking of Dynamically-Varying Security Policies in Database-Backed Applications. In USENIX OSDI 2010.
[5]
B. J. Corcoran, N. Swamy, and M. W. Hicks. Cross-tier, Label-based Security Enforcement for Web Applications. In ACM SIGMOD Int. Conf. on Management of Data, 2009.
[6]
B. Davis and H. Chen. DBTaint: Cross-Application Information Flow Tracking via Databases. In USENIX WebApps 2010.
[7]
L. M. de Moura and N. Bjørner. Z3: An efficient smt solver. In TACAS 2008.
[8]
D. E. Denning and P. J. Denning. Certification of Programs for Secure Information Flow. Comm. of the ACM, 1977.
[9]
W. Enck, P. Gilbert, B. Chun, L. P. Cox, J. Jung, P. M., and A. Sheth. TaintDroid: An Information-Flow Tracking System for Realtime Privacy Monitoring on Smartphones. In USENIX OSDI 2010.
[10]
J. A. Goguen and J. Meseguer. Security Policies and Security Models. In IEEE SSP 1982.
[11]
D. Hedin and A. Sabelfeld. Information-Flow Security for a Core of JavaScript. In IEEE CSF 2012.
[12]
N. Heintze and J. G. Riecke. The SLam Calculus: Programming with Secrecy and Integrity. In POPL 1998.
[13]
K. Honda, V. T. Vasconcelos, and N. Yoshida. Secure information flow as typed process behaviour. In ESOP 2000, LNCS.
[14]
C. Hritcu, M. Greenberg, B. Karel, B. C. Pierce, and G. Morrisett. All your ifcexception are belong to us. In IEEE SSP 2013.
[15]
P. Li and S. Zdancewic. Practical information-flow control in web-based information systems. In IEEE CSFW 2005.
[16]
J. Liu, M. D. George, K. Vikram, X. Qi, L. Waye, and A. C. Myers. Fabric: a platform for secure distributed computation and storage. In ACM SOSP 2009.
[17]
L. Lourenço and L. Caires. Information Flow Analysis for Valued-Indexed Data Security Compartments. In TGC 2013.
[18]
A. C. Myers. JFlow: Practical Mostly-Static Information Flow Control. In POPL 1999.
[19]
A. C. Myers and B. Liskov. A Decentralized Model for Information Flow Control. In ACM SOSP 1997.
[20]
A. Nanevski, A. Banerjee, and D. Garg. Verification of Information Flow and Access Control Policies with Dependent Types. In IEEE SSP 2011.
[21]
F. Pottier and V. Simonet. Information flow inference for ML. In POPL 2002.
[22]
A. Sabelfeld and A. C. Myers. Language-Based Information-Flow Security. IEEE JSAC, 21(1):5--19, Jan. 2003.
[23]
A. Sabelfeld and D. Sands. A Per Model of Secure Information Flow in Sequential Programs. Higher-Order and Symbolic Computation, 2001.
[24]
N. Swamy, B. J. Corcoran, and M. Hicks. Fable: A language for enforcing user-defined security policies. In IEEE SSP 2008.
[25]
N. Swamy, J. Chen, and R. Chugh. Enforcing Stateful Authorization and Information Flow Policies in Fine. In ESOP 2010.
[26]
N. Swamy, J. Chen, C. Fournet, P. Strub, K. Bhargavan, and J. Yang. Secure Distributed Programming with Value-dependent Types. In ICFP 2011.
[27]
S. Tse and S. Zdancewic. Run-time Principals in Information-flow Type Systems. ACM Trans. Program. Lang. Syst., 2007.
[28]
D. M. Volpano, C. E. Irvine, and G. Smith. A Sound Type System for Secure Flow Analysis. Journal of Computer Security, 1996.
[29]
H. Xi and F. Pfenning. Dependent Types in Practical Programming. In POPL 1999.
[30]
S. Zdancewic and A. C. Myers. Observational determinism for concurrent program security. In IEEE CSFW 2003.
[31]
N. Zeldovich, S. Boyd-Wickizer, and D. Mazières. Securing Distributed Systems with Information Flow Control. In USENIX NSDI 2008.
[32]
L. Zheng and A. C. Myers. Dynamic Security Labels and Static Information Flow Control. Int. J. Inf. Sec., 2007.
[33]
G. Barthe, C. Fournet, B. Grégoire, P. Strub, N. Swamy and S. Z. Béguelin. Probabilistic relational verification for cryptographic implementations. In POPL 2014.
[34]
L. Lourenço and L. Caires. Dependent Information Flow Types. Technical report, UNL, 2014.
[35]
DIFT Prototype. http://ctp.di.fct.unl.pt/DIFTprototype.

Cited By

View all
  • (2022)SNITCH: A Platform for Information Flow ControlIntegrated Formal Methods10.1007/978-3-031-07727-2_24(365-368)Online publication date: 1-Jun-2022
  • (2021)SecRSL: security separation logic for C11 release-acquire concurrencyProceedings of the ACM on Programming Languages10.1145/34854765:OOPSLA(1-26)Online publication date: 20-Oct-2021
  • (2021)Hybrid Information Flow Control for Low-Level CodeSoftware Engineering and Formal Methods10.1007/978-3-030-92124-8_9(141-159)Online publication date: 3-Dec-2021
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices
ACM SIGPLAN Notices  Volume 50, Issue 1
POPL '15
January 2015
682 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2775051
  • Editor:
  • Andy Gill
Issue’s Table of Contents
  • cover image ACM Conferences
    POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
    January 2015
    716 pages
    ISBN:9781450333009
    DOI:10.1145/2676726
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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2015
Published in SIGPLAN Volume 50, Issue 1

Check for updates

Author Tags

  1. dependent type systems
  2. information flow

Qualifiers

  • Research-article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

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

Other Metrics

Citations

Cited By

View all
  • (2022)SNITCH: A Platform for Information Flow ControlIntegrated Formal Methods10.1007/978-3-031-07727-2_24(365-368)Online publication date: 1-Jun-2022
  • (2021)SecRSL: security separation logic for C11 release-acquire concurrencyProceedings of the ACM on Programming Languages10.1145/34854765:OOPSLA(1-26)Online publication date: 20-Oct-2021
  • (2021)Hybrid Information Flow Control for Low-Level CodeSoftware Engineering and Formal Methods10.1007/978-3-030-92124-8_9(141-159)Online publication date: 3-Dec-2021
  • (2019)SNITCH: Dynamic Dependent Information Flow Analysis for Independent Java BytecodeElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.302.2302(16-31)Online publication date: 27-Aug-2019
  • (2019)Abstract Semantic DependencyStatic Analysis10.1007/978-3-030-32304-2_19(389-410)Online publication date: 2-Oct-2019
  • (2018)MAC A verified static information-flow control libraryJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2017.12.00395(148-180)Online publication date: Feb-2018
  • (2017)Hails: Protecting data privacy in untrusted web applicationsJournal of Computer Security10.3233/JCS-1580125:4-5(427-461)Online publication date: 10-Jul-2017
  • (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
  • (2024)Disjunctive Policies for Database-Backed Programs2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00017(388-402)Online publication date: 8-Jul-2024
  • (2024)Detecting Speculative Execution Vulnerabilities on Weak Memory ModelsFormal Methods10.1007/978-3-031-71162-6_25(482-500)Online publication date: 9-Sep-2024
  • 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