Skip to main content
SpringerLink
Log in

Comparative Analysis of Leakage Tools on Scalable Case Studies

  • Conference paper
  • First Online:
Model Checking Software (SPIN 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9232))

Included in the following conference series:

Abstract

Quantitative security techniques have been proven effective to measure the security of systems against various types of attackers. However, such techniques are often tested against small-scale academic examples.

In this paper we analyze two scalable, real life privacy case studies: the privacy of the energy consumption data of the users of a smart grid network and the secrecy of the voters’ voting preferences with different types of voting protocols.

We contribute a new trace analysis algorithm for leakage calculation in QUAIL. We analyze both case studies with three state-of-the-art information leakage computation tools: LeakWatch, Moped-QLeak, and our tool QUAIL equipped with the new algorithm. We highlight the relative advantages and drawbacks of the tools and compare their usability and effectiveness in analyzing the case studies.

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.

    http://fortiss.org.

  2. 2.

    The files used for our experiments are available at https://project.inria.fr/quail/casestudies/.

  3. 3.

    livinglab.fortiss.org.

References

  1. Alvim, M.S., Chatzikokolakis, K., Palamidessi, C., Smith, G.: Measuring information leakage using generalized gain functions. In: Chong, S. (ed.) CSF, pp. 265–279. IEEE (2012)

    Google Scholar 

  2. Backes, M., Doychev, G., Köpf, B.: Preventing side-channel leaks in web traffic: A formal approach. In: NDSS. The Internet Society (2013)

    Google Scholar 

  3. Biondi, F., Legay, A., Malacaria, P., Wąsowski, A.: Quantifying information leakage of randomized protocols. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 68–87. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  4. Biondi, F., Legay, A., Nielsen, B.F., Malacaria, P., Wasowski, A.: Information leakage of non-terminating processes. In: Raman and Suresh [28], pp. 517–529

    Google Scholar 

  5. 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 

  6. Boreale, M.: Quantifying information leakage in process calculi. Inf. Comput. 207(6), 699–725 (2009)

    Article  MATH  MathSciNet  Google Scholar 

  7. Boreale, M., Buscemi, M.G.: Experimenting with STA, a tool for automatic analysis of security protocols. In: SAC, pp. 281–285. ACM (2002)

    Google Scholar 

  8. Boreale, M., Clark, D., Gorla, D.: A semiring-based trace semantics for processes with applications to information leakage analysis. Math. Struct. Comput. Sci. 25(2), 259–291 (2015)

    Article  MathSciNet  Google Scholar 

  9. Boreale, M., Pampaloni, F.: Quantitative information flow under generic leakage functions and adaptive adversaries. In: Ábrahám, E., Palamidessi, C. (eds.) FORTE 2014. LNCS, vol. 8461, pp. 166–181. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  10. Bytschkow, D., Quilbeuf, J., Igna, G., Ruess, H.: Distributed MILS architectural approach for secure smart grids. In: Cuéllar [15], pp. 16–29

    Google Scholar 

  11. Chadha, R., Mathur, U., Schwoon, S.: Computing information flow using symbolic model-checking. In: Raman and Suresh [28], pp. 505–516

    Google Scholar 

  12. Chothia, T., Guha, A.: A statistical test for information leaks using continuous mutual information. In: CSF, pp. 177–190. IEEE Computer Society (2011)

    Google Scholar 

  13. Chothia, T., Kawamoto, Y., Novakovic, C.: LeakWatch: estimating information leakage from Java programs. In: Kutyłowski, M., Vaidya, J. (eds.) ICAIS 2014, Part II. LNCS, vol. 8713, pp. 219–236. Springer, Heidelberg (2014)

    Google Scholar 

  14. Chothia, T., Kawamoto, Y., Novakovic, C., Parker, D.: Probabilistic point-to-point information leakage. In: CSF, pp. 193–205. IEEE (2013)

    Google Scholar 

  15. Cuéllar, J. (ed.): SmartGridSec 2014. LNCS, vol. 8448. Springer, Heidelberg (2014)

    Google Scholar 

  16. Denning, D.E.: A lattice model of secure information flow. Commun. ACM 19(5), 236–243 (1976)

    Article  MATH  MathSciNet  Google Scholar 

  17. Esparza, J., Kiefer, S., Schwoon, S.: Abstraction refinement with Craig interpolation and symbolic pushdown systems. J. Satisfiability, Boolean Model. Comput. 5, 27–56 (2008). Special Issue on Constraints to Formal Verification

    MathSciNet  Google Scholar 

  18. Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy, pp. 11–20. IEEE Computer Society (1982)

    Google Scholar 

  19. Gray III, J.W.: Toward a mathematical foundation for information flow security. In: IEEE Symposium on Security and Privacy, pp. 21–35 (1991)

    Google Scholar 

  20. Kang, M.G., McCamant, S., Poosankam, P., Song, D.: DTA++: dynamic taint analysis with targeted control-flow propagation. In: NDSS. The Internet Society (2011)

    Google Scholar 

  21. Köpf, B., Mauborgne, L., Ochoa, M.: Automatic quantification of cache side-channels. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 564–580. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  22. Koss, D., Sellmayr, F., Bauereiß, S., Bytschkow, D., Gupta, P.K., Schätz, B.: Establishing a smart grid node architecture and demonstrator in an office environment using the SOA approach. In: SE4SG. ICSE, pp. 8–14. IEEE (2012)

    Google Scholar 

  23. Newsome, J., McCamant, S., Song, D.: Measuring channel capacity to distinguish undue influence. In: Chong, S., Naumann, D.A. (eds.) PLAS. ACM (2009)

    Google Scholar 

  24. Norris, P.: Electoral Engineering: Voting Rules and Political Behavior. Cambridge University Press, Cambridge (2004). Cambridge Studies in Comparative Politics

    Book  Google Scholar 

  25. Phan, Q., Malacaria, P.: Abstract model counting: a novel approach for quantification of information leaks. In: Moriai, S., Jaeger, T., Sakurai, K. (eds.) ASIACCS, pp. 283–292. ACM (2014)

    Google Scholar 

  26. Phan, Q., Malacaria, P., Pasareanu, C.S., d’Amorim, M.: Quantifying information leaks using reliability analysis. In: Rungta, N., Tkachuk, O. (eds.) SPIN, pp. 105–108. ACM (2014)

    Google Scholar 

  27. Phan, Q., Malacaria, P., Tkachuk, O., Pasareanu, C.S.: Symbolic quantitative information flow. ACM SIGSOFT Softw. Eng. Notes 37(6), 1–5 (2012)

    Article  Google Scholar 

  28. Raman, V., Suresh, S.P. (eds.) FSTTCS, vol. 29. LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2014)

    Google Scholar 

  29. Rottondi, C., Fontana, S., Verticale, G.: A privacy-friendly framework for vehicle-to-grid interactions. In: Cuéllar [15], pp. 125–138

    Google Scholar 

  30. 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. Inria, Rennes, France

    Fabrizio Biondi, Axel Legay & Jean Quilbeuf

Authors
  1. Fabrizio Biondi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Axel Legay
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jean Quilbeuf
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Fabrizio Biondi or Jean Quilbeuf .

Editor information

Editors and Affiliations

  1. Stellenbosch University, Matieland, South Africa

    Bernd Fischer

  2. Stellenbosch University, Matieland, South Africa

    Jaco Geldenhuys

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Biondi, F., Legay, A., Quilbeuf, J. (2015). Comparative Analysis of Leakage Tools on Scalable Case Studies. In: Fischer, B., Geldenhuys, J. (eds) Model Checking Software. SPIN 2015. Lecture Notes in Computer Science(), vol 9232. Springer, Cham. https://doi.org/10.1007/978-3-319-23404-5_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-23404-5_17

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-23403-8

  • Online ISBN: 978-3-319-23404-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation