article

Downgrading policies and relaxed noninterference

Authors:

Steve ZdancewicAuthors Info & Claims

ACM SIGPLAN Notices, Volume 40, Issue 1

Pages 158 - 170

https://doi.org/10.1145/1047659.1040319

Published: 12 January 2005 Publication History

Abstract

In traditional information-flow type systems, the security policy is often formalized as noninterference properties. However, noninterference alone is too strong to express security properties useful in practice. If we allow downgrading in such systems, it is challenging to formalize the security policy as an extensional property of the system.This paper presents a generalized framework of downgrading policies. Such policies can be specified in a simple and tractable language and can be statically enforced by mechanisms such as type systems. The security guarantee is then formalized as a concise extensional property using program equivalences. This relaxed noninterference generalizes traditional pure noninterference and precisely characterizes the information released due to downgrading.

References

[1]

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

[2]

Hubie Chen and Stephen Chong. Owned policies for information security. In Proc. of the IEEE Computer Security Foundations Workshop, 2004.

Digital Library

[3]

R. Giacobazzi and I. Mastroeni. Abstract non-interference: Parameterizing non-interference by abstract interpretation. In Proc. 31st ACM Symp. on Principles of Programming Languages (POPL), pages 186--197, January 2004.

Digital Library

[4]

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.

[5]

James W. Gray, III. Towards a mathematical foundation for information flow security. In Proc. IEEE Symposium on Security and Privacy, pages 21--34. IEEE Computer Society Press, 1991.

[6]

Gavin Lowe. Quantifying information flow. In Proc. of the IEEE Computer Security Foundations Workshop, pages 18--31. IEEE Computer Society Press, 2002.

Digital Library

[7]

Heiko Mantel and David Sands. Controlled declassification based on intransitive noninterference. In Proceedings of The Second Asian Symposium on Programming Languages and Systems, volume 3302 of LNCS. Springer, 2004.

[8]

John McLean. Security models and information flow. In Proc. IEEE Symposium on Security and Privacy, pages 180--187. IEEE Computer Society Press, 1990.

[9]

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.

Digital Library

[10]

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

[11]

Andrew C Myers, Andrei Sabelfeld, and Steve Zdancewic. Enforcing robust declassification. In Proc. of the 17th IEEE Computer Security Foundations Workshop, pages 172--186. IEEE Computer Society Press, June 2004.

Digital Library

[12]

Alessandra Di Pierro, Chris Hankin, and Herbert Wiklicky. Approximate non-interference. In Proc. of the IEEE Computer Security Foundations Workshop, pages 1--17. IEEE Computer Society Press, 2002.

Digital Library

[13]

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

[14]

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

[15]

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

Digital Library

[16]

Andrei Sabelfeld and Andrew Myers. A model for delimited information release. In Proceedings of the International Symposium on Software Security (ISSS'03), 2004.

[17]

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

[18]

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

[19]

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

[20]

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

Digital Library

Cited By

Li PZhang D(2022)Towards a General-Purpose Dynamic Information Flow Policy2022 IEEE 35th Computer Security Foundations Symposium (CSF)10.1109/CSF54842.2022.9919639(260-275)Online publication date: Aug-2022
https://doi.org/10.1109/CSF54842.2022.9919639
Fan YSong FChen TZhang LLiu W(2022)PoS4MPC: Automated Security Policy Synthesis for Secure Multi-party ComputationComputer Aided Verification10.1007/978-3-031-13185-1_19(385-406)Online publication date: 7-Aug-2022
https://dl.acm.org/doi/10.1007/978-3-031-13185-1_19
Nelson LBornholt JKrishnamurthy ATorlak EWang X(2020)Noninterference specifications for secure systemsACM SIGOPS Operating Systems Review10.1145/3421473.342147854:1(31-39)Online publication date: 31-Aug-2020
https://dl.acm.org/doi/10.1145/3421473.3421478
Show More Cited By

Index Terms

Downgrading policies and relaxed noninterference

Recommendations

Security policies for downgrading
CCS '04: Proceedings of the 11th ACM conference on Computer and communications security

A long-standing problem in information security is how to specify and enforce expressive security policies that control information flow while also permitting information release (i.e., declassification) where appropriate. This paper presents security ...
Downgrading policies and relaxed noninterference
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

In traditional information-flow type systems, the security policy is often formalized as noninterference properties. However, noninterference alone is too strong to express security properties useful in practice. If we allow downgrading in such systems, ...
Inference of Expressive Declassification Policies
SP '11: Proceedings of the 2011 IEEE Symposium on Security and Privacy

We explore the inference of expressive human-readable declassification policies as a step towards providing practical tools and techniques for strong language-based information security. Security-type systems can enforce expressive information-security ...

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 40, Issue 1

Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2005

391 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1047659

Issue’s Table of Contents

POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2005
402 pages
ISBN:158113830X
DOI:10.1145/1040305
General Chair:
Jens Palsberg
University of California, Los Angeles, CA
,
Program Chair:
Martín Abadi
University of California, Santa Cruz, CA

Copyright © 2005 ACM.

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: 12 January 2005

Published in SIGPLAN Volume 40, Issue 1

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

123
Total Citations
View Citations
823
Total Downloads

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

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Li PZhang D(2022)Towards a General-Purpose Dynamic Information Flow Policy2022 IEEE 35th Computer Security Foundations Symposium (CSF)10.1109/CSF54842.2022.9919639(260-275)Online publication date: Aug-2022
https://doi.org/10.1109/CSF54842.2022.9919639
Fan YSong FChen TZhang LLiu W(2022)PoS4MPC: Automated Security Policy Synthesis for Secure Multi-party ComputationComputer Aided Verification10.1007/978-3-031-13185-1_19(385-406)Online publication date: 7-Aug-2022
https://dl.acm.org/doi/10.1007/978-3-031-13185-1_19
Nelson LBornholt JKrishnamurthy ATorlak EWang X(2020)Noninterference specifications for secure systemsACM SIGOPS Operating Systems Review10.1145/3421473.342147854:1(31-39)Online publication date: 31-Aug-2020
https://dl.acm.org/doi/10.1145/3421473.3421478
Ngo MNaumann DRezk T(2020)Type-Based Declassification for FreeFormal Methods and Software Engineering10.1007/978-3-030-63406-3_11(181-197)Online publication date: 19-Dec-2020
https://doi.org/10.1007/978-3-030-63406-3_11
Cruz RTanter É(2019)Existential Types for Relaxed NoninterferenceProgramming Languages and Systems10.1007/978-3-030-34175-6_5(73-92)Online publication date: 18-Nov-2019
https://doi.org/10.1007/978-3-030-34175-6_5
Ene CMounier LPotet M(2019)Output-Sensitive Information Flow AnalysisFormal Techniques for Distributed Objects, Components, and Systems10.1007/978-3-030-21759-4_6(93-110)Online publication date: 29-May-2019
https://doi.org/10.1007/978-3-030-21759-4_6
Lester MOng LSchäfer M(2016)Information flow analysis for a dynamically typed language with staged metaprogrammingJournal of Computer Security10.3233/JCS-16055724:5(541-582)Online publication date: 8-Nov-2016
https://doi.org/10.3233/JCS-160557
Rafnsson WSabelfeld A(2016)Secure multi-execution: Fine-grained, declassification-aware, and transparentJournal of Computer Security10.3233/JCS-15054124:1(39-90)Online publication date: 1-Mar-2016
https://doi.org/10.3233/JCS-150541
Costanzo DShao ZGu R(2016)End-to-end verification of information-flow security for C and assembly programsACM SIGPLAN Notices10.1145/2980983.290810051:6(648-664)Online publication date: 2-Jun-2016
https://dl.acm.org/doi/10.1145/2980983.2908100
Costanzo DShao ZGu RKrintz CBerger E(2016)End-to-end verification of information-flow security for C and assembly programsProceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2908080.2908100(648-664)Online publication date: 2-Jun-2016
https://dl.acm.org/doi/10.1145/2908080.2908100
Show More Cited By

View Options

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 Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents