Measuring the confinement of probabilistic systems. (English) Zbl 1142.68444
Summary: We lay the semantic basis for a quantitative security analysis of probabilistic systems by introducing notions of approximate confinement based on various process equivalences. We re-cast the operational semantics classically expressed via probabilistic transition systems (PTS) in terms of linear operators and we present a technique for defining approximate semantics as probabilistic abstract interpretations of the PTS semantics. An operator norm is then used to quantify this approximation. This provides a quantitative measure \(\varepsilon\) of the indistinguishability of two processes and therefore of their confinement. In this security setting a statistical interpretation is then given of the quantity \(\varepsilon\) which relates it to the number of tests needed to breach the security of the system.
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
| 68Q10 | Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) |
| 68Q55 | Semantics in the theory of computing |
| 60C05 | Combinatorial probability |
Keywords:
Security analysis; Probabilistic bisimulation; Probabilistic weak bisimulation; Static program analysis; Statistical testingSoftware:
PRISMReferences:
| [1] | A. Aldini, M. Bravetti, R. Gorrieri, A process algebraic approach for the analysis of probabilistic non-interference, J. Comput. Security, 2003, to appear.; A. Aldini, M. Bravetti, R. Gorrieri, A process algebraic approach for the analysis of probabilistic non-interference, J. Comput. Security, 2003, to appear. |
| [2] | A. Aldini, A. Di Pierro, A quantitative approach to noninterference for probabilistic systems, in: M. Bravetti, G. Gorrieri (Eds.), Electronic Notes in Theoretical Computer Science, Vol. 99. Elsevier Science, Amsterdam, 2004 (Proc. MEFISTO Project 2003, Formal Methods for Security and Time).; A. Aldini, A. Di Pierro, A quantitative approach to noninterference for probabilistic systems, in: M. Bravetti, G. Gorrieri (Eds.), Electronic Notes in Theoretical Computer Science, Vol. 99. Elsevier Science, Amsterdam, 2004 (Proc. MEFISTO Project 2003, Formal Methods for Security and Time). |
| [3] | Applebaum, D., Probability and Information—An Integrated Approach (1996), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0857.60001 |
| [4] | C. Baier, H. Hermanns, Weak bisimulation for fully probabilistic processes, in: Proc. 9th Int. Conf. Computer Aided Verification, Lecture Notes in Computer Science, Vol. 1254, Springer, Berlin, 1997, pp. 119-130.; C. Baier, H. Hermanns, Weak bisimulation for fully probabilistic processes, in: Proc. 9th Int. Conf. Computer Aided Verification, Lecture Notes in Computer Science, Vol. 1254, Springer, Berlin, 1997, pp. 119-130. |
| [5] | J.A. Bergstra, A. Ponse, S.A. Smolka (Eds.), Handbook of Process Algebra, Elsevier Science, Amsterdam, 2001.; J.A. Bergstra, A. Ponse, S.A. Smolka (Eds.), Handbook of Process Algebra, Elsevier Science, Amsterdam, 2001. · Zbl 0971.00006 |
| [6] | Beutler, F. J., The operator theory of the pseudo-inverse, J. Math. Anal. Appl., 10 (1965), 451-470, 471-493 · Zbl 0151.19205 |
| [7] | Biggs, N., Algebraic Graph Theory (1993), Cambridge Mathematical Library, Cambridge University Press: Cambridge Mathematical Library, Cambridge University Press Cambridge |
| [8] | Billingsley, P., Probability and Measure (1986), Wiley: Wiley New York · Zbl 0649.60001 |
| [9] | Böttcher, A.; Silbermann, B., Introduction to Large Truncated Toeplitz Matrices (1999), Springer: Springer New York · Zbl 0916.15012 |
| [10] | F. van Breugel, J. Worrell, An algorithm for quantitative verification of probabilistic transition systems, in: Proc. CONCUR’01, Lecture Notes in Computer Science, Vol. 2154, Springer, Berlin, 2001.; F. van Breugel, J. Worrell, An algorithm for quantitative verification of probabilistic transition systems, in: Proc. CONCUR’01, Lecture Notes in Computer Science, Vol. 2154, Springer, Berlin, 2001. · Zbl 1006.68079 |
| [11] | F. van Breugel, J. Worrell, Towards quantitative verification of probabilistic transition systems, in: Proc. ICALP’01, Lecture Notes in Computer Science, Vol. 2076, Springer, Berlin, 2001, pp. 421-432.; F. van Breugel, J. Worrell, Towards quantitative verification of probabilistic transition systems, in: Proc. ICALP’01, Lecture Notes in Computer Science, Vol. 2076, Springer, Berlin, 2001, pp. 421-432. · Zbl 0986.68093 |
| [12] | Campbell, S. L.; Meyer, D., Generalized Inverse of Linear Transformations (1979), Constable and Company: Constable and Company London · Zbl 0417.15002 |
| [13] | Cavusoglu, H.; Mishra, B.; Raghunathan, S., A model for evaluating IT security investments, Comm. ACM, 47, 7, 87-92 (2004) |
| [14] | A.Z.R. Cleaveland, S. Smolka, Testing preorders for probabilistic processes, in: Proc. ICALP 92, Lecture Notes in Computer Science, Vol. 623, Springer, Berlin, 1992, pp. 708-719.; A.Z.R. Cleaveland, S. Smolka, Testing preorders for probabilistic processes, in: Proc. ICALP 92, Lecture Notes in Computer Science, Vol. 623, Springer, Berlin, 1992, pp. 708-719. · Zbl 1425.68289 |
| [15] | J.B. Conway, A Course in Functional Analysis, second ed., Graduate Texts in Mathematics, Vol. 96, Springer, New York, 1990.; J.B. Conway, A Course in Functional Analysis, second ed., Graduate Texts in Mathematics, Vol. 96, Springer, New York, 1990. · Zbl 0706.46003 |
| [16] | Cousot, P.; Cousot, R., Abstract interpretationa unified lattice model for static analysis of programs by construction or approximation of fixpoints, (Proc. POPL’77. Proc. POPL’77, Los Angeles (1977)), 238-252 |
| [17] | Cousot, P.; Cousot, R., Systematic design of program analysis frameworks, (Proc. POPL’79. Proc. POPL’79, San Antonio, TX (1979)), 269-282 · Zbl 0788.68094 |
| [18] | Cousot, P.; Cousot, R., Abstract interpretation and applications to logic programs, J. Logic Program., 13, 2-3, 103-180 (1992) · Zbl 0776.68024 |
| [19] | Dams, D.; Gerth, R.; Grumberg, O., Abstract interpretation of reactive systems, ACM Trans. Program. Languages Systems, 19, 2, 253-291 (1997) |
| [20] | K.R. Davidson, C*-Algebras by Example, Fields Institute Monographs, Vol. 6, American Mathematical Society, Providence, RI, 1996.; K.R. Davidson, C*-Algebras by Example, Fields Institute Monographs, Vol. 6, American Mathematical Society, Providence, RI, 1996. · Zbl 0958.46029 |
| [21] | Desharnais, J.; Edalat, A.; Panangaden, P., Bisimulation for labelled Markov processes, Inform. Comput., 179, 163-193 (2002) · Zbl 1096.68103 |
| [22] | J. Desharnais, R. Jagadeesan, V. Gupta, P. Panangaden, Metrics for labeled Markov systems, in: Proc. 10th Int. Conf. on Concurrency Theory, Lecture Notes in Computer Science, Vol. 1664, Springer, Berlin, 1999, pp. 258-273.; J. Desharnais, R. Jagadeesan, V. Gupta, P. Panangaden, Metrics for labeled Markov systems, in: Proc. 10th Int. Conf. on Concurrency Theory, Lecture Notes in Computer Science, Vol. 1664, Springer, Berlin, 1999, pp. 258-273. · Zbl 0939.68081 |
| [23] | J. Desharnais, R. Jagadeesan, V. Gupta, P. Panangaden, The metric analogue of weak bisimulation for probabilistic processes, in: Proc. LICS’02, , IEEE, Copenhagen, Denmark, 22-25 July 2002, pp. 413-422.; J. Desharnais, R. Jagadeesan, V. Gupta, P. Panangaden, The metric analogue of weak bisimulation for probabilistic processes, in: Proc. LICS’02, , IEEE, Copenhagen, Denmark, 22-25 July 2002, pp. 413-422. |
| [24] | F. Deutsch, Bet approximation in inner product spaces, CMS Books in Mathematics, Vol. 7, Springer, New York, Berlin, 2001.; F. Deutsch, Bet approximation in inner product spaces, CMS Books in Mathematics, Vol. 7, Springer, New York, Berlin, 2001. · Zbl 0980.41025 |
| [25] | R. Diestel, Graph theory, Graduate Texts in Mathematics, Vol. 173, Springer, New York, Heidelberg, Berlin, 1997.; R. Diestel, Graph theory, Graduate Texts in Mathematics, Vol. 173, Springer, New York, Heidelberg, Berlin, 1997. · Zbl 0873.05001 |
| [26] | E.A. Feinberg, A. Shwartz (Eds.), Handbook of Markov Decision Processes, Kluwer, Dordrecht, 2002.; E.A. Feinberg, A. Shwartz (Eds.), Handbook of Markov Decision Processes, Kluwer, Dordrecht, 2002. · Zbl 0979.90001 |
| [27] | Fillmore, P. A., A User’s Guide to Operator Algebras (1996), Wiley: Wiley New York, Chichester · Zbl 0853.46053 |
| [28] | R.J. van Glabbeek, The Linear Time—Branching Time Spectrum I. The Semantics of Concrete, Sequential Processes, Elsevier Science, Amsterdam, 2001, pp. 3-99 (Chapter 1).; R.J. van Glabbeek, The Linear Time—Branching Time Spectrum I. The Semantics of Concrete, Sequential Processes, Elsevier Science, Amsterdam, 2001, pp. 3-99 (Chapter 1). · Zbl 1035.68073 |
| [29] | van Glabbeek, R. J.; Smolka, S. A.; Steffen, B., Reactive, generative and stratified models of probabilistic processes, Inform. Comput., 121, 59-80 (1995) · Zbl 0832.68042 |
| [30] | C. Godsil, G. Royle, Algebraic graph theory, Graduate Texts in Mathematics, Vol. 207, Springer, New York, Heidelberg, Berlin, 2001.; C. Godsil, G. Royle, Algebraic graph theory, Graduate Texts in Mathematics, Vol. 207, Springer, New York, Heidelberg, Berlin, 2001. · Zbl 0968.05002 |
| [31] | J. Goguen, J. Meseguer, Security policies and security models, in: IEEE Symp. on Security and Privacy, IEEE Computer Society Press, Rockville, MD, 1982, pp. 11-20.; J. Goguen, J. Meseguer, Security policies and security models, in: IEEE Symp. on Security and Privacy, IEEE Computer Society Press, Rockville, MD, 1982, pp. 11-20. |
| [32] | Gray, J. W., Towards a mathematical foundation for information flow security, (Proc.1991 Symp. on Research in Security and Privacy, IEEE. Proc.1991 Symp. on Research in Security and Privacy, IEEE, Oakland, CA (May 1991)), 21-34 |
| [33] | W.H. Greub, Linear Algebra, third ed., Grundlehren der mathematischen Wissenschaften, Vol. 97, Springer, Berlin, New York, 1967.; W.H. Greub, Linear Algebra, third ed., Grundlehren der mathematischen Wissenschaften, Vol. 97, Springer, Berlin, New York, 1967. · Zbl 0147.27408 |
| [34] | Grimmett, G. R.; Stirzaker, D. R., Probability and Random Processes (1992), Clarendon Press: Clarendon Press Oxford · Zbl 0759.60002 |
| [35] | Grinstead, C. M.; Snell, J. L., Introduction to Probability (1997), American Mathematical Society: American Mathematical Society Providence, RI · Zbl 0914.60004 |
| [36] | H. Hansson, Time and probability in formal design of distributed systems, Ph.D. Thesis, Uppsala University, 1994.; H. Hansson, Time and probability in formal design of distributed systems, Ph.D. Thesis, Uppsala University, 1994. |
| [37] | Hennessy, M. C.B., Algebraic Theory of Processes (1988), MIT Press: MIT Press Cambridge, MA · Zbl 0437.68002 |
| [38] | Jonsson, B.; Yi, W., Compositional testing preorders for probabilistic processes, (Proc. LICS’95 (1995)), 431-443 |
| [39] | B. Jonsson, W. Yi, K.G. Larsen, Probabilistic Extensions of Process Algebras, Elsevier Science, Amsterdam, 2001, pp. 685-710 (Chapter 11).; B. Jonsson, W. Yi, K.G. Larsen, Probabilistic Extensions of Process Algebras, Elsevier Science, Amsterdam, 2001, pp. 685-710 (Chapter 11). · Zbl 1062.68081 |
| [40] | R.V. Kadison, J.R. Ringrose, Fundamentals of the theory of operator algebras: Vol. I—elementary theory, Graduate Studies in Mathematics, Vol. 15, American Mathematical Society, Providence, RI, 1997 (reprint from Academic Press edition 1983).; R.V. Kadison, J.R. Ringrose, Fundamentals of the theory of operator algebras: Vol. I—elementary theory, Graduate Studies in Mathematics, Vol. 15, American Mathematical Society, Providence, RI, 1997 (reprint from Academic Press edition 1983). · Zbl 0518.46046 |
| [41] | Kemeny, J. G.; Snell, J. L., Finite Markov Chains (1960), D. Van Nostrand Company: D. Van Nostrand Company Princeton, NJ · Zbl 0112.09802 |
| [42] | M. Kwiatkowska, G. Norman, D. Parker, PRISM: Probabilistic Symbolic Model Checker, in: TOOLS 2002, Lecture Notes in Computer Science, Vol. 2324, Springer, Berlin, 2002, pp. 200-204.; M. Kwiatkowska, G. Norman, D. Parker, PRISM: Probabilistic Symbolic Model Checker, in: TOOLS 2002, Lecture Notes in Computer Science, Vol. 2324, Springer, Berlin, 2002, pp. 200-204. · Zbl 1047.68533 |
| [43] | Lampson, B. W., A note on the confinement problem, Comm. ACM, 16, 10, 613-615 (1973) |
| [44] | Larsen, K. G.; Skou, A., Bisimulation through probabilistic testing, Inform. Comput., 94, 1-28 (1991) · Zbl 0756.68035 |
| [45] | R. Milner, A Calculus of Communicating Systems, Lecture Notes in Computer Science, Vol. 92, Springer, Berlin, New York, 1980.; R. Milner, A Calculus of Communicating Systems, Lecture Notes in Computer Science, Vol. 92, Springer, Berlin, New York, 1980. · Zbl 0452.68027 |
| [46] | Mohar, B.; Woess, W., A survey on spectra of infinite graphs, Bull. London Math. Soc., 21, 209-234 (1988) · Zbl 0645.05048 |
| [47] | Murphy, G. J., \(C^*\)-Algebras and Operator Theory (1990), Academic Press: Academic Press San Diego · Zbl 0714.46041 |
| [48] | De Nicola, R.; Hennessy, M. C.B., Testing equivalences for processes, Theoret. Comput. Sci., 34, 83-133 (1983) · Zbl 0985.68518 |
| [49] | Nielson, F.; Riis Nielson, H.; Hankin, C., Principles of Program Analysis (1999), Springer: Springer Berlin, Heidelberg · Zbl 0932.68013 |
| [50] | A. Philippou, I. Lee, O. Sokolsky, Weak bisimulation for probabilistic processes, in: Proc. CONCUR 2000, Lecture Notes in Computer Science, Vol. 1887, Springer, Berlin, 2000, pp. 334-349.; A. Philippou, I. Lee, O. Sokolsky, Weak bisimulation for probabilistic processes, in: Proc. CONCUR 2000, Lecture Notes in Computer Science, Vol. 1887, Springer, Berlin, 2000, pp. 334-349. · Zbl 0999.68146 |
| [51] | A. Di Pierro, C. Hankin, H. Wiklicky, Probabilistic confinement in a declarative framework, in: Declarative Programming—Selected Papers from AGP 2000, La Havana, Cuba, Electronic Notes in Theoretical Computer Science, Vol. 48, Elsevier, Amsterdam, 2001, pp. 1-23.; A. Di Pierro, C. Hankin, H. Wiklicky, Probabilistic confinement in a declarative framework, in: Declarative Programming—Selected Papers from AGP 2000, La Havana, Cuba, Electronic Notes in Theoretical Computer Science, Vol. 48, Elsevier, Amsterdam, 2001, pp. 1-23. · Zbl 1263.68044 |
| [52] | Di Pierro, A.; Hankin, C.; Wiklicky, H., Approximate non-interference, (Proc. CSFW’02. Proc. CSFW’02, IEEE, Cape Breton, Canada (24-26 June 2002)), 3-17 |
| [53] | A. Di Pierro, C. Hankin, H. Wiklicky, Approximate confinement under uniform attacks, in: Proc. SAS’02, Lecture Notes in Computer Science, Vol. 2477, Springer, Berlin, 2002, pp. 310-325.; A. Di Pierro, C. Hankin, H. Wiklicky, Approximate confinement under uniform attacks, in: Proc. SAS’02, Lecture Notes in Computer Science, Vol. 2477, Springer, Berlin, 2002, pp. 310-325. · Zbl 1015.68069 |
| [54] | A. Di Pierro, C. Hankin, H. Wiklicky, Quantitative relations and approximate process equivalences, in: R. Amadio, D. Lugiez (Eds.), Proc. CONCUR 2003, 14th Int. Conf. on Concurrency Theory, Lecture Notes in Computer Science, Vol. 2761, Springer, Berlin, 2003, pp. 508-522.; A. Di Pierro, C. Hankin, H. Wiklicky, Quantitative relations and approximate process equivalences, in: R. Amadio, D. Lugiez (Eds.), Proc. CONCUR 2003, 14th Int. Conf. on Concurrency Theory, Lecture Notes in Computer Science, Vol. 2761, Springer, Berlin, 2003, pp. 508-522. · Zbl 1274.68227 |
| [55] | Di Pierro, A.; Hankin, C.; Wiklicky, H., Approximate non-interference, J. Comput. Security, 12, 1, 37-81 (2004) |
| [56] | Di Pierro, A.; Wiklicky, H., Concurrent constraint programmingtowards probabilistic abstract interpretation, (Proc. PPDP’00. Proc. PPDP’00, ACM, Montréal, Canada (2000)), 127-138 |
| [57] | A. Di Pierro, H. Wiklicky, Measuring the precision of abstract interpretations, in: Proc. LOPSTR’00, Lecture Notes in Computer Science, Vol. 2042, Springer, Berlin, 2001, pp. 147-164.; A. Di Pierro, H. Wiklicky, Measuring the precision of abstract interpretations, in: Proc. LOPSTR’00, Lecture Notes in Computer Science, Vol. 2042, Springer, Berlin, 2001, pp. 147-164. · Zbl 1018.68505 |
| [58] | P.Y.A. Ryan, J. McLean, J. Millen, V. Gilgor, Non-interference who needs it? in: Proc. 14th IEEE Computer Security Foundations Workshop, IEEE, Cape Breton, Nova Scotia, Canada, June 2001, pp. 237-238.; P.Y.A. Ryan, J. McLean, J. Millen, V. Gilgor, Non-interference who needs it? in: Proc. 14th IEEE Computer Security Foundations Workshop, IEEE, Cape Breton, Nova Scotia, Canada, June 2001, pp. 237-238. |
| [59] | Ryan, P. Y.A.; Schneider, S. A., Process algebra and non-interference, J. Comput. Security, 9, 1,2, 75-103 (2001), (special issue on CSFW-12) |
| [60] | D.A. Schmidt, Binary relations for abstraction and refinement, in: Workshop on Refinement and Abstraction, Amagasaki, Japan, November 1999.; D.A. Schmidt, Binary relations for abstraction and refinement, in: Workshop on Refinement and Abstraction, Amagasaki, Japan, November 1999. |
| [61] | R. Segala, N. Lynch, Probabilistic simulations for probabilistic processes, in: Proc. CONCUR 94, Lecture Notes in Computer Science, Vol. 836, Springer, Berlin, 1994, pp. 481-496.; R. Segala, N. Lynch, Probabilistic simulations for probabilistic processes, in: Proc. CONCUR 94, Lecture Notes in Computer Science, Vol. 836, Springer, Berlin, 1994, pp. 481-496. · Zbl 0839.68067 |
| [62] | Shao, J., Mathematical Statistics, Springer Texts in Statistics (1999), Springer: Springer New York, Berlin, Heidelberg · Zbl 0935.62004 |
| [63] | G. Smith, Probabilistic noninterference through weak probabilistic bi-simulation, in: Proc. 16th Computer Security Foundations Workshop (CSFW’03), IEEE, 2003, pp. 3-13.; G. Smith, Probabilistic noninterference through weak probabilistic bi-simulation, in: Proc. 16th Computer Security Foundations Workshop (CSFW’03), IEEE, 2003, pp. 3-13. |
| [64] | E.D. Sontag, Mathematical Control Theory: Deterministic Finite Dimensional Systems, Texts in Applied Mathematics, Vol. 6, Springer, New York, Heidelberg, Berlin, 1990.; E.D. Sontag, Mathematical Control Theory: Deterministic Finite Dimensional Systems, Texts in Applied Mathematics, Vol. 6, Springer, New York, Heidelberg, Berlin, 1990. · Zbl 0703.93001 |
| [65] | M. Vardi, Automatic verification of probabilistic concurrent finite-state programs, in: Proc. FOCS’85, 1985, pp. 332-344.; M. Vardi, Automatic verification of probabilistic concurrent finite-state programs, in: Proc. FOCS’85, 1985, pp. 332-344. |
| [66] | de Vink, E. P.; Rutten, J. J.M. M., Bisimulation for probabilistic transition systems: a coalgebraic approach, Theoret. Comput. Sci., 221, 271-293 (1999) · Zbl 0930.68092 |
| [67] | Whittaker, J., Graphical Models in Applied Multivariate Statistics (1990), Wiley: Wiley Chicester, New York · Zbl 0732.62056 |
| [68] | W. Woess, Random walks on infinite graphs and groups, Cambridge Tracts in Mathematics, Vol. 138, Cambridge University Press, Cambridge, 2000.; W. Woess, Random walks on infinite graphs and groups, Cambridge Tracts in Mathematics, Vol. 138, Cambridge University Press, Cambridge, 2000. · Zbl 0951.60002 |
| [69] | Yosida, K., Functional Analysis (1980), Springer: Springer Berlin, Heidelberg, New York · Zbl 0152.32102 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
