Article

Assessing security threats of looping constructs

Author:

Pasquale MalacariaAuthors Info & Claims

POPL '07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 225 - 235

https://doi.org/10.1145/1190216.1190251

Published: 17 January 2007 Publication History

Abstract

There is a clear intuitive connection between the notion of leakage of information in a program and concepts from information theory. This intuition has not been satisfactorily pinned down, until now. In particular, previous information-theoretic models of programs are imprecise, due to their overly conservative treatment of looping constructs. In this paper we provide the first precise information-theoretic semantics of looping constructs. Our semantics describes both the amount and rate of leakage; if either is small enough, then a program might be deemed "secure". Using the semantics we provide an investigation and classification of bounded and unbounded covert channels.

References

[1]

D. Bell and L. LaPadula, "Secure computer systems: Unified exposition and Multics interpretation", Technical Report MTR-2997, MITRE Corp, 1997.

[2]

D. Clark and S. Hunt and P. Malacaria "Quantitative Analysis of the Leakage of Confidential Data" Electronic Notes in Theoretical Computer Science volume 59, issue 3, Elsevier, 2002.

[3]

D. Clark and S. Hunt and P. Malacaria, "Quantified Interference for a While Language", Elsevier, Electronic Notes in Theoretical Computer Science 112, pages 149--166, 2005.

Digital Library

[4]

D. Clark and S. Hunt and P. Malacaria, "Quantitative Information Flow, Relations and Polymorphic Types", Journal of Logic and Computation, Special Issue on Lambda-calculus, type theory and natural language, 2005, volume 18, number 2, pages 181--199.

Digital Library

[5]

M. R. Clarkson and A. C. Myers and F. B. Schneider, "Belief in Information Flow", Proc. 18th IEEE Computer Security Foundations Workshop (CSFW 18), IEEE Computer Society Press, 2005.

Digital Library

[6]

T. M. Cover and J. A. Thomas, "Elements of Information Theory", 1991, Wiley Interscience.

Digital Library

[7]

D. E. R. Denning, "A Lattice Model of Secure Information Flow", Communications of the ACM, volume 19, number 5, May 1976.

Digital Library

[8]

D. E. R. Denning, "Cryptography and Data Security", 1982, Addison-Wesley.

Digital Library

[9]

A. Di Pierro and C. Hankin and H. Wiklicky, "Probabilistic confinement in a declarative framework", Electronic Notes in Theoretical Computer Science, volume 48, Elsevier 2001.

[10]

A. Di Pierro and C. Hankin and H. Wiklicky, "Quantitative static analysis of distributed systems", Journal of Functional Programming, 2005.

Digital Library

[11]

J. Goguen and J. Meseguer, "Security Policies and Security Models", IEEE Symposium on Security and Privacy, pages 11--20, IEEE Computer Society Press, 1982.

[12]

J. W. Gray III and P. F. Syverson, "A Logical Approach to Multilevel Security of Probabilistic Systems", Distributed Computing, volume 11, number 2, 1998, pages 73--90.

Digital Library

[13]

W. Gray, III, James, "Toward a Mathematical Foundation for Information Flow Security", Proc. 1991 IEEE Symposium on Security and Privacy, Oakland, CA, May 1991, pages 21--34.

[14]

S. Isthiaq and P.W. O'Hearn, "BI as an assertion language for mutable data structures", pages = "14--26", 28th POPL London 2001.

Digital Library

[15]

G. Lowe, "Quantifying Information Flow", Proceedings of the Workshop on Automated Verification of Critical Systems, 2001.

[16]

D.Malone and W. Sullivan, "Guesswork and entropy", IEEE Transactions on Information Theory, volume 50, number 3, March 2004.

Digital Library

[17]

J. L. Massey, "Guessing and entropy", Proc. IEEE International Symposium on Information Theory, 1994, Trondheim, Norway.

[18]

J. McLean, "Security models and information flow", Proceedings of the 1990 IEEE Symposium on Security and Privacy, 1990, Oakland, California.

[19]

J. Millen, "Covert channel capacity", Proc. 1987 IEEE Symposium on Research in Security and Privacy, IEEE Computer Society Press, 1987.

[20]

J. C. Reynolds, "Syntactic control of interference", Conf. Record 5th ACM Symp. on Principles of Programming Languages 1978.

Digital Library

[21]

J. Reynolds, "Separation logic: a logic for shared mutable data structures", Invited Paper, LICS'02, 2002.

Digital Library

[22]

P. Y. A. Ryan and J. McLean and J. Millen and V. Gilgor, "Non-interference, who needs it?", Proceedings of the 14th IEEE Security Foundations Workshop, Cape Breton, Nova Scotia, Canada, June 2001.

Digital Library

[23]

C. Shannon, "A mathematical theory of communication", The Bell System Technical Journal, volume 27, July and October, 1948, pages 379--423 and 623--656.

[24]

D. Volpano and G. Smith, "A Type-Based Approach to Program Security", Proceedings of TAPSOFT '97 (Colloquium on Formal Approaches in Software Engineering), April 1997, Lecture Notes in Computer Science, number 1214, pages 607--621.

Digital Library

[25]

D. G. Weber, "Quantitative Hookup security for covert channel analysis", Proceedings of the 1988 Workshop on the Foundations of Computer Security, 1988, Fanconia, New Hampshire, U.S.A.

[26]

G. Winskel, "The formal semantics of programming languages: an introduction", MIT Press 1993.

Digital Library

[27]

T. Wittbold, "Network of Covert Channels", Proceedings of the 1990 Workshop on the Foundations of Computer Security, 1990.

Cited By

Alvim MFernandes NMcIver ANunes GLuo BLiao XXu JKirda ELie D(2024)The Privacy-Utility Trade-off in the Topics APIProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security10.1145/3658644.3670368(1106-1120)Online publication date: 2-Dec-2024
https://dl.acm.org/doi/10.1145/3658644.3670368
Alvim MFernandes NMcIver AMorgan CNunes GMeng WJensen CCremers CKirda E(2023)A Novel Analysis of Utility in Privacy Pipelines, Using Kronecker Products and Quantitative Information FlowProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security10.1145/3576915.3623081(1718-1731)Online publication date: 15-Nov-2023
https://dl.acm.org/doi/10.1145/3576915.3623081
Sundarapandi GHossain RJasrai CSultana KCodabux Z(2022)Common Programming Mistakes Leading to Information Disclosure: A Preliminary Study2022 IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER)10.1109/SANER53432.2022.00091(743-747)Online publication date: Mar-2022
https://doi.org/10.1109/SANER53432.2022.00091
Show More Cited By

Recommendations

An information-theoretic model for adaptive side-channel attacks
CCS '07: Proceedings of the 14th ACM conference on Computer and communications security

We present a model of adaptive side-channel attacks which we combine with information-theoretic metrics to quantify the information revealed to an attacker. This allows us to express an attacker's remaining uncertainty about a secret as a function of ...
Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints
POPL '77: Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages

A program denotes computations in some universe of objects. Abstract interpretation of programs consists in using that denotation to describe computations in another universe of abstract objects, so that the results of abstract execution give some ...
Automatic discovery of linear restraints among variables of a program
POPL '78: Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2007

400 pages

ISBN:1595935754

DOI:10.1145/1190216

General Chair:
Martin Hofmann
Ludwig-Maximilians U, Munich, Germany
,
Program Chair:
Matthias Felleisen
Northeastern University, Boston MA

ACM SIGPLAN Notices Volume 42, Issue 1
Proceedings of the 2007 POPL Conference
January 2007
379 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1190215
Issue’s Table of Contents

Copyright © 2007 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: 17 January 2007

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

POPL07

Sponsor:

POPL07: The 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 17 - 19, 2007

Nice, France

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

134
Total Citations
View Citations
670
Total Downloads

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

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Alvim MFernandes NMcIver ANunes GLuo BLiao XXu JKirda ELie D(2024)The Privacy-Utility Trade-off in the Topics APIProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security10.1145/3658644.3670368(1106-1120)Online publication date: 2-Dec-2024
https://dl.acm.org/doi/10.1145/3658644.3670368
Alvim MFernandes NMcIver AMorgan CNunes GMeng WJensen CCremers CKirda E(2023)A Novel Analysis of Utility in Privacy Pipelines, Using Kronecker Products and Quantitative Information FlowProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security10.1145/3576915.3623081(1718-1731)Online publication date: 15-Nov-2023
https://dl.acm.org/doi/10.1145/3576915.3623081
Sundarapandi GHossain RJasrai CSultana KCodabux Z(2022)Common Programming Mistakes Leading to Information Disclosure: A Preliminary Study2022 IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER)10.1109/SANER53432.2022.00091(743-747)Online publication date: Mar-2022
https://doi.org/10.1109/SANER53432.2022.00091
Bechberger JWeigl A(2021)Upper Bound Computation of Information Leakages for Unbounded RecursionSoftware Engineering and Formal Methods10.1007/978-3-030-92124-8_10(160-177)Online publication date: 3-Dec-2021
https://doi.org/10.1007/978-3-030-92124-8_10
Chatzikokolakis KFernandes NPalamidessi C(2019)Comparing Systems: Max-Case Refinement Orders and Application to Differential Privacy2019 IEEE 32nd Computer Security Foundations Symposium (CSF)10.1109/CSF.2019.00037(442-44215)Online publication date: Jun-2019
https://doi.org/10.1109/CSF.2019.00037
Biondi FKawamoto YLegay ATraonouez L(2019)Hybrid statistical estimation of mutual information and its application to information flowFormal Aspects of Computing10.1007/s00165-018-0469-z31:2(165-206)Online publication date: 1-Apr-2019
https://dl.acm.org/doi/10.1007/s00165-018-0469-z
Terauchi TAntonopoulos T(2019)A Formal Analysis of Timing Channel Security via BucketingUrbanization and Its Impact in Contemporary China10.1007/978-3-030-17138-4_2(29-50)Online publication date: 3-Apr-2019
https://doi.org/10.1007/978-3-030-17138-4_2
Zhou ZQian ZReiter MZhang Y(2018)Static Evaluation of Noninterference Using Approximate Model Counting2018 IEEE Symposium on Security and Privacy (SP)10.1109/SP.2018.00052(514-528)Online publication date: May-2018
https://doi.org/10.1109/SP.2018.00052
Chatzikokolakis K(2018)On the Additive Capacity Problem for Quantitative Information FlowQuantitative Evaluation of Systems10.1007/978-3-319-99154-2_1(1-19)Online publication date: 15-Aug-2018
https://doi.org/10.1007/978-3-319-99154-2_1
Finkbeiner BHahn CTorfah H(2018)Model Checking Quantitative HyperpropertiesComputer Aided Verification10.1007/978-3-319-96145-3_8(144-163)Online publication date: 18-Jul-2018
https://doi.org/10.1007/978-3-319-96145-3_8
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.

Media

Figures

Other

Tables

View Table of Contents