• 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
  • 2028
  • 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
September 9, 2026
‘Balkan Hospitality Opens Doors: Studying Dialects on the Verge of Extinction
You cannot study spoken dialects from books. Instead, you need to go to a village, seek out its elders, and earn the trust of local residents before you can record hours of spontaneous stories. This is how Natalia Muravleva, Associate Professor at the Faculty of Humanities, conducts her research. Her internship in Serbia continued her long-standing study of dialects spoken by Macedonian settlers. In this interview, she discusses how diaspora cultural centres help researchers reach informants, why native speakers need to be interviewed only in their own language (otherwise, as she puts it, they may 'break'), and how a single field season helped her finalise her monograph. She also shares warm memories of autumn in Belgrade and of colleagues with whom grammar can be discussed in three languages at once.
September 9, 2026
Scientists Train Neural Network to Generate Process Plans from 3D Models
Researchers at the HSE FCS AI and Digital Science Institute have developed CAD2TechSpec, a framework that converts 3D models of mechanical parts into machining process plans—step-by-step instructions for machine tools. The solution aims to reduce the time required for the design and preparation of technical process documentation in mechanical engineering, aircraft manufacturing, and other high-tech industries. The study findings have been published in PeerJ Computer Science.
September 7, 2026
Biologists Discover 'Molecular Fingerprint' of Preeclampsia
Researchers at HSE University employed a new method to model hypoxia in placental cells during pregnancies complicated by preeclampsia and identified molecular markers of tissue hypoxia. Since hypoxia is one of the key mechanisms underlying preeclampsia, these findings are important for a more accurate and timely diagnosis of the disease and for the development of effective treatment methods. The paper has been published in Placenta.

 

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