skip to main content
10.1145/2993600.2993603acmconferencesArticle/Chapter ViewAbstractPublication PagespldiConference Proceedingsconference-collections
research-article

Future-dependent Flow Policies with Prophetic Variables

Published: 24 October 2016 Publication History

Abstract

Content-dependency often plays an important role in the information flow security of real world IT systems. Content-dependency gives rise to informative policies and permissive static enforcement, and sometimes avoids the need for downgrading. We develop a static type system to soundly enforce future-dependent flow policies --- policies that can depend on not only the current values of variables, but also their final values. The final values are referred to using what we call prophetic variables, just as the initial values can be referenced using logical variables in Hoare logic. We develop and enforce a notion of future-dependent security for open systems, in the spirit of "non-deducibility on strategies". We also illustrate our approach in scenarios where future-dependency has advantages over present-dependency and avoids mixtures of upgradings and downgradings.

References

[1]
T. Amtoft, J. Dodds, Z. Zhang, A. W. Appel, L. Beringer, J. Hatcliff, X. Ou, and A. Cousino. A certificate infrastructure for machine-checked proofs of conditional information flow. In Principles of Security and Trust - First International Conference, POST 2012, pages 369--389, 2012.
[2]
T. Amtoft, J. Hatcliff, E. Rodrıguez, Robby, J. Hoag, and D. Greve. Specification and checking of software contracts for conditional information flow. In FM 2008: Formal Methods, 15th International Symposium on Formal Methods, pages 229--245, 2008.
[3]
N. Broberg and D. Sands. Flow locks: Towards a core calculus for dynamic flow policies. In Programming Languages and Systems, 15th European Symposium on Programming, ESOP 2006, pages 180--196, 2006.
[4]
N. Broberg and D. Sands. Paralocks: role-based information flow control and beyond. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pages 431--444, 2010.
[5]
S. Chong and A. C. Myers. Security policies for downgrading. In Proceedings of the 11th ACM Conference on Computer and Communications Security, CCS 2004, pages 198--209, 2004.
[6]
R. Dimitrova, B. Finkbeiner, M. Kovács, M. N. Rabe, and H. Seidl. Model checking information flow in reactive systems. In Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, pages 169--185, 2012.
[7]
J. A. Goguen and J. Meseguer. Security policies and security models. In IEEE Symposium on Security and Privacy, pages 11--20, 1982.
[8]
X. Li, F. Nielson, H. R. Nielson, and X. Feng. Disjunctive information flow for communicating processes. In Trustworthy Global Computing - 10th International Symposium, TGC 2015, Revised Selected Papers, pages 95--111, 2015.
[9]
L. Lourenço and L. Caires. Dependent information flow types. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, pages 317--328, 2015.
[10]
H. Mantel, D. Sands, and H. Sudbrock. Assumptions and guarantees for compositional noninterference. In Proceedings of the 24th IEEE Computer Security Foundations Symposium, CSF 2011, pages 218--232, 2011.
[11]
K. K. Micinski, J. Fetter-Degges, J. Jeon, J. S. Foster, and M. R. Clarkson. Checking interaction-based declassification policies for android using symbolic execution. In Computer Security - ESORICS 2015 - 20th European Symposium on Research in Computer Security, pages 520--538, 2015.
[12]
T. Murray, R. Sison, E. Pierzchalski, and C. Rizkallah. Compositional verification and refinement of concurrent value-dependent noninterference. In 29th IEEE Computer Security Foundations Symposium, CSF 2016, 2016.
[13]
A. C. Myers and B. Liskov. A decentralized model for information flow control. In Proceedings of the Sixteenth ACM Symposium on Operating System Principles, SOSP 1997, pages 129--142, 1997.
[14]
A. Nanevski, A. Banerjee, and D. Garg. Verification of information flow and access control policies with dependent types. In 32nd IEEE Symposium on Security and Privacy, S&P 2011, pages 165--179, 2011.
[15]
H. R. Nielson, F. Nielson, and X. Li. Hoare logic for disjunctive information flow. In Programming Languages with Applications to Biology and Security - Essays Dedicated to Pierpaolo Degano on the Occasion of His 65th Birthday, pages 47--65, 2015.
[16]
W. Rafnsson, D. Hedin, and A. Sabelfeld. Securing interactive programs. In 25th IEEE Computer Security Foundations Symposium, CSF 2012, pages 293--307, 2012.
[17]
A. Sabelfeld and H. Mantel. Securing communication in a concurrent language. In Static Analysis, 9th International Symposium, SAS 2002, pages 376--394, 2002.
[18]
A. Sabelfeld and A. C. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1):5--19, 2003.
[19]
A. Sabelfeld and A. C. Myers. A model for delimited information release. In Software Security - Theories and Systems, Second Mext-NSF-JSPS International Symposium, ISSS 2003, pages 174--191, 2003.
[20]
S. Tse and S. Zdancewic. Run-time principals in information-flow type systems. ACM Trans. Program. Lang. Syst., 30(1), 2007.
[21]
D. M. Volpano, G. Smith, and C. E. Irvine. A sound type system for secure flow analysis. Journal of Computer Security, 4(2/3):167--188, 1996.
[22]
J. T. Wittbold and D. M. Johnson. Information flow in nondeterministic systems. In Proceedings of the 1990 IEEE Symposium on Security and Privacy, pages 144--161, 1990.
[23]
S. Zdancewic and A. C. Myers. Robust declassification. In 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), page 15, 2001.
[24]
L. Zheng and A. C. Myers. Dynamic security labels and static information flow control. Int. J. Inf. Sec., 6(2--3):67--84, 2007.

Cited By

View all
  • (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
  • (2018)A Permission-Dependent Type System for Secure Information Flow Analysis2018 IEEE 31st Computer Security Foundations Symposium (CSF)10.1109/CSF.2018.00023(218-232)Online publication date: Jul-2018

Index Terms

  1. Future-dependent Flow Policies with Prophetic Variables

    Recommendations

    Comments

    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
    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: 24 October 2016

    Permissions

    Request permissions for this article.

    Check for updates

    Author Tags

    1. future-dependent policies
    2. information flow control
    3. prophetic variables
    4. security type systems

    Qualifiers

    • Research-article

    Conference

    CCS'16
    Sponsor:

    Acceptance Rates

    PLAS '16 Paper Acceptance Rate 6 of 11 submissions, 55%;
    Overall Acceptance Rate 43 of 77 submissions, 56%

    Contributors

    Other Metrics

    Bibliometrics & Citations

    Bibliometrics

    Article Metrics

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

    Other Metrics

    Citations

    Cited By

    View all
    • (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
    • (2018)A Permission-Dependent Type System for Secure Information Flow Analysis2018 IEEE 31st Computer Security Foundations Symposium (CSF)10.1109/CSF.2018.00023(218-232)Online publication date: Jul-2018

    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