{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:42:19Z","timestamp":1775054539807,"version":"3.50.1"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030549961","type":"print"},{"value":"9783030549978","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"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":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-54997-8_12","type":"book-chapter","created":{"date-parts":[[2020,8,10]],"date-time":"2020-08-10T20:11:50Z","timestamp":1597090310000},"page":"185-199","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Runtime Verification of Linux Kernel Security Module"],"prefix":"10.1007","author":[{"given":"Denis","family":"Efremov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ilya","family":"Shchepetkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,8,11]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010)","edition":"1"},{"issue":"6","key":"12_CR2","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R., et al.: Rodin: an open toolset for modelling and reasoning in event-B. Int. J. Softw. Tools Technol. Transf. 12(6), 447\u2013466 (2010). \nhttps:\/\/doi.org\/10.1007\/s10009-010-0145-y","journal-title":"Int. J.. Softw. Tools Technol. Transf."},{"key":"12_CR3","first-page":"1","volume":"77","author":"JR Abrial","year":"2007","unstructured":"Abrial, J.R., Hallerstede, S.: Refinement, decomposition, and instantiation of discrete models: application to event-B. Fundamenta Informaticae 77, 1\u201328 (2007)","journal-title":"Fundamenta Informaticae"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Bell, D.E., La Padula, L.J.: Secure Computer System: Unified Exposition and MULTICS Interpretation. ESD-TR-75-306, Electronic Systems DivisiDon, AFSC, Hanscom AFB, 1976 (1976)","DOI":"10.21236\/ADA023588"},{"key":"12_CR5","unstructured":"Bell, D.E., LaPadula, L.J.: Secure Computer Systems: Mathematical Foundations. ESD-TR-73-278 v. 1, Electronic Systems Division, AFSC, Hanscom AFB (1973)"},{"key":"12_CR6","unstructured":"Belousov, K., Viro, A.: Linux kernel LSM file permission hook restriction bypass (2006). \nhttps:\/\/vulners.com\/osvdb\/OSVDB:25747"},{"key":"12_CR7","unstructured":"Biba, K.: Integrity considerations for secure computer systems. Technical report MTR-3153, The MITRE Corporation (1977)"},{"key":"12_CR8","unstructured":"Devyanin, P.N.: The models of security of computer systems: access control and information flows. Goryachaya Liniya-Telecom, Moscow, Russia (2013). (in Russian)"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-662-43652-3_30","volume-title":"International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"P Devyanin","year":"2014","unstructured":"Devyanin, P., Khoroshilov, A., Kuliamin, V., Petrenko, A., Shchepetkov, I.: Formal verification of OS security model with alloy and event-B. In: Ait Ameur, Y., Schewe, K.D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 309\u2013313. Springer, Heidelberg (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-662-43652-3_30"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-319-41579-6_9","volume-title":"Perspectives of System Informatics","author":"PN Devyanin","year":"2016","unstructured":"Devyanin, P.N., Khoroshilov, A.V., Kuliamin, V.V., Petrenko, A.K., Shchepetkov, I.V.: Using refinement in formal development of OS security model. In: Mazzara, M., Voronkov, A. (eds.) PSI 2015. LNCS, vol. 9609, pp. 107\u2013115. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-41579-6_9"},{"key":"12_CR11","doi-asserted-by":"publisher","unstructured":"Edwards, A., Jaeger, T., Zhang, X.: Runtime verification of authorization hook placement for the Linux security modules framework. In: Proceedings of the 9th ACM Conference on Computer and Communications Security, pp. 225\u2013234. CCS 2002. ACM, New York (2002). \nhttps:\/\/doi.org\/10.1145\/586110.586141\n\n, \nhttp:\/\/doi.acm.org\/10.1145\/586110.586141","DOI":"10.1145\/586110.586141"},{"key":"12_CR12","unstructured":"Georget, L.: Add missing LSM hooks in MQ timed send, receive and splice (2016). \nhttp:\/\/thread.gmane.org\/gmane.linux.kernel.lsm\/28737"},{"key":"12_CR13","doi-asserted-by":"publisher","unstructured":"Georget, L., Jaume, M., Tronel, F., Piolle, G., Tong, V.V.T.: Verifying the reliability of operating system-level information flow control systems in Linux. In: 2017 IEEE\/ACM 5th International FME Workshop on Formal Methods in Software Engineering (FormaliSE), pp. 10\u201316, May 2017. \nhttps:\/\/doi.org\/10.1109\/FormaliSE.2017.1","DOI":"10.1109\/FormaliSE.2017.1"},{"key":"12_CR14","unstructured":"Goyal, V.: Overlayfs SELinux support (2016). \nhttps:\/\/lwn.net\/Articles\/693663\/"},{"issue":"1","key":"12_CR15","doi-asserted-by":"publisher","first-page":"115","DOI":"10.3233\/JCS-2005-13105","volume":"13","author":"JD Guttman","year":"2005","unstructured":"Guttman, J.D., Herzog, A.L., Ramsdell, J.D., Skorupka, C.W.: Verifying information flow goals in security-enhanced linux. J. Comput. Secur. 13(1), 115\u2013134 (2005)","journal-title":"J. Comput. Secur."},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-662-43652-3_22","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"N Huynh","year":"2014","unstructured":"Huynh, N., Frappier, M., Mammar, A., Laleau, R., Desharnais, J.: Validating the RBAC ANSI 2012 standard using B. In: Ait Ameur, Y., Schewe, K.D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 255\u2013270. Springer, Heidelberg (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-662-43652-3_22"},{"key":"12_CR17","unstructured":"ISO\/IEC 15408\u20131:2009. Information technology - Security techniques - Evaluation criteria for IT security - Part 1: Introduction and general model. ISO (2009)"},{"key":"12_CR18","unstructured":"ISO\/IEC 15408\u20132:2008. Information technology - Security techniques - Evaluation criteria for IT security - Part 2: Security functional components. ISO (2008)"},{"key":"12_CR19","unstructured":"Jacob, B., Larson, P., Leitao, B., Da Silva, S.: SystemTap: instrumenting the Linux kernel for analyzing performance and functional problems. In: IBM Redbook, vol. 116 (2008)"},{"key":"12_CR20","unstructured":"Jurgens, D.: SELinux support for Infiniband RDMA (2016). \nhttps:\/\/lwn.net\/Articles\/684431\/"},{"key":"12_CR21","doi-asserted-by":"publisher","unstructured":"Kozachok, A.: TLA+ based access control model specification. In: Proceedings of the Institute for System Programming of the RAS, vol. 30, pp. 147\u2013162, January 2018. \nhttps:\/\/doi.org\/10.15514\/ISPRAS-2018-30(5)-9","DOI":"10.15514\/ISPRAS-2018-30(5)-9"},{"key":"12_CR22","unstructured":"Larson, P.: Testing Linux with the Linux test project. In: Ottawa Linux Symposium, p. 265 (2002)"},{"key":"12_CR23","unstructured":"Morris, J., Smalley, S., Kroah-Hartman, G.: Linux security modules: general security support for the Linux kernel. In: USENIX Security Symposium, pp. 17\u201331. ACM Berkeley, CA (2002)"},{"key":"12_CR24","unstructured":"RusBITech: Astra Linux\u00ae Special Edition. \nhttps:\/\/astralinux.ru\/products\/astra-linux-special-edition\/"},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"Tsirunyan, K., Martirosyan, V., Tsyvarev, A.: The Spruce System: quality verification of Linux file systems drivers. In: Proceedings of the Spring\/Summer Young Researchers Colloquium on Software Engineering. ISP RAS (2012)","DOI":"10.15514\/SYRCOSE-2012-6-25"},{"key":"12_CR26","unstructured":"Vykov, D.: Syzkaller (2015). \nhttps:\/\/github.com\/google\/syzkaller"},{"key":"12_CR27","unstructured":"Write, C.: LSM update, another missing hook (2005). \nhttps:\/\/lwn.net\/Articles\/155496\/"},{"key":"12_CR28","doi-asserted-by":"crossref","unstructured":"Zanin, G., Mancini, L.V.: Towards a formal model for security policies specification and validation in the SELinux system. In: Proceedings of the Ninth ACM Symposium on Access Control Models and Technologies, pp. 136\u2013145. ACM (2004)","DOI":"10.1145\/990036.990059"}],"container-title":["Lecture Notes in Computer Science","Formal Methods. FM 2019 International Workshops"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-54997-8_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,10]],"date-time":"2020-08-10T20:15:18Z","timestamp":1597090518000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-54997-8_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030549961","9783030549978"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-54997-8_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"11 August 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/formalmethods2019.inesctec.pt\/?page_id=84","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"129","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"44","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"34% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5,5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}