{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,12,20]],"date-time":"2023-12-20T00:34:35Z","timestamp":1703032475903},"reference-count":36,"publisher":"Pleiades Publishing Ltd","issue":"7","license":[{"start":{"date-parts":[[2020,12,1]],"date-time":"2020-12-01T00:00:00Z","timestamp":1606780800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,12,1]],"date-time":"2020-12-01T00:00:00Z","timestamp":1606780800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Program Comput Soft"],"published-print":{"date-parts":[[2020,12]]},"DOI":"10.1134\/s0361768820070026","type":"journal-article","created":{"date-parts":[[2020,12,11]],"date-time":"2020-12-11T12:09:05Z","timestamp":1607688545000},"page":"443-453","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Integrating RBAC, MIC, and MLS in Verified Hierarchical Security Model for Operating System"],"prefix":"10.1134","volume":"46","author":[{"given":"P. N.","family":"Devyanin","sequence":"first","affiliation":[]},{"given":"A. V.","family":"Khoroshilov","sequence":"additional","affiliation":[]},{"given":"V. V.","family":"Kuliamin","sequence":"additional","affiliation":[]},{"given":"A. K.","family":"Petrenko","sequence":"additional","affiliation":[]},{"given":"I. V.","family":"Shchepetkov","sequence":"additional","affiliation":[]}],"member":"137","published-online":{"date-parts":[[2020,12,11]]},"reference":[{"key":"3538_CR1","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1109\/2.485845","volume":"29","author":"R.S. Sandhu","year":"1996","unstructured":"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\u201347. https:\/\/doi.org\/10.1109\/2.485845","journal-title":"Computer"},{"key":"3538_CR2","unstructured":"Smalley, S., Vance, C., and Salamon, W., Implementing SELinux as a linux security module, Tech. Rep., NAI Labs, 2001, no. 01-043."},{"key":"3538_CR3","volume-title":"Security enhanced (SE) Android: bringing flexible MAC to Android, Proc. Network & Distributed System Security Symp.","author":"S. Smalley","year":"2013","unstructured":"Smalley, S. and Craig, R., Security enhanced (SE) Android: bringing flexible MAC to Android, Proc. Network & Distributed System Security Symp. \n (NDSS), San Diego, 2013."},{"key":"3538_CR4","volume-title":"Analysis of the Windows Vista security model, Tech. Rep.","author":"M. Conover","year":"2008","unstructured":"Conover, M., Analysis of the Windows Vista security model, Tech. Rep., Symantec Corp., 2008."},{"key":"3538_CR5","unstructured":"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."},{"key":"3538_CR6","unstructured":"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)."},{"key":"3538_CR7","unstructured":"Biba, K.J., Integrity considerations for secure computer systems, Tech. Rep., The MITRE Corp., 1977, no. MTR-3153."},{"key":"3538_CR8","series-title":"Role hierarchies and constraints for lattice-based access controls","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61770-1_28","volume-title":"Computer Security \u2013 ESORICS 96, LNCS 1146:65\u201379","author":"R. Sandhu","year":"1996","unstructured":"Sandhu, R., Role hierarchies and constraints for lattice-based access controls, in Computer Security \u2013 ESORICS 96, LNCS 1146:65\u201379, Bertino, E., Kurth, H., Martella, G., and Montolivo, E., Eds., Springer-Verlag, 1996. https:\/\/doi.org\/10.1007\/3-540-61770-1_28"},{"key":"3538_CR9","volume-title":"The Models of Security of Computer Systems: access Control and Information Flows","author":"P.N. Devyanin","year":"2013","unstructured":"Devyanin, P.N., The Models of Security of Computer Systems: access Control and Information Flows, Hot-line Telecom, 2013."},{"key":"3538_CR10","series-title":"Formal verification of OS security model with alloy and event-B","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43652-3_30","volume-title":"ABZ 2014: Abstract State Machines, Alloy, B, TLA, VDM, and Z. LNCS","author":"P.N. Devyanin","year":"2014","unstructured":"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\u2013313. https:\/\/doi.org\/10.1007\/978-3-662-43652-3_30"},{"key":"3538_CR11","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J.-R. Abrial","year":"2010","unstructured":"Abrial, J.-R., Modeling in Event-B: System and Software Engineering, Cambridge Univ. Press, 2010."},{"key":"3538_CR12","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"J.-R. Abrial","year":"2010","unstructured":"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\u2013466. https:\/\/doi.org\/10.1007\/s10009-010-0145-y","journal-title":"Int. J. Software Tools Tech. Transf."},{"key":"3538_CR13","unstructured":"ISO\/IEC 15408-1:2009: Information Technology \u2013 Security Techniques \u2013 Evaluation Criteria for IT Security \u2013 Part 1: Introduction and General Model, ISO, 2009."},{"key":"3538_CR14","unstructured":"ISO\/IEC 15408-2:2008: Information Technology \u2013 Security Techniques \u2013 Evaluation Criteria for IT Security \u2013 Part 2: Security Functional Components, ISO, 2008."},{"key":"3538_CR15","unstructured":"Astra Linux. https:\/\/en.wikipedia.org\/wiki\/Astra_Linux. Accessed Jan. 21, 2019."},{"key":"3538_CR16","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1145\/300830.300839","volume":"2","author":"R. Sandhu","year":"1999","unstructured":"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\u2013135. https:\/\/doi.org\/10.1145\/300830.300839","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"3538_CR17","unstructured":"American National Standard for Information Technology \u2013 Role Based Access Control. ANSI INCITS 359-2004, 2004."},{"key":"3538_CR18","doi-asserted-by":"crossref","unstructured":"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).","DOI":"10.21236\/ADA023588"},{"key":"3538_CR19","doi-asserted-by":"publisher","unstructured":"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\u201341. https:\/\/doi.org\/10.1109\/SFCS.1976.1","DOI":"10.1109\/SFCS.1976.1"},{"key":"3538_CR20","doi-asserted-by":"publisher","unstructured":"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\u201354. https:\/\/doi.org\/10.11145\/800215.806569.","DOI":"10.11145\/800215.806569"},{"key":"3538_CR21","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1145\/989.991","volume":"2","author":"C.E. Landwehr","year":"1984","unstructured":"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\u2013222. https:\/\/doi.org\/10.1145\/989.991","journal-title":"ACM Trans. Comput. Syst."},{"key":"3538_CR22","unstructured":"Security-Enhanced Linux. http:\/\/www.nsa.gov\/what-we-do\/research\/selinux\/. Accessed Jan. 21, 2019."},{"key":"3538_CR23","unstructured":"PostgreSQL. https:\/\/en.wikipedia.org\/wiki\/PostgreSQL. Accessed Jan. 21, 2019."},{"key":"3538_CR24","unstructured":"D-Bus. https:\/\/en.wikipedia.org\/wiki\/D-Bus. Accessed Jan. 21, 2019."},{"key":"3538_CR25","unstructured":"Window System. https:\/\/en.wikipedia.org\/wiki\/X_Window_System. Accessed Jan. 21, 2019."},{"key":"3538_CR26","series-title":"Review of existing analysis tools for SELinux security policies: challenges and a proposed solution","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-59041-7_7","volume-title":"MCETECH 2017: ETechnologies: Embracing the Internet of Things","author":"A. Eaman","year":"2017","unstructured":"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\u2013135. https:\/\/doi.org\/10.1007\/978-3-319-59041-7_7"},{"key":"3538_CR27","doi-asserted-by":"publisher","unstructured":"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\u2013145. https:\/\/doi.org\/10.1145\/990036.990059","DOI":"10.1145\/990036.990059"},{"key":"3538_CR28","doi-asserted-by":"publisher","unstructured":"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\u2013309. https:\/\/doi.org\/10.1007\/978-3-319-27998-5_19","DOI":"10.1007\/978-3-319-27998-5_19"},{"key":"3538_CR29","doi-asserted-by":"crossref","unstructured":"Amthor, P., Kuhnhauser, W.E., and P\u00f6lck, A., Model-based safety analysis of SELinux security policies, Proc. 5th Int. Conf. on Network and System Security (NSS), Milan, 2011, pp. 208\u2013215.","DOI":"10.1109\/ICNSS.2011.6060002"},{"key":"3538_CR30","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1145\/360303.360333","volume":"19","author":"M.A. Harrison","year":"1976","unstructured":"Harrison, M.A., Ruzzo, W.L., and Ullman, J.D., Protection in operating systems, Commun. ACM, 1976, vol. 19, no. 8, pp. 461\u2013471. https:\/\/doi.org\/10.1145\/360303.360333","journal-title":"Commun. ACM"},{"key":"3538_CR31","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1145\/1805874.1805982","volume":"13","author":"B. Hicks","year":"2010","unstructured":"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.1805982","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"3538_CR32","unstructured":"Tschantz, M.C., The clarity of languages for access-control policies, PhD Thesis, Providence, RI: Brown Univ., 2005."},{"key":"3538_CR33","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1134\/S0361768816040022","volume":"42","author":"P.N. Devyanin","year":"2016","unstructured":"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\u2013205. https:\/\/doi.org\/10.1134\/S0361768816040022","journal-title":"Prog. Comput. Software"},{"key":"3538_CR34","series-title":"Why3 \u2013 where programs meet provers","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J.-C. Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C. and Paskevich, A., Why3 \u2013 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_8"},{"key":"3538_CR35","series-title":"Deductive verification of unmodified Linux kernel library functions","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03421-4_15","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"D. Efremov","year":"2018","unstructured":"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_15"},{"key":"3538_CR36","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1109\/2.48795","volume":"23","author":"J. McLean","year":"1990","unstructured":"McLean, J., The specification and modeling of computer security, Computer, 1990, vol. 23, no. 1, pp. 9\u201316. https:\/\/doi.org\/10.1109\/2.48795","journal-title":"Computer"}],"container-title":["Programming and Computer Software"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768820070026.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1134\/S0361768820070026\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768820070026.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,11]],"date-time":"2020-12-11T12:09:56Z","timestamp":1607688596000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1134\/S0361768820070026"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,12]]},"references-count":36,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2020,12]]}},"alternative-id":["3538"],"URL":"https:\/\/doi.org\/10.1134\/s0361768820070026","relation":{},"ISSN":["0361-7688","1608-3261"],"issn-type":[{"value":"0361-7688","type":"print"},{"value":"1608-3261","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,12]]},"assertion":[{"value":"13 January 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 February 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 February 2020","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 December 2020","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}