skip to main content
10.1145/2993600.2993605acmconferencesArticle/Chapter ViewAbstractPublication PagespldiConference Proceedingsconference-collections
short-paper
Open access

Short Paper: Bounding Information Leakage Using Implication Graph

Published: 24 October 2016 Publication History

Abstract

Quantitative information-flow analysis (QIF) is an important approach to assess confidentiality property of software systems. A crucial step towards its practical application is to develop automatic techniques for measuring the information leakage in a system. In this paper, we address this question in the context of deterministic imperative programs and under the min-entropy measure of information leakage. In this context, calculating the maximum leakage of a program reduces to counting the number of possible outputs that it can produce. Our approach is based on an new abstract domain over implication graphs. Unlike numeric abstract domains, implication graphs describe relationships among bits. By executing a program on the domain over implication graphs, we can determine some implication constraints among pairs of bits in the output. By counting the number of solutions to the implication constraints, we can deduce an upper-bound on the leakage. We present the mathematical definition of the abstract domain, and explore its effectiveness in measuring leakage on a few case studies.

References

[1]
M. Alvim, M. Andrés, and C. Palamidessi. Probabilistic information flow. In Proc.\ 25th IEEE Symposium on Logic in Computer Science (LICS 2010), pages 314--321, 2010.
[2]
M. S. Alvim, K. Chatzikokolakis, C. Palamidessi, and G. Smith. Measuring information leakage using generalized gain functions. In Proc. 25th IEEE Computer Security Foundations Symposium (CSF 2012), pages 265--279, June 2012.
[3]
B. Aspvall, M. F. Plass, and R. E. Tarjan. A linear-time algorithm for testing the truth of certain quantified boolean formulas. Information Processing Letters, 8(3):121--123, 1979.
[4]
M. Backes, B. Köpf, and A. Rybalchenko. Automatic discovery and quantification of information leaks. In Proc. 30th IEEE Symposium on Security and Privacy, pages 141--153, 2009.
[5]
C. Braun, K. Chatzikokolakis, and C. Palamidessi. Quantitative notions of leakage for one-try attacks. In Proc. 25th Conference on Mathematical Foundations of Programming Semantics (MFPS 2009), volume 249 of ENTCS, pages 75--91, 2009.
[6]
D. Clark, S. Hunt, and P. Malacaria. Quantitative information flow, relations and polymorphic types. Journal of Logic and Computation, 18(2):181--199, 2005.
[7]
M. Clarkson, A. Myers, and F. Schneider. Belief in information flow. In Proc.\ 18th IEEE Computer Security Foundations Workshop (CSFW '05), pages 31--45, 2005.
[8]
P. Cousot and R. Cousot. Basic concepts of abstract interpretation. In Building the Information Society, pages 359--366. Kluwer Academic Publishers, 2004.
[9]
A. V. Goldberg and A. V. Karzanov. Path problems in skew-symmetric graphs. Combinatorica, 16(3):353--382, 1996.
[10]
S. Hamadou, V. Sassone, and C. Palamidessi. Reconciling belief and vulnerability in information flow. In Proc. 31st IEEE Symposium on Security and Privacy, pages 79--92, 2010.
[11]
M. Heule, M. J\"arvisalo, and A. Biere. Efficient cnf simplification based on binary implication graphs. In SAT, pages 201--215, 2011.
[12]
J. Heusser and P. Malacaria. Quantifying information leaks in software. In Proc. ACSAC '10, pages 261--269, 2010.
[13]
B. Köpf and D. Basin. An information-theoretic model for adaptive side-channel attacks. In Proc. 14th ACM Conference on Computer and Communications Security (CCS '07), pages 286--296, 2007.
[14]
B. Köpf, L. Mauborgne, and M. Ochoa. Automatic quantification of cache side-channels. In Proc. 24th International Conference on Computer-Aided Verification (CAV '12), pages 564--580, 2012.
[15]
M. R. Krom. The decision problem for a class of first-order formulas in which all disjunctions are binary. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 13:15--20, 1967.
[16]
Z. Meng and G. Smith. Calculating bounds on information leakage using two-bit patterns. In Proc. Sixth Workshop on Programming Languages and Analysis for Security (PLAS '11), pages 1:1--1:12, 2011.
[17]
Z. Meng and G. Smith. Faster two-bit pattern analysis of leakage. In Proc. 2nd International Workshop on Quantitative Aspects in Security Assurance (QASA '13), pages 2:1--2:14, 2013.
[18]
A. Miné. The octagon abstract domain. Higher Order Symbol. Comput., 19:31--100, Mar. 2006.
[19]
J. Newsome, S. McCamant, and D. Song. Measuring channel capacity to distinguish undue influence. In Proc. Fourth Workshop on Programming Languages and Analysis for Security (PLAS '09), pages 73--85, 2009.
[20]
Q.-S. Phan and P. Malacaria. Abstract model counting: A novel approach for quantification of information leaks. In Proceedings of the 9th ACM Symposium on Information, Computer and Communications Security, ASIA CCS '14, pages 283--292, New York, NY, USA, 2014. ACM.
[21]
Q.-S. Phan, P. Malacaria, O. Tkachuk, and C. S. Corina S. Pasareanu. Symbolic quantitative information flow. SIGSOFT Software Engineering Notes, 37(6):1--5, Nov. 2012.
[22]
L. Roditty. A faster and simpler fully dynamic transitive closure. In Proceedings of the Fourteenth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA '03, pages 404--412, 2003.
[23]
G. Smith. On the foundations of quantitative information flow. In L. de Alfaro, editor, Proc. 12th International Conference on Foundations of Software Science and Computational Structures (FoSSaCS '09), volume 5504 of Lecture Notes in Computer Science, pages 288--302, 2009.

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
PLAS '16: Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security
October 2016
116 pages
ISBN:9781450345743
DOI:10.1145/2993600
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: 24 October 2016

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. abstract interpretation
  2. privacy
  3. quantitative information flow

Qualifiers

  • Short-paper

Conference

CCS'16
Sponsor:

Acceptance Rates

PLAS '16 Paper Acceptance Rate 6 of 11 submissions, 55%;
Overall Acceptance Rate 43 of 77 submissions, 56%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • 0
    Total Citations
  • 369
    Total Downloads
  • Downloads (Last 12 months)63
  • Downloads (Last 6 weeks)10
Reflects downloads up to 20 Feb 2025

Other Metrics

Citations

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media