Top

Programming and Computer Software

Published in:

01-12-2020

Integrating RBAC, MIC, and MLS in Verified Hierarchical Security Model for Operating System

Authors: P. N. Devyanin, A. V. Khoroshilov, V. V. Kuliamin, A. K. Petrenko, I. V. Shchepetkov

Published in: Programming and Computer Software | Issue 7/2020

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Designing a trusted access control mechanism of an operating system (OS) is a complex task if the goal is to achieve high level of security assurance and guarantees of unwanted information flows absence. Even more complex it becomes when the integration of several heterogeneous mechanisms, like role-based access control (RBAC), mandatory integrity control (MIC), and multi-level security (MLS) is considered. This paper presents results of development of a hierarchical integrated model of access control and information flows (HIMACF), which provides a holistic integration of RBAC, MIC, and MLS preserving key security properties of all those mechanisms. Previous version of this model is called MROSL DP-model. Now the model is formalized using Event-B formal method and its correctness is formally verified. In the hierarchical representation of the model, each hierarchy level (module) corresponds to a separate security control mechanism, so the model can be verified with less effort reusing the results of verification of lower level modules. The model is implemented in a Linux-based operating system using the Linux Security Modules infrastructure.

next article Occlusion Culling Algorithm Based on Software Visibility Checks

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Here and further we use \(\mathcal{P}(X)\) to denote the set of all subsets of X.

Sandhu, R.S., Coyne, E.J., Feinstein, H.L., and Youman, C.E., Role-based access control models, Computer, 1996, vol. 29, no. 2, pp. 38–47. https://doi.org/10.1109/2.485845CrossRef

Smalley, S., Vance, C., and Salamon, W., Implementing SELinux as a linux security module, Tech. Rep., NAI Labs, 2001, no. 01-043.

Smalley, S. and Craig, R., Security enhanced (SE) Android: bringing flexible MAC to Android, Proc. Network & Distributed System Security Symp. (NDSS), San Diego, 2013.

Conover, M., Analysis of the Windows Vista security model, Tech. Rep., Symantec Corp., 2008.

Cunningham, A. and Hutchinson, L., OS X 10.11 El Capitan: the Ars Technica review. https://arstechnica.com/apple/2015/09/os-x-10-11-el-capitan-the-ars-technica-review/. Accessed Jan. 21, 2019.

Bell, D.E. and LaPadula, L.J., Secure computer systems: mathematical foundations, Electronic Systems Division, AFSC, Hanscom AFB, 1973, no. ESD-TR-73-278 v. 1 (also MTR-2547, v. 1).

Biba, K.J., Integrity considerations for secure computer systems, Tech. Rep., The MITRE Corp., 1977, no. MTR-3153.

Sandhu, R., Role hierarchies and constraints for lattice-based access controls, in Computer Security – ESORICS 96, LNCS 1146:65–79, Bertino, E., Kurth, H., Martella, G., and Montolivo, E., Eds., Springer-Verlag, 1996. https://doi.org/10.1007/3-540-61770-1_28CrossRef

Devyanin, P.N., The Models of Security of Computer Systems: access Control and Information Flows, Hot-line Telecom, 2013.

10.

Devyanin, P.N., Khoroshilov, A.V., Kuliamin, V.V., Petrenko, A.K., and Shchepetkov, I.V., Formal verification of OS security model with alloy and event-B, in ABZ 2014: Abstract State Machines, Alloy, B, TLA, VDM, and Z. LNCS, Ait Ameur, Y. and Schewe, K.-D., Eds., Springer-Verlag, 2014, pp. 309–313. https://doi.org/10.1007/978-3-662-43652-3_30CrossRef

11.

Abrial, J.-R., Modeling in Event-B: System and Software Engineering, Cambridge Univ. Press, 2010.CrossRef

12.

Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., and Voisin, L., Rodin: an open toolset for modelling and reasoning in Event-B, Int. J. Software Tools Tech. Transf., 2010, vol. 12, no. 6, pp. 447–466. https://doi.org/10.1007/s10009-010-0145-yCrossRef

13.

ISO/IEC 15408-1:2009: Information Technology – Security Techniques – Evaluation Criteria for IT Security – Part 1: Introduction and General Model, ISO, 2009.

14.

ISO/IEC 15408-2:2008: Information Technology – Security Techniques – Evaluation Criteria for IT Security – Part 2: Security Functional Components, ISO, 2008.

15.

Astra Linux. https://en.wikipedia.org/wiki/Astra_Linux. Accessed Jan. 21, 2019.

16.

Sandhu, R., Bhamidipati, V., and Munawer, Q., The ARBAC97 model for role-based administration of roles, ACM Trans. Inf. Syst. Secur., 1999, vol. 2, no. 1, pp. 105–135. https://doi.org/10.1145/300830.300839CrossRef

17.

American National Standard for Information Technology – Role Based Access Control. ANSI INCITS 359-2004, 2004.

18.

Bell, D.E. and LaPadula, L.J., Secure Computer System: Unified Exposition and MULTICS Interpretation, Electronic System Division, AFSC, Hanscom AFB, 1976, no. ESD-TR-75-306 (also MTR-2997).

19.

Jones, A.K., Lipton, R.J., and Snyder, L., A linear time algorithm for deciding security, Proc. 17th Annu. Symp. on Foundations of Computer Science, Houston, 1976, pp. 33–41. https://doi.org/10.1109/SFCS.1976.1

20.

Bishop, M. and Snyder, L., The transfer of information and authority in a protection system, Proc. 7th ACM Symp. on Operating System Principles, Pacific Grove, CA, 1979, pp. 45–54. https://doi.org/10.11145/800215.806569.

21.

Landwehr, C.E., Heitmeyer, C.L., and McLean, J., A security model for military message systems, ACM Trans. Comput. Syst., 1984, vol. 2, no. 3, pp. 198–222. https://doi.org/10.1145/989.991CrossRef

22.

Security-Enhanced Linux. http://www.nsa.gov/what-we-do/research/selinux/. Accessed Jan. 21, 2019.

23.

PostgreSQL. https://en.wikipedia.org/wiki/PostgreSQL. Accessed Jan. 21, 2019.

24.

D-Bus. https://en.wikipedia.org/wiki/D-Bus. Accessed Jan. 21, 2019.

25.

Window System. https://en.wikipedia.org/wiki/X_Window_System. Accessed Jan. 21, 2019.

26.

Eaman, A., Sistany, B., and Felty, A., Review of existing analysis tools for SELinux security policies: challenges and a proposed solution, in MCETECH 2017: ETechnologies: Embracing the Internet of Things, Aimeur, E., Ruhi, U., and Weiss, M., Eds., Cham: Springer, 2017, pp. 116–135. https://doi.org/10.1007/978-3-319-59041-7_7CrossRef

27.

Zanin, G. and Mancini, L.V., Towards a formal model for security policies specification and validation in the Selinux system, in Proc. of 9th ACM Symp. on Access Control Models and Technologies, New York: Yorktown Heights, 2004, pp. 136–145. https://doi.org/10.1145/990036.990059

28.

Zhai, G., Guo, T., and Huang, J., SCIATool: a tool for analyzing SELinux policies based on access control spaces, information flows and CPNs, in Proc. 6th Int. Conf. on Trusted Systems, New York: Springer Verlag, 2015, vol. 9473, pp. 294–309. https://doi.org/10.1007/978-3-319-27998-5_19

29.

Amthor, P., Kuhnhauser, W.E., and Pölck, A., Model-based safety analysis of SELinux security policies, Proc. 5th Int. Conf. on Network and System Security (NSS), Milan, 2011, pp. 208–215.

30.

Harrison, M.A., Ruzzo, W.L., and Ullman, J.D., Protection in operating systems, Commun. ACM, 1976, vol. 19, no. 8, pp. 461–471. https://doi.org/10.1145/360303.360333CrossRefMATH

31.

Hicks, B., Rueda, S., St.Clair, L., Jaeger, T., and McDaniel, P., A logical specification and analysis for SELinux MLS policy, ACM Trans. Inf. Syst. Secur., 2010, vol. 13, no. 3, art. no. 26. https://doi.org/10.1145/1805874.1805982CrossRef

32.

Tschantz, M.C., The clarity of languages for access-control policies, PhD Thesis, Providence, RI: Brown Univ., 2005.

33.

Devyanin, P.N., Kuliamin, V.V., Petrenko, A.K., Khoroshilov, A.V., and Shchepetkov, I.V., Comparison of specification decomposition methods in Event-B, Prog. Comput. Software, 2016, vol. 42, no. 4, pp. 198–205. https://doi.org/10.1134/S0361768816040022CrossRefMATH

34.

Filliâtre, J.-C. and Paskevich, A., Why3 – where programs meet provers, in Programming Languages and Systems, Felleisen, M. and Gardner, P., Eds., Springer-Verlag, 2013. https://doi.org/10.1007/978-3-642-37036-6_8CrossRef

35.

Efremov, D., Mandrykin, M., and Khoroshilov, A., Deductive verification of unmodified Linux kernel library functions, in Leveraging Applications of Formal Methods, Verification and Validation, Margaria, T. and Steffen, B., Eds., Springer-Verlag, 2018. https://doi.org/10.1007/978-3-030-03421-4_15CrossRef

36.

McLean, J., The specification and modeling of computer security, Computer, 1990, vol. 23, no. 1, pp. 9–16. https://doi.org/10.1109/2.48795CrossRef

Title: Integrating RBAC, MIC, and MLS in Verified Hierarchical Security Model for Operating System
Authors: P. N. Devyanin
A. V. Khoroshilov
V. V. Kuliamin
A. K. Petrenko
I. V. Shchepetkov
Publication date: 01-12-2020
Publisher: Pleiades Publishing
Published in: Programming and Computer Software / Issue 7/2020
Print ISSN: 0361-7688
Electronic ISSN: 1608-3261
DOI: https://doi.org/10.1134/S0361768820070026

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Technik"

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Premium Partner