More Web Proxy on the site http://driver.im/

article

A Type System for Robust Declassification

Author:

Steve ZdancewicAuthors Info & Claims

Electronic Notes in Theoretical Computer Science (ENTCS), Volume 83

Pages 263 - 277

https://doi.org/10.1016/S1571-0661(03)50014-7

Published: 01 January 2013 Publication History

Abstract

Language-based approaches to information security have led to the development of security type systems that permit the programmer to describe confidentiality policies on data. Security type systems are usually intended to enforce noninterference, a property that requires that high-security information not affect low-security computation. However, in practice, noninterference is often too restrictive-the desired policy does permit some information leakage. To compensate for the strictness of noninterference, practical approaches include some mechanism for declassifying high-security information. But such declassification is potentially dangerous, and its use should be restricted to prevent unintended information leaks. Zdancewic and Myers previously introduced the notion of robust declassification in an attempt to capture the desired restrictions on declassification, but that work did not propose a method for determining when a program satisfies the robust declassification condition. This paper motivates robust declassification and shows that a simple change to a security type system can enforce it. The idea is to extend the lattice of security labels to include integrity constraints as well as confidentiality constraints and then require that the decision to perform a declassification have high integrity.

References

[1]

Martín Abadi, Anindya Banerjee, Nevin Heintze, and Jon Riecke. A core calculus of dependency. In Proc. 26th ACM Symp. on Principles of Programming Languages (POPL), pages 147-160, San Antonio, TX, January 1999.

Digital Library

[2]

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

Digital Library

[3]

William R. Bevier, Richard M. Cohen, and William D. Young. Connection policies and controlled interference. In Proc. of the 8th IEEE Computer Security Foundations Workshop, pages 167-176, 1995.

Digital Library

[4]

Elena Ferrari, Pierangela Samarati, Elisa Bertino, and Sushil Jajodia. Providing flexibility in information flow control for object-oriented systems. In Proc. IEEE Symposium on Security and Privacy, pages 130-140, Oakland, CA, USA, May 1997.

Digital Library

[5]

Cedric Fournet and Andrew Gordon. Stack inspection: Theory and variants. In Proc. 29th ACM Symp. on Principles of Programming Languages (POPL), pages 307-318, 2002.

[6]

J. A. Goguen and J. Meseguer. Security policies and security models. In Proc. IEEE Symposium on Security and Privacy, pages 11-20. IEEE Computer Society Press, April 1982.

[7]

Nevin Heintze and Jon G. Riecke. The SLam calculus: Programming with secrecy and integrity. In Proc. 25th ACM Symp. on Principles of Programming Languages (POPL), pages 365-377, San Diego, California, January 1998.

Digital Library

[8]

Kohei Honda and Nobuko Yoshida. A uniform type structure for secure information flow. In Proc. 29th ACM Symp. on Principles of Programming Languages (POPL), pages 81-92, January 2002.

Digital Library

[9]

Pierre Jouvelot and David K. Gifford. Algebraic reconstruction of types and effects. In ACM Symposium on Principles of Programming Languages, pages 303-310, January 1991.

Digital Library

[10]

Andrew C. Myers. JFlow: Practical mostly-static information flow control. In Proc. 26th ACM Symp. on Principles of Programming Languages (POPL), pages 228-241, San Antonio, TX, January 1999.

[11]

Andrew C. Myers. Mostly-static decentralized information flow control. Technical Report MIT/LCS/TR-783, Massachusetts Institute of Technology, Cambridge, MA, January 1999. Ph.D. thesis.

Digital Library

[12]

Andrew C. Myers and Barbara Liskov. Protecting privacy using the decentralized label model. ACM Transactions on Software Engineering and Methodology, 9(4):410-442, 2000.

Digital Library

[13]

Andrew C. Myers, Nathaniel Nystrom, Lantian Zheng, and Steve Zdancewic. Jif: Java information flow. Software release. Located at http://www.cs.cornell.edu/jif, July 2001.

[14]

Sylvan Pinsky. Absorbing covers and intransitive non-interference. In Proc. IEEE Symposium on Security and Privacy, 1995.

Digital Library

[15]

François Pottier and Sylvain Conchon. Information flow inference for free. In Proc. 5th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 46-57, September 2000.

Digital Library

[16]

François Pottier and Vincent Simonet. Information flow inference for ML. In Proc. 29th ACM Symp. on Principles of Programming Languages (POPL), Portland, Oregon, January 2002.

Digital Library

[17]

John C. Reynolds. Syntactic control of interference. In Proc. 5th ACM Symp. on Principles of Programming Languages (POPL), pages 39-46, 1978.

Digital Library

[18]

A. W. Roscoe and M. H. Goldsmith. What is intransitive noninterference? In Proc. of the 12th IEEE Computer Security Foundations Workshop, 1999.

Digital Library

[19]

John Rushby. Noninterference, transitivity and channel-control security policies. Technical report, SRI, 1992.

[20]

Andrei Sabelfeld and Andrew C. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1):5-19, January 2003.

Digital Library

[21]

Andrei Sabelfeld and David Sands. Probabilistic noninterference for multi-threaded programs. In Proc. of the 13th IEEE Computer Security Foundations Workshop, pages 200-214. IEEE Computer Society Press, July 2000.

Digital Library

[22]

Umesh Shankar, Kunal Talwar, Jeffrey S. Foster, and David Wagner. Detecting format string vulnerabilities with type qualifiers. In Proceedings of the 10th USENIX Security Symposium, 2001.

Digital Library

[23]

Geoffrey Smith. A new type system for secure information flow. In Proc. of the 14th IEEE Computer Security Foundations Workshop, pages 115-125. IEEE Computer Society Press, June 2001.

[24]

Dennis Volpano and Geoffrey Smith. Verifying secrets and relative secrecy. In Proc. 27th ACM Symp. on Principles of Programming Languages (POPL), pages 268-276. ACM Press, January 2000.

Digital Library

[25]

Dennis Volpano, Geoffrey Smith, and Cynthia Irvine. A sound type system for secure flow analysis. Journal of Computer Security, 4(3):167-187, 1996.

Digital Library

[26]

Dan S. Wallach, Andrew W. Appel, and Edward W. Felten. The security architecture formerly known as stack inspection: A security mechanism for language-based systems. ACM Transactions on Software Engineering and Methodology, 9(4), October 2000.

Digital Library

[27]

Dan S. Wallach and Edward W. Felten. Understanding Java stack inspection. In Proc. IEEE Symposium on Security and Privacy, Oakland, California, USA, May 1998.

[28]

Stephan A. Zdancewic. Programming Languages for Information Security. PhD thesis, Cornell University, August 2002.

Digital Library

[29]

Steve Zdancewic and Andrew C. Myers. Robust declassification. In Proc. of 14th IEEE Computer Security Foundations Workshop, pages 15-23, Cape Breton, Canada, June 2001.

Digital Library

[30]

Steve Zdancewic and Andrew C. Myers. Secure information flow via linear continuations. Higher Order and Symbolic Computation, 15(2/3), 2002.

[31]

Steve Zdancewic, Lantian Zheng, Nathaniel Nystrom, and Andrew C. Myers. Secure program partitioning. Transactions on Computer Systems, 20(3):283-328, 2002.

Digital Library

[32]

Lantian Zheng, Stephen Chong, Steve Zdancewic, and Andrew C. Myers. Building secure distributed systems using replication and partitioning. In IEEE 2003 Symposium on Security and Privacy. ieee, 2003.

Digital Library

Cited By

Ghosal SShyamasundar R(2022)Preventing Privacy-Violating Information Flows in JavaScript Applications Using Dynamic LabellingInformation Systems Security10.1007/978-3-031-23690-7_12(202-219)Online publication date: 16-Dec-2022
https://dl.acm.org/doi/10.1007/978-3-031-23690-7_12
Salvaneschi GKöhler MSokolowski DHaller PErdweg SMezini M(2019)Language-integrated privacy-aware distributed queriesProceedings of the ACM on Programming Languages10.1145/33605933:OOPSLA(1-30)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360593
Austin TSchmitz TFlanagan C(2017)Multiple Facets for Dynamic Information Flow with ExceptionsACM Transactions on Programming Languages and Systems10.1145/302408639:3(1-56)Online publication date: 10-May-2017
https://dl.acm.org/doi/10.1145/3024086
Show More Cited By

A Type System for Robust Declassification
1. Security and privacy
  1. Systems security
2. Social and professional topics
  1. Computing / technology policy

Recommendations

Trusted declassification:: high-level policy for a security-typed language
PLAS '06: Proceedings of the 2006 workshop on Programming languages and analysis for security

Security-typed languages promise to be a powerful tool with which provably secure software applications may be developed. Programs written in these languages enforce a strong, global policy of noninterferencewhich ensures that high-security data will ...
Combining Robust Declassification and Intransitive Noninterference
IMSCCS '07: Proceedings of the Second International Multi-Symposiums on Computer and Computational Sciences

Language-based information flow security properties such as noninterference ensure that confidential data does not affect the publicly visible behavior. But real computing systems sometimes need to dynamically release certain amount of sensitive ...
Enforcing robust declassification and qualified robustness
Special issue on CSFW17

Noninterference requires that there is no information flow from sensitive to public data in a given system. However, many systems release sensitive information as part of their intended function and therefore violate noninterference. To control ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Electronic Notes in Theoretical Computer Science (ENTCS)

Electronic Notes in Theoretical Computer Science (ENTCS) Volume 83, Issue

January, 2013

297 pages

ISSN:1571-0661

Issue’s Table of Contents

Copyright © Elsevier B.V. © 2003.

Publisher

Elsevier Science Publishers B. V.

Netherlands

Publication History

Published: 01 January 2013

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 21 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ghosal SShyamasundar R(2022)Preventing Privacy-Violating Information Flows in JavaScript Applications Using Dynamic LabellingInformation Systems Security10.1007/978-3-031-23690-7_12(202-219)Online publication date: 16-Dec-2022
https://dl.acm.org/doi/10.1007/978-3-031-23690-7_12
Salvaneschi GKöhler MSokolowski DHaller PErdweg SMezini M(2019)Language-integrated privacy-aware distributed queriesProceedings of the ACM on Programming Languages10.1145/33605933:OOPSLA(1-30)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360593
Austin TSchmitz TFlanagan C(2017)Multiple Facets for Dynamic Information Flow with ExceptionsACM Transactions on Programming Languages and Systems10.1145/302408639:3(1-56)Online publication date: 10-May-2017
https://dl.acm.org/doi/10.1145/3024086
Austin TYang JFlanagan CSolar-Lezama ANaldurg PSwamy N(2013)Faceted execution of policy-agnostic programsProceedings of the Eighth ACM SIGPLAN workshop on Programming languages and analysis for security10.1145/2465106.2465121(15-26)Online publication date: 20-Jun-2013
https://dl.acm.org/doi/10.1145/2465106.2465121
Austin TFlanagan CField JHicks M(2012)Multiple facets for dynamic information flowProceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/2103656.2103677(165-178)Online publication date: 25-Jan-2012
https://dl.acm.org/doi/10.1145/2103656.2103677
Austin TFlanagan C(2012)Multiple facets for dynamic information flowACM SIGPLAN Notices10.1145/2103621.210367747:1(165-178)Online publication date: 25-Jan-2012
https://dl.acm.org/doi/10.1145/2103621.2103677
Almeida Matos ABoudol G(2009)On declassification and the non-disclosure policyJournal of Computer Security10.5555/1662658.166266217:5(549-597)Online publication date: 1-Oct-2009
https://dl.acm.org/doi/10.5555/1662658.1662662
Tse SZdancewic S(2007)Run-time principals in information-flow type systemsACM Transactions on Programming Languages and Systems10.1145/1290520.129052630:1(6-es)Online publication date: 1-Nov-2007
https://dl.acm.org/doi/10.1145/1290520.1290526
Nielsen JSchwartzbach MHicks M(2007)A domain-specific programming language for secure multiparty computationProceedings of the 2007 workshop on Programming languages and analysis for security10.1145/1255329.1255333(21-30)Online publication date: 14-Jun-2007
https://dl.acm.org/doi/10.1145/1255329.1255333
Myers ASabelfeld AZdancewic S(2006)Enforcing robust declassification and qualified robustnessJournal of Computer Security10.5555/1150577.115058014:2(157-196)Online publication date: 20-Apr-2006
https://dl.acm.org/doi/10.5555/1150577.1150580
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents