research-article

Encoding information flow in Aura

Authors:

Steve ZdancewicAuthors Info & Claims

PLAS '09: Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security

Pages 17 - 29

https://doi.org/10.1145/1554339.1554344

Published: 15 June 2009 Publication History

Abstract

Two of the main ways to protect security-sensitive resources in computer systems are to enforce access-control policies and information-flow policies. In this paper, we show how to enforce information-flow policies in Aura, which is a programming language for access control. When augmented with this mechanism for enforcing information-flow polices, Aura can further improve the security of reference monitors that implement access control.

We show how to encode security types and lattices of security labels using Aura's existing constructs for authorization logic. We prove a noninterference theorem for this encoding. We also investigate how to use expressive access-control policies specified in authorization logic as the policies for information declassification.

References

[1]

M. Abadi. Logic in access control. In Proceedings of the 18th Symposium on Logic in Computer Science (LICS), June 2003.

Digital Library

[2]

M. Abadi. Access control in a core calculus of dependency. In Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, ICFP, 2006.

Digital Library

[3]

M. Abadi. Access control in a core calculus of dependency. Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin ENTCS, 172:5--31, April 2007.

Digital Library

[4]

M. Abadi, A. Banerjee, N. Heintze, and J. Riecke. A core calculus of dependency. In Proc. 26th ACM Symp. on Principles of Programming Languages (POPL), Jan. 1999.

Digital Library

[5]

M. Abadi, M. Burrows, B. W. Lampson, and G. D. Plotkin. A calculus for access control in distributed systems. Transactions on Programming Languages and Systems, 15(4):706--734, Sept. 1993.

Digital Library

[6]

A. Askarov and A. Sabelfeld. Gradual release: Unifying declassification, encryption and key release policies. In Proceedings of the 2007 IEEE Symposium on Security and Privacy, 2007.

Digital Library

[7]

A. Askarov and A. Sabelfeld. Localized delimited release: combining the what and where dimensions of information release. In PLAS '07: Proceedings of the 2007 workshop on Programming languages and analysis for security, 2007.

Digital Library

[8]

A. Banerjee, D. A. Naumann, and S. Rosenberg. Expressive declassification policies and modular static enforcement. Security and Privacy, IEEE Symposium on, 2008.

Digital Library

[9]

H. P. Barendregt. Lambda calculi with types. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 117--309. Clarendon Press, Oxford, 1992.

Digital Library

[10]

N. Broberg and D. Sands. Flow locks: Towards a core calculus for dynamic flow policies. In In ESOP 2006: the 15th European Symposium on Programming, 2006.

Digital Library

[11]

J. Cederquist, R. Corin, M. Dekker, S. Etalle, and J. den Hartog. An audit logic for accountability. In The Proceedings of the 6th IEEE International Workshop on Policies for Distributed Systems and Networks, 2005.

Digital Library

[12]

The Coq Development Team. The Coq Proof Assistant Reference Manual version 8.1, 2007. Available from http://coq.inria.fr/.

[13]

H. DeYoung, D. Garg, and F. Pfenning. An authorization logic with explicit time. In Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF-21), June 2008.

Digital Library

[14]

D. Garg and F. Pfenning. Non-interference in constructive authorization logic. In CSFW '06: Proceedings of the 19th IEEE workshop on Computer Security Foundations, 2006.

Digital Library

[15]

N. Heintze and J. G. Riecke. The SLam calculus: Programming with secrecy and integrity. In Proc. 25th ACM Symp. on Principles of Programming Languages (POPL), Jan. 1998.

Digital Library

[16]

L. Jia, J. A. Vaughan, K. Mazurak, J. Zhao, L. Zarko, J. Schorr, and S. Zdancewic. Aura: A programming language for authorization and audit,. In 13th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2008.

Digital Library

[17]

L. Jia and S. Zdancewic. Encoding information flow in AURA, technical appendix. Technical Report MS-CIS-09-08, University of Pennsylvania, 2009. Available at http://www.seas.upenn.edu/~liminjia/research/papers/aura-flow-tr.pdf.

[18]

P. Li and S. Zdancewic. Downgrading Policies and Relaxed Noninterference. In Proc. ACM Symp. on Principles of Programming Languages (POPL), pages 158--170, 2005.

Digital Library

[19]

P. Li and S. Zdancewic. Encoding information flow in Haskell. In CSFW '06: Proceedings of the 19th IEEE workshop on Computer Security Foundations, 2006.

Digital Library

[20]

H. Mantel and A. Reinhard. Controlling the what and where of declassification in language-based security. In In ESOP 2007: the 16th European Symposium on Programming, 2007.

Digital Library

[21]

A. C. Myers. JFlow: Practical mostly-static information flow control. In Proc. 26th ACM Symp. on Principles of Programming Languages (POPL), Jan. 1999.

Digital Library

[22]

A. C. Myers, A. Sabelfeld, and S. Zdancewic. Enforcing robust declassification and qualified robustness. Journal of Computer Security, 14(2):157--196, 2006.

[23]

F. Pottier and V. Simonet. Information flow inference for ML. ACM Trans. Program. Lang. Syst., 25(1):117--158, 2003.

Digital Library

[24]

A. Russo, K. Claessen, and J. Hughes. A library for light-weight information-flow security in Haskell. In Proceedings of the first ACM SIGPLAN symposium on Haskell, 2008.

Digital Library

[25]

A. Sabelfeld and A. C. Myers. A Model for Delimited Release. In International Symposium on Software Security, 2003.

[26]

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

Digital Library

[27]

A. Sabelfeld and D. Sands. Dimensions and principles of declassification. In CSFW '05: Proceedings of the 18th IEEE workshop on Computer Security Foundations, 2005.

Digital Library

[28]

V. Simonet. Flow Caml in a nutshell. In Proceedings of the first APPSEM-II workshop, Mar. 2003.

[29]

J. A. Vaughan, L. Jia, K. Mazurak, and S. Zdancewic. Evidence-based audit. In Proc. of the IEEE Computer Security Foundations Symposium, 2008.

Digital Library

[30]

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

Digital Library

[31]

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

Digital Library

[32]

S. Zdancewic and A. C. Myers. Secure information flow and CPS. In Proc. of the 10th European Symposium on Programming, Apr. 2001.

Digital Library

Cited By

Ahmadpanah MAskarov ASabelfeld A(2021)Nontransitive Policies Transpiled2021 IEEE European Symposium on Security and Privacy (EuroS&P)10.1109/EuroSP51992.2021.00043(543-561)Online publication date: Sep-2021
https://doi.org/10.1109/EuroSP51992.2021.00043
Polikarpova NStefan DYang JItzhaky SHance TSolar-Lezama A(2020)Liquid information flow controlProceedings of the ACM on Programming Languages10.1145/34089874:ICFP(1-30)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3408987
Hirsch AAmorim PCecchetti ETate RArden O(2020)First-Order Logic for Flow-Limited Authorization2020 IEEE 33rd Computer Security Foundations Symposium (CSF)10.1109/CSF49147.2020.00017(123-138)Online publication date: Jun-2020
https://doi.org/10.1109/CSF49147.2020.00017
Show More Cited By

Index Terms

Encoding information flow in Aura
1. Security and privacy
  1. Security services
    1. Access control
  2. Systems security
    1. Information flow control
    2. Operating systems security
2. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features

Recommendations

Encoding information flow in AURA

Two of the main ways to protect security-sensitive resources in computer systems are to enforce access-control policies and information-flow policies. In this paper, we show how to enforce information-flow policies in AURA, which is a programming ...
Flow-Limited Authorization
CSF '15: Proceedings of the 2015 IEEE 28th Computer Security Foundations Symposium

Because information flow control mechanisms often rely on an underlying authorization mechanism, their security guarantees can be subverted by weaknesses in authorization. Conversely, the security of authorization can be subverted by information flows ...
A language for information flow: dynamic tracking in multiple interdependent dimensions
PLAS '09: Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security

This paper presents λ_I, a language for dynamic tracking of information flow across multiple, interdependent dimensions of information. Typical dimensions of interest are integrity and confidentiality. λ_I supports arbitrary domain-specific policies that ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLAS '09: Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security

June 2009

130 pages

ISBN:9781605586458

DOI:10.1145/1554339

Conference Chairs:
Stephen Chong
Harvard University
,
David Naumann
Stevens Institute of Technology

Copyright © 2009 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]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 15 June 2009

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

PLDI '09

Sponsor:

SIGPLAN

PLDI '09: ACM SIGPLAN Conference on Programming Language Design and Implementation

June 15 - 21, 2009

Dublin, Ireland

Acceptance Rates

PLAS '09 Paper Acceptance Rate 8 of 19 submissions, 42%;

Overall Acceptance Rate 43 of 77 submissions, 56%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
157
Total Downloads

Downloads (Last 12 months)4
Downloads (Last 6 weeks)1

Reflects downloads up to 16 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Ahmadpanah MAskarov ASabelfeld A(2021)Nontransitive Policies Transpiled2021 IEEE European Symposium on Security and Privacy (EuroS&P)10.1109/EuroSP51992.2021.00043(543-561)Online publication date: Sep-2021
https://doi.org/10.1109/EuroSP51992.2021.00043
Polikarpova NStefan DYang JItzhaky SHance TSolar-Lezama A(2020)Liquid information flow controlProceedings of the ACM on Programming Languages10.1145/34089874:ICFP(1-30)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3408987
Hirsch AAmorim PCecchetti ETate RArden O(2020)First-Order Logic for Flow-Limited Authorization2020 IEEE 33rd Computer Security Foundations Symposium (CSF)10.1109/CSF49147.2020.00017(123-138)Online publication date: Jun-2020
https://doi.org/10.1109/CSF49147.2020.00017
Broberg Nvan Delft BSands D(2017)Paragon – Practical programming with information flow controlJournal of Computer Security10.3233/JCS-1579125:4-5(323-365)Online publication date: 10-Jul-2017
https://doi.org/10.3233/JCS-15791
Nanevski ABanerjee AGarg D(2013)Dependent Type Theory for Verification of Information Flow and Access Control PoliciesACM Transactions on Programming Languages and Systems10.1145/2491522.249152335:2(1-41)Online publication date: 1-Jul-2013
https://dl.acm.org/doi/10.1145/2491522.2491523
Amir-Mohammadian SFallah M(2013)Noninterference in a predicative polymorphic calculus for access controlComputer Languages, Systems and Structures10.1016/j.cl.2013.06.00139:3(109-120)Online publication date: 1-Oct-2013
https://dl.acm.org/doi/10.1016/j.cl.2013.06.001
Broberg NDelft BSands D(2013)Paragon for Practical Programming with Information-Flow ControlProceedings of the 11th Asian Symposium on Programming Languages and Systems - Volume 830110.1007/978-3-319-03542-0_16(217-232)Online publication date: 9-Dec-2013
https://dl.acm.org/doi/10.1007/978-3-319-03542-0_16
Birgisson ARusso ASabelfeld AAskarov AGuttman J(2011)Capabilities for information flowProceedings of the ACM SIGPLAN 6th Workshop on Programming Languages and Analysis for Security10.1145/2166956.2166961(1-15)Online publication date: 5-Jun-2011
https://dl.acm.org/doi/10.1145/2166956.2166961
Swamy NChen JFournet CStrub PBhargavan KYang JChakravarty MHu ZDanvy O(2011)Secure distributed programming with value-dependent typesProceedings of the 16th ACM SIGPLAN international conference on Functional programming10.1145/2034773.2034811(266-278)Online publication date: 19-Sep-2011
https://dl.acm.org/doi/10.1145/2034773.2034811
Swamy NChen JFournet CStrub PBhargavan KYang J(2011)Secure distributed programming with value-dependent typesACM SIGPLAN Notices10.1145/2034574.203481146:9(266-278)Online publication date: 19-Sep-2011
https://dl.acm.org/doi/10.1145/2034574.2034811
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 Table of Conten