Advertisement

Confidentiality for Multithreaded Programs via Bisimulation

  • Andrei Sabelfeld
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2890)

Abstract

Bisimulation has been a popular foundation for characterizing the confidentiality properties of concurrent programs. However, because a variety of bisimulation definitions are available in the literature, it is often difficult to pin down the “right” definition for modeling a particular attacker. Focusing on timing- and probability-sensitive confidentiality for shared-memory multithreaded programs, we clarify the relation between different kinds of bisimulation by proving inclusion results. As a consequence, we derive the relationship between scheduler-specific, scheduler-independent, and strong confidentiality definitions. A key result justifying strong confidentiality is that it is the most accurate (largest) compositional indistinguishability-based confidentiality property that implies scheduler-independent confidentiality.

Keywords

Security Property Parallel Composition Process Algebra Concurrent Program Strong Security 
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.
    Agat, J.: Transforming out timing leaks. In: Proc. ACM Symp. on Principles of Programming Languages, January 2000, pp. 40–53 (2000)Google Scholar
  2. 2.
    Aldini, A.: Probabilistic information flow in a process algebra. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 152–168. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  3. 3.
    Aldini, A., Bravetti, M., Gorrieri, R.: A process algebraic approach for the analysis of probabilistic non-interference. Technical Report UBLCS-2002-02, University of Bologna, Bologna, Italy (2002)Google Scholar
  4. 4.
    Boudol, G., Castellani, I.: Noninterference for concurrent programs. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 382–395. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  5. 5.
    Cerans, K.: Decidability of bisimulation equivalences for parallel timer processes. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 302–315. Springer, Heidelberg (1992)Google Scholar
  6. 6.
    Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Comm. of the ACM 20(7), 504–513 (1977)zbMATHCrossRefGoogle Scholar
  7. 7.
    Felten, E.W., Schneider, M.A.: Timing attacks on web privacy. In: ACM Conference on Computer and Communications Security, pp. 25–32 (2000)Google Scholar
  8. 8.
    Focardi, R., Gorrieri, R.: A classification of security properties for process algebras. J. Computer Security 3(1), 5–33 (1995)Google Scholar
  9. 9.
    Focardi, R., Gorrieri, R., Martinelli, F.: Information flow analysis in a discretetime process algebra. In: Proc. IEEE Computer Security Foundations Workshop, July 2000, pp. 170–184 (2000)Google Scholar
  10. 10.
    Focardi, R., Gorrieri, R., Martinelli, F.: Real-time information flow analysis. IEEE J. Selected Areas in Communications 21(1), 20–35 (2003)CrossRefGoogle Scholar
  11. 11.
    Giambiagi, P., Dam, M.: On the secure implementation of security protocols. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 144–158. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  12. 12.
    Goguen, J.A., Meseguer, J.: Security policies and security models. In: Proc. IEEE Symp. on Security and Privacy, April 1982, pp. 11–20 (1982)Google Scholar
  13. 13.
    Gray III., J.W.: Probabilistic interference. In: Proc. IEEE Symp. on Security and Privacy, May 1990, pp. 170–179 (1990)Google Scholar
  14. 14.
    Honda, K., Yoshida, N.: A uniform type structure for secure information flow. In: Proc. ACM Symp. on Principles of Programming Languages, January 2002, pp. 81–92 (2002)Google Scholar
  15. 15.
    Jürjens, J.: Secure information flow for concurrent processes. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 395–409. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  16. 16.
    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)Google Scholar
  17. 17.
    Kozen, D.: Language-based security. In: Kutyłowski, M., Wierzbicki, T., Pacholski, L. (eds.) MFCS 1999. LNCS, vol. 1672, pp. 284–298. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  18. 18.
    Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Information and Computation 94(1), 1–28 (1991)zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    Mantel, H.: On the composition of secure systems. In: Proc. IEEE Symp. on Security and Privacy, May 2002, pp. 81–94 (2002)Google Scholar
  20. 20.
    Mantel, H., Sabelfeld, A.: A unifying approach to the security of distributed and multi-threaded programs. J. Computer Security (2003) (to appear)Google Scholar
  21. 21.
    McCullough, D.: Specifications for multi-level security and hook-up property. In: Proc. IEEE Symp. on Security and Privacy, April 1987, pp. 161–166 (1987)Google Scholar
  22. 22.
    McLean, J.: Security models and information flow. In: Proc. IEEE Symp. on Security and Privacy, May 1990, pp. 180–187 (1990)Google Scholar
  23. 23.
    McLean, J.: A general theory of composition for trace sets closed under selective interleaving functions. In: Proc. IEEE Symp. on Security and Privacy, May 1994, pp. 79–93 (1994)Google Scholar
  24. 24.
    Ryan, P., Schneider, S.: Composing and decomposing systems under security properties. In: Proc. IEEE Computer Security Foundations Workshop, March 1995, pp. 9–15 (1995)Google Scholar
  25. 25.
    Ryan, P., Schneider, S.: Process algebra and non-interference. In: Proc. IEEE Computer Security Foundations Workshop, June 1999, pp. 214–227 (1999)Google Scholar
  26. 26.
    Sabelfeld, A.: The impact of synchronisation on secure information flow in concurrent programs. In: Bjørner, D., Broy, M., Zamulin, A.V. (eds.) PSI 2001. LNCS, vol. 2244, pp. 227–241. Springer, Heidelberg (2001)Google Scholar
  27. 27.
    Sabelfeld, A., Mantel, H.: Static confidentiality enforcement for distributed programs. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 376–394. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  28. 28.
    Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Selected Areas in Communications 21(1), 5–19 (2003)CrossRefGoogle Scholar
  29. 29.
    Sabelfeld, A., Sands, D.: Probabilistic noninterference for multi-threaded programs. In: Proc. IEEE Computer Security Foundations Workshop, July 2000, pp. 200–214 (2000)Google Scholar
  30. 30.
    Sabelfeld, A., Sands, D.: A per model of secure information flow in sequential programs. Higher Order and Symbolic Computation 14(1), 59–91 (2001)zbMATHCrossRefGoogle Scholar
  31. 31.
    Schneider, F.B., Morrisett, G., Harper, R.: A language-based approach to security. In: Wilhelm, R. (ed.) Informatics: 10 Years Back, 10 Years Ahead. LNCS, vol. 2000, pp. 86–101. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  32. 32.
    Schneider, S.: May testing, non-interference, and compositionality. Technical Report CSD-TR-00-02, Royal Holloway, University of London (January 2001)Google Scholar
  33. 33.
    Smith, G.: A new type system for secure information flow. In: Proc. IEEE Computer Security Foundations Workshop, June 2001, pp. 115–125 (2001)Google Scholar
  34. 34.
    Volpano, D., Smith, G.: Verifying secrets and relative secrecy. In: Proc. ACM Symp. on Principles of Programming Languages, January 2000, pp. 268–276 (2000)Google Scholar
  35. 35.
    Volpano, D., Smith, G., Irvine, C.: A sound type system for secure flow analysis. J. Computer Security 4(3), 167–187 (1996)Google Scholar
  36. 36.
    Wang, Y.: Real-time behaviour of asynchronous agents. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 502–520. Springer, Heidelberg (1990)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Andrei Sabelfeld
    • 1
  1. 1.Department of Computer ScienceCornell UniversityIthacaUSA

Personalised recommendations