×

Multilevel transitive and intransitive non-interference, causally. (English) Zbl 1380.68292

Summary: We develop a theory of non-interference for multilevel security based on causality, with Petri nets as a reference model. We first focus on transitive non-interference, where the relation representing the admitted flow is transitive. Then we extend the approach to intransitive non-interference, where the transitivity assumption is dismissed, leading to a framework which is suited to model a controlled disclosure of information. Efficient verification algorithms based on the unfolding semantics of Petri nets stem out of the theory. We also argue about the possibility of performing a compositional verification.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q55 Semantics in the theory of computing
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

Anica; PEP; MultiUbic
PDFBibTeX XMLCite
Full Text: DOI HAL

References:

[1] Goguen, J. A.; Meseguer, J., Security policies and security models, (Proceedings of the Symposium on Security and Privacy (1982), IEEE Computer Society), 11-20
[2] Focardi, R.; Gorrieri, R., Classification of security properties (part I: information flow), (Proceedings of FOSAD’00 (2001), Springer), 331-396 · Zbl 1007.68508
[3] Ryan, P.; Schneider, Y., Process algebra and non-interference, J. Comput. Secur., 9, 1/2, 75-103 (2001)
[4] Mantel, H., Possibilistic definitions of security - an assembly kit, (Proceedings of CSFW’00 (2000), IEEE Computer Society), 185-199
[5] Busi, N.; Gorrieri, R., Structural non-interference in elementary and trace nets, Math. Structures Comput. Sci., 19, 6, 1065-1090 (2009) · Zbl 1191.68431
[6] Best, E.; Darondeau, P.; Gorrieri, R., On the decidability of non interference over unbounded Petri nets, (Chatzikokolakis, K.; Cortier, V., Proceedings of SecCo’10. Proceedings of SecCo’10, EPTCS, vol. 51 (2010), Open Publishing Association), 16-33
[7] Baldan, P.; Carraro, A., A causal view on non-interference, Fund. Inform., 140, 1, 1-38 (2015) · Zbl 1335.68162
[8] McCullough, D., Noninterference and the composability of security properties, (Symposium on Security and Privacy (1988), IEEE Computer Society), 178-186
[9] Wittbold, J.; Johnson, D., Information flow in nondeterministic systems, (Symposium on Security and Privacy (1990), IEEE Computer Society), 148-161
[10] Nielsen, M.; Plotkin, G.; Winskel, G., Petri nets, event structures and domains, part 1, Theoret. Comput. Sci., 13, 85-108 (1981) · Zbl 0452.68067
[11] Denning, D. E., A lattice model of secure information flow, Commun. ACM, 19, 5, 236-243 (1976) · Zbl 0322.68034
[12] Rushby, J. M., Design and verification of secure systems, (Proceedings of SOSP’81 (1981), ACM), 12-21
[13] Baldan, P.; Burato, F.; Carraro, A., Intransitive non-interference by unfolding, (Lanese, I.; Madelaine, E., Proceedings of FACS’14. Proceedings of FACS’14, Lecture Notes in Comput. Sci., vol. 8997 (2014), Springer), 269-287
[14] Beggiato, A., MultiUBIC, doi:
[15] Service Technology, ANICA: Automated Non-Interference Check Assistant
[16] Gorrieri, R.; Vernali, M., On intransitive non-interference in some models of concurrency, (Aldini, A.; Gorrieri, R., Proceedings of FOSAD’11. Proceedings of FOSAD’11, Lecture Notes in Comput. Sci., vol. 6858 (2011), Springer), 125-151 · Zbl 1344.68073
[17] Esparza, J.; Heljanko, K., Unfoldings - A Partial order Approach to Model Checking, Monogr. Theoret. Comput. Sci. EATCS Ser. (2008), Springer · Zbl 1153.68035
[18] McMillan, K. L., A technique of state space search based on unfolding, Form. Methods Syst. Des., 6, 1, 45-65 (1995) · Zbl 0829.68085
[19] Khomenko, V.; Koutny, M.; Vogler, W., Canonical prefixes of Petri net unfoldings, Acta Inform., 40, 95-118 (2003) · Zbl 1072.68072
[20] Meseguer, J.; Montanari, U.; Sassone, V., Representation theorems for Petri nets, (Freksa, C.; Jantzen, M.; Valk, R., Foundations of Computer Science: Potential - Theory - Cognition. Foundations of Computer Science: Potential - Theory - Cognition, Lecture Notes in Comput. Sci., vol. 1337 (1997), Springer), 239-249 · Zbl 0885.68115
[21] Rushby, J., Noninterference, transitivity, and channel-control security policies (Dec. 1992), Tech. rep.
[22] Esparza, J.; Römer, S.; Vogler, W., An improvement of McMillan’s unfolding algorithm, Form. Methods Syst. Des., 20, 20, 285-310 (2002) · Zbl 1017.68085
[23] Best, E.; Grahlmann, B., PEP Documentation and User Guide 1.8 (1998)
[24] Frau, S.; Gorrieri, R.; Ferigato, C., Petri net security checker: structural non-interference at work, (Degano, P.; Guttman, F.; Martinelli, J., Proceedings of FAST’08. Proceedings of FAST’08, Lecture Notes in Comput. Sci., vol. 5491 (2008), Springer), 210-225
[25] Accorsi, R.; Lehmann, A., Automatic information flow analysis of business process models, (Barros, A.; Gal, A.; Kindler, E., Proceedings of BPM’12. Proceedings of BPM’12, Lecture Notes in Comput. Sci., vol. 7481 (2012), Springer), 172-187
[26] Haar, S., Types of asynchronous diagnosability and the reveals-relation in occurrence nets, IEEE Trans. Automat. Control, 55, 10, 2310-2320 (2010) · Zbl 1368.68262
[27] Hadj-Alouane, B. N.; Lafrance, S.; Lin, F.; Mullins, J.; Yeddes, M. M., On the verification of intransitive noninterference in multilevel security, IEEE Trans. Syst. Man Cybern., Part B, 35, 5, 948-958 (2005)
[28] Bryans, J.; Koutny, M.; Ryan, P., Modelling dynamic opacity using Petri nets with silent actions, (Dimitrakos, T.; Martinelli, F., Proceedings of FAST’05. Proceedings of FAST’05, Lecture Notes in Comput. Sci., vol. 173 (2005), Springer), 159-172
[29] Best, E.; Darondeau, P., Deciding selective declassification of Petri nets, (POST’12. POST’12, Lecture Notes in Comput. Sci., vol. 7215 (2012), Springer), 290-308 · Zbl 1353.68196
[30] Mantel, H.; Sands, D., Controlled declassification based on intransitive noninterference, (APLAS’04 (2004)), 129-145 · Zbl 1116.68397
[31] van Glabbeek, R.; Goltz, U., Refinement of actions and equivalence notions for concurrent systems, Acta Inform., 37, 4/5, 229-327 (2001) · Zbl 0969.68081
[32] Fröschle, S., Causality, behavioural equivalences, and the security of cyberphysical systems, (Meyer, R.; Platzer, A.; Wehrheim, H., Correct System Design. Correct System Design, Lecture Notes in Comput. Sci., vol. 9360 (2015), Springer), 83-98 · Zbl 1444.68041
[33] Lluch-Lafuente, A.; Nielson, F.; Nielson, H. R., Discretionary information flow control for interaction-oriented specifications, (Logic, Rewriting, and Concurrency - Essays dedicated to José Meseguer on the Occasion of His 65th Birthday. Logic, Rewriting, and Concurrency - Essays dedicated to José Meseguer on the Occasion of His 65th Birthday, Lecture Notes in Comput. Sci., vol. 9200 (2015), Springer), 427-450 · Zbl 1321.68349
[34] Hack, M., Decidability Questions for Petri Nets, Outstanding Dissertations in the Computer Sciences (1975), Garland Publishing
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.