Document Open Access Logo

Computing Information Flow Using Symbolic Model-Checking

Authors Rohit Chadha, Umang Mathur, Stefan Schwoon

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2014.505.pdf
  • Filesize: 0.55 MB
  • 12 pages

Document Identifiers

Author Details

Rohit Chadha
Umang Mathur
Stefan Schwoon

Cite AsGet BibTex

Rohit Chadha, Umang Mathur, and Stefan Schwoon. Computing Information Flow Using Symbolic Model-Checking. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 505-516, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
https://doi.org/10.4230/LIPIcs.FSTTCS.2014.505

Abstract

Several measures have been proposed in literature for quantifying the information leaked by the public outputs of a program with secret inputs. We consider the problem of computing information leaked by a deterministic or probabilistic program when the measure of information is based on (a) min-entropy and (b) Shannon entropy. The key challenge in computing these measures is that we need the total number of possible outputs and, for each possible output, the number of inputs that lead to it. A direct computation of these quantities is infeasible because of the state-explosion problem. We therefore propose symbolic algorithms based on binary decision diagrams (BDDs). The advantage of our approach is that these symbolic algorithms can be easily implemented in any BDD-based model-checking tool that checks for reachability in deterministic non-recursive programs by computing program summaries. We demonstrate the validity of our approach by implementing these algorithms in a tool Moped-QLeak, which is built upon Moped, a model checker for Boolean programs. Finally, we show how this symbolic approach extends to probabilistic programs.
Keywords
  • Information leakage
  • Min Entropy
  • Shannon Entropy
  • Abstract decision diagrams
  • Program summaries

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. S. B. Akers. Binary decision diagrams. IEEE Trans. Comput., 27(6):509-516, 1978. Google Scholar
  2. M. E. Andrés, C. Palamidessi, P. van Rossum, and G. Smith. Computing the leakage of information-hiding systems. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 373-389, 2010. Google Scholar
  3. M. Backes, B. Köpf, and A. Rybalchenko. Automatic discovery and quantification of information leaks. In IEEE Symposium on Security and Privacy, pages 141-153, 2009. Google Scholar
  4. F. Biondi, A. Legay, L. Traonouez, and A. Wasowski. Quail: A quantitative security analyzer for imperative code. In Computer Aided Verification, pages 702-707, 2013. Google Scholar
  5. R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677-691, August 1986. Google Scholar
  6. R. Chadha, D. Kini, and M. Viswanathan. Quantitative information flow in boolean programs. In Principles of Security and Trust, pages 103-119, 2014. Google Scholar
  7. K. Chatzikokolakis, T. Chothia, and A. Guha. Statistical measurement of information leakage. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 390-404, 2010. Google Scholar
  8. K. Chatzikokolakis, C. Palamidessi, and P. Panangaden. Probability of error in information-hiding protocols. In IEEE Computer Security Foundations Symp., pages 341-354, 2007. Google Scholar
  9. K. Chatzikokolakis, C. Palamidessi, and P. Panangaden. Anonymity protocols as noisy channels. Information and Computation, 206(2-4), 2008. Google Scholar
  10. T. Chothia, Y. Kawamoto, C. Novakovic, and D. Parker. Probabilistic point-to-point information leakage. In IEEE Computer Security Foundations Symp., pages 193-205, 2013. Google Scholar
  11. D. Clark, S. Hunt, and P. Malacaria. A static analysis for quantifying information flow in a simple imperative language. Journal of Computer Security, 15(3):321-371, 2007. Google Scholar
  12. E. M. Clarke, K. L. Mcmillan, X. Zhao, M. Fujita, and J. Yang. Spectral transforms for large boolean functions with applications to technology mapping. Formal Methods in System Design, 10(2-3):137-148, 1997. Google Scholar
  13. J. Esparza, S. Kiefer, and S. Schwoon. Abstraction refinement with Craig interpolation and symbolic pushdown systems. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 3920, pages 489-503, 2006. Google Scholar
  14. A. Hinton, M. Z. Kwiatkowska, G. Norman, and D. Parker. Prism: A tool for automatic verification of probabilistic systems. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 441-444, 2006. Google Scholar
  15. V. Klebanov. Precise quantitative information flow analysis using symbolic model counting. 1st International Workshop on Quantitative Aspects of Security Assurance, 2012. Google Scholar
  16. V. Klebanov, N. Manthey, and C. J. Muise. SAT-based analysis and quantification of information flow in programs. In International Conference on Quantitative Evaluation of Systems, pages 177-192, 2013. Google Scholar
  17. B. Köpf and D. A. Basin. An information-theoretic model for adaptive side-channel attacks. In ACM Conference on Computer and Communications Security, pages 286-296, 2007. Google Scholar
  18. B. Köpf and A. Rybalchenko. Approximation and randomization for quantitative information-flow analysis. In IEEE Computer Security Foundations Symp., pages 3-14, 2010. Google Scholar
  19. C. Y. Lee. Representation of switching circuits by binary-decision programs. Bell System Technical Journal, 38:985-999, 1959. Google Scholar
  20. Z. Meng and G. Smith. Faster two-bit pattern analysis of leakage. 2nd International Workshop on Quantitative Aspects of Security Assurance, 2013. Google Scholar
  21. Z. Meng and G. Smith. Calculating bounds on information leakage using two-bit patterns. In Workshop on Programming Languages and Analysis for Security, 2011. Google Scholar
  22. J. K. Millen. Covert channel capacity. In IEEE Symposium on Security and Privacy, pages 60-66, 1987. Google Scholar
  23. Q. Phan and P. Malacaria. Abstract model counting: a novel approach for quantification of information leaks. In ACM Symposium on Information, Computer and Communications Security, pages 283-292, 2014. Google Scholar
  24. J. M. Rutten, M. Kwiatkowska, G. Norman, and D. Parker. Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. AMS, 2004. Google Scholar
  25. G. Smith. On the foundations of quantitative information flow. In International Conference on Foundations of Software Science and Computation Structures, pages 288-302, 2009. Google Scholar
  26. P. Černý, K. Chatterjee, and T. A. Henzinger. The complexity of quantitative information flow problems. In IEEE Computer Security Foundations Symposium, pages 205-217, 2011. Google Scholar
  27. H. Yasuoka and T. Terauchi. Quantitative Information Flow - Verification Hardness and Possibilities. In IEEE Computer Security Foundations Symposium, pages 15-27, 2010. Google Scholar
  28. H. Yasuoka and T. Terauchi. Quantitative information flow as safety and liveness hyperproperties. In Quantitative Aspects of Programming Languages and Systems, pages 77-91, 2012. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact