Abstract
Structural non-interference is a semi-static technique defined over Petri nets to check the absence of illegal information flows. This paper presents the main algorithmic features of this new technique and its implementation in a software tool, called the Petri Net Security Checker.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Busi, N., Gorrieri, R.: A Survey on Non-Interference with Petri Nets. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 328–344. Springer, Heidelberg (2004)
Busi, N., Gorrieri, R.: Positive Non-Interference in Elementary and Trace Nets. In: Cortadella, J., Reisig, W. (eds.) ICATPN 2004. LNCS, vol. 3099, pp. 1–16. Springer, Heidelberg (2004)
Busi, N., Gorrieri, R.: Structural Non-Interference in Elementary and Trace Nets. In: Mathematical Structures in Computer Science (2008) (accepted for publication) (2008/4/3), http://www.cs.unibo.it/~gorrieri/Papers/bg08.ps
Brooks, S.D., Hoare, C.A.R., Roscoe, A.W.: A Theory of Communicating Sequential Processes. Journal of the ACM 31(3), 560–599 (1984)
Engelfriet, J., Rozenberg, G.: Elementary Net Systems. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 12–121. Springer, Heidelberg (1998)
Focardi, R., Gorrieri, R.: A Classification of Security Properties. Journal of Computer Security 3(1), 5–33 (1995)
Focardi, R., Gorrieri, R.: The Compositional Security Checker: A Tool for the Verification of Information Flow Security Properties. IEEE Transactions on Software Engineering 23(9), 550–571 (1997)
Focardi, R., Gorrieri, R.: Classification of Security Properties (Part I: Information Flow). In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol. 2171, pp. 331–396. Springer, Heidelberg (2001)
Frau, S.: Uno strumento sotware per l’analisi di proprietà di sicurezza su reti di Petri. Master thesis (in Italian), University of Bologna (March 2008)
Goguen, J.A., Meseguer, J.: Security Policy and Security Models. In: Proc. of Symposium on Security and Privacy, pp. 11–20. IEEE CS Press, Los Alamitos (1982)
Martinelli, F.: Partial Model Checking and Theorem Proving for Ensuring Security Properties. In: Proc. of Computer Security Foundations Workshop, pp. 44–52. IEEE CS Press, Los Alamitos (1998)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Roscoe, A.W.: CSP and Determinism in Security Modelling. In: Proc. of IEEE Symposium on Security and Privacy, pp. 114–127. IEEE CS Press, Los Alamitos (1995)
Ryan, P.Y.A.: Mathematical models of computer security. In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol. 2171, pp. 1–62. Springer, Heidelberg (2001)
Ryan, P.Y.A., Schneider, S.: Process Algebra and Noninterference. In: Proc. of 12th Computer Security Foundations Workshop, pp. 214–227. IEEE CS Press, Los Alamitos (1999)
Java Technology. Sun Microsystems (2008/4/3), http://java.sun.com/
Eclipse.org. Eclipse Foundation (2008/4/3), http://www.eclipse.org/
http://www2.informatik.hu-berlin.de/top/pnml/download/about/PNML_LNCS.pdf (2008/4/3)
Platform Independent Petri Net Editor (2008/4/3), http://pipe2.sourceforge.net/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Frau, S., Gorrieri, R., Ferigato, C. (2009). Petri Net Security Checker: Structural Non-interference at Work. In: Degano, P., Guttman, J., Martinelli, F. (eds) Formal Aspects in Security and Trust. FAST 2008. Lecture Notes in Computer Science, vol 5491. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-01465-9_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-01465-9_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-01464-2
Online ISBN: 978-3-642-01465-9
eBook Packages: Computer ScienceComputer Science (R0)