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

Article

Flow locks: towards a core calculus for dynamic flow policies

Authors:

Niklas Broberg,

David SandsAuthors Info & Claims

ESOP'06: Proceedings of the 15th European conference on Programming Languages and Systems

Pages 180 - 196

https://doi.org/10.1007/11693024_13

Published: 27 March 2006 Publication History

Abstract

Security is rarely a static notion. What is considered to be confidential or untrusted data varies over time according to changing events and states. The static verification of secure information flow has been a popular theme in recent programming language research, but information flow policies considered are based on multilevel security which presents a static view of security levels. In this paper we introduce a very simple mechanism for specifying dynamic information flow policies, flow locks, which specify conditions under which data may be read by a certain actor. The interface between the policy and the code is via instructions which open and close flow locks. We present a type and effect system for an ML-like language with references which permits the completely static verification of flow lock policies, and prove that the system satisfies a semantic security property generalising noninterference. We show that this simple mechanism can represent a number of recently proposed information flow paradigms for declassification.

References

[1]

M. Abadi, A. Banerjee, N. Heintze, and J. Riecke. A core calculus of dependency. In Proc. ACM Symp. on Principles of Programming Languages, pages 147-160, Jan. 1999.

Digital Library

[2]

A. Almeida Matos and G. Boudol. On declassification and the non-disclosure policy. In Proc. IEEE Computer Security Foundations Workshop, June 2005.

Digital Library

[3]

A. Askarov and A. Sabelfeld. Security-typed languages for implementation of cryptographic protocols: A case study. In Proc. European Symp. on Research in Computer Security, volume 3679 of LNCS, 2005.

Digital Library

[4]

A. Banerjee and D. A. Naumann. Stack-based access control and secure information flow. Journal of Functional Programming, 15(2):131-177, Mar. 2005.

Digital Library

[5]

S. Chong and A. C. Myers. Security policies for downgrading. In ACM Conference on Computer and Communications Security, pages 198-209, Oct. 2004.

Digital Library

[6]

D. E. Denning and P. J. Denning. Certification of programs for secure information flow. Comm. of the ACM, 20(7):504-513, July 1977.

Digital Library

[7]

M. Hicks, S. Tse, B. Hicks, and S. Zdancewic. Dynamic updating of information-flow policies. In Proc. Foundations of Computer Security Workshop, 2005.

[8]

H. Mantel and D. Sands. Controlled downgrading based on intransitive (non)interference. In Proc. Asian Symp. on Programming Languages and Systems, volume 3302 of LNCS, pages 129-145. Springer-Verlag, Nov. 2004.

[9]

A. C. Myers. JFlow: Practical mostly-static information flow control. In Proc. ACM Symp. on Principles of Programming Languages, pages 228-241, Jan. 1999.

Digital Library

[10]

A. C. Myers and B. Liskov. A decentralized model for information flow control. In Proc. ACM Symp. on Operating System Principles, pages 129-142, Oct. 1997.

Digital Library

[11]

A. C. Myers and B. Liskov. Complete, safe information flow with decentralized labels. In Proc. IEEE Symp. on Security and Privacy, pages 186-197, May 1998.

[12]

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

Digital Library

[13]

A. C. Myers, A. Sabelfeld, and S. Zdancewic. Enforcing robust declassification. In Proc. IEEE Computer Security Foundations Workshop, pages 172-186, June 2004.

Digital Library

[14]

S. Pinsky. Absorbing covers and intransitive non-interference. In Proc. IEEE Symp. on Security and Privacy, pages 102-113, May 1995.

Digital Library

[15]

J. M. Rushby. Noninterference, transitivity, and channel-control security policies. Technical Report CSL-92-02, SRI International, 1992.

[16]

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

Digital Library

[17]

A. Sabelfeld and D. Sands. Probabilistic noninterference for multi-threaded programs. In Proc. IEEE Computer Security Foundations Workshop, pages 200-214, July 2000.

Digital Library

[18]

A. Sabelfeld and D. Sands. Dimensions and principles of declassification. In Proc. IEEE Computer Security Foundations Workshop, 2005.

Digital Library

[19]

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

[20]

S. Tse and S. Zdancewic. Designing a security-typed language with certificate-based declassification. In Proc. European Symp. on Programming, volume 3444 of LNCS, pages 279-294. Springer-Verlag, Apr. 2005.

Digital Library

[21]

D. Volpano, G. Smith, and C. Irvine. A sound type system for secure flow analysis. J. Computer Security, 4(3):167-187, 1996.

Digital Library

[22]

S. Zdancewic and A. C. Myers. Robust declassification. In Proc. IEEE Computer Security Foundations Workshop, pages 15-23, June 2001.

Digital Library

[23]

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

Cited By

Wolf FMüller PLuo BLiao XXu JKirda ELie D(2024)Verifiable Security Policies for Distributed SystemsProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security10.1145/3658644.3690303(4-18)Online publication date: 2-Dec-2024
https://dl.acm.org/doi/10.1145/3658644.3690303
Menz JHirsch ALi PGarg D(2023)Compositional Security Definitions for Higher-Order Where DeclassificationProceedings of the ACM on Programming Languages10.1145/35860417:OOPSLA1(406-433)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586041
Kozyri ESchneider F(2020)RIFJournal of Computer Security10.3233/JCS-19131628:2(191-228)Online publication date: 1-Jan-2020
https://dl.acm.org/doi/10.3233/JCS-191316
Show More Cited By

Recommendations

Nonmalleable Information Flow Control
CCS '17: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security

Noninterference is a popular semantic security condition because it offers strong end-to-end guarantees, it is inherently compositional, and it can be enforced using a simple security type system. Unfortunately, it is too restrictive for real systems. ...
Language-based information-flow security

Current standard security practices do not provide substantial assurance that the end-to-end behavior of a computing system satisfies important security policies such as confidentiality. An end-to-end confidentiality policy might assert that secret ...
Scalable reader-writer locks
SPAA '09: Proceedings of the twenty-first annual symposium on Parallelism in algorithms and architectures

We present three new reader-writer lock algorithms that scale under high read-only contention. Many previous reader-writer locks suffer significant degradation when many readers attempt to acquire the lock concurrently, even though they are all allowed ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

ESOP'06: Proceedings of the 15th European conference on Programming Languages and Systems

March 2006

342 pages

ISBN:354033095X

Editor:
Peter Sestoft
IT University of Copenhagen, Denmark

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 27 March 2006

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

26
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

Wolf FMüller PLuo BLiao XXu JKirda ELie D(2024)Verifiable Security Policies for Distributed SystemsProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security10.1145/3658644.3690303(4-18)Online publication date: 2-Dec-2024
https://dl.acm.org/doi/10.1145/3658644.3690303
Menz JHirsch ALi PGarg D(2023)Compositional Security Definitions for Higher-Order Where DeclassificationProceedings of the ACM on Programming Languages10.1145/35860417:OOPSLA1(406-433)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586041
Kozyri ESchneider F(2020)RIFJournal of Computer Security10.3233/JCS-19131628:2(191-228)Online publication date: 1-Jan-2020
https://dl.acm.org/doi/10.3233/JCS-191316
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
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
Yang JHance TAustin TSolar-Lezama AFlanagan CChong S(2016)Precise, dynamic information flow for database-backed applicationsACM SIGPLAN Notices10.1145/2980983.290809851:6(631-647)Online publication date: 2-Jun-2016
https://dl.acm.org/doi/10.1145/2980983.2908098
Benton NHofmann MNigam VCheney JVidal G(2016)Effect-dependent transformations for concurrent programsProceedings of the 18th International Symposium on Principles and Practice of Declarative Programming10.1145/2967973.2968602(188-201)Online publication date: 5-Sep-2016
https://dl.acm.org/doi/10.1145/2967973.2968602
Yang JHance TAustin TSolar-Lezama AFlanagan CChong SKrintz CBerger E(2016)Precise, dynamic information flow for database-backed applicationsProceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2908080.2908098(631-647)Online publication date: 2-Jun-2016
https://dl.acm.org/doi/10.1145/2908080.2908098
Hassan DSabry ALazarus RKfoury ABeal J(2013)Encoding secure information flow with restricted delegation and revocation in HaskellProceedings of the 1st annual workshop on Functional programming concepts in domain-specific languages10.1145/2505351.2505354(11-18)Online publication date: 22-Sep-2013
https://dl.acm.org/doi/10.1145/2505351.2505354
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
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents