article

Open access

Run-time principals in information-flow type systems

Authors:

Steve ZdancewicAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 30, Issue 1

Pages 6 - es

https://doi.org/10.1145/1290520.1290526

Published: 01 November 2007 Publication History

Abstract

Information-flow type systems are a promising approach for enforcing strong end-to-end confidentiality and integrity policies. Such policies, however, are usually specified in terms of static information—data is labeled high or low security at compile time. In practice, the confidentiality of data may depend on information available only while the system is running.

This article studies language support for run-time principals, a mechanism for specifying security policies that depend on which principals interact with the system. We establish the basic property of noninterference for programs written in such language, and use run-time principals for specifying run-time authority in downgrading mechanisms such as declassification.

In addition to allowing more expressive security policies, run-time principals enable the integration of language-based security mechanisms with other existing approaches such as Java stack inspection and public key infrastructures. We sketch an implementation of run-time principals via public keys such that principal delegation is verified by certificate chains.

References

[1]

Abadi, M. 1998. On SDSI's linked local name spaces. J. Comput. Secur. 6, 1-2, 3--21.

Digital Library

[2]

Abadi, M., Banerjee, A., Heintze, N., and Riecke, J. 1999. A core calculus of dependency. In Proceedings of the 26th ACM Symposium on Principles of Programming Languages (POPL) (San Antonio, TX), ACM, New York, 147--160.

Digital Library

[3]

Abadi, M., Burrows, M., Lampson, B. W., and Plotkin, G. D. 1993. A calculus for access control in distributed systems. ACM Trans. Prog. Lang. Syst. 15, 4 (Sept.), 706--734.

Digital Library

[4]

Agat, J. 2000. Transforming out timing leaks. In Proceedings of the 27th Annual ACM Symposium on Principles of Programming Languages (POPL) (Boston, MA). ACM, New York, 40--53.

Digital Library

[5]

Aspinall, D. 1994. Subtyping with singleton types. Comput. Sci. Logic. 1--15.

Digital Library

[6]

Banerjee, A. and Naumann, D. A. 2002. Secure information flow and pointer confinement in a java-like language. In Proceedings of the 15th IEEE Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos, CA. 253--267.

Digital Library

[7]

Banerjee, A. and Naumann, D. A. 2003. Using access control for secure information flow in a Java-like language. In Proceedings of the 16th IEEE Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos, CA. 155--169.

[8]

Chothia, T., Duggan, D., and Vitek, J. 2003. Type-based distributed access control. In Proceedings of the IEEE Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos, CA. 170.

[9]

Crary, K., Kliger, A., and Pfenning, F. 2004. A monadic analysis of information flow security with mutable sate. J. Funct. Prog. 15, 2 (Mar.), 249--291.

Digital Library

[10]

Crary, K., Walker, D., and Morrisett, G. 1999. Typed memory management in a calculus of capabilities. In Proceedings of the 26th ACM Symposium on Principles of Programming Languages (POPL) (San Antonio, TX). ACM, New York, 262--275.

Digital Library

[11]

Crary, K., Weirich, S., and Morrisett, G. 2002. Intensional polymorphism in type erasure semantics. J. Funct. Prog. 12, 6 (Nov.), 567--600.

Digital Library

[12]

Fournet, C. and Gordon, A. 2002. Stack inspection: Theory and variants. In Proceedings of the 29th ACM Symposium on Principles of Programming Languages (POPL). ACM, New York, 307--318.

Digital Library

[13]

Gasser, M. and McDermott, E. 1990. An architecture for practical delegation in a distributed system. In Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society Press, Los Alamitos, CA, 20--30.

[14]

Goguen, J. A. and Meseguer, J. 1982. Security policies and security models. In Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society Press, Los Alamitos, CA, 11--20.

[15]

Gunter, C. A. and Jim, T. 2000. Generalized certificate revocation. In Procedings of the 27th ACM Symposium on Principles of Programming Languages (POPL) (Boston, MA). ACM, New York, 316--329.

Digital Library

[16]

Heintze, N. and Riecke, J. G. 1998. The SLam calculus: Programming with secrecy and integrity. In Proceedings of the 25th ACM Symposium on Principles of Programming Languages (POPL). (San Diego, CA). ACM, New York, 365--377.

Digital Library

[17]

Howell, J. and Kotz, D. 2000. End-to-end authorization. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI). 151--164.

Digital Library

[18]

Jim, T. 2001. SD3: A trust management system with certificate revocation. In Proceedings of the IEEE Symposium on Security and Privacy. IEEE Computer Society Press, Los Alamitos, CA, 106--115.

Digital Library

[19]

Jouvelot, P., and Gifford, D. K. 1991. Algebraic reconstruction of types and effects. In Proceedings of the ACM Symposium on Principles of Programming Languages. ACM, New York, 303--310.

Digital Library

[20]

Li, P., Mao, Y., and Zdancewic, S. 2003. Information integrity policies. In Proceedings of the Workshop on Formal Aspects in Security & Trust (FAST). 53--70.

[21]

Mitchell, J. C. 1996. Foundations for Programming Languages. Foundations of Computing Series. The MIT Press, Cambridge, MA.

Digital Library

[22]

Myers, A. C., Chong, S., Nystrom, N., Zheng, L., and Zdancewic, S. 1999. Jif: Java information flow. http://www.cs.cothell.edu/sit.

[23]

Myers, A. C. and Liskov, B. 1998. Complete, safe information flow with decentralized labels. In Proceedings of the IEEE Symposium on Security and Privacy (Oakland, CA). 186--197.

[24]

Myers, A. C. and Liskov, B. 2000. Protecting privacy using the decentralized label model. ACM Trans. Softw. Eng. Meth. 9, 4, 410--442.

Digital Library

[25]

Myers, A. C., Sabelfeld, A., and, Zdancewic, S. 2004. Enforcing robust declassification. In Proceedings of the IEEE Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos, CA, 172--186.

[26]

Myers, A. C., Sabelfeld, A., and Zdancewic, S. 2006. Enforcing robust declassification and qualified robustness. J. Comput. Secur. 14, 2, 157--196.

Digital Library

[27]

Pierce, B. C. 2002. Types and Programming Languages. MIT Press, Cambridge, MA.

Digital Library

[28]

Pitts, A. 1998. Existential types: Logical relations and operational equivalence. In Proceedings of the International Colloquium on Automata, Languages and Programming. 309--326.

Digital Library

[29]

Pottier, F. and Conchon, S. 2000. Information flow inference for free. In Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming (ICFP). ACM, New York, 46--57.

Digital Library

[30]

Pottier, F. and Simonet, V. 2002. Information flow inference for ML. In Proceedings of the 29th ACM Symposium on Principles of Programming Languages (POPL) (Portland, Oregon). ACM, New York, 319--330.

Digital Library

[31]

Pottier, F., Skalka, C., and Smith, S. F. 2001. A systematic approach to static access control. In Proceedings of the European Symposium on Programming. 344--382.

Digital Library

[32]

Sabelfeld, A. and Myers, A. C. 2003. Language-based information-flow security. IEEE J. Sel. Areas Commun. 21, 1 (Jan.), 5--19.

Digital Library

[33]

Sabelfeld, A. and Sands, D. 2001. A PER model of secure information flow in sequential programs. Higher-Order Symb. Comput. 14, 1 (Mar.), 59--91.

Digital Library

[34]

Simonet, V. 2003. Flow caml in a nutshell. In Proceedings of the 1st APPSEM-II Workshop, G. Hutton, Ed. 152--165.

[35]

Simonet, V. and Pottier, F. 2007. Constraint-based type inference with guarded algebraic data types. ACM Trans. Prog. Lang. Syst. 29,1.

Digital Library

[36]

Tse, S. and Zdancewic, S. 2004. Run-time principals in information-flow type systems. In Proceedings of the IEEE Symposium on Security and Privacy.

[37]

Tse, S. and Zdancewic, S. 2005. Designing a security-typed language with certificate-based declassification. In Proceedings of the European Symposium on Programming.

Digital Library

[38]

Volpano, D., Smith, G., and Irvine, C. 1996. A sound type system for secure flow analysis. J. Comput. Sec. 4, 3, 167--187.

Digital Library

[39]

Wadler, P. 1989. Theorems for free&excl; In Proceedings of the ACM Symposium on Functional Programming Languages and Computer Architecture. ACM, New York, 347--359.

Digital Library

[40]

Wallach, D. S., Appel, A. W., and Felten, E. W. 2000. The security architecture formerly known as stack inspection: A security mechanism for language-based systems. ACM Trans. Softw. Eng. Method. 9, 4 (Oct.), 341--378.

Digital Library

[41]

Wallach, D. S. and Felten, E. W. 1998. Understanding Java stack inspection. In Proceedings of the IEEE Symposium on Security and Privacy (Oakland, CA). ACM, New York, 52--63.

[42]

Zdancewic, S. 2003. A type system for robust declassification. In Proceedings of the 19th Conference on the Mathematical Foundations of Programming Semantics. Electronic Notes in Theoretical Computer Science.

Digital Library

[43]

Zdancewic, S. and Myers, A. C. 2001. Secure information flow and CPS. In Proceedings of the 10th European Symposium on Programming. Lecture Notes in Computer Science, vol. 2028. Springer Verlag, New York, 46--61.

Digital Library

[44]

Zdancewic, S. and Myers, A. C. 2002. Secure information flow via linear continuations. High. Order Symb. Comput. 15, 2/3, 209--234.

Digital Library

[45]

Zheng, L. and Myers, A. C. 2004. Dynamic security labels and noninterference. In Formal Aspects in Security and Trust.

Cited By

Xu ZChen HTiu ALiu YSareen K(2021)A permission-dependent type system for secure information flow analysisJournal of Computer Security10.3233/JCS-20003629:2(161-228)Online publication date: 1-Jan-2021
https://dl.acm.org/doi/10.3233/JCS-200036
Patrignani MAhmed AClarke D(2019)Formal Approaches to Secure CompilationACM Computing Surveys10.1145/328098451:6(1-36)Online publication date: 4-Feb-2019
https://dl.acm.org/doi/10.1145/3280984
Vorreiter Pedersen MAskarov A(2019)Static Enforcement of Security in Runtime Systems2019 IEEE 32nd Computer Security Foundations Symposium (CSF)10.1109/CSF.2019.00030(335-33515)Online publication date: Jun-2019
https://doi.org/10.1109/CSF.2019.00030
Show More Cited By

Index Terms

Run-time principals in information-flow type systems
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features

Recommendations

Quantum Information-Flow Security: Noninterference and Access Control
CSF '13: Proceedings of the 2013 IEEE 26th Computer Security Foundations Symposium

Quantum cryptography has been extensively studied in the last twenty years, but information-flow security of quantum computing and communication systems has been almost untouched in the previous research. Due to the essential difference between ...
A library for light-weight information-flow security in haskell
HASKELL '08

Protecting confidentiality of data has become increasingly important for computing systems. Information-flow techniques have been developed over the years to achieve that purpose, leading to special-purpose languages that guarantee information-flow ...
Information flow control of component-based distributed systems

Noninterference is a strong security policy that enforces confidentiality and integrity. Many solutions are proposed in the state of the art for verifying this policy in programs, but few tools are proposed to implement it. In this paper, we define a ...

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 30, Issue 1

November 2007

241 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/1290520

Issue’s Table of Contents

Copyright © 2007 ACM.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 November 2007

Published in TOPLAS Volume 30, Issue 1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

21
Total Citations
View Citations
683
Total Downloads

Downloads (Last 12 months)79
Downloads (Last 6 weeks)24

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Xu ZChen HTiu ALiu YSareen K(2021)A permission-dependent type system for secure information flow analysisJournal of Computer Security10.3233/JCS-20003629:2(161-228)Online publication date: 1-Jan-2021
https://dl.acm.org/doi/10.3233/JCS-200036
Patrignani MAhmed AClarke D(2019)Formal Approaches to Secure CompilationACM Computing Surveys10.1145/328098451:6(1-36)Online publication date: 4-Feb-2019
https://dl.acm.org/doi/10.1145/3280984
Vorreiter Pedersen MAskarov A(2019)Static Enforcement of Security in Runtime Systems2019 IEEE 32nd Computer Security Foundations Symposium (CSF)10.1109/CSF.2019.00030(335-33515)Online publication date: Jun-2019
https://doi.org/10.1109/CSF.2019.00030
Li PZhang D(2018)A derivation framework for dependent security label inferenceProceedings of the ACM on Programming Languages10.1145/32764852:OOPSLA(1-26)Online publication date: 24-Oct-2018
https://dl.acm.org/doi/10.1145/3276485
Chen HTiu AXu ZLiu Y(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
https://doi.org/10.1109/CSF.2018.00023
Ramezanifarkhani TOwe OTokas S(2018)A secrecy-preserving language for distributed and object-oriented systemsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2018.04.00199(1-25)Online publication date: Oct-2018
https://doi.org/10.1016/j.jlamp.2018.04.001
Li PZhang D(2017)Towards a Flow- and Path-Sensitive Information Flow Analysis2017 IEEE 30th Computer Security Foundations Symposium (CSF)10.1109/CSF.2017.17(53-67)Online publication date: Aug-2017
https://doi.org/10.1109/CSF.2017.17
Li XNielson FRiis Nielson HMurray TStefan D(2016)Future-dependent Flow Policies with Prophetic VariablesProceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security10.1145/2993600.2993603(29-42)Online publication date: 24-Oct-2016
https://dl.acm.org/doi/10.1145/2993600.2993603
Zhang DWang YSuh GMyers A(2015)A Hardware Design Language for Timing-Sensitive Information-Flow SecurityACM SIGARCH Computer Architecture News10.1145/2786763.269437243:1(503-516)Online publication date: 14-Mar-2015
https://dl.acm.org/doi/10.1145/2786763.2694372
Zhang DWang YSuh GMyers A(2015)A Hardware Design Language for Timing-Sensitive Information-Flow SecurityACM SIGPLAN Notices10.1145/2775054.269437250:4(503-516)Online publication date: 14-Mar-2015
https://dl.acm.org/doi/10.1145/2775054.2694372
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Figures

Tables

Media

View Issue’s Table of Contents