Abstract
This paper concerns the analysis of information leaks in security systems. We address the problem of specifying and analyzing large systems in the (standard) channel model used in quantitative information flow (QIF). We propose several operators which match typical interactions between system components. We explore their algebraic properties with respect to the security-preserving refinement relation defined by Alvim et al. and McIver et al. [1, 2].
We show how the algebra can be used to simplify large system specifications in order to facilitate the computation of information leakage bounds. We demonstrate our results on the specification and analysis of the Crowds Protocol. Finally, we use the algebra to justify a new algorithm to compute leakage bounds for this protocol.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
A complete, formal definition of such bijections can be found in an accompanying technical report [13].
- 2.
As a counter-example, consider channels \(C_{1}= \left( {\begin{matrix} 1 &{} 0 \\ 1 &{} 0 \\ 0 &{} 1 \end{matrix}}\right) \) and \(C_{2}= \left( {\begin{matrix} 1 &{} 0 \\ 0 &{} 1 \\ 0 &{} 1 \end{matrix}} \right) \). Let
and \(g_{id}: \mathcal {X}\times \mathcal {X}\rightarrow [0,1]\) s.t. \(g_{id}(x_1,x_2)=1\) if \(x_1=x_2\) and 0 otherwise. Then, \(V_{g_{id}}[\pi _u \, \rangle \, C_2] \le V_{g_{id}}[\pi _u \, \rangle \, C_1]\), but \(V_{g_{id}}[\pi _u \, \rangle \, C_2 \parallel C_1] > V_{g_{id}}[\pi _u \, \rangle \, C_1 \parallel C_1]\). - 3.
To simplify notation, we assume cascading has precedence over hidden choice, i.e., \(AB{\;{{}_{ p }{\oplus }}\;}CD = (AB) {\;{{}_{ p }{\oplus }}\;}(CD)\).
and References
Alvim, M.S., Chatzikokolakis, K., Palamidessi, C., Smith, G.: Measuring information leakage using generalized gain functions. In: Proceedings of CSF, pp. 265–279 (2012)
McIver, A., Morgan, C., Smith, G., Espinoza, B., Meinicke, L.: Abstract channels and their robust information-leakage ordering. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 83–102. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54792-8_5
Clark, D., Hunt, S., Malacaria, P.: Quantitative information flow, relations and polymorphic types. J. Logic Comput. 18(2), 181–199 (2005)
Köpf, B., Basin, D.A.: An information-theoretic model for adaptive side-channel attacks. In: Proceedings of CCS, pp. 286–296. ACM (2007)
Chatzikokolakis, K., Palamidessi, C., Panangaden, P.: On the Bayes risk in information-hiding protocols. J. Comput. Secur. 16(5), 531–571 (2008)
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). https://doi.org/10.1007/978-3-642-00596-1_21
McIver, A., Meinicke, L., Morgan, C.: Compositional closure for Bayes risk in probabilistic noninterference. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 223–235. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14162-1_19
Boreale, M., Pampaloni, F.: Quantitative information flow under generic leakage functions and adaptive adversaries. Log. Methods Comput. Sci. 11(4) (2015)
Alvim, M.S., Chatzikokolakis, K., McIver, A., Morgan, C., Palamidessi, C., Smith, G.: Axioms for information leakage. In: Proceedings of CSF, pp. 77–92 (2016)
Chaum, D.: The dining cryptographers problem: Unconditional sender and recipient untraceability. J. Cryptol. 1(1), 65–75 (1988)
Alvim, M.S., Chatzikokolakis, K., McIver, A., Morgan, C., Palamidessi, C., Smith, G.: Additive and multiplicative notions of leakage, and their capacities. In: Proceedings of CSF, pp. 308–322. IEEE (2014)
Reiter, M.K., Rubin, A.D.: Crowds: anonymity for web transactions. ACM Trans. Inf. Syst. Secur. 1(1), 66–92 (1998)
Américo, A., Alvim, M.S., McIver, A.: An algebraic approach for reasoning about information flow. CoRR abs/1801.08090 (2018)
Shannon, C.E.: A mathematical theory of communication. Bell Syst. Tech. J. 27(379–423), 625–56 (1948)
Massey, J.L.: Guessing and entropy. In: Proceedings of the IEEE International Symposium on Information Theory, p. 204. IEEE (1994)
Braun, C., Chatzikokolakis, K., Palamidessi, C.: Quantitative notions of leakage for one-try attacks. In: Proceedings of MFPS. ENTCS, vol. 249, pp. 75–91. Elsevier (2009)
Kocher, P.C.: Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems. In: Koblitz, N. (ed.) CRYPTO 1996. LNCS, vol. 1109, pp. 104–113. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-68697-5_9
Brumley, D., Boneh, D.: Remote timing attacks are practical. In: Proceedings of the 12th Conference on USENIX Security Symposium. SSYM 2003, vol. 12, p. 1. USENIX Association, Berkeley (2003)
Nohl, K., Evans, D., Starbug, S., Plötz, H.: Reverse-engineering a cryptographic RFID tag. In: Proceedings of the 17th Conference on Security Symposium. SS 2008, pp. 185–193. USENIX Association, Berkeley (2008)
Warner, S.L.: Randomized response: a survey technique for eliminating evasive answer bias. J. Am. Stat. Assoc. 60(309), 63–69 (1965). PMID: 12261830
Goldschlag, D.M., Reed, M.G., Syverson, P.F.: Hiding routing information. In: Anderson, R. (ed.) IH 1996. LNCS, vol. 1174, pp. 137–150. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61996-8_37
Dingledine, R., Mathewson, N., Syverson, P.F.: Tor: the second-generation onion router. In: Proceedings of the 13th USENIX Security Symposium, pp. 303–320. USENIX (2004)
Strassen, V.: Gaussian elimination is not optimal. Numer. Math. 13(4), 354–356 (1969)
Andrés, M.E., Palamidessi, C., van Rossum, P., Smith, G.: Computing the leakage of information-hiding systems. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 373–389. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12002-2_32
Espinoza, B., Smith, G.: Min-entropy as a resource. Inf. Comput. 226, 57–75 (2013)
Kawamoto, Y., Chatzikokolakis, K., Palamidessi, C.: On the compositionality of quantitative information flow. Log. Methods Comput. Sci. 13(3) (2017)
Engelhardt, K.: A better composition operator for quantitative information flow analyses. In: European Symposium on Research in Computer Security, Proceedings, Part I, pp. 446–463 (2017)
Alvim, M.S., Chatzikokolakis, K., Kawamoto, Y., Palamidessi, C.: Leakage and protocol composition in a game-theoretic perspective. In: Bauer, L., Küsters, R. (eds.) POST 2018. LNCS, vol. 10804, pp. 134–159. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89722-6_6
Acknowledgments
Arthur Américo and Mário S. Alvim are supported by CNPq, CAPES, and FAPEMIG. Annabelle McIver is supported by ARC grant DP140101119.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Américo, A., Alvim, M.S., McIver, A. (2018). An Algebraic Approach for Reasoning About Information Flow. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds) Formal Methods. FM 2018. Lecture Notes in Computer Science(), vol 10951. Springer, Cham. https://doi.org/10.1007/978-3-319-95582-7_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-95582-7_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-95581-0
Online ISBN: 978-3-319-95582-7
eBook Packages: Computer ScienceComputer Science (R0)