Skip to main content
SpringerLink
Log in

Confidentiality for Probabilistic Multi-threaded Programs and Its Verification

  • Conference paper
Engineering Secure Software and Systems (ESSoS 2013)

Part of the book series: Lecture Notes in Computer Science ((LNSC,volume 7781))

Included in the following conference series:

Abstract

Confidentiality is an important concern in today’s information society: electronic payment and personal data should be protected appropriately. This holds in particular for multi-threaded applications, which are generally seen the future of high-performance computing. Multi-threading poses new challenges to data protection, in particular, data races may be exploited in security attacks. Also, the role of the scheduler is seminal in the multi-threaded context.

This paper proposes a new notion of confidentiality for probabilistic and non-probabilistic multi-threaded programs, formalized as scheduler-specific probabilistic observational determinism (SSPOD), together with verification methods. Essentially, SSPOD ensures that no information about the private data can be derived either from the public data, or from the probabilities of the public data being changed. Moreover, SSPOD explicitly depends on a given (class of) schedulers.

Formally, this is expressed by using two conditions: (i) each publicly visible variable individually behaves deterministically with probability 1, and (ii) for every trace considering all publicly visible variables, there always exists a matching trace with equal probability. We verify these conditions by a clever combination of new and existing algorithms over probabilistic Kripke structures.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 72.00
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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aho, A.V., Hopcroft, J.E.: The Design and Analysis of Computer Algorithms, 1st edn. Addison-Wesley (1974)

    Google Scholar 

  2. Alvim, M.S., Andrés, M.E., Chatzikokolakis, K., Palamidessi, C.: On the Relation between Differential Privacy and Quantitative Information Flow. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol. 6756, pp. 60–76. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  3. Alvim, M.S., Andrés, M.E., Chatzikokolakis, K., Palamidessi, C.: Quantitative Information Flow and Applications to Differential Privacy. In: Aldini, A., Gorrieri, R. (eds.) FOSAD VI 2011. LNCS, vol. 6858, pp. 211–230. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  4. Andres, M.E., Palamidessi, C., Sokolova, A., Van Rossum, P.: Information hiding in probabilistic concurrent systems. Journal of Theoretical Computer Science 412(28), 3072–3089 (2011)

    Article  MATH  Google Scholar 

  5. Baier, C., Kwiatkowska, M.: On the verification of qualitative properties of probabilistic processes under fairness constraints. Information Processing Letters 66, 71–79 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  6. Barthe, G., D’Argenio, P., Rezk, T.: Secure information flow by self-composition. In: CSFW, pp. 100–114. IEEE Press (2004)

    Google Scholar 

  7. Blom, S., van de Pol, J., Weber, M.: LTSmin: Distributed and Symbolic Reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 354–359. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  8. Blondeel, H.-C.: Security by logic: characterizing non-interference in temporal logic. Master’s thesis, KTH Sweden (2007)

    Google Scholar 

  9. Chen, H., Malacaria, P.: Quantitative analysis of leakage for multi-threaded programs. In: PLAS 2007 (2007)

    Google Scholar 

  10. Christoff, L., Christoff, I.: Efficient Algorithms for Verification of Equivalences for Probabilistic Processes. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 310–321. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  11. Doyen, L., Henzinger, T.A., Raskin, J.F.: Equivalence of labeled Markov chains. Int. J. Found. Comput. Sci. 19(3), 549–563 (2008)

    Article  MathSciNet  Google Scholar 

  12. Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy (1982)

    Google Scholar 

  13. Gurfinkel, A., Chechik, M.: Why Waste a Perfectly Good Abstraction? In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 212–226. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  14. Huisman, M., Ngo, T.M.: Scheduler-Specific Confidentiality for Multi-threaded Programs and Its Logic-Based Verification. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS, vol. 7421, pp. 178–195. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  15. Huisman, M., Worah, P., Sunesen, K.: A temporal logic characterization of observation determinism. In: CSFW. IEEE Computer Society (2006)

    Google Scholar 

  16. Kiefer, S., Murawski, A.S., Ouaknine, J., Wachter, B., Worrell, J.: Language Equivalence for Probabilistic Automata. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 526–540. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  17. Kripke, S.A.: Semantical considerations on modal logic. Acta Philosophica Fennica 16, 83–94 (1963)

    MathSciNet  MATH  Google Scholar 

  18. Mantel, H., Sands, D., Sudbrock, H.: Assumptions and guarantees for compositional noninterference. In: CSF 2011, pp. 218–232 (2011)

    Google Scholar 

  19. Mantel, H., Sudbrock, H.: Flexible Scheduler-Independent Security. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol. 6345, pp. 116–133. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  20. Ngo, T.M., Stoelinga, M., Huisman, M.: Confidentiality for probabilistic multi-threaded programs and its verification. Full version, http://wwwhome.ewi.utwente.nl/~ngominhtri/

  21. Ngo, T.M., Stoelinga, M., Huisman, M.: Effective verification of confidentiality for multi-threaded programs. Manuscript 201X

    Google Scholar 

  22. Peled, D., Wilke, T.: Stutter-invariant temporal properties are expressible without the next-time operator. Information Processing Letters 63, 243–246 (1997)

    Article  MathSciNet  Google Scholar 

  23. Roscoe, A.W.: CSP and determinism in security modeling. In: IEEE Symposium on Security and Privacy, pp. 114–127. IEEE Computer Society (1995)

    Google Scholar 

  24. Sabelfeld, A., Sands, D.: Probabilistic noninterference for multi-threaded programs. In: CSFW, pp. 200–214 (2000)

    Google Scholar 

  25. Smith, G.: Probabilistic noninterference through weak probabilistic bisimulation. In: CSFW (2003)

    Google Scholar 

  26. 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)

    Chapter  Google Scholar 

  27. Stoelinga, M.I.A.: Alea jacta est: verification of probabilistic, real-time and parametric systems. PhD thesis, University of Nijmegen, The Netherlands (April 2002)

    Google Scholar 

  28. Terauchi, T.: A type system for observational determinism. In: CSF (2008)

    Google Scholar 

  29. Tzeng, W.G.: A polynomial-time algorithm for the equivalence of probabilistic automata. SIAM Journal on Computing 21, 216–227 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  30. Volpano, D., Smith, G.: Probabilistic noninterference in a concurrent language. Journal of Computer Security 7, 231–253 (1999)

    Google Scholar 

  31. Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: CSFW, pp. 29–43. IEEE (2003)

    Google Scholar 

  32. Zhu, J., Srivatsa, M.: Quantifying information leakage in finite order deterministic programs. In: CoRR 2010 (2010)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Twente, Netherlands

    Tri Minh Ngo, Mariëlle Stoelinga & Marieke Huisman

Authors
  1. Tri Minh Ngo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mariëlle Stoelinga
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Marieke Huisman
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, TU Dortmund und Fraunhofer ISST, Otto-Hahn-Straße 14, 44221, Dortmund, Germany

    Jan Jürjens

  2. One Microsoft Way, Microsoft Research, 98052-6399, Redmond, WA, USA

    Benjamin Livshits

  3. Department of Computer Science, Katholieke Universiteit Leuven, Celestijnenlaan 200A, 3001, Heverlee, Belgium

    Riccardo Scandariato

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Minh Ngo, T., Stoelinga, M., Huisman, M. (2013). Confidentiality for Probabilistic Multi-threaded Programs and Its Verification. In: Jürjens, J., Livshits, B., Scandariato, R. (eds) Engineering Secure Software and Systems. ESSoS 2013. Lecture Notes in Computer Science, vol 7781. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-36563-8_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-36563-8_8

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-36562-1

  • Online ISBN: 978-3-642-36563-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation