Skip to main content

Experiments in Information Flow Analysis

  • Conference paper
  • First Online:
Mathematics of Program Construction (MPC 2019)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11825))

Included in the following conference series:

Abstract

Designing programs that do not leak confidential information continues to be a challenge. Part of the difficulty arises when partial information leaks are inevitable, implying that design interventions can only limit rather than eliminate their impact.

We show, by example, how to gain a better understanding of the consequences of information leaks by modelling what adversaries might be able to do with any leaked information.

Our presentation is based on the theory of Quantitative Information Flow, but takes an experimental approach to explore potential vulnerabilities in program designs. We make use of the tool Kuifje [12] to interpret a small programming language in a probabilistic semantics that supports quantitative information flow analysis.

This research was supported by the Australian Research Council Grant DP140101119.

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

Access this chapter

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.

    Stochastic means that the rows sum to 1, i.e. \(\sum _{y\in \mathcal{Y}}C_{xy}=1\).

  2. 2.

    We assume for convenience that when we write \(p_y\) the terms C, \(\pi \) and y are understood from the context. Notation suited for formal calculation would need to incorporate C and \(\pi \) explicitly.

  3. 3.

    In the traditional analysis Paris only employs this strategy after interviewing approximately N/e candidates. Here we are interested in studying this strategy at each stage of the interviewing procedure.

  4. 4.

    Interestingly the two —although the actions wrt. \(g_2\) and \(g_3\) are different, in the case they are interpreted over the scenario of 6 candidates they dictate the same behaviour. Under the \(g_2\) strategy which becomes operational after interviewing 2 candidates, it is never to appoint candidate 2, but take the very next best. Under the \(g_3\) case (which becomes operational after interviewing three candidates) it is to take candidate 3 if she is the best so far, or if not select the next best.

  5. 5.

    In this case, we imagine that an adversary uses an input gs in order to extract some information. His actions described by \(\mathcal{W}\) are related to what he is able to do in the face of his current uncertainty.

References

  1. Alvim, M.S., Chatzikokolakis, K., McIver, A., Morgan, C., Palamidessi, C., Smith, G.: Additive and multiplicative notions of leakage, and their capacities. In: IEEE 27th Computer Security Foundations Symposium, CSF 2014, Vienna, Austria, 19–22 July 2014, pp. 308–322. IEEE (2014)

    Google Scholar 

  2. Alvim, M.S., Chatzikokolakis, K., Palamidessi, C., Smith, G.: Measuring information leakage using generalized gain functions. In: Proceedings 25th IEEE Computer Security Foundations Symposium (CSF 2012), pp. 265–279, June 2012

    Google Scholar 

  3. Clark, D., Hunt, S., Malacaria, P.: Quantitative analysis of the leakage of confidential data. Electr. Notes Theor. Comput. Sci. 59(3), 238–251 (2001)

    Article  Google Scholar 

  4. Clark, D., Hunt, S., Malacaria, P.: Quantified interference for a while language. Electr. Notes Theor. Comput. Sci. 112, 149–166 (2005)

    Article  Google Scholar 

  5. Clarkson, M.R., Myers, A.C., Schneider, F.B.: Belief in information flow. In: 18th IEEE Computer Security Foundations Workshop, (CSFW-18 2005), Aix-en-Provence, France, 20–22 June 2005, pp. 31–45 (2005)

    Google Scholar 

  6. Freeman, P.R.: The secretary problem and its extensions: a review. Int. Stat. Rev. 51, 189–206 (1983)

    Article  MathSciNet  Google Scholar 

  7. Gardner, M.: Mathematical games. Sci. Am. 202(2), 178–179 (1960)

    Article  Google Scholar 

  8. Gardner, M.: Mathematical games. Sci. Am. 202(3), 152 (1960)

    Article  Google Scholar 

  9. Gilbert, J., Mosteller, F.: Recognising the maximum of a sequence. J. Am. Stat. Assoc. 61, 35–73 (1966)

    Article  Google Scholar 

  10. Giry, M.: A categorical approach to probability theory. In: Banaschewski, B. (ed.) Categorical Aspects of Topology and Analysis. LNM, vol. 915, pp. 68–85. Springer, Heidelberg (1982). https://doi.org/10.1007/BFb0092872

    Chapter  Google Scholar 

  11. Jacobs, B., Zanasi, F.: A predicate/state transformer semantics for Bayesian learning. Electr. Notes Theor. Comput. Sci. 325, 185–200 (2016)

    Article  MathSciNet  Google Scholar 

  12. Morgan, C., Gibbons, J., Mciver, A., Schrijvers, T.: Quantitative information flow with monads in haskell. In: Foundations of Probabilistic Programming. CUP (2019, to appear)

    Google Scholar 

  13. Mardziel, P., Alvim, M.S., Hicks, M.W., Clarkson, M.R.: Quantifying information flow for dynamic secrets. In: 2014 IEEE Symposium on Security and Privacy, SP 2014, Berkeley, CA, USA, 18–21 May 2014, pp. 540–555 (2014)

    Google Scholar 

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

    Chapter  Google Scholar 

  15. McIver, A., Morgan, C., Rabehaja, T.: Abstract hidden markov models: a monadic account of quantitative information flow. In Proceedings LiCS 2015 (2015)

    Google Scholar 

  16. Morgan, C.: The shadow knows: refinement of ignorance in sequential programs. Sci. Comput. Program. 74(8), 629–653 (2009). Treats Oblivious Transfer

    Article  Google Scholar 

  17. Shannon, C.E.: A mathematical theory of communication. Bell Syst. Tech. J. 27(379–423), 623–656 (1948)

    Article  MathSciNet  Google Scholar 

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

    Chapter  Google Scholar 

Download references

Acknowledgements

I thank Tom Schrijvers for having the idea of embedding these ideas in Haskell, based on Carroll Morgan’s talk at IFIP WG2.1 in Vermont, and for carrying it out to produce the tool Kuifje. Together with Jeremy Gibbons all four of us wrote the first paper devoted to it [12]. (It was Jeremy who suggested the name “Kuifje”, the Dutch name for TinTin—and hence his “QIF”.) Carroll Morgan translated the example programs into Kuifje.

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Annabelle McIver .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

McIver, A. (2019). Experiments in Information Flow Analysis. In: Hutton, G. (eds) Mathematics of Program Construction. MPC 2019. Lecture Notes in Computer Science(), vol 11825. Springer, Cham. https://doi.org/10.1007/978-3-030-33636-3_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-33636-3_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-33635-6

  • Online ISBN: 978-3-030-33636-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics