Advertisement

Adversaries and Information Leaks (Tutorial)

  • Geoffrey Smith
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4912)

Abstract

Secure information flow analysis aims to prevent programs from leaking their H (high) inputs to their L (low) outputs. A major challenge in this area is to relax the standard noninterference properties to allow “small” leaks, while still preserving security. In this tutorial paper, we consider three instances of this theme. First, we consider a type system that enforces the usual Denning restrictions, except that it specifies that encrypting a H plaintext yields a L ciphertext. We argue that this type system ensures security, assuming strong encryption, by giving a reduction that maps a noninterference adversary (which tries to guess which of two H inputs was used, given the L outputs) to an IND-CPA adversary (which tries to guess which of two plaintexts are encrypted, given the ciphertext). Second, we explore termination leaks in probabilistic programs when typed under the Denning restrictions. Using a notion of probabilistic simulation, we show that such programs satisfy an approximate noninterference property, provided that their probability of nontermination is small. Third, we consider quantitative information flow, which aims to measure the amount of information leaked. We argue that the common information-theoretic measures in the literature are unsuitable, because these measures fail to distinguish between programs that are wildly different from the point of view of an adversary trying to guess the H input.

Keywords

Type System Secure Information Shannon Entropy Information Leak Public Output 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Sabelfeld, A., Myers, A.C.: Language-based information flow security. IEEE Journal on Selected Areas in Communications 21(1), 5–19 (2003)CrossRefGoogle Scholar
  2. 2.
    Denning, D., Denning, P.: Certification of programs for secure information flow. Communications of the ACM 20(7), 504–513 (1977)zbMATHCrossRefGoogle Scholar
  3. 3.
    Volpano, D., Smith, G., Irvine, C.: A sound type system for secure flow analysis. Journal of Computer Security 4(2,3), 167–187 (1996)Google Scholar
  4. 4.
    Smith, G., Alpízar, R.: Secure information flow with random assignment and encryption. In: Proc. 4th ACM Workshop on Formal Methods in Security Engineering, Fairfax, Virginia, pp. 33–43 (November 2006)Google Scholar
  5. 5.
    Smith, G., Alpízar, R.: Fast probabilistic simulation, nontermination, and secure information flow. In: Proc. 2007 ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, San Diego, California, pp. 67–71 (June 2007)Google Scholar
  6. 6.
    Bellare, M., Rogaway, P.: Introduction to modern cryptography (2005), http://www-cse.ucsd.edu/users/mihir/cse207/classnotes.html
  7. 7.
    Courant, J., Ene, C., Lakhnech, Y.: Computationally sound typing for non-interference: The case of deterministic encryption. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 364–375. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  8. 8.
    Laud, P.: Semantics and program analysis of computationally secure information flow. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 77–91. Springer, Heidelberg (2001)Google Scholar
  9. 9.
    Laud, P.: Handling encryption in an analysis for secure information flow. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 159–173. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  10. 10.
    Laud, P., Vene, V.: A type system for computationally secure information flow. In: Liśkiewicz, M., Reischuk, R. (eds.) FCT 2005. LNCS, vol. 3623, pp. 365–377. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  11. 11.
    Askarov, A., Hedin, D., Sabelfeld, A.: Cryptographically-masked flows. In: Proceedings of the 13th International Static Analysis Symposium, Seoul, Korea, pp. 353–369 (2006)Google Scholar
  12. 12.
    Laud, P.: On the computational soundness of cryptographically masked flows. In: Proceedings 35th Symposium on Principles of Programming Languages, San Francisco, California (January 2008)Google Scholar
  13. 13.
    Vaughan, J., Zdancewic, S.: A cryptographic decentralized label model. In: IEEE Symposium on Security and Privacy, Oakland, California, pp. 192–206 (2007)Google Scholar
  14. 14.
    Fournet, C., Rezk, T.: Cryptographically sound implementations for typed information-flow security. In: Proceedings 35th Symposium on Principles of Programming Languages, San Francisco, California (January 2008)Google Scholar
  15. 15.
    Backes, M., Pfitzmann, B.: Relating symbolic and cryptographic secrecy. In: Proceeding 26th IEEE Symposium on Security and Privacy, Oakland, California (2005)Google Scholar
  16. 16.
    Laud, P.: Secrecy types for a simulatable cryptographic library. In: Proceedings 12th CCS (ACM Conference on Computer and Communications Security), pp. 26–35 (2005)Google Scholar
  17. 17.
    Feller, W.: An Introduction to Probability Theory and Its Applications, 3rd edn., vol. I. John Wiley & Sons, Inc., Chichester (1968)zbMATHGoogle Scholar
  18. 18.
    Sabelfeld, A., Sands, D.: Probabilistic noninterference for multi-threaded programs. In: Proceedings 13th IEEE Computer Security Foundations Workshop, Cambridge, UK, pp. 200–214 (July 2000)Google Scholar
  19. 19.
    Jonsson, B., Larsen, K.: Specification and refinement of probabilistic processes. In: Proc. 6th IEEE Symposium on Logic in Computer Science, pp. 266–277 (1991)Google Scholar
  20. 20.
    Baier, C., Katoen, J.-P., Hermanns, H., Wolf, V.: Comparative branching-time semantics for Markov chains. Information and Computation 200(2), 149–214 (2005)zbMATHCrossRefMathSciNetGoogle Scholar
  21. 21.
    Di Pierro, A., Hankin, C., Wiklicky, H.: Approximate non-interference. In: Proceedings 15th IEEE Computer Security Foundations Workshop, Cape Breton, Nova Scotia, Canada, pp. 1–17 (June 2002)Google Scholar
  22. 22.
    Clark, D., Hunt, S., Malacaria, P.: Quantitative analysis of the leakage of confidential data. Electronic Notes in Theoretical Computer Science 59(3) (2002)Google Scholar
  23. 23.
    Clark, D., Hunt, S., Malacaria, P.: Quantitative information flow, relations and polymorphic types. Journal of Logic and Computation 18(2), 181–199 (2005)CrossRefMathSciNetGoogle Scholar
  24. 24.
    Malacaria, P.: Assessing security threats of looping constructs. In: Proceedings 34th Symposium on Principles of Programming Languages, Nice, France, pp. 225–235 (January 2007)Google Scholar
  25. 25.
    Köpf, B., Basin, D.: An information-theoretic model for adaptive side-channel attacks. In: Proceedings 14th ACM Conference on Computer and Communications Security, Alexandria, Virginia (2007)Google Scholar
  26. 26.
    Clarkson, M., Myers, A., Schneider, F.: Belief in information flow. In: Proceedings 18th IEEE Computer Security Foundations Workshop, Aix-en-Provence, France, pp. 31–45 (June 2005)Google Scholar
  27. 27.
    Lowe, G.: Quantifying information flow. In: Proceedings 15th IEEE Computer Security Foundations Workshop, Cape Breton, Nova Scotia, Canada, pp. 18–31 (June 2002)Google Scholar
  28. 28.
    Chatzikokolakis, K., Palamidessi, C., Panangaden, P.: Anonymity protocols as noisy channels. Information and Computation (to appear, 2008)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Geoffrey Smith
    • 1
  1. 1.School of Computing and Information SciencesFlorida International UniversityMiamiUSA

Personalised recommendations