Modeling of Access Control System in Event-B
Abstract
Computer security is a major challenge in the current era of ubiquitous computing and the Internet. The external security measures are good but not enough to secure software systems. That is why the internal security of software systems is of much importance and more emphasis needs to be given to describe internal design of software systems. Access control system is a mechanism to ensure the internal security of software systems. There are various access control systems which are claimed to provide a secure way to access the resources but in reality these systems have many loopholes and drawbacks. Authentication and authorization are the major key elements of access control systems. Authentication is a mechanism to verify unique identification of a user in the system, and authorization is to grant access to a user to system resources. In this paper, a new generic and simplified model of access control any system is proposed which is based on formal methods. The formal method used in this access control system is Event-B. Event-B is a formal specification and modeling language based on set theory and first order logic. Authentication process ensures that which type of users are allowed to access the system. In authorization mechanism it is ensured that a user is granted access to a system resource only if he/she has access rights for that particular resource. The resulting formal models are analyzed and verified by using RODIN tools.
References
D.D. Clark and D.R. Wilson, “A comparison of commercial and military computer security policiesâ€, IEEE Symposium on Security and Privacy, pp. 184–184, 1987.
S. Hussain, P. Dunne and G. Rasool, “Formal Specification of Security Properties using Z Notationâ€, Research Journal of Applied Sciences, Engineering and Technology, vol. 5, no. 19, pp. 4664–4670, 2013. [3] S. Hussain, G. Rasool, M. Atef and A.K. Shahid, “A review of approaches to model security into software systemsâ€, Journal of Basic and Applied Scientific Research, vol. 3, no. 4, pp. 642–647, 2013.
S. Hussain, G. Rasool, M. Atef and A.K. Shahid, “FDMSWAP: Formal Development Methodology for Secure Web Applicationsâ€, Journal of Basic and Applied Scientific Research, vol. 3, no. 4, pp. 1123-1128, 2013. [5] T.S. Hoang, D. Basin and J.-R. Abrial, “Specifying access control in Event-Bâ€, Technical Report, vol. 624, 2009.
D. Gollmann, “Computer Securityâ€, Wiley Interdisciplinary Reviews: Computational Statistics, vol. 2, no.5, pp. 544-554, 2010. [7] J. Barkley, K. Beznosov and J. Uppal, “Supporting relationships in access control using role based access controlâ€, Proceedings of the fourth ACM workshop on Role-based access control, pp. 55–65, 1999. [8] E.C. Cheng, “An object-oriented organizational model to support dynamic role-based access control in electronic commerceâ€, Decision Support Systems, vol. 29, no. 4, pp. 357–369, 2000. [9] J.R. Abrial, Modeling in Event-B: System and Software Development, Cambridge University Press, 2010. [10] J.R. Abrial, “Formal methods: Theory becoming practiceâ€, J. UCS, vol. 13, no. 5, pp. 619–628, 2007. [11] M.A. Harrison, W.L. Ruzzo and J.D. Ullman, “Protection in operating systemsâ€, Communications of the ACM, vol. 19 no. 8, pp. 461-471, 1976. [12] S.I. Gavrila and J.F Barkley, “Formal specification for role based access control user/role and role/role relationship managementâ€, Proceedings of the third ACM workshop on Role-based access control, October 1998, pp. 81-90. [13] E. Bertino, P.A Bonatti and E. Ferrari, “TRBAC: A temporal role-based access control modelâ€, ACM Transactions on Information and System Security (TISSEC), vol. 4, no. 3, pp.191-233, 2001. [14] R. Sandhu, D. Ferraiolo and R. Kuhn, “The NIST model for role-based access control: Towards a unified standardâ€, ACM Workshop on Role-based Access Control, pp. 1-11, July 2000. [15] D.E. Bell and L.J. LaPadula, “Secure computer systems: Mathematical foundationsâ€, Mitre Corp Bedford MA, vol. 1, no. MTR-2547, 1973. [16] K.J. Biba, “Integrity considerations for secure computer systemsâ€, Mitre Corp Bedford MA, vol. 1, no. MTR-3153, 1977.
S. Hussain et al. / The Nucleus 55, No. 2 (2018) 74-84
M.A. Bishop, “The art and science of computer security, Addison-Wesley Longman Publishing Co., Inc., 2002. [18] A. Belapurkar, A. Chakrabarti, H. Ponnapalli, N. Varadarajan, S. Padmanabhuni and S. Sundarrajan, “Distributed systems security: issues, processes and solutionsâ€, John Wiley & Sons, 2009. [19] R. Baskerville, and M. Siponen, “An information security meta-policy for emergent organizationsâ€, Logistics Information Management, vol. 15, no. 5/6, pp. 337-346, 2002. [20] J. Rees, S. Bandyopadhyay and E.H. Spafford, “PFIRES: A policy framework for information securityâ€, Communications of the ACM, vol. 46, no 7, pp.101-106, 2003. [21] C.W. Probst, R.R. Hansen and F. Nielson, “Where can an insider attack?â€, Proc. of International Workshop on Formal Aspects in Security and Trust, Heidelberg, Berlin: Springer, , pp.127-142, 2004. [22] M. Abrams, and D. Bailey, “Abstraction and refinement of layered security policyâ€, Information Security: An Integrated Collection of Essays, pp.126-136, 19995. [23] I.M. Olson and M.D. Abrams, “Information security policyâ€, Information Security: An Integrated Collection of Essays, 1995. [24] D. Pavlovic and D.R. Smith, 2003. “Software development by refinementâ€, Formal Methods at the Crossroads from Panacea to Foundational Support, Heidelberg, Berlin: Springer, 2003, pp. 267-286. [25] D. Sannella and A. Tarlecki, “Foundations of algebraic specification and formal software developmentâ€, Springer Science & Business Media, 2012. [26] W. Pieters, T. Dimkov and D. Pavlovic, “Security policy alignment: A formal approachâ€, IEEE Systems Journal, vol. 7, no. 2, pp.275-287, 2013. [27] S. Fugkeaw, P. Manpanpanich and S. Juntapremjitt, “A hybrid multi-application authentication and authorization model using multi-agent system and PKIâ€, Proc. of the Fourth IASTED Asian Conference on Communication Systems and Networks, ACTA Press, pp. 96-101, March 2007. [28] J. Li, and D. Cordes, “A scalable authorization approach for the Globus grid systemâ€, Future Generation Computer Systems, vol. 21, no. 2, pp. 291-301, 2005. [29] E. Palomar, J.M. Estevez-Tapiador, J.C. Hernandez-Castro and A. Ribagorda, “Certificate-based access control in pure p2p networksâ€, Sixth IEEE International Conference on Peer-to-Peer Computing, pp. 177-184, 2006. [30] O. Cánovas, A.F. Gómez-Skarmeta, G. López and M. Sánchez, “Deploying authorization mechanisms for federated services in eduroam (DAMe)â€, Internet Research, vol. 17, no. 5, pp.479-494, 2007. [31] A. Gbadegesin, R. Batoukov and D.R. Reed, “Flexible scalable application authorization for cloud computing environmentsâ€, U.S. Patent 8,418,222, Microsoft Corporation, 2013. [32] J.A Calero, G.M. Perez and A.G. Skarmeta, “Towards an authorisation model for distributed systems based on the Semantic Webâ€, IET information security, vol. 4, no. 4, pp.411-421, 2010. [33] A. Moini, and A.M. Madni, “Leveraging biometrics for user authentication in online learning: A systems perspectiveâ€, IEEE Systems Journal, vol. 3 no, 4, pp. 469-476, 2009. [34] D. Arora, S. Ravi, A. Raghunathan and N.K. Jha, “Hardware-assisted run-time monitoring for secure program execution on embedded processorsâ€, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, vol. 14, no. 12, pp. 1295-1308, 2006. [35] D.D. Hwang, P. Schaumont, K. Tiri and I. Verbauwhede, “Securing embedded systemsâ€, IEEE Security & Privacy, vol. 4, no. 2, pp.40-49, 2006. [36] D. Mu, W. Hu, B. Mao and B. Ma, “A bottom-up approach to verifiable embedded system information flow securityâ€, IET Information Security, vol. 8, no. 1, pp. 12-17, 2014. [37] M. Abadi and R. Needham, “Prudent engineering practice for cryptographic protocolsâ€, IEEE transactions on Software Engineering, no. 1, pp. 6–15, 1996. [38] P. England, B. Lampson, J. Manferdelli and B. Willman, “A trusted open platformâ€, Computer, vol. 36, no. 7, pp. 55-62, 2003. [39] J.R. Abrial and S. Hallerstede, “Refinement, decomposition and instantiation of discrete models: Application to Event-Bâ€, Fundamenta Informaticae, vol. 77, no, 1-2, pp. 1-28, 2007. [40] J.P. Bowen, K. Bogdanov, J.A. Clark, M. Harman, R.M. Hierons and P. Krause, 2002, August. “FORTEST: Formal methods and testingâ€, in Proc. of IEEE 26th Annual International of Computer Software and Applications Conference, pp. 91-101, August 2002. [41] J.R. Abrial, M. Butler, S. Hallerstede, T.S. Hoang, F. Mehta and L. Voisin, “Rodin: An open toolset for modelling and reasoning in Event-Bâ€, Int. Journal on Software Tools for Technology Transfer, vol. 12, no. 6, pp. 447-466, 2010. [42] P. Bjesse, “What is formal verification?â€, ACM SIGDA Newsletter, vol. 35, no. 24, p. 1, 2005. [43] L. Ma and J. J. Tsai, “Formal modeling and analysis of a secure mobile-agent systemâ€, IEEE Transactions on Systems, Man and Cybernetics-Part A: Systems and Humans, vol. 38, no. 1, pp. 180–196, 2008. [44] J. Bendisposto, M. Jastram, M. Leuschel, C. Lochert, B. Scheuermann and I. Weigelt, “Validating Wireless Congestion Control and Realiability Protocols using ProB and Rodinâ€, Workshop on Formal Methods for Wireless Systems, August 2008. [45] N.A. Zafar, “Safety control management at airport taxiing to take-off procedureâ€, Arabian Journal for Science and Engineering, vol. 39, no. 8, pp. 6137-6148, 2014. [46] N.A. Zafar, “Formal Model of Aircrafts Safety Separationâ€, International Journal of Innovative Computing, Information and Control, vol. 10, no. 4, pp. 1401-1412, 2014.
