Rule formats for compositional non-interference properties. (English) Zbl 1072.68073
Summary: We introduce the transition rule formats rooted SBSNNI and CP\(_{\text{BNDC}}\). We prove that the non-interference property rooted SBSNNI introduced in the present paper, and the already known non-interference property CP\(_{\text{BNDC}}\), are preserved by constructs of all process algebras with SOS transition rules respecting the restrictions of the formats rooted SBSNNI and CP\(_{\text{BNDC}}\), respectively. To show that our formats have practical applications, we prove that a slight variant of Focardi and Gorrieri’s security process algebra, the Kleene star recursion construct, the replication construct of polyadic \(\pi\)-calculus, and a process algebra extending BPA\(_{\varepsilon\tau}\) to deal with two level systems, respect both formats. By means of some counterexamples, we prove also that all restrictions of the formats are necessary.
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
Keywords:
transition rule formatsReferences:
| [1] | Aceto, L.; Fokkink, W. J.; Verhoef, C., Structural operational semantics, (Bergstra, J. A.; Ponse, A.; Smolka, S. A., Handbook of Process Algebra (2001), Elsevier: Elsevier Amsterdam), 197-292 · Zbl 1062.68074 |
| [2] | P.G. Allen, A comparison of non-interference and non-deducibility using CSP, Proc. IEEE Computer Security Foundation Workshop, IEEE Computer Society Press, 1991, 43-54; P.G. Allen, A comparison of non-interference and non-deducibility using CSP, Proc. IEEE Computer Security Foundation Workshop, IEEE Computer Society Press, 1991, 43-54 |
| [3] | J.C.M. Baeten, W.P. Weijland, Process algebra, Cambridge Tracts in Theoretical Computer Science, 18, Cambridge University Press, 1990; J.C.M. Baeten, W.P. Weijland, Process algebra, Cambridge Tracts in Theoretical Computer Science, 18, Cambridge University Press, 1990 · Zbl 0716.68002 |
| [4] | D. Bell, L.J. La Padula, Secure computer systems: unified exposition and multics interpretation, Technical Report ESD-TR-75-301, MITRE MTR-2997, 1976; D. Bell, L.J. La Padula, Secure computer systems: unified exposition and multics interpretation, Technical Report ESD-TR-75-301, MITRE MTR-2997, 1976 |
| [5] | Bloom, B., Structural operational semantics for weak bisimulation, Theoretical Computer Science, 146, 1-2, 25-68 (1995) · Zbl 0873.68130 |
| [6] | A. Bossi, R. Focardi, C. Piazza, S. Rossi, A proof system for information flow security, Proc. International Workshop on Logic Based Program Development and Transformation, Lecture Notes in Computer Science, vol. 2664, Springer, Berlin, 2002, pp. 199-218; A. Bossi, R. Focardi, C. Piazza, S. Rossi, A proof system for information flow security, Proc. International Workshop on Logic Based Program Development and Transformation, Lecture Notes in Computer Science, vol. 2664, Springer, Berlin, 2002, pp. 199-218 · Zbl 1278.68158 |
| [7] | A. Bossi, R. Focardi, C. Piazza, S. Rossi, Bisimulation and unwinding for verifying possibilistic security properties, Proc. International Conference on Verification, Model Checking and Abstract Interpretation, Lecture Notes in Computer Science, vol. 2575, Springer, Berlin, 2003, pp. 223-237; A. Bossi, R. Focardi, C. Piazza, S. Rossi, Bisimulation and unwinding for verifying possibilistic security properties, Proc. International Conference on Verification, Model Checking and Abstract Interpretation, Lecture Notes in Computer Science, vol. 2575, Springer, Berlin, 2003, pp. 223-237 · Zbl 1022.68085 |
| [8] | A. Bossi, D. Macedonio, C. Piazza, S. Rossi, Information flow security and recursive systems, Proc. Italian Conference on Theoretical Computer Science, Lecture Notes in Computer Science, vol. 2841, Springer, Berlin, 2003, pp. 369-382; A. Bossi, D. Macedonio, C. Piazza, S. Rossi, Information flow security and recursive systems, Proc. Italian Conference on Theoretical Computer Science, Lecture Notes in Computer Science, vol. 2841, Springer, Berlin, 2003, pp. 369-382 · Zbl 1257.68055 |
| [9] | Focardi, R.; Gorrieri, R., A classification of security properties for process algebras, Journal of Computer Security, 3, 1, 5-33 (1995) |
| [10] | Focardi, R.; Gorrieri, R., The compositionality security checker: a tool for the verification of information flow properties, IEEE Transactions on Software Engineering, 23, 9, 550-571 (1997) |
| [11] | R. Focardi, R. Gorrieri, Classification of security properties (Part I: Information flow), in Foundations of Security Analysis and Design Summer School, Tutorial Lectures, Lecture Notes in Computer Science, vol. 2171, Springer, Berlin, 2001, pp. 331-396; R. Focardi, R. Gorrieri, Classification of security properties (Part I: Information flow), in Foundations of Security Analysis and Design Summer School, Tutorial Lectures, Lecture Notes in Computer Science, vol. 2171, Springer, Berlin, 2001, pp. 331-396 · Zbl 1007.68508 |
| [12] | R. Focardi, S. Rossi, Information flow security in dynamic contexts, Proc. IEEE Computer Security Foundation Workshop, IEEE Computer Society Press, 2002, pp. 307-319; R. Focardi, S. Rossi, Information flow security in dynamic contexts, Proc. IEEE Computer Security Foundation Workshop, IEEE Computer Society Press, 2002, pp. 307-319 |
| [13] | Fokkink, W. J., Rooted branching bisimulation as a congruence, Journal of Computer and System Sciences, 60, 1, 13-37 (2000) · Zbl 0955.68074 |
| [14] | Groote, J. F.; Vaandrager, F., Structured operational semantics and bisimulation as a congruence, Information and Computation, 100, 2, 202-260 (1992) · Zbl 0752.68053 |
| [15] | J. Goguen, J. Meseguer, Security policy and security models, Proc. IEEE Symposium on Security and Privacy, IEEE Computer Society Press, 1982, pp. 11-20; J. Goguen, J. Meseguer, Security policy and security models, Proc. IEEE Symposium on Security and Privacy, IEEE Computer Society Press, 1982, pp. 11-20 |
| [16] | D.M. Johnson, F.J. Thayer, Security and the composition of machines, Proc. IEEE Computer Security Foundation Workshop, IEEE Computer Society Press, 1988, pp. 72-89; D.M. Johnson, F.J. Thayer, Security and the composition of machines, Proc. IEEE Computer Security Foundation Workshop, IEEE Computer Society Press, 1988, pp. 72-89 |
| [17] | Keller, R., Formal verification of parallel programs, Communications of the ACM, 19, 371-384 (1976) · Zbl 0329.68016 |
| [18] | Kleene, S. C., Representation of events in nerve nets and finite automata, Automata Studies (1956), Princeton University Press, pp. 3-41 |
| [19] | H. Mantel, On the composition of secure systems, Proc. IEEE Symposium on Security and Privacy, IEEE Computer Society Press, 2002, pp. 88-101; H. Mantel, On the composition of secure systems, Proc. IEEE Symposium on Security and Privacy, IEEE Computer Society Press, 2002, pp. 88-101 |
| [20] | F. Martinelli, Partial model checking and theorem proving for ensuring security properties, Proc. IEEE Computer Security Foundation Workshop, IEEE Computer Society Press, 1998, pp. 44-52; F. Martinelli, Partial model checking and theorem proving for ensuring security properties, Proc. IEEE Computer Security Foundation Workshop, IEEE Computer Society Press, 1998, pp. 44-52 |
| [21] | D. McCullough, Specification for multi-level security and hook-up property, Proc. IEEE Symposium on Security and Privacy, IEEE Computer Society Press, 1987, pp. 161-166; D. McCullough, Specification for multi-level security and hook-up property, Proc. IEEE Symposium on Security and Privacy, IEEE Computer Society Press, 1987, pp. 161-166 |
| [22] | McCullough, D., A hookup theorem for multilevel security, IEEE Transactions on Software Engineering, 16, 6, 563-568 (1990) |
| [23] | J. McLean, A general theory of composition for trace sets closed under selective interleaving functions, Proc. IEEE Symposium on Security and Privacy, IEEE Computer Society Press, 1994, pp. 79-93; J. McLean, A general theory of composition for trace sets closed under selective interleaving functions, Proc. IEEE Symposium on Security and Privacy, IEEE Computer Society Press, 1994, pp. 79-93 |
| [24] | McLean, J., A general theory of composition for a class of “possibilistic” security properties, IEEE Transactions on Software Engineering, 22, 1, 53-67 (1996) |
| [25] | Milner, R., A complete inference system for a class of regular behaviors, Journal of Computer and System Sciences, 28, 3, 439-466 (1984) · Zbl 0562.68065 |
| [26] | Milner, R., Communication and Concurrency (1989), Prentice-Hall: Prentice-Hall London · Zbl 0683.68008 |
| [27] | R. Milner, The polyadic \(π\)-calculus: a tutorial, Technical Report ECS-LFCS-91-180, Department of Computer Science, Edinburgh University, 1991; R. Milner, The polyadic \(π\)-calculus: a tutorial, Technical Report ECS-LFCS-91-180, Department of Computer Science, Edinburgh University, 1991 |
| [28] | G. Plotkin, A structural approach to operational semantics, Technical Report DAIMI FN-19, University of Aarhus, 1981; G. Plotkin, A structural approach to operational semantics, Technical Report DAIMI FN-19, University of Aarhus, 1981 |
| [29] | A.W. Roscoe, J.C.P. Woodcock, L. Wulf, Non-interference through determinism, Proc. European Symposium on Research in Computer Security, Lecture Notes in Computer Science, vol. 875, Springer, Berlin, 1994, pp. 33-53; A.W. Roscoe, J.C.P. Woodcock, L. Wulf, Non-interference through determinism, Proc. European Symposium on Research in Computer Security, Lecture Notes in Computer Science, vol. 875, Springer, Berlin, 1994, pp. 33-53 · Zbl 1477.68063 |
| [30] | P.Y.A. Ryan, A CSP formulation of non-interference and unwinding, Proc. IEEE Computer Security Foundation Workshop, IEEE Computer Society Press, 1990; P.Y.A. Ryan, A CSP formulation of non-interference and unwinding, Proc. IEEE Computer Security Foundation Workshop, IEEE Computer Society Press, 1990 · Zbl 0825.68229 |
| [31] | De Simone, R., Higher level synchronization devices in SCCS-Meije, Theoretical Computer Science, 37, 245-267 (1985) · Zbl 0598.68027 |
| [32] | S. Tini, Rule formats for non-interference, Proc. European Symposium on Programming, Lecture Notes in Computer Science, vol. 2618, Springer, Berlin, 2003, pp. 129-143; S. Tini, Rule formats for non-interference, Proc. European Symposium on Programming, Lecture Notes in Computer Science, vol. 2618, Springer, Berlin, 2003, pp. 129-143 · Zbl 1032.68105 |
| [33] | I. Ulidowski, Equivalences on observable processes, Proc. IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, 1992, pp. 148-159; I. Ulidowski, Equivalences on observable processes, Proc. IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, 1992, pp. 148-159 |
| [34] | Ulidowski, I.; Phillips, I. C.C, Ordered SOS process languages for branching and eager bisimulations, Information and Computation, 178, 1, 180-213 (2002) · Zbl 1012.68116 |
| [35] | Vrancken, J. L.M, The algebra of communicating processes with empty process, Theoretical Computer Science, 177, 2, 287-328 (1997) · Zbl 0901.68112 |
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.
