article

Dynamic security labels and static information flow control

Authors:

Andrew C. MyersAuthors Info & Claims

International Journal of Information Security, Volume 6, Issue 2-3

Pages 67 - 84

Published: 01 March 2007 Publication History

Abstract

This paper presents a language in which information flow is securely controlled by a type system, yet the security class of data can vary dynamically. Information flow policies provide the means to express strong security requirements for data confidentiality and integrity. Recent work on security-typed programming languages has shown that information flow can be analyzed statically, ensuring that programs will respect the restrictions placed on data. However, real computing systems have security policies that cannot be determined at the time of program analysis. For example, a file has associated access permissions that cannot be known with certainty until it is opened. Although one security-typed programming language has included support for dynamic security labels, there has been no demonstration that a general mechanism for dynamic labels can securely control information flow. In this paper, we present an expressive language-based mechanism for reasoning about dynamic security labels. The mechanism is formally presented in a core language based on the typed lambda calculus; any well-typed program in this language is secure because it satisfies noninterference.

References

[1]

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

Digital Library

[2]

Amtoft, T., Banerjee, A.: Information flow analysis in logical form. In: The 11th International Symposium on Static Analysis Proceedings. pp. 100---115, Verona (2004)

[3]

Aspinall, D.: Subtyping with singleton types. In: Computer Science Logic (CSL), Kazimierz, Poland. pp. 1---15. Springer, Heidelberg (1994)

[4]

Banerjee, A., Naumann, D.A.: Secure information flow and pointer confinement in a Java-like language. In: Proceedings of 15th IEEE Computer Security Foundations Workshop (2002)

[5]

Banerjee, A., Naumann, D.A.: Using access control for secure information flow in a Java-like language. In: Proceedings of 16th IEEE Computer Security Foundations Workshop. pp. 155---169 (2003)

[6]

Bell, D.E. LaPadula, L.J.: Secure computer systems: mathematical foundations and model. Technical Report M74-244, MITRE Corp., Bedford (1973)

[7]

Denning D.E. (1982). Cryptography and Data Security. Addison-Wesley, Reading

[8]

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

Digital Library

[9]

Department of Defense:Department of Defense Trusted Computer System Evaluation Criteria, DOD 5200.28-STD (The Orange Book) edition (1985)

[10]

Efstathopoulos, P., Krohn, M., VanDeBogart, S., Frey, C., Ziegler, D., Kohler, E., Mazières, D., Kaashoek, F., Morris, R.: Labels and event processes in the Asbestos operating system. In Proceedings of 20th ACM Symposium on Operating System Principles (SOSP) (2005)

[11]

Fenton J.S. (1974). Memoryless subsystems. Comput. J. 17(2): 143---147

[12]

Foley, S., Gong, L., Qian, X.: A security model of dynamic labeling providing a tiered approach to verification. In: IEEE Symposium on Security and Privacy. pp. 142---154, IEEE Computer Society Press, Oakland (1996)

[13]

Goguen, J.A., Meseguer, J.: Security policies and security models. In: Proceedings of IEEE Symposium on Security and Privacy. pp. 11---20 (1982)

[14]

Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java language specification 2nd edn., Addison Wesley, Reading (2000). ISBN 0-201-31008-2

[15]

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

[16]

Hunt, S., Sands, D.: On flow-sensitive security types. In: Proceedings of 33th ACM Symposium on Principles of Programming Languages (POPL). pp. 79---90, Charleston (2006)

Digital Library

[17]

McIlroy M.D. and Reeds J.A. (1992). Multilevel security in the UNIX tradition. Softw Practice Exp 22(8): 673---694

Digital Library

[18]

McLean, J.: The algebra of security. In: IEEE Symposium on Security and Privacy. pp. 2---7. Oakland, California (1988)

[19]

Meadows, C.: Policies for dynamic upgrading. In: Database Security, IV: Status and Prospects. pp. 241---250. North Holland (1991)

[20]

Mitchell J.C. (1996). Foundations for Programming Languages. The MIT Press, Cambridge

[21]

Myers, A.C.: JFlow: Practical mostly-static information flow control. In: Proceedings of 26th ACM Symposium on Principles of Programming Languages (POPL). pp. 228---241, San Antonio (1999)

Digital Library

[22]

Myers, A.C., Liskov, B.: A decentralized model for information flow control. In: Proceedings of 17th ACM Symposium on Operating System Principles (SOSP). pp. 129---142, Saint-Malo (1997)

Digital Library

[23]

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

Digital Library

[24]

Myers A.C., Zheng, L., Zdancewic, S., Chong, S., Nystrom, N.: Jif: Java information flow. Software release, at http://www.cs. cornell.edu/jif, July 2001

[25]

Palsberg, J., Ørbæk, P.: Trust in the ¿-calculus. In: Proceedings of 2nd International Symposium on Static Analysis. number 983 in Lecture Notes in Computer Science, pp. 314---329. Springer (1995)

[26]

Pottier, F., Simonet, V.: Information flow inference for ML. In: Proceedings of 29th ACM Symposium on Principles of Programming Languages (POPL). pp. 319---330 (2002)

Digital Library

[27]

Sabelfeld, A., Mantel, H.: Static confidentiality enforcement for distributed programs. In: Proceedings of the 9th International Static Analysis Symposium. vol. 2477 of LNCS, Madrid. Springer, Heidelberg (2002)

[28]

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

Digital Library

[29]

Spencer, R., Smalley, S., Loscocco, P., Hibler, M., Andersen, D., Lepreau, J.: The Flask security architecture: System support for diverse security policies. In: The 8th USENIX Security Symposium Proceedings. pp. 123---139 (1999)

[30]

Sutherland, I., Perlo, S., Varadarajan, R.: Deducibility security with dynamic level assignments. In: Proceedings of 2nd IEEE Computer Security Foundations Workshop. Franconia (1989)

[31]

Tse, S., Zdancewic, S.: Run-time principals in information-flow type systems. In: IEEE Symposium on Security and Privacy. Oakland (2004)

[32]

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

Digital Library

[33]

Weissman, C.: Security controls in the ADEPT-50 time-sharing system. In: AFIPS Conference Proceedings. vol. 35, pp. 119---133 (1969)

Digital Library

[34]

Woodward, J.P.L.: Exploiting the dual nature of sensitivity labels. In: IEEE Symposium on Security and Privacy. pp. 23---30, Oakland, California (1987)

[35]

Xi, H.: Imperative programming with dependent types. In: Proceedings of 15th Symposium on Logic in Computer Science. Santa, Barbara (2000)

[36]

Xi, H., Pfenning, F.: Dependent types in practical programming. In: Proceedings of 26th ACM Symposium on Principles of Programming Languages (POPL). pp. 214---227, San Antonio (1999)

Digital Library

[37]

Zdancewic S. and Myers A.C. (2002). Secure information flow via linear continuations. Higher Order Symbolic Computat 15(2---3): 209---234

[38]

Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: Proceedings of 16th IEEE Computer Security Foundations Workshop. pp. 29---43, Pacific Grove (2003)

[39]

Zheng, L., Myers, A.C.: Dynamic security labels and noninterference. In: Proceedings of 2nd Workshop on Formal Aspects in Security and Trust, IFIP TC1 WG1.7. Springer, Heidelberg (2004)

[40]

Zheng, L., Myers, A.C.: Dynamic security labels and noninterference. Technical Report 2004---1924, Cornell University Computing and Information Science (2004)

Cited By

Ghosal SShyamasundar RJuristo N(2021)An axiomatic approach to detect information leaks in concurrent programsProceedings of the 43rd International Conference on Software Engineering: New Ideas and Emerging Results10.1109/ICSE-NIER52604.2021.00015(31-35)Online publication date: 25-May-2021
https://dl.acm.org/doi/10.1109/ICSE-NIER52604.2021.00015
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
Ferraiuolo AZhao MMyers ASuh GLie DMannan MBackes MWang X(2018)HyperFlowProceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security10.1145/3243734.3243743(1583-1600)Online publication date: 15-Oct-2018
https://dl.acm.org/doi/10.1145/3243734.3243743
Show More Cited By

Index Terms

Dynamic security labels and static information flow control

Recommendations

Information Flow Based Security Control Beyond RBAC: How to enable fine-grained security policy enforcement in business processes beyond limitations ... access control (RBAC) (IT im Unternehmen)
Flexible dynamic information flow control in Haskell
Haskell '11

We describe a new, dynamic, floating-label approach to language-based information flow control, and present an implementation in Haskell. A labeled IO monad, LIO, keeps track of a current label and permits restricted access to IO functionality, while ...
Security Information Flow Control Model and Method in MILS
CIS '12: Proceedings of the 2012 Eighth International Conference on Computational Intelligence and Security

Multiple Independent Levels of Security (MILS) is a high-assurance architecture which protects information sharing at different security levels. MILS ensures mutual independence and prevents the spread of the error effectively between partitions. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image International Journal of Information Security

International Journal of Information Security Volume 6, Issue 2-3

March 2007

129 pages

ISSN:1615-5262

EISSN:1615-5270

Issue’s Table of Contents

Copyright © Copyright © 2007 Springer-Verlag.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 March 2007

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

30
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 22 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ghosal SShyamasundar RJuristo N(2021)An axiomatic approach to detect information leaks in concurrent programsProceedings of the 43rd International Conference on Software Engineering: New Ideas and Emerging Results10.1109/ICSE-NIER52604.2021.00015(31-35)Online publication date: 25-May-2021
https://dl.acm.org/doi/10.1109/ICSE-NIER52604.2021.00015
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
Ferraiuolo AZhao MMyers ASuh GLie DMannan MBackes MWang X(2018)HyperFlowProceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security10.1145/3243734.3243743(1583-1600)Online publication date: 15-Oct-2018
https://dl.acm.org/doi/10.1145/3243734.3243743
Broberg Nvan Delft BSands DMurray TSabelfeld ABauer L(2017)Paragon – Practical programming with information flow controlJournal of Computer Security10.3233/JCS-1579125:4-5(323-365)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.3233/JCS-15791
Gruetter SMurray TBielova NGaboardi M(2017)Short PaperProceedings of the 2017 Workshop on Programming Languages and Analysis for Security10.1145/3139337.3139345(43-48)Online publication date: 30-Oct-2017
https://dl.acm.org/doi/10.1145/3139337.3139345
Cecchetti EMyers AArden OThuraisingham BEvans DMalkin TXu D(2017)Nonmalleable Information Flow ControlProceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security10.1145/3133956.3134054(1875-1891)Online publication date: 30-Oct-2017
https://dl.acm.org/doi/10.1145/3133956.3134054
Ferraiuolo AXu RZhang DMyers ASuh G(2017)Verification of a Practical Hardware Security Architecture Through Static Information Flow AnalysisACM SIGARCH Computer Architecture News10.1145/3093337.303773945:1(555-568)Online publication date: 4-Apr-2017
https://dl.acm.org/doi/10.1145/3093337.3037739
Ferraiuolo AXu RZhang DMyers ASuh G(2017)Verification of a Practical Hardware Security Architecture Through Static Information Flow AnalysisACM SIGPLAN Notices10.1145/3093336.303773952:4(555-568)Online publication date: 4-Apr-2017
https://dl.acm.org/doi/10.1145/3093336.3037739
Ferraiuolo AHua WMyers ASuh G(2017)Secure Information Flow Verification with Mutable Dependent TypesProceedings of the 54th Annual Design Automation Conference 201710.1145/3061639.3062316(1-6)Online publication date: 18-Jun-2017
https://dl.acm.org/doi/10.1145/3061639.3062316
Ferraiuolo AXu RZhang DMyers ASuh GChen YTemam OCarter J(2017)Verification of a Practical Hardware Security Architecture Through Static Information Flow AnalysisProceedings of the Twenty-Second International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3037697.3037739(555-568)Online publication date: 4-Apr-2017
https://dl.acm.org/doi/10.1145/3037697.3037739
Show More Cited By

View Options

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

Media

Figures

Other

Tables

View Issue’s Table of Contents