Skip to main content

2016 | OriginalPaper | Buchkapitel

Hybrid Statistical Estimation of Mutual Information for Quantifying Information Flow

verfasst von : Yusuke Kawamoto, Fabrizio Biondi, Axel Legay

Erschienen in: FM 2016: Formal Methods

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Analysis of a probabilistic system often requires to learn the joint probability distribution of its random variables. The computation of the exact distribution is usually an exhaustive precise analysis on all executions of the system. To avoid the high computational cost of such an exhaustive search, statistical analysis has been studied to efficiently obtain approximate estimates by analyzing only a small but representative subset of the system’s behavior. In this paper we propose a hybrid statistical estimation method that combines precise and statistical analyses to estimate mutual information and its confidence interval. We show how to combine the analyses on different components of the system with different precision to obtain an estimate for the whole system. The new method performs weighted statistical analysis with different sample sizes over different components and dynamically finds their optimal sample sizes. Moreover it can reduce sample sizes by using prior knowledge about systems and a new abstraction-then-sampling technique based on qualitative analysis. We show the new method outperforms the state of the art in quantifying information leakage.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Literatur
2.
Zurück zum Zitat Backes, M., Köpf, B., Rybalchenko, A.: 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, pp. 141–153. IEEE Computer Society (2009) Backes, M., Köpf, B., Rybalchenko, A.: 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, pp. 141–153. IEEE Computer Society (2009)
3.
Zurück zum Zitat Barbot, B., Haddad, S., Picaronny, C.: Coupling and importance sampling for statistical model checking. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 331–346. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28756-5_23 CrossRef Barbot, B., Haddad, S., Picaronny, C.: Coupling and importance sampling for statistical model checking. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 331–346. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-28756-5_​23 CrossRef
4.
Zurück zum Zitat Barthe, G., Köpf, B.: Information-theoretic bounds for differentially private mechanisms. In: Proceedings of CSF, pp. 191–204. IEEE (2011) Barthe, G., Köpf, B.: Information-theoretic bounds for differentially private mechanisms. In: Proceedings of CSF, pp. 191–204. IEEE (2011)
5.
Zurück zum Zitat Biondi, F., Legay, A., Malacaria, P., Wasowski, A.: Quantifying information leakage of randomized protocols. Theor. Comput. Sci. 597, 62–87 (2015)MathSciNetCrossRefMATH Biondi, F., Legay, A., Malacaria, P., Wasowski, A.: Quantifying information leakage of randomized protocols. Theor. Comput. Sci. 597, 62–87 (2015)MathSciNetCrossRefMATH
7.
Zurück zum Zitat 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). doi:10.1007/978-3-642-39799-8_49 CrossRef 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). doi:10.​1007/​978-3-642-39799-8_​49 CrossRef
8.
Zurück zum Zitat Boreale, M., Paolini, M.: On formally bounding information leakage by statistical estimation. In: Chow, S.S.M., Camenisch, J., Hui, L.C.K., Yiu, S.M. (eds.) ISC 2014. LNCS, vol. 8783, pp. 216–236. Springer, Heidelberg (2014). doi:10.1007/978-3-319-13257-0_13 Boreale, M., Paolini, M.: On formally bounding information leakage by statistical estimation. In: Chow, S.S.M., Camenisch, J., Hui, L.C.K., Yiu, S.M. (eds.) ISC 2014. LNCS, vol. 8783, pp. 216–236. Springer, Heidelberg (2014). doi:10.​1007/​978-3-319-13257-0_​13
9.
Zurück zum Zitat Brillinger, D.R.: Some data analysis using mutual information. Braz. J. Probab. Stat. 18(6), 163–183 (2004)MathSciNetMATH Brillinger, D.R.: Some data analysis using mutual information. Braz. J. Probab. Stat. 18(6), 163–183 (2004)MathSciNetMATH
10.
Zurück zum Zitat Chadha, R., Mathur, U., Schwoon, S.: Computing information flow using symbolic model-checking. In: Raman, V., Suresh, S.P. (eds.) FSTTCS 2014. Proceedings. LIPIcs, vol. 29, pp. 505–516. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2014) Chadha, R., Mathur, U., Schwoon, S.: Computing information flow using symbolic model-checking. In: Raman, V., Suresh, S.P. (eds.) FSTTCS 2014. Proceedings. LIPIcs, vol. 29, pp. 505–516. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2014)
11.
Zurück zum Zitat Chakraborty, S., Fremont, D.J., Meel, K.S., Seshia, S.A., Vardi, M.Y.: On parallel scalable uniform SAT witness generation. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 304–319. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_25 Chakraborty, S., Fremont, D.J., Meel, K.S., Seshia, S.A., Vardi, M.Y.: On parallel scalable uniform SAT witness generation. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 304–319. Springer, Heidelberg (2015). doi:10.​1007/​978-3-662-46681-0_​25
13.
Zurück zum Zitat Chatzikokolakis, K., Chothia, T., Guha, A.: Statistical measurement of information leakage. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 390–404. Springer, Heidelberg (2010). doi:10.1007/978-3-642-12002-2_33 CrossRef Chatzikokolakis, K., Chothia, T., Guha, A.: Statistical measurement of information leakage. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 390–404. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-12002-2_​33 CrossRef
14.
Zurück zum Zitat Chatzikokolakis, K., Palamidessi, C., Panangaden, P.: Anonymity protocols as noisy channels. Inf. Comp. 206(2–4), 378–401 (2008)MathSciNetCrossRefMATH Chatzikokolakis, K., Palamidessi, C., Panangaden, P.: Anonymity protocols as noisy channels. Inf. Comp. 206(2–4), 378–401 (2008)MathSciNetCrossRefMATH
15.
Zurück zum Zitat Chaum, D.: The dining cryptographers problem: unconditional sender and recipient untraceability. J. Cryptol. 1, 65–75 (1988)MathSciNetCrossRefMATH Chaum, D.: The dining cryptographers problem: unconditional sender and recipient untraceability. J. Cryptol. 1, 65–75 (1988)MathSciNetCrossRefMATH
19.
20.
Zurück zum Zitat Chothia, T., Kawamoto, Y., Novakovic, C.: LeakWatch: estimating information leakage from java programs. In: Kutyłowski, M., Vaidya, J. (eds.) ESORICS 2014. LNCS, vol. 8713, pp. 219–236. Springer, Heidelberg (2014). doi:10.1007/978-3-319-11212-1_13 Chothia, T., Kawamoto, Y., Novakovic, C.: LeakWatch: estimating information leakage from java programs. In: Kutyłowski, M., Vaidya, J. (eds.) ESORICS 2014. LNCS, vol. 8713, pp. 219–236. Springer, Heidelberg (2014). doi:10.​1007/​978-3-319-11212-1_​13
21.
Zurück zum Zitat Chothia, T., Kawamoto, Y., Novakovic, C., Parker, D.: Probabilistic point-to-point information leakage. In: Proceedings of CSF 2013, pp. 193–205. IEEE (2013) Chothia, T., Kawamoto, Y., Novakovic, C., Parker, D.: Probabilistic point-to-point information leakage. In: Proceedings of CSF 2013, pp. 193–205. IEEE (2013)
22.
Zurück zum Zitat Clark, D., Hunt, S., Malacaria, P.: Quantitative analysis of the leakage of confidential data. Electr. Notes Theor. Comput. Sci. 59(3), 238–251 (2001)CrossRef Clark, D., Hunt, S., Malacaria, P.: Quantitative analysis of the leakage of confidential data. Electr. Notes Theor. Comput. Sci. 59(3), 238–251 (2001)CrossRef
23.
Zurück zum Zitat Clark, D., Hunt, S., Malacaria, P.: A static analysis for quantifying information flow in a simple imperative language. J. Comput. Secur. 15(3), 321–371 (2007)CrossRef Clark, D., Hunt, S., Malacaria, P.: A static analysis for quantifying information flow in a simple imperative language. J. Comput. Secur. 15(3), 321–371 (2007)CrossRef
24.
25.
Zurück zum Zitat Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157–1210 (2010)CrossRef Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157–1210 (2010)CrossRef
26.
Zurück zum Zitat Cover, T.M., Thomas, J.A.: Elements of Information Theory, 2nd edn. A Wiley-Interscience publication, Wiley, New York (2006)MATH Cover, T.M., Thomas, J.A.: Elements of Information Theory, 2nd edn. A Wiley-Interscience publication, Wiley, New York (2006)MATH
30.
Zurück zum Zitat Fremont, D.J., Seshia, S.A.: Speeding up SMT-based quantitative program analysis. In: Rümmer, P., Wintersteiger, C.M. (eds.) SMT 2014. Proceedings. CEUR Workshop Proceedings, vol. 1163, pp. 3–13. CEUR-WS.org (2014) Fremont, D.J., Seshia, S.A.: Speeding up SMT-based quantitative program analysis. In: Rümmer, P., Wintersteiger, C.M. (eds.) SMT 2014. Proceedings. CEUR Workshop Proceedings, vol. 1163, pp. 3–13. CEUR-WS.org (2014)
31.
Zurück zum Zitat Gallager, R.G.: Information Theory and Reliable Communication. Wiley, New York (1968)MATH Gallager, R.G.: Information Theory and Reliable Communication. Wiley, New York (1968)MATH
32.
Zurück zum Zitat Gray, J.W.: Toward a mathematical foundation for information flow security. In: IEEE Symposium on Security and Privacy, pp. 21–35 (1991) Gray, J.W.: Toward a mathematical foundation for information flow security. In: IEEE Symposium on Security and Privacy, pp. 21–35 (1991)
33.
Zurück zum Zitat Jensen, F.V.: Introduction to Bayesian Networks, 1st edn. Springer, Secaucus (1996) Jensen, F.V.: Introduction to Bayesian Networks, 1st edn. Springer, Secaucus (1996)
34.
Zurück zum Zitat Kang, M.G., McCamant, S., Poosankam, P., Song, D.: DTA++: dynamic taint analysis with targeted control-flow propagation. In: Proceedings of NDSS 2011. The Internet Society (2011) Kang, M.G., McCamant, S., Poosankam, P., Song, D.: DTA++: dynamic taint analysis with targeted control-flow propagation. In: Proceedings of NDSS 2011. The Internet Society (2011)
36.
Zurück zum Zitat Kawamoto, Y., Chatzikokolakis, K., Palamidessi, C.: Compositionality results for quantitative information flow. In: Norman, G., Sanders, W. (eds.) QEST 2014. LNCS, vol. 8657, pp. 368–383. Springer, Heidelberg (2014). doi:10.1007/978-3-319-10696-0_28 Kawamoto, Y., Chatzikokolakis, K., Palamidessi, C.: Compositionality results for quantitative information flow. In: Norman, G., Sanders, W. (eds.) QEST 2014. LNCS, vol. 8657, pp. 368–383. Springer, Heidelberg (2014). doi:10.​1007/​978-3-319-10696-0_​28
37.
Zurück zum Zitat Kawamoto, Y., Given-Wilson, T.: Quantitative information flow for scheduler-dependent systems. In: Proceedings of QAPL 2015, vol. 194, pp. 48–62 (2015) Kawamoto, Y., Given-Wilson, T.: Quantitative information flow for scheduler-dependent systems. In: Proceedings of QAPL 2015, vol. 194, pp. 48–62 (2015)
38.
Zurück zum Zitat Köpf, B., Basin, D.A.: An information-theoretic model for adaptive side-channel attacks. In: Proceedings of CCS, pp. 286–296. ACM (2007) Köpf, B., Basin, D.A.: An information-theoretic model for adaptive side-channel attacks. In: Proceedings of CCS, pp. 286–296. ACM (2007)
39.
Zurück zum Zitat Köpf, B., Rybalchenko, A.: Approximation and randomization for quantitative information-flow analysis. In: Proceedings CSF 2010, pp. 3–14. IEEE Computer Society (2010) Köpf, B., Rybalchenko, A.: Approximation and randomization for quantitative information-flow analysis. In: Proceedings CSF 2010, pp. 3–14. IEEE Computer Society (2010)
40.
Zurück zum Zitat Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 122–135. Springer, Heidelberg (2010). doi:10.1007/978-3-642-16612-9_11 CrossRef Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 122–135. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-16612-9_​11 CrossRef
41.
Zurück zum Zitat MacKay, D.J.C.: Information Theory, Inference & Learning Algorithms. Cambridge University Press, New York (2002) MacKay, D.J.C.: Information Theory, Inference & Learning Algorithms. Cambridge University Press, New York (2002)
42.
Zurück zum Zitat McCamant, S., Ernst, M.D.: Quantitative information flow as network flow capacity. In: Gupta, R., Amarasinghe, S.P. (eds.) Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, 7–13 June 2008, pp. 193–205. ACM (2008) McCamant, S., Ernst, M.D.: Quantitative information flow as network flow capacity. In: Gupta, R., Amarasinghe, S.P. (eds.) Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, 7–13 June 2008, pp. 193–205. ACM (2008)
43.
Zurück zum Zitat Moddemeijer, R.: On estimation of entropy and mutual information of continuous distributions. Sig. Process. 16, 233–248 (1989)MathSciNetCrossRef Moddemeijer, R.: On estimation of entropy and mutual information of continuous distributions. Sig. Process. 16, 233–248 (1989)MathSciNetCrossRef
44.
Zurück zum Zitat Newsome, J., McCamant, S., Song, D.: Measuring channel capacity to distinguish undue influence. In: Chong, S., Naumann, D.A. (eds.) Proceedings of the 2009 Workshop on Programming Languages and Analysis for Security, PLAS 2009, Dublin, Ireland, 15–21 June 2009, pp. 73–85. ACM (2009) Newsome, J., McCamant, S., Song, D.: Measuring channel capacity to distinguish undue influence. In: Chong, S., Naumann, D.A. (eds.) Proceedings of the 2009 Workshop on Programming Languages and Analysis for Security, PLAS 2009, Dublin, Ireland, 15–21 June 2009, pp. 73–85. ACM (2009)
45.
Zurück zum Zitat Phan, Q., Malacaria, P.: Abstract model counting: a novel approach for quantification of information leaks. In: Moriai, S., Jaeger, T., Sakurai, K. (eds.) Proceedings of AsiaCCS 2014, pp. 283–292. ACM (2014) Phan, Q., Malacaria, P.: Abstract model counting: a novel approach for quantification of information leaks. In: Moriai, S., Jaeger, T., Sakurai, K. (eds.) Proceedings of AsiaCCS 2014, pp. 283–292. ACM (2014)
46.
Zurück zum Zitat Phan, Q., Malacaria, P., Pasareanu, C.S., d’Amorim, M.: Quantifying information leaks using reliability analysis. In: Rungta, N., Tkachuk, O. (eds.) Proceedings of SPIN 2014, pp. 105–108. ACM (2014) Phan, Q., Malacaria, P., Pasareanu, C.S., d’Amorim, M.: Quantifying information leaks using reliability analysis. In: Rungta, N., Tkachuk, O. (eds.) Proceedings of SPIN 2014, pp. 105–108. ACM (2014)
49.
Zurück zum Zitat Wilde, M.M.: Quantum Information Theory, 1st edn. Cambridge University Press, New York (2013)CrossRefMATH Wilde, M.M.: Quantum Information Theory, 1st edn. Cambridge University Press, New York (2013)CrossRefMATH
50.
Zurück zum Zitat Yasuoka, H., Terauchi, T.: Quantitative information flow as safety and liveness hyperproperties. Theor. Comput. Sci. 538, 167–182 (2014)MathSciNetCrossRefMATH Yasuoka, H., Terauchi, T.: Quantitative information flow as safety and liveness hyperproperties. Theor. Comput. Sci. 538, 167–182 (2014)MathSciNetCrossRefMATH
Metadaten
Titel
Hybrid Statistical Estimation of Mutual Information for Quantifying Information Flow
verfasst von
Yusuke Kawamoto
Fabrizio Biondi
Axel Legay
Copyright-Jahr
2016
DOI
https://doi.org/10.1007/978-3-319-48989-6_25