Hostname: page-component-745bb68f8f-cphqk Total loading time: 0 Render date: 2025-01-09T17:26:44.014Z Has data issue: false hasContentIssue false
  • English
  • Français

Quantifying opacity†

Published online by Cambridge University Press:  12 November 2014

BÉATRICE BÉRARD ,
JOHN MULLINS  and
MATHIEU SASSOLAS
BÉATRICE BÉRARD
Affiliation:
Sorbonne Université, Université P. & M. Curie, LIP6, CNRS UMR 7606, Paris, France Email: beatrice.berard@lip6.fr
JOHN MULLINS
Affiliation:
École Polytechnique de Montréal, Dept. of Comp. & Soft. Eng., Montreal (Quebec), Canada Email: john.mullins@polymtl.ca
MATHIEU SASSOLAS*
Affiliation:
Sorbonne Université, Université P. & M. Curie, LIP6, CNRS UMR 7606, Paris, France Email: beatrice.berard@lip6.fr Université Paris-Est, LACL, Créteil, France Email: mathieu.sassolas@u-pec.fr
*
‡Corresponding author: mathieu.sassolas@u-pec.fr – Université Paris-Est, LACL, 61 avenue du Général de gaulle, F-94010 Créteil Cedex, France.
Get access Rights & Permissions [Opens in a new window]

Abstract

Opacity is a general language-theoretic framework in which several security properties of a system can be expressed. Its parameters are a predicate, given as a subset of runs of the system, and an observation function, from the set of runs into a set of observables. The predicate describes secret information in the system and, in the possibilistic setting, it is opaque if its membership cannot be inferred from observation.

In this paper, we propose several notions of quantitative opacity for probabilistic systems, where the predicate and the observation function are seen as random variables. Our aim is to measure (i) the probability of opacity leakage relative to these random variables and (ii) the level of uncertainty about membership of the predicate inferred from observation. We show how these measures extend possibilistic opacity, we give algorithms to compute them for regular secrets and observations, and we apply these computations on several classical examples. We finally partially investigate the non-deterministic setting.

Type
Special Issue: Quantitative Information Flow
Information
Mathematical Structures in Computer Science , Volume 25 , Issue 2: Quantitative Information Flow , February 2015 , pp. 361 - 403
Copyright
Copyright © Cambridge University Press 2014 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

†

Part of this work has been published in the proceedings of Qest'10 (Bérard et al. 2010).

References

Aldini, A. and Bernardo, M. (2009) A general framework for nondeterministic, probabilistic, and stochastic noninterference. In: Degano, P. and Viganò, L. (eds.) Proceedings of Foundations and Applications of Security Analysis; ARSPA-WITS 2009. Springer Lecture Notes in Computer Science 5511 191–245.Google Scholar
Aldini, A., Bravetti, M. and Gorrieri, R. (2004) A process-algebraic approach for the analysis of probabilistic noninterference. Journal of Computer Security 12 (2)191–245.CrossRefGoogle Scholar
Alur, R., Černý, P. and Zdancewic, S. (2006) Preserving secrecy under refinement. In: Proceedings of the 33rd International Colloquium on Automata, Languages and Programming (ICALP'06). Springer Lecture Notes in Computer Science 4052 107–118.CrossRefGoogle Scholar
Alvim, M. S., Andrés, M. E. and Palamidessi, C. (2010) Information flow in interactive systems. In: Gastin, P. and Laroussinie, F. (eds.) Proceedings of the 21th International Conference on Concurrency Theory (CONCUR'10). Springer Lecture Notes in Computer Science 6269 102–116.CrossRefGoogle Scholar
Andrés, M. E., Palamidessi, C., van Rossum, P. and Smith, G. (2010) Computing the leakage of information-hiding systems. In: Proceedings 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'10) Springer Lecture Notes in Computer Science. 6015 373–389.CrossRefGoogle Scholar
Bérard, B., Mullins, J. and Sassolas, M. (2010) Quantifying opacity. In: Ciardo, G. and Segala, R. (eds.) Proceedings of the 7th International Conference on Quantitative Evaluation of Systems (QEST'10), IEEE Computer Society 263–272.Google Scholar
Bianco, A. and de Alfaro, L. (1995) Model checking of probabilistic and nondeterministic systems. In: Proceedings 15th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'95). Springer Lecture Notes in Computer Science 1026 499–513.CrossRefGoogle Scholar
Boreale, M. (2009) Quantifying information leakage in process calculi. Information and Computation 207 (6)699–725.CrossRefGoogle Scholar
Boreale, M., Clark, D. and Gorla, D. (2010) A semiring-based trace semantics for processes with applications to information leakage analysis. In: Calude, C. S. and Sassone, V. (eds.) Proceedings of 6th IFIP TC 1/WG 2.2 International Conference, TCS 2010, Held as Part of WCC 2010 (IFIP TCS). Springer International Federation for Information Processing 323 340–354.Google Scholar
Boreale, M., Pampaloni, F. and Paolini, M. (2011a) Asymptotic information leakage under one-try attacks. In: Hofmann, M. (ed.) Foundations of Software Science and Computational Structures - 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011. Springer Lecture Notes in Computer Science 6604 396–410.CrossRefGoogle Scholar
Boreale, M., Pampaloni, F. and Paolini, M. (2011b) Quantitative information flow, with a view. In: Atluri, V. and Díaz, C. (eds.) Proceedings of 16th European Symposium on Research in Computer Security (ESORICS 2011). Springer Lecture Notes in Computer Science 6879 588–606.CrossRefGoogle Scholar
Bryans, J. W., Koutny, M., Mazaré, L. and Ryan, P. Y. A. (2008) Opacity generalised to transition systems. International Journal of Information Security 7 (6)421–435.CrossRefGoogle Scholar
Chatzikokolakis, K., Palamidessi, C. and Panangaden, P. (2008) Anonymity protocols as noisy channels. Information and Computation 206 (2–4)378–401.CrossRefGoogle Scholar
Chaum, D. (1988) The dining cryptographers problem: Unconditional sender and recipient untraceability. Journal of Cryptology 1 65–75.CrossRefGoogle Scholar
Courcoubetis, C. and Yannakakis, M. (1998) Markov decision processes and regular events. IEEE Transactions on Automatc Control 43 (10)1399–1418.CrossRefGoogle Scholar
Dubreil, J., Darondeau, P. and Marchand, H. (2010) Supervisory control for opacity. IEEE Transactions on Automatic Control 55 (5) 1089 –1100.CrossRefGoogle Scholar
Eftenie, A. (2010) Computing quantitative opacity with tpot – Available at http://www.polymtl.ca/crac/TPOT/.Google Scholar
Giro, S. and D'Argenio, P. R. (2009) On the expressive power of schedulers in distributed probabilistic systems. Electronic Notes in Theoretical Computer Science 253 (3)45–71.CrossRefGoogle Scholar
Goguen, J. A. and Meseguer, J. (1982) Security policy and security models. In: Proceedings of IEEE Symposium on Security and Privacy, IEEE Computer Society Press 11–20.Google Scholar
Hansson, H. and Jonsson, B. (1994) A logic for reasoning about time and reliability. Formal Aspects of Computing 6 (5)512–535.CrossRefGoogle Scholar
Kemeny, J. G. and Snell, J. L. (1976) Finite Markov Chains, Undergraduate Texts in Mathemetics, Sringer-Verlag.Google Scholar
Lakhnech, Y. and Mazaré, L. (2005) Probabilistic opacity for a passive adversary and its application to Chaum's voting scheme, Technical Report 4, Verimag.Google Scholar
Lin, F. (2011) Opacity of discrete event systems and its applications. Automatica 47 (3)496–503.CrossRefGoogle Scholar
Lowe, G. (2004) Defining information flow quantity. Journal of Computer Security 12 (3–4)619–653.CrossRefGoogle Scholar
Mantel, H. and Sudbrock, H. (2009) Information-theoretic modeling and analysis of interrupt-related covert channels. In: Degano, P., Guttman, J. and Martinelli, F. (eds.) Proceedings of the Workshop on Formal Aspects in Security and Trust, FAST 2008. Springer Lecture Notes in Computer Science 5491 67–81.CrossRefGoogle Scholar
Mazaré, L. (2005) Decidability of opacity with non-atomic keys. In: Proceedings 2nd Workshop on Formal Aspects in Security and Trust (FAST'04). Springer International Federation for Information Processing 173 71–84.CrossRefGoogle Scholar
McIver, A., Meinicke, L. and Morgan, C. (2010) Compositional closure for bayes risk in probabilistic noninterference. In: Abramsky, S., Gavoille, C., Kirchner, C., auf der Heide, F. M. and Spirakis, P. G. (eds.) Proceeding of 37th International Colloquium on Automata, Languages and Programming (ICALP'10), Part II. Springer Lecture Notes in Computer Science 6199 223–235.CrossRefGoogle Scholar
Millen, J. K. (1987) Covert channel capacity. In: Proceedings of IEEE Symposium on Research in Computer Security and Privacy 144–161.CrossRefGoogle Scholar
Reiter, M. K. and Rubin, A. D. (1998) Crowds: Anonymity for web transactions. ACM Transactions on Information and System Security 1 (1)66–92.CrossRefGoogle Scholar
Segala, R. (1995) Modeling and Verification of Randomized Distributed Real-Time Systems. Ph.D. thesis, MIT, Department of Electrical Engineering and Computer Science.Google Scholar
Smith, G. (2009) On the foundations of quantitative information flow. In: Proceedings 12th International Conference on Foundations of Software Science and Computational Structures (FOSSACS'09), Springer-Verlag 288–302.Google Scholar
Wittbold, J. T. and Johnson, D. M. (1990) Information flow in nondeterministic systems. In Proceedings of IEEE Symposium on Research in Computer Security and Privacy 144–161.CrossRefGoogle Scholar