Article

On flow-sensitive security types

Authors:

Sebastian Hunt,

David SandsAuthors Info & Claims

POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 79 - 90

https://doi.org/10.1145/1111037.1111045

Published: 11 January 2006 Publication History

Abstract

This article investigates formal properties of a family of semantically sound flow-sensitive type systems for tracking information flow in simple While programs. The family is indexed by the choice of flow lattice.By choosing the flow lattice to be the powerset of program variables, we obtain a system which, in a very strong sense, subsumes all other systems in the family (in particular, for each program, it provides a principal typing from which all others may be inferred). This distinguished system is shown to be equivalent to, though more simply described than, Amtoft and Banerjee's Hoare-style independence logic (SAS'04).In general, some lattices are more expressive than others. Despite this, we show that no type system in the family can give better results for a given choice of lattice than the type system for that lattice itself.Finally, for any program typeable in one of these systems, we show how to construct an equivalent program which is typeable in a simple flow-insensitive system. We argue that this general approach could be useful in a proof-carrying-code setting.

References

[1]

Torben Amtoft and Anindya Banerjee. Information flow analysis in logical form. In SAS 2004 (11th Static Analysis Symposium), Verona, Italy, August 2004, volume 3148 of LNCS, pages 100--115. Springer-Verlag, 2004.

[2]

Wolfram Amme, Niall Dalton, Jeffery von Ronne, and Michael Franz. SafeTSA: A type safe and referentially secure mobile-code representation based on static single assignment form. In SIGPLAN '01 Conference on Programming Language Design and Implementation, pages 137--147, 2001.

Digital Library

[3]

Andrew W. Appel. Modern Compiler Implementation in Java. Cambridge University Press, Cambridge, 1998.

Digital Library

[4]

GR. Andrews and RP. Reitman. An axiomatic approach to information flow in programs. ACM TOPLAS, 2(1):56--75, January 1980.

Digital Library

[5]

J.-P. Banâtre, CBryce, and DLe Métayer. Compile-time detection of information flow in sequential programs. In Proc. European Symp. on Research in Computer Security, volume 875 of LNCS, pages 55--73. Springer-Verlag, 1994.

Digital Library

[6]

P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. ACM Symp. on Principles of Programming Languages, pages 238--252, January 1977.

Digital Library

[7]

P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 269--282, San Antonio, Texas, 1979. ACM Press, New York, NY.

Digital Library

[8]

Ron Cytron, Jeanne Ferrante, Barry K. Rosen, Mark K. Wegman, and F. Kenneth Zadeck. An efficient method of computing static single assignment form. In 16th Annual ACM Symposium on Principles of Programming Languages, pages 25--35, 1989.

Digital Library

[9]

Paul R. Carini and Michael Hind. Flow-sensitive interprocedural constant propagation. In PLDI '95: Proceedings of the ACM SIGPLAN 1995 conference on Programming language design and implementation, pages 23--31. ACM Press, 1995.

Digital Library

[10]

D. Clark, C. Hankin, and S. Hunt. Information flow for Algol-like languages. Journal of Computer Languages, 28(1):3--28, April 2002.

Digital Library

[11]

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

[12]

B. Davey and H. Priestley. Introduction to Lattices and Order. Cambridge University Press, 1990.

[13]

Roberto Giacobazzi, Francesco Ranzato, and Francesca Scozzari. Making abstract interpretations complete. J. ACM, 47(2):361--416, 2000.

Digital Library

[14]

S. Genaim and F. Spoto. Information Flow Analysis for Java Bytecode. In RCousot, editor, Proc. of the Sixth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05), volume 3385 of Lecture Notes in Computer Science, pages 346--362, Paris, France, January 2005. Springer-Verlag.

Digital Library

[15]

N. Heintze and J. G. Riecke. The SLam calculus: programming with secrecy and integrity. In Proc. ACM Symp. on Principles of Programming Languages, pages 365--377, January 1998.

Digital Library

[16]

S. Hunt and D. Sands. Binding Time Analysis: A New PERspective. In Proceedings of the ACM Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'91), pages 154--164, September 1991. ACM SIGPLAN Notices 26(9).

Digital Library

[17]

D. Hedin and D. Sands. Timing aware information flow security for a JavaCard-like bytecode. In First Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE '05), 2005. To Appear, ENTCS.

Digital Library

[18]

F. Nielson, H. Riis Nielson, and C. Hankin. Principles of Program Analysis. Springer-Verlag, 1999.

Digital Library

[19]

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

Digital Library

[20]

A. Sabelfeld and D. Sands. A per model of secure information flow in sequential programs. Higher Order and Symbolic Computation, 14(1):59--91, March 2001. Earlier version in ESOP'99.

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]

J.B. Wells. The essence of principal typings. In Proc. International Colloquium on Automata, Languages and Programming, volume 2380 of LNCS, pages 913--925. Springer-Verlag, 2002.

Digital Library

Cited By

Ahmadian ASoloviev MBalliu M(2024)Disjunctive Policies for Database-Backed Programs2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00017(388-402)Online publication date: 8-Jul-2024
https://doi.org/10.1109/CSF61375.2024.00017
Pasqua MMiculan M(2024)Behavioral equivalences for AbUTheoretical Computer Science10.1016/j.tcs.2024.114537998:COnline publication date: 1-Jun-2024
https://dl.acm.org/doi/10.1016/j.tcs.2024.114537
Raimondi GBesson FJensen T(2023)Type-directed Program Transformation for Constant-Time EnforcementProceedings of the 25th International Symposium on Principles and Practice of Declarative Programming10.1145/3610612.3610618(1-13)Online publication date: 22-Oct-2023
https://dl.acm.org/doi/10.1145/3610612.3610618
Show More Cited By

Index Terms

On flow-sensitive security types
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
2. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning
      1. Program analysis
    2. Program semantics

Recommendations

On flow-sensitive security types
Proceedings of the 2006 POPL Conference

This article investigates formal properties of a family of semantically sound flow-sensitive type systems for tracking information flow in simple While programs. The family is indexed by the choice of flow lattice.By choosing the flow lattice to be the ...
Flow-sensitive type qualifiers
PLDI '02: Proceedings of the ACM SIGPLAN 2002 conference on Programming language design and implementation

We present a system for extending standard type systems with flow-sensitive type qualifiers. Users annotate their programs with type qualifiers, and inference checks that the annotations are correct. In our system only the type qualifiers are modeled ...
Flow-sensitive type qualifiers

We present a system for extending standard type systems with flow-sensitive type qualifiers. Users annotate their programs with type qualifiers, and inference checks that the annotations are correct. In our system only the type qualifiers are modeled ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2006

432 pages

ISBN:1595930272

DOI:10.1145/1111037

General Chair:
Greg Morrisett
Harvard University, USA
,
Program Chair:
Simon Peyton Jones
Microsoft Research, UK

ACM SIGPLAN Notices Volume 41, Issue 1
Proceedings of the 2006 POPL Conference
January 2006
421 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1111320
Issue’s Table of Contents

Copyright © 2006 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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 January 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

POPL06

Sponsor:

POPL06: The 33rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2006

January 11 - 13, 2006

South Carolina, Charleston, USA

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

163
Total Citations
View Citations
995
Total Downloads

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

Reflects downloads up to 23 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ahmadian ASoloviev MBalliu M(2024)Disjunctive Policies for Database-Backed Programs2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00017(388-402)Online publication date: 8-Jul-2024
https://doi.org/10.1109/CSF61375.2024.00017
Pasqua MMiculan M(2024)Behavioral equivalences for AbUTheoretical Computer Science10.1016/j.tcs.2024.114537998:COnline publication date: 1-Jun-2024
https://dl.acm.org/doi/10.1016/j.tcs.2024.114537
Raimondi GBesson FJensen T(2023)Type-directed Program Transformation for Constant-Time EnforcementProceedings of the 25th International Symposium on Principles and Practice of Declarative Programming10.1145/3610612.3610618(1-13)Online publication date: 22-Oct-2023
https://dl.acm.org/doi/10.1145/3610612.3610618
Xu ZChen HTiu ALiu YSareen K(2021)A permission-dependent type system for secure information flow analysisJournal of Computer Security10.3233/JCS-20003629:2(161-228)Online publication date: 1-Jan-2021
https://dl.acm.org/doi/10.3233/JCS-200036
Balliu MMerro MPasqua MShcherbakov M(2021)Friendly FireACM Transactions on Privacy and Security10.1145/344496324:3(1-40)Online publication date: 1-Apr-2021
https://dl.acm.org/doi/10.1145/3444963
Mu CLi G(2021)Integrating Information Flow Analysis in Unifying Theories of Programming2021 IEEE 26th Pacific Rim International Symposium on Dependable Computing (PRDC)10.1109/PRDC53464.2021.00018(67-76)Online publication date: Dec-2021
https://doi.org/10.1109/PRDC53464.2021.00018
Mudduluru RWaataja JMilstein SErnst M(2021)Verifying Determinism in Sequential Programs2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE)10.1109/ICSE43902.2021.00017(37-49)Online publication date: May-2021
https://doi.org/10.1109/ICSE43902.2021.00017
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
Oak AAhmadian ABalliu MSalvaneschi G(2021)Language Support for Secure Software Development with Enclaves2021 IEEE 34th Computer Security Foundations Symposium (CSF)10.1109/CSF51468.2021.00037(1-16)Online publication date: Jun-2021
https://doi.org/10.1109/CSF51468.2021.00037
Hunt SSands D(2021)A Quantale of Information2021 IEEE 34th Computer Security Foundations Symposium (CSF)10.1109/CSF51468.2021.00031(1-15)Online publication date: Jun-2021
https://doi.org/10.1109/CSF51468.2021.00031
Show More Cited By

View Options

Get Access

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.

Media

Figures

Other

Tables

View Table of Contents