• 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 11, 2026
Doctoral Student at HSE University Reveals Hidden Layout of Ancient Parion
İdil Malgil, a researcher at HSE University, conducted a UAV-based LiDAR survey of the ancient Roman city of Parion in present-day Turkey. The high density of the scans allowed the team to detect subtle terrain features concealed beneath the ground and vegetation. The survey revealed traces of entire neighbourhoods, terraced structures, and walls that had remained invisible during routine excavations and could not be identified through aerial photography. The findings have been published in Ancient Civilizations from Scythia to Siberia.
June 11, 2026
Mathematicians from Nizhny Novgorod and Shanghai Study System Stability
Mathematicians at HSE University–Nizhny Novgorod, in collaboration with colleagues from Tongji University in Shanghai, are investigating the fundamental causes of structural stability in systems and the mechanisms underlying its disruption. In this interview with the HSE News Service, Prof. Olga Pochinka, Head of the International Laboratory of Dynamical Systems and Applications at HSE University–Nizhny Novgorod and leader of the project ‘Qualitative Theory of Systems of Ordinary and Partial Differential Equations,’ discusses the project, which is being implemented as part of HSE University's International Academic Cooperation programme.
June 11, 2026
Neurolinguists Assist in Awake Surgery on 11-Year-Old Patient with Epilepsy
Researchers at the HSE Centre for Language and Brain took part in a rare awake neurosurgical procedure performed on an 11-year-old patient with drug-resistant epilepsy. Working alongside surgeons at the Voyno-Yasenetsky Centre of Specialised Medical Care for Children in Solntsevo, they monitored the resection of a portion of the left temporal lobe, where the epileptic focus had been identified.

 

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