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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Aho, A.V., Hopcroft, J.E.: The Design and Analysis of Computer Algorithms, 1st edn. Addison-Wesley (1974)
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)
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)
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)
Baier, C., Kwiatkowska, M.: On the verification of qualitative properties of probabilistic processes under fairness constraints. Information Processing Letters 66, 71–79 (1998)
Barthe, G., D’Argenio, P., Rezk, T.: Secure information flow by self-composition. In: CSFW, pp. 100–114. IEEE Press (2004)
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)
Blondeel, H.-C.: Security by logic: characterizing non-interference in temporal logic. Master’s thesis, KTH Sweden (2007)
Chen, H., Malacaria, P.: Quantitative analysis of leakage for multi-threaded programs. In: PLAS 2007 (2007)
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)
Doyen, L., Henzinger, T.A., Raskin, J.F.: Equivalence of labeled Markov chains. Int. J. Found. Comput. Sci. 19(3), 549–563 (2008)
Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy (1982)
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)
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)
Huisman, M., Worah, P., Sunesen, K.: A temporal logic characterization of observation determinism. In: CSFW. IEEE Computer Society (2006)
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)
Kripke, S.A.: Semantical considerations on modal logic. Acta Philosophica Fennica 16, 83–94 (1963)
Mantel, H., Sands, D., Sudbrock, H.: Assumptions and guarantees for compositional noninterference. In: CSF 2011, pp. 218–232 (2011)
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)
Ngo, T.M., Stoelinga, M., Huisman, M.: Confidentiality for probabilistic multi-threaded programs and its verification. Full version, http://wwwhome.ewi.utwente.nl/~ngominhtri/
Ngo, T.M., Stoelinga, M., Huisman, M.: Effective verification of confidentiality for multi-threaded programs. Manuscript 201X
Peled, D., Wilke, T.: Stutter-invariant temporal properties are expressible without the next-time operator. Information Processing Letters 63, 243–246 (1997)
Roscoe, A.W.: CSP and determinism in security modeling. In: IEEE Symposium on Security and Privacy, pp. 114–127. IEEE Computer Society (1995)
Sabelfeld, A., Sands, D.: Probabilistic noninterference for multi-threaded programs. In: CSFW, pp. 200–214 (2000)
Smith, G.: Probabilistic noninterference through weak probabilistic bisimulation. In: CSFW (2003)
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)
Stoelinga, M.I.A.: Alea jacta est: verification of probabilistic, real-time and parametric systems. PhD thesis, University of Nijmegen, The Netherlands (April 2002)
Terauchi, T.: A type system for observational determinism. In: CSF (2008)
Tzeng, W.G.: A polynomial-time algorithm for the equivalence of probabilistic automata. SIAM Journal on Computing 21, 216–227 (1992)
Volpano, D., Smith, G.: Probabilistic noninterference in a concurrent language. Journal of Computer Security 7, 231–253 (1999)
Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: CSFW, pp. 29–43. IEEE (2003)
Zhu, J., Srivatsa, M.: Quantifying information leakage in finite order deterministic programs. In: CoRR 2010 (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)