skip to main content
10.1145/2676726.2676994acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
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
  • (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
  • (2023)Data-Dependent Confidentiality in DCR GraphsProceedings of the 25th International Symposium on Principles and Practice of Declarative Programming10.1145/3610612.3610619(1-13)Online publication date: 22-Oct-2023
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

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
  • 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
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

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2015

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. dependent type systems
  2. information flow

Qualifiers

  • Research-article

Conference

POPL '15
Sponsor:

Acceptance Rates

POPL '15 Paper Acceptance Rate 52 of 227 submissions, 23%;
Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

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

Other Metrics

Citations

Cited By

View all
  • (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
  • (2023)Data-Dependent Confidentiality in DCR GraphsProceedings of the 25th International Symposium on Principles and Practice of Declarative Programming10.1145/3610612.3610619(1-13)Online publication date: 22-Oct-2023
  • (2023)CAD for Information Leakage AssessmentCAD for Hardware Security10.1007/978-3-031-26896-0_4(81-102)Online publication date: 28-Jan-2023
  • (2022)Compositional noninterference on hardware weak memory modelsScience of Computer Programming10.1016/j.scico.2022.102779217:COnline publication date: 1-May-2022
  • (2022)A Dependent Dependency CalculusProgramming Languages and Systems10.1007/978-3-030-99336-8_15(403-430)Online publication date: 5-Apr-2022
  • (2021)A permission-dependent type system for secure information flow analysisJournal of Computer Security10.3233/JCS-200036(1-68)Online publication date: 17-Feb-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
  • (2021)Compositional Non-Interference for Fine-Grained Concurrent Programs2021 IEEE Symposium on Security and Privacy (SP)10.1109/SP40001.2021.00003(1416-1433)Online publication date: May-2021
  • (2021)Information-flow control on ARM and POWER multicore processorsFormal Methods in System Design10.1007/s10703-021-00376-258:1-2(251-293)Online publication date: 8-Jun-2021
  • 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