Skip to main content
SpringerLink
Log in

Efficient SAT-Based Pre-image Enumeration for Quantitative Information Flow in Programs

  • Conference paper
  • First Online:
Book cover Data Privacy Management and Security Assurance (DPM 2016, QASA 2016)

Part of the book series: Lecture Notes in Computer Science ((LNSC,volume 9963))

Abstract

Quantitative Information Flow Analysis (QIF) measures the loss of an attacker’s uncertainty about the confidential information (pre-image) inside a software system after observing the system outputs (image). In this paper, we supplement the SAT-based QIF analysis for deterministic and terminating C programs, by introducing three algorithms for counting the pre-images and images, which utilizes advantages of incremental SAT solvers. Our tool sharpPI is competitive to mql, quail and chimp. An implementation is provided under http://formal.iti.kit.edu/sharpPI.

A. Weigl—This work was supported by the DFG (German Research Foundation) in Priority Programme Reliably Secure Software Systems (RS3) – DFG Priority Programme 1496. Thanks to Vladimir Klebanov for feedback during the creation of this paper and Laurent Simon for a dessert in Lisbon.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    https://sites.google.com/site/mopedqleak/, Access: 2016-07-15.

  2. 2.

    https://project.inria.fr/quail/, Version: 2.0.

  3. 3.

    http://www.cs.bham.ac.uk/research/projects/infotools/chimp/, Version: 2.1.

References

  1. Biondi, F., Legay, A., Quilbeuf, J.: Comparative analysis of leakage tools on scalable case studies. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 263–281. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  2. Biondi, F., Legay, A., Traonouez, L.-M., Wąsowski, A.: QUAIL: a quantitative security analyzer for imperative code. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 702–707. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  3. Chadha, R., Mathur, U., Schwoon, S.: Computing information flow using symbolic model-checking. In: Raman, V., Suresh, S.P., (eds.) 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS ), vol. 29 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 505–516, Dagstuhl, Germany, Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2014)

    Google Scholar 

  4. Chothia, T., Kawamoto, Y., Novakovic, C., Parker, D.: Probabilistic point-to-point information leakage. In: Proceedings of the 26th IEEE Computer Security Foundations Symposium (CSF 2013), pp. 193–205. IEEE Computer Society, June 2013

    Google Scholar 

  5. Klebanov, V., Manthey, N., Muise, C.: SAT-based analysis and quantification of information flow in programs. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 177–192. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  6. Kroening, D., Tautschnig, M.: CBMC – C bounded model checker. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 389–391. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  7. Smith, G.: On the foundations of quantitative information flow. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 288–302. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Karlsruhe Institute of Technology, Am Fasanengarten 5, 76131, Karlsruhe, Germany

    Alexander Weigl

Authors
  1. Alexander Weigl
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Alexander Weigl .

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università degli Studi di Milano, Crema, Italy

    Giovanni Livraga

  2. University of Skövde , Skövde, Sweden

    Vicenç Torra

  3. University of Urbino , Urbino, Italy

    Alessandro Aldini

  4. IIT National Research Council CNR , Pisa, Italy

    Fabio Martinelli

  5. Technische Universität Darmstadt , Darmstadt, Germany

    Neeraj Suri

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Weigl, A. (2016). Efficient SAT-Based Pre-image Enumeration for Quantitative Information Flow in Programs. In: Livraga, G., Torra, V., Aldini, A., Martinelli, F., Suri, N. (eds) Data Privacy Management and Security Assurance. DPM QASA 2016 2016. Lecture Notes in Computer Science(), vol 9963. Springer, Cham. https://doi.org/10.1007/978-3-319-47072-6_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-47072-6_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-47071-9

  • Online ISBN: 978-3-319-47072-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation