research-article

Open access

Obtaining Information Leakage Bounds via Approximate Model Counting

Authors:

Surendra Ghentiyala,

Tevfik BultanAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 7, Issue PLDI

Article No.: 167, Pages 1488 - 1509

https://doi.org/10.1145/3591281

Published: 06 June 2023 Publication History

Abstract

Information leaks are a significant problem in modern software systems. In recent years, information theoretic concepts, such as Shannon entropy, have been applied to quantifying information leaks in programs. One recent approach is to use symbolic execution together with model counting constraints solvers in order to quantify information leakage. There are at least two reasons for unsoundness in quantifying information leakage using this approach: 1) Symbolic execution may not be able to explore all execution paths, 2) Model counting constraints solvers may not be able to provide an exact count. We present a sound symbolic quantitative information flow analysis that bounds the information leakage both for the cases where the program behavior is not fully explored and the model counting constraint solver is unable to provide a precise model count but provides an upper and a lower bound. We implemented our approach as an extension to KLEE for computing sound bounds for information leakage in C programs.

References

[1]

Badr F Albanna, Christopher Hillar, Jascha Sohl-Dickstein, and Michael R DeWeese. 2017. Minimum and maximum entropy distributions for binary systems with known means and pairwise correlations. Entropy, 19, 8 (2017), 427.

[2]

Timos Antonopoulos, Paul Gazzillo, Michael Hicks, Eric Koskinen, Tachio Terauchi, and Shiyi Wei. 2017. Decomposition instead of self-composition for proving the absence of timing channels. In ACM SIGPLAN Notices. 52, 362–375.

Digital Library

[3]

Abdulbaki Aydin, Lucas Bang, and Tevfik Bultan. 2015. Automata-Based Model Counting for String Constraints. In Proceedings of the 27th International Conference on Computer Aided Verification (CAV). 255–272.

[4]

Michael Backes, Boris Köpf, and Andrey Rybalchenko. 2009. Automatic Discovery and Quantification of Information Leaks. In 30th IEEE Symposium on Security and Privacy (S&P 2009), 17-20 May 2009, Oakland, California, USA. 141–153.

[5]

Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella. 2008. The Parma Polyhedra Library: Toward a Complete Set of Numerical Abstractions for the Analysis and Verification of Hardware and Software Systems. Science of Computer Programming, 72, 1–2 (2008), 3–21.

Digital Library

[6]

V. Baldoni, N. Berline, J.A. De Loera, B. Dutra, M. Köppe, S. Moreinis, G. Pinto, M. Vergne, and J. Wu. 2014. LattE integrale v1.7.2. http://www.math.ucdavis.edu/ latte/.

[7]

Lucas Bang, Abdulbaki Aydin, Quoc-Sang Phan, Corina S. Păsăreanu, and Tevfik Bultan. 2016. String Analysis for Side Channels with Segmented Oracles. In Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE 2016). ACM, New York, NY, USA.

Digital Library

[8]

Lucas Bang, Nicolas Rosner, and Tevfik Bultan. 2018. Online Synthesis of Adaptive Side-Channel Attacks Based On Noisy Observations. In Proceedings of the IEEE European Symposium on Security and Privacy.

[9]

Alexander I. Barvinok. 1994. A Polynomial Time Algorithm for Counting Integral Points in Polyhedra When the Dimension is Fixed. Math. Oper. Res., 19, 4 (1994), 769–779. https://doi.org/10.1287/moor.19.4.769

Digital Library

[10]

Tevfik Bultan. 2019. Quantifying Information Leakage Using Model Counting Constraint Solvers. In Verified Software. Theories, Tools, and Experiments - 11th International Conference, VSTTE 2019, New York City, NY, USA, July 13-14, 2019, Revised Selected Papers. 30–35.

[11]

Cristian Cadar, Daniel Dunbar, and Dawson R Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In OSDI. 8, 209–224.

Digital Library

[12]

Supratik Chakraborty, Kuldeep S Meel, and Moshe Y Vardi. 2013. A scalable approximate model counter. In International Conference on Principles and Practice of Constraint Programming. 200–216.

[13]

Tom Chothia, Yusuke Kawamoto, and Chris Novakovic. 2014. LeakWatch: Estimating Information Leakage from Java Programs. In Computer Security - ESORICS 2014 - 19th European Symposium on Research in Computer Security, Wroclaw, Poland, September 7-11, 2014. Proceedings, Part II, Miroslaw Kutylowski and Jaideep Vaidya (Eds.) (Lecture Notes in Computer Science, Vol. 8713). Springer, 219–236. isbn:978-3-319-11211-4 https://doi.org/10.1007/978-3-319-11212-1_13

Digital Library

[14]

David Clark, Sebastian Hunt, and Pasquale Malacaria. 2007. A static analysis for quantifying information flow in a simple imperative language. J. Comput. Secur., 15, 3 (2007), Aug., 321–371. issn:0926-227X http://dl.acm.org/citation.cfm?id=1370628.1370629

Digital Library

[15]

Thomas M. Cover and Joy A. Thomas. 2006. Elements of Information Theory (Wiley Series in Telecommunications and Signal Processing). Wiley-Interscience. isbn:0471241954

Digital Library

[16]

Jaco Geldenhuys, Matthew B. Dwyer, and Willem Visser. 2012. Probabilistic symbolic execution. In International Symposium on Software Testing and Analysis, ISSTA 2012, Minneapolis, MN, USA, July 15-20, 2012. 166–176.

Digital Library

[17]

Silviu Guiasu and Abe Shenitzer. 1985. The principle of maximum entropy. The mathematical intelligencer, 7, 1 (1985), 42–48.

[18]

Karla Leigh Hoffman. 1981. A method for globally minimizing concave functions over convex sets. Mathematical Programming, 20, 1 (1981), 01 Dec, 22–32. issn:1436-4646 https://doi.org/10.1007/BF01589330

[19]

Timotej Kapus, Martin Nowack, and Cristian Cadar. 2019. Constraints in Dynamic Symbolic Execution: Bitvectors or Integers? In International Conference on Tests and Proofs. 41–54.

Digital Library

[20]

Seonmo Kim. 2018. SearchMC. https://github.com/seonmokim/SearchMC

[21]

Vladimir Klebanov, Norbert Manthey, and Christian Muise. 2013. SAT-Based Analysis and Quantification of Information Flow in Programs. In Quantitative Evaluation of Systems (Lecture Notes in Computer Science, Vol. 8054). Springer Berlin Heidelberg, 177–192. isbn:978-3-642-40195-4 https://doi.org/10.1007/978-3-642-40196-1_16

Digital Library

[22]

Boris Köpf and David A. Basin. 2007. An information-theoretic model for adaptive side-channel attacks. In Proceedings of the 2007 ACM Conference on Computer and Communications Security, CCS 2007, Alexandria, Virginia, USA, October 28-31, 2007, Peng Ning, Sabrina De Capitani di Vimercati, and Paul F. Syverson (Eds.). ACM, 286–296. isbn:978-1-59593-703-2 https://doi.org/10.1145/1315245.1315282

Digital Library

[23]

Pasquale Malacaria, MHR Khouzani, Corina S Pasareanu, Quoc-Sang Phan, and Kasper Luckow. 2018. Symbolic side-channel analysis for probabilistic programs. In 2018 IEEE 31st Computer Security Foundations Symposium (CSF). 313–327.

[24]

CPLEX User’s Manual. 1987. Ibm ilog cplex optimization studio. Version, 12, 1987-2018 (1987), 1.

[25]

Stephen McCamant and Michael D. Ernst. 2008. Quantitative information flow as network flow capacity. In Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation (PLDI ’08). ACM, New York, NY, USA. 193–205. isbn:978-1-59593-860-2 https://doi.org/10.1145/1375581.1375606

Digital Library

[26]

James Newsome, Stephen McCamant, and Dawn Song. 2009. Measuring channel capacity to distinguish undue influence. In Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security. 73–85.

Digital Library

[27]

Quoc-Sang Phan, Pasquale Malacaria, Corina S. Păsăreanu, and Marcelo d’Amorim. 2014. Quantifying information leaks using reliability analysis. In Proceedings of the International Symposium on Model Checking of Software, SPIN 2014, San Jose, CA, USA. 105–108.

Digital Library

[28]

Quoc-Sang Phan, Pasquale Malacaria, Oksana Tkachuk, and Corina S. Pasareanu. 2012. Symbolic quantitative information flow. ACM SIGSOFT Software Engineering Notes, 37, 6 (2012), 1–5. https://doi.org/10.1145/2382756.2382791

Digital Library

[29]

Quoc-Sang Phan, Lucas Bang, Corina S. Pasareanu, Pasquale Malacaria, and Tevfik Bultan. 2017. Synthesis of Adaptive Side-Channel Attacks. In 2017 IEEE 30th Computer Security Foundations Symposium (CSF). 328–342. https://doi.org/10.1109/CSF.2017.8

[30]

Quoc-Sang Phan and Pasquale Malacaria. 2014. 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). ACM, New York, NY, USA. 283–292. isbn:978-1-4503-2800-5 https://doi.org/10.1145/2590296.2590328

Digital Library

[31]

Corina S. Păsăreanu, Quoc-Sang Phan, and Pasquale Malacaria. 2016. Multi-run side-channel analysis using Symbolic Execution and Max-SMT. In Proceedings of the 2016 IEEE 29th Computer Security Foundations Symposium (CSF ’16). IEEE Computer Society, Washington, DC, USA. 14 pages.

[32]

PyParma. 2015. PyParma. https://github.com/haudren/pyparma

[33]

Seemanta Saha, William Eiers, Ismet Burak Kadron, Lucas Bang, and Tevfik Bultan. 2019. Incremental Attack Synthesis. SIGSOFT Softw. Eng. Notes, 44, 4 (2019), dec, 16. issn:0163-5948 https://doi.org/10.1145/3364452.336445759

Digital Library

[34]

Seemanta Saha, Ismet Burak Kadron, William Eiers, Lucas Bang, and Tevfik Bultan. 2019. Attack Synthesis for Strings using Meta-Heuristics. CoRR, abs/1907.11710 (2019), arXiv:1907.11710. arxiv:1907.11710

[35]

Khayyam Salehi, Jaber Karimpour, Habib Izadkhah, and Ayaz Isazadeh. 2019. Channel Capacity of Concurrent Probabilistic Programs. Entropy, 21, 9 (2019), 885.

[36]

Geoffrey Smith. 2009. On the Foundations of Quantitative Information Flow. In Foundations of Software Science and Computational Structures, 12th International Conference, FOSSACS 2009, York, UK, March 22-29, 2009. Proceedings. 288–302.

[37]

Celina G Val, Michael A Enescu, Sam Bayless, William Aiello, and Alan J Hu. 2016. Precisely measuring quantitative information flow: 10k lines of code and beyond. In 2016 IEEE European Symposium on Security and Privacy (EuroS&P). 31–46.

Cited By

Meel KChakraborty SMathur U(2024)A faster FPRAS for #NFAProceedings of the ACM on Management of Data10.1145/36516132:2(1-22)Online publication date: 14-May-2024
https://dl.acm.org/doi/10.1145/3651613
Cai LSong FChen T(2024)Towards Efficient Verification of Constant-Time Cryptographic ImplementationsProceedings of the ACM on Software Engineering10.1145/36437721:FSE(1019-1042)Online publication date: 12-Jul-2024
https://dl.acm.org/doi/10.1145/3643772

Index Terms

Obtaining Information Leakage Bounds via Approximate Model Counting
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software notations and tools
    1. General programming languages

Recommendations

Parameterized model counting for string and numeric constraints
ESEC/FSE 2018: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering

Recently, symbolic program analysis techniques have been extended to quantitative analyses using model counting constraint solvers. Given a constraint and a bound, a model counting constraint solver computes the number of solutions for the constraint ...
Two approximate algorithms for model counting

Model counting is the problem of computing the number of models or satisfying assignments for a given propositional formula, and is # P -complete. Owing to its inherent complexity, approximate model counting is an alternative in practice. Model counting ...
Model Counting for Complex Data Structures
SPIN 2015: Proceedings of the 22nd International Symposium on Model Checking Software - Volume 9232

We extend recent approaches for calculating the probability of program behaviors, to allow model counting for complex data structures with numeric fields. We use symbolic execution with lazy initialization to compute the input structures leading to the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 7, Issue PLDI

June 2023

2020 pages

EISSN:2475-1421

DOI:10.1145/3554310

Editor:
Michael Hicks
Amazon, USA

Issue’s Table of Contents

Copyright © 2023 Owner/Author.

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 06 June 2023

Published in PACMPL Volume 7, Issue PLDI

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

NSF (National Science Foundation)

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
563
Total Downloads

Downloads (Last 12 months)329
Downloads (Last 6 weeks)41

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Meel KChakraborty SMathur U(2024)A faster FPRAS for #NFAProceedings of the ACM on Management of Data10.1145/36516132:2(1-22)Online publication date: 14-May-2024
https://dl.acm.org/doi/10.1145/3651613
Cai LSong FChen T(2024)Towards Efficient Verification of Constant-Time Cryptographic ImplementationsProceedings of the ACM on Software Engineering10.1145/36437721:FSE(1019-1042)Online publication date: 12-Jul-2024
https://dl.acm.org/doi/10.1145/3643772

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents