• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • A
  • A
  • A
  • A
  • A
Обычная версия сайта
  • RU
  • EN
  • HSE University
  • Publications
  • Book chapter
  • Formal Modeling of Multi-Level Security and Integrity Control Implemented with SELinux
  • RU
  • EN
Расширенный поиск
Высшая школа экономики
Национальный исследовательский университет
Priority areas
  • business informatics
  • economics
  • engineering science
  • humanitarian
  • IT and mathematics
  • law
  • management
  • mathematics
  • sociology
  • state and public administration
by year
  • 2027
  • 2026
  • 2025
  • 2024
  • 2023
  • 2022
  • 2021
  • 2020
  • 2019
  • 2018
  • 2017
  • 2016
  • 2015
  • 2014
  • 2013
  • 2012
  • 2011
  • 2010
  • 2009
  • 2008
  • 2007
  • 2006
  • 2005
  • 2004
  • 2003
  • 2002
  • 2001
  • 2000
  • 1999
  • 1998
  • 1997
  • 1996
  • 1995
  • 1994
  • 1993
  • 1992
  • 1991
  • 1990
  • 1989
  • 1988
  • 1987
  • 1986
  • 1985
  • 1984
  • 1983
  • 1982
  • 1981
  • 1980
  • 1979
  • 1978
  • 1977
  • 1976
  • 1975
  • 1974
  • 1973
  • 1972
  • 1971
  • 1970
  • 1969
  • 1968
  • 1967
  • 1966
  • 1965
  • 1964
  • 1963
  • 1958
  • More
Subject
News
June 2, 2026
HSE Study Reveals Imbalance in the Generative AI Market
Researchers at HSE University analysed how effectively the global generative artificial intelligence market converts investment into real revenue, concluding that AI is currently developing faster than it is paying off. The results have been published in the journal Foresight and STI Governance.
June 2, 2026
Discovering Science through Russian Language: HSE Prep Year Students Present at International Conference in Kazan
On May 23, 2026, the V International Scientific and Practical Conference ‘Discovering the World of Science’ took place in Kazan at the Preparatory Faculty for International Students of Kazan Federal University. Four students of the HSE International Preparatory Year took part in the event: two delivered their presentations in person, while two participated online. Their work was supervised by Acting Director of the International Prep Year Irina Isaeva and lecturer Ekaterina Kozhemyakova.
May 25, 2026
HSE Scientists Train Neural Network to 'Hear' Faults in Electric Motors
Researchers at the AI and Digital Science Institute of the HSE Faculty of Computer Science have developed a new method—the Signature-Guided Data Augmentation (SGDA) framework—that achieves 99% accuracy in motor fault detection and 86% accuracy in fault classification. The application of this approach can reduce industrial equipment repair costs, minimise downtime, and improve production safety. The study results have been published in Engineering Applications of Artificial Intelligence.

 

Have you spotted a typo?
Highlight it, click Ctrl+Enter and send us a message. Thank you for your help!

Publications
  • Books
  • Articles
  • Chapters of books
  • Working papers
  • Report a publication
  • Research at HSE

?

Formal Modeling of Multi-Level Security and Integrity Control Implemented with SELinux

P. 131–136.
Kuliamin V., Khoroshilov A. V., Medvedev D.

The paper presents formal security model of Linux distributions provided by Bazealt SPO, which integrates multi-level security (MLS) and mandatory integrity control (MIC) implemented on the base of SELinux framework. The model also includes information flows analysis framework described as an extended Take-Grant model. The main novelty of the model is the integration of MLS and MIC that can be implemented in SELinux. The model is specified in a hierarchical manner on Event-B language, its security properties are represented as invariants and formally proved.

Language: English
DOI
Text on another site
Keywords: information flowsrefinementevent-bformal security modeSELinuxmandatory integrity controlmulti-level security deductive verification

In book

Actual Problems of Systems and Software Engineering APSSE 2019 (Invited Papers)
Los Alamitos, Washington, Tokyo: IEEE Computer Society, 2019.
Similar publications
Property-Preserving Transformations of Elementary Net Systems Based on Morphisms
Bernardinello L., Irina Lomazova, Nesterov R. et al., , in: Transactions on Petri Nets and Other Models of Concurrency XVIVol. 13220: Lecture Notes in Computer Science.: Springer, 2022. P. 1–23.
Structural transformations that preserve properties of formal models of concurrent systems make their verification easier. We define structural transformations that allow to abstract and refine elementary net systems. Relations between abstract models and their refinements are formalized using morphisms. Transformations proposed in this paper induce morphisms between elementary net systems as well as preserve their ...
Added: March 23, 2022
Deductive Binary Code Verification Against Source-Code-Level Specifications
Kamkin A., Khoroshilov A. V., Коцыняк А. М. et al., Lecture Notes in Computer Science 2020 Vol. 12165 P. 43–58
There is a high demand in practical methods and tools to ensure total correctness of critical software components. A usual assumption is that the machine code (or binary code) generated by a compiler follows the semantics of the programming language. Unfortunately, modern compilers such as GCC and LLVM are too complex to be thoroughly verified, ...
Added: June 22, 2021
A State-based Refinement Technique for Event-B
Khoroshilov A. V., Kuliamin V., Petrenko A. K. et al., , in: Proceedings of the 2020 Ivannikov Memorial Workshop.: Los Alamitos: IEEE Communications Society, 2020. P. 55–60.
Formal models can be used to describe and reason about the behavior and properties of a given system. In some cases, it is even possible to prove that the system satisfies the given properties. This allows detecting design errors and inconsistencies early and fixing them before starting development. Such models are usually created using stepwise ...
Added: October 29, 2020
Property-Preserving Transformations of Elementary Net Systems Based on Morphisms
Bernardinello L., Lomazova I. A., Nesterov R. et al., , in: Proceedings of the International Workshop on Petri Nets and Software Engineering co-located with 41st International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS 2020)Vol. 2651: CEUR Workshop Proceedings.: CEUR-WS.org, 2020. P. 49–67.
Structural transformations that preserve properties of formal models of concurrent systems make their verification easier. We define structural transformations that allow to abstract and refine elementary net systems. Relations between abstract models and their refinements are formalized using morphisms. Transformations proposed in this paper induce morphisms between elementary net systems as well as preserve their ...
Added: August 12, 2020
Structural Synthesis of the IoT System for the Fog Computing
Saksonov E., Leokhin Y., Panfilov, P., , in: 24th Conference of Open Innovations Association FRUCT, FRUCT 2019.: IEEE Computer Society, 2019. P. 381–387.
The paper presents the results of the structural design of the Internet of Things system, allowing to distinguish subsystems for cloud and fog computing to calculate parameters of information flows between them, and to support the structure optimization tasks. ...
Added: June 15, 2019
Kernels and Cokernels in the Category of Augmented Involutive Stereotype Algebras
S. S. Akbarov, Journal of Algebra and its Applications 2020 Vol. 19 No. 6 P. 1–28
We prove several properties of kernels and cokernels in the category of augmented involutive stereotype algebras: 1) this category has kernels and cokernels, 2) the cokernel is preserved under the passage to the group stereotype algebras, and 3) the notion of cokernel allows to prove that the continuous envelope Env C*(Z · K) of the group algebra of ...
Added: June 8, 2019
Трансформация социокультурной реальности и коммуникативное пространство университета
Shteynman M. A., В кн.: Философия коммуникации: университетское образования в социокультурной динамике информационного общества.: СПб.: Издательство Политехнического университета, 2015. С. 19–25.
Nowadays, our socio-cultural reality is being transformed rapidly and radically. These changes are mostly caused by a dominance of what A. Moles called "mosaic cutlure". Present-day university is no exeption, and its education model faces the same challenges, Hence one of the most effective ways for univrsity of surviving in modern society is to develop ...
Added: October 31, 2018
Философия коммуникации: университетское образования в социокультурной динамике информационного общества
СПб.: Издательство Политехнического университета, 2015.
Представлено разностороннее видение феномена коммуникации в контексте формирования стратегий современного образования. Авторы рассматривают феномен коммуникации в качестве конституирующего и регулирующего фактора социокультурной реальности, в существенной мере определяющего динамику ментальности современника. Акцентировано социальное значение новейших технологий информационного общества, порождающих новые дискурсы и познавательные установки в исследовании жизни социума и человека. ...
Added: October 31, 2018
Доверие как продукт вовлеченности в информационные потоки
Vólchenko O., Мониторинг общественного мнения: Экономические и социальные перемены 2014 № 4 С. 128–140
The purpose of the study is to examine how the involvement in information channels influences the trust. The author chooses the information approach towards the analysis of the phenomenon of trust as a means to overcome the lack of knowledge or uncertainty. The article highlights that trust is tightly connected to the assessment of the ...
Added: January 13, 2017
Envelopes and refinements in categories, with applications to functional analysis
Akbarov S. S., Dissertationes Mathematicae 2016 Vol. 513 P. 1–188
An envelope in a category is a construction that generalizes the operations of “exterior completion”, like completion of a locally convex space, or the Stone–Čech compactification of a topological space, or the universal enveloping algebra of a Lie algebra. Dually, a refinement generalizes the operations of “interior enrichment”, like bornologification (or saturation) of a locally ...
Added: September 23, 2016
When Not All Bits Are Equal: Worth-Based Information Flow
Scedrov A., Alvim M. S., Schneider F. B., , in: Principles of Security and Trust - Proceedings of the 3rd International Conference, POST 2014Vol. 8414.: Springer, 2014. P. 120–139.
Added: May 29, 2015
Checking Conformance of High-Level Business Process Models to Event Logs
Antonina K. Begicheva, Lomazova I. A., , in: Proceedings of the 8th Spring/Summer Young Researchers’ Colloquium on Software Engineering (SYRCoSE 2014).: M.: -, 2014. P. 77–82.
Process mining is a new technology, that provides us a variety of methods to discover, monitor and improve real processes by extracting knowledge from event logs. The two most prominent process mining tasks are process discovery and conformance checking. Conformance checking deals with diagnosing and quantifying discrepancies between observed behavior, represented in event logs, and ...
Added: June 2, 2014
Разработка автоматизированной системы управления потоками данных на предприятии (II часть)
Morozova T., Промышленные АСУ и контроллеры 2013 № 7 С. 3–12
The paper realized the most important purpose of the automated system of performance management (ASPM), which is to organize the relationships between all the departments, and the creation of a single data warehouse database that contains all the necessary business information about the company, about our services, all services of the company, etc. on At ...
Added: December 6, 2013
Оптимизация RAID массива для достижения максимальной производительности систем регистрации данных
Uvaysov S. U., Aminev D., Качество. Инновации. Образование 2012 № 12 С. 93–96
Исследована проблема регистрации информационных потоков в RAID массивы. Определен набор параметров, влияющих на их производительность. Представлены результаты тестирования RAID системы и определены значения параметров, обеспечивающие максимальную производительность. ...
Added: January 24, 2013
Dynamics of Information Systems: Mathematical Foundations
NY: Springer, 2012.
This proceedings publication is a compilation of selected contributions from the “Third International Conference on the Dynamics of Information Systems” which took place at the University of Florida, Gainesville, February 16–18, 2011. The purpose of this conference was to bring together scientists and engineers from industry, government, and academia in order to exchange new discoveries ...
Added: December 19, 2012
Performance Management Systems: Conceptual Modeling
Isaev D., , in: International Proceedings of Economics Development and Research. Economics and Business Information. Selected, peer reviewed papers from the 2011 International Conference on Economics and Business Information (ICEBI 2011), May 28-29, 2011, Bangkok, ThailandVol. 9.: Singapore: IACSIT Pre, 2011. P. 17–24.
The aim of the paper is to develop a methodological approach to conceptual modeling of performance management systems. For these purposes such systems are considered as means of information support of corporate governance and strategic management and include such components as analytical methods, management processes, information systems and personnel competences. As a result, a modeling ...
Added: July 19, 2012
  • About
  • About
  • Key Figures & Facts
  • Sustainability at HSE University
  • Faculties & Departments
  • International Partnerships
  • Faculty & Staff
  • HSE Buildings
  • HSE University for Persons with Disabilities
  • Public Enquiries
  • Studies
  • Admissions
  • Programme Catalogue
  • Undergraduate
  • Graduate
  • Exchange Programmes
  • Summer University
  • Summer Schools
  • Semester in Moscow
  • Business Internship
  • Research
  • International Laboratories
  • Research Centres
  • Research Projects
  • Monitoring Studies
  • Conferences & Seminars
  • Academic Jobs
  • Yasin (April) International Academic Conference on Economic and Social Development
  • Media & Resources
  • Publications by staff
  • HSE Journals
  • Publishing House
  • iq.hse.ru: commentary by HSE experts
  • Library
  • Economic & Social Data Archive
  • Video
  • HSE Repository of Socio-Economic Information
  • HSE1993–2026
  • Contacts
  • Copyright
  • Privacy Policy
  • Site Map
Edit