Abstract
Authorization and protection deal with the problem of the control of access to resources. A key aspect of modern computing systems is resource sharing, so a need arose to govern access to these resources only to authorized users. In multi-user operating systems (such as Linux) authorization is of great interest. Computer security and authorization as a subset is characterized by the fact that a security fault or hole can be very costly. It is of great interest therefore to formalize and reason about security. Z notation is a powerful well-known formal notation based on set theory and predicate calculus which provides both abstraction and formalism. This work reports a formal expression in the Z notation for the basic protection (authorization) system of the Linux operating system.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Akyildiz, I. And Benson G., 1989, “Security Models of Distributed Systems”. In Proceedings of the 4th International Symposium on Computer and Information Sciences, A. Dogacand E. Gelenbe, Eds.Turkey.
Bell and LaPadula, 1973, “Secure Computer Systems : Mathematical Foundations”. ESD-TR-278, 1 , ESD/AFSC, Hanscom AFB, Bedford, Ma.
Bertino Elisa et al, 1996, “A Temporal Access Control Mechanism for Database Systems”, IEEE Transactions on Knowledge and Data Engineering Vol. 8, No. 1.
Bertino Elisa et al, 1996, “Supporting Periodic Authorization and Temporal Reasoning in Database Access Control,” Proceeding of the 22nd VLDB conference Mumbai, India.
Bertino Elisa, P. Sammarati and S. Jajodia, 1997, “An Extended Authorization Model for Relational Databases.” IEEE Transactions on Knowledge and Data Engineering.
Bertino Elisa et al, 1997, “A Flexible model for the Specification and Enforcement of Authorizations in Workflow Management Systems” Technical Report, University of Milano.
Boswell A., 1995, “Specification and Validation of a Security Policy Model,” in IEEE Transactions on Software Engineering, Vol. 21, No.2Benson G., I. Akyildiz and W. Applebe, 1990, “A Formal Protection Model of Security in Centralized, Parallel and Distributed Systems.” ACM Transaction on Computer Systems.
Boyd Colin, 1993, “Security Architectures Using Formal Methods,” IEEE Journal On Selected Areas In Communications.
Charles P. Pfleeger, 1989, “Security In Computing,” Prentice Hall.
Denning D.E., 1976, “A Lattice Model of Secure Information Flow”. Communications of the ACM.
Denning Dorothy, 1982, “Cryptography and Data Security,” Addison-Wesley.
Glasgow J., G.MacEwen and P. Panangaden, 1992, “A Logic for Reasoning About Security,” ACM Transaction on Computer Systems.
Goscinski A. G., 1991 “Distributed Operating Systems The Logical Design,” Adison-Wesly.
Graham and Denning, 1972, “Protection Principles and practices.” Proceedings of the AFIPS Spring Joint Computer Conference.
Harrison, Ruzzo and Ullman, 1976, “Protection in operating system,” Communications of the ACM.
Johnson Michael & Troan Erik, 2005, “Linux Application Development”, 2nd edition, Pearson Education.
Kwon J., Chang-Joo Moon, 2007, “Visual Modeling and Formal Specification of Constraints of RBAC Using Semantic Web Technology,” Knowledge-Based System, Volume 20, Issue 4.
Lampson B. W., 1971, “Protection”. Fifth Princeton Conference on Information and Systems Sciences.
Landwehr C.E., 1981, “Formal Models for Computer Security.” ACM Computing Surveys 13(3).
Leiss Ernst, 1982, “Principles of Data Security,” Plenum Press.
Mclean John, 1990, “The Specification And Modeling Of Computer Security.” IEEE Computer, Volume 23, Issue 1.
Peleg M., Dizza Beimel, Dov Dori, Yaron Denekamp, 2008, “Situation -Based Access Control: Privacy Management Via Modeling of Patient Data Access Scenarios” Journal of Biomedical Informatics.
Potter B., Sinclair J. And Till D. 1996 “An Introduction to Formal Specification and Z,” 2nd edition, Prentice Hall.
Rayis Osama, 1996, “Software Protection through dedicated Hardware. Ms Thesis Middle East Technical University.
Rayis Osama, 1997, “An Adaptable Workflow Environment, Authorization Model Definition,” Technical Report SRDC - Middle East Technical University.
Sandhu Ravi and Pierangela Samarati, 1994, “Access Control: Principles and Practice”. IEEE Communications, 32(9):40-48.
Sandhu Ravi, Edward J. Coyne, Hal L. Feinstein and Charles E. Youman, 1996 “Role-Based Access Control Models,” IEEE Computer, 29(2):38-47.
Snekkenes E., 1990, “Authentication in Open Systems”, in Protocol Spec. Testing & Ver., Elsevier Science Publishers.
Stallings B., 2007 “Role-Based Access Control in Computer Security” Prentice Hall.
Stallings W., Brown L., 2007, “Computer Security: Principles and Practice,” Prentice Hall.
Tomur E., Erten Y., 2006 “Application Of Temporal and Spatial Role Based Access Control In 802.11 Wireless Networks,” Computers & Security, Vol. 25, Issue 6.
Vijayalakshmi Atluri and Wei-Kuang Huang, 1996, “An Authorization Model for Workflows”, Computer Security - ESORICS 96, Rome.
Wordsworth J.B., 1992, “Software Development with Z”, Addison-Wesley.
Torvalds L., 2008, “The Linux Kernel,” http://www.kernel.org/
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer Science+Business Media B.V.
About this paper
Cite this paper
Rayis, O.A. (2010). Formally Specifying Linux Protection. In: Sobh, T., Elleithy, K., Mahmood, A. (eds) Novel Algorithms and Techniques in Telecommunications and Networking. Springer, Dordrecht. https://doi.org/10.1007/978-90-481-3662-9_12
Download citation
DOI: https://doi.org/10.1007/978-90-481-3662-9_12
Published:
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-3661-2
Online ISBN: 978-90-481-3662-9
eBook Packages: EngineeringEngineering (R0)