• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • A
  • A
  • A
  • A
  • A
Обычная версия сайта
  • RU
  • EN
  • HSE University
  • Publications
  • Book chapter
  • Formal Verification of OS Security Model with Alloy and Event-B
  • 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
July 24, 2026
'Physics Is What the World Is Literally Built On'
Physicist Nina Dzhanayeva, recipient of a Vladimir Potanin Foundation scholarship, focuses her research on nanophotonics. In this interview for the HSE Young Scientists project, she discusses nanowells, scientific intuition, and how physics can help in making frangipane cream puffs.
July 20, 2026
Scientists Create Open Dataset for Studying Concentration
A team of Russian researchers, including scientists from HSE University–St Petersburg, has developed the first open multimodal dataset containing recordings of brain activity, heart function, and video observations to help researchers understand what happens in the human brain during deep concentration. In the future, the dataset could accelerate the development of neural interfaces, rehabilitation technologies, and AI systems. The article has been published in Scientific Data.
July 20, 2026
‘Science Is Universal-It Knows No Borders
Fuad Aleskerov, Tenured Professor and Director of the International Centre of Decision Choice and Analysis at HSE University, together with his colleagues, has developed methods of network analysis in bibliometrics that have made it possible to identify patterns in the appearance and citation of publications in academic journals, as well as their influence on each other. When one or a number of studies are frequently cited by a wide range of journals, this is an indicator that the research is of high quality. By contrast, extensive cross-citation within a limited group of journals increases the likelihood of identifying a network of predatory publications.

 

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 Verification of OS Security Model with Alloy and Event-B

P. 309–313.
Khoroshilov A. V., Petrenko A. K., Девянин П. Н., Kuliamin V., Щепетков И. В.

The paper presents a work-in-progress on formal verification
of operating system security model, which integrates control of confi-
dentiality and integrity levels with role-based access control. The main
goal is to formalize completely the security model and to prove its con-
sistency and conformance to basic correctness requirements concerning
keeping levels of integrity and confidentiality. Additional goal is to per-
form data flow analysis of the model to check whether it can preserve
security in the face of certain attacks. Alloy and Event-B were used for
formalization and verification of the model. Alloy was applied to provide
quick constraint-based checking and uncover various issues concerning
inconsistency or incompleteness of the model. Event-B was applied for
full-scale deductive verification. Both tools worked well on first steps of
model development, while after certain complexity was reached Alloy
began to demonstrate some scalability issues.

Language: English
DOI
Text on another site
Keywords: formal modelsecurity model of informational telecommunication systemsdeductive verification

In book

Abstract State Machines, Alloy, B, TLA, VDM, and Z
Heidelberg: Springer, 2014.
Similar publications
Friend or Foe: A Computational Model of Identity Construction During Political Mobilization
Andrei Akhremenko, Koncha V., Journal of Social Policy Studies 2025 Vol. 23 No. 4 P. 781–794
Due to the heterogeneous composition of modern opposition movements, protesters may have two different types of identity: a narrow one associated with their political group or organization or a widespread identity related to the opposition as a whole. Accordingly, the authorities can use two types of repression: broad, directed against the entire opposition, or targeted, ...
Added: May 13, 2024
Отключение интернета как теоретическая проблема политической науки, или что мы (не) понимаем в сетевой протестной мобилизации
Akhremenko A. S., Полис. Политические исследования 2024 № 2 С. 118–134
The influence of Internet communication on “street” protest activity is the focus of this paper. In recent years, there has been some stagnation in this area of research: a shortage of breakthrough works that indicate new research directions or at least significantly strengthen the empirical foundation of already established hypotheses. The paradox is that when ...
Added: March 31, 2024
Modeling the Protest-Repression Nexus
Akhremenko A. S., Petrov A., , in: Proceedings of the Conference on Modeling and Analysis of Complex Systems and Processes 2020 (MACSPro 2020)Vol. 2795.: CEUR Workshop Proceedings, 2020. Ch. 1 P. 1–11.
Over the last 30 years, numerous studies have shown that repression can de-crease, increase, or have some kind of a nonlinear or mixed impact on the intensity of protest. This problem is usually referred to as the “protest-repression nexus” or the “punishment puzzle”, and it is still not resolved. The mathematical and computational model that we present in ...
Added: March 3, 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
A Memory Model for Deductively Verifying Linux Kernel Module
Khoroshilov A. V., Мандрыкин М. У., , in: Perspectives of System Informatics - 11th International Andrei P. Ershov Informatics Conference, PSI 2017, Moscow, Russia, June 27-29, 2017, Revised Selected Papers, Lecture Notes in Computer ScienceVol. 10742.: Springer, 2018. P. 256–275.
Several previous evaluations of memory models for SMT-based deductive verification tools have shown that the choice of memory model may significantly affect both the number of automatically discharged verification conditions and the capabilities of the verification tool. One of the most efficient memory models for deductive verification of low-level C code is based on region ...
Added: February 12, 2018
Verification, Model Checking, and Abstract Interpretation. 18th International Conference, VMCAI 2017, Paris, France, January 15–17, 2017, Proceedings
Bouajjani A., Monniaux D., Cham: Springer, 2016.
This book constitutes the refereed proceedings of the 18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017, held in Paris, France, in January 2017. The 27 full papers together with 3 invited keynotes presented were carefully reviewed and selected from 60 submissions. VMCAI provides topics including: program verification, model checking, abstract interpretation ...
Added: March 29, 2017
High-Level Memory Model with Low-Level Pointer Cast Support for Jessie Intermediate Language
Khoroshilov A. V., Мандрыкин М. У., Programming and Computer Software 2015 Vol. 41 No. 4 P. 197–207
The paper presents a target analyzable language used for verification of real world production GNU C programs (Linux kernel modules). The language represents an extension of the existing intermediate language used by the Jessie plugin for the Frama C static analysis framework. Compared to the original Jessie, the extension is fully compatible with the C semantics of arrays, ...
Added: October 30, 2015
A formal model and verification problems for Software Defined Networks
Smeliansky R. L., Chemeritsky E. V., Zakharov V., Automatic Control and Computer Sciences 2014 Vol. 48 No. 7 P. 398–406
Software-dened networking (SDN) is an approach to building computer net- works that separate and abstract data planes and control planes of these systems. In a SDN a centralized controller manages a distributed set of switches. A set of open commands for packet forwarding and ow-table updating was dened in the form of a protocol known ...
Added: September 30, 2015
Формализованная модель безопасности рабочих процессов информационно-телекоммуникационных систем, функционирующих на основе технологии облачных вычислений
Tsaregorodtsev A. V., Нелинейный мир 2013 Т. 11 № 9 С. 610–621
Use of cloud computing applications and services requires review and adaptation of existing formal models for informational telecommunication systems security. It is necessary to consider the benefits of cloud deployment models and provide the procedure for allocating process among components of cloud computing environment for achieving confidentiality and data protection. ...
Added: March 26, 2015
Efficiency, Policy Selection and Growth in Democracy and Autocracy: A Formal Dynamical Model
Andrei Akhremenko, Petrov A., / NRU Higher School of Economics. Series PS "Political Science". 2014. No. WP BRP 16/PS/2014.
The main focus of this paper is the impact of efficiency losses, related to public capital stock, on the prospects of economic growth in democratic and autocratic political environments. We introduce a distinction between two types of efficiency loss: along with the loss of public capital during its accumulation, we take into account the process ...
Added: October 24, 2014
МОДЕЛИРОВАНИЕ ВЛИЯНИЯ ПРАВИЛА РАСПРЕДЕЛЕНИЯ ОБЩЕСТВЕННОГО РЕСУРСА НА ЭФФЕКТИВНОСТЬ
Akhremenko A. S., Petrov A., В кн.: Математическое моделирование и информатика социальных процессов. Сборник трудовВып. 16.: М.: Экон-Информ, 2014. С. 15–20.
В настоящей работе рассматривается динамическая модель, в центре внимания которой находится влияние на эффективность социально-политической системы со стороны уровня налоговой нагрузки и правила распределения бюджетных средств на инвестиции в инфраструктуру и производственный ресурс ...
Added: October 24, 2014
Математическое моделирование и информатика социальных процессов. Сборник трудов
М.: Экон-Информ, 2014.
The articles in this collection are written on the basis of reports made in 2013 at the sociological faculty of Moscow State University M.V. Lomonosova at the annual meeting of the XVI Interdisciplinary Scientific Seminar "Mathematical modeling of social processes" named Hero of Socialist Labor Academician A.A. Samarskogo. The publication is intended for researchers, teachers, students, ...
Added: October 24, 2014
Формальная модель лучших практик построения дорожных карт
Efimenko I., Khoroshevsky V. F., В кн.: XIV Национальная конференция по искусственному интеллекту с международным участием КИИ-2014.: Каз.: Российская ассоциация искусственного интеллекта, 2014. С. 118–127.
В работе обсуждаются вопросы создания формальной модели предметной области дорожного картирования на основе анализа лучших практик в данной области. Создание такой модели позволит обобщить опыт построения технологических дорожных карт и обеспечит основу для разработки средств автоматизации формирования и использования дорожных карт. Разработана система онтологий, специфицирующих ключевые информационные объекты сферы дорожного картирования, а также процессные модели лучших ...
Added: October 23, 2014
Институциональное инвестирование и эффективность общественной системы: опыт математического моделирования
Akhremenko A. S., Petrov A., В кн.: Метод: московский ежегодник трудов из обществоведческих дисциплинВып. 4.: М.: ИНИОН РАН, 2014. С. 62–82.
The article provides an overview of formal model that demonstrates the connections between institutional investment and social efficiency. The results of a set of computational experiments are described and analyzed. Some problems of mathematical modeling methodology are also discussed in the paper. ...
Added: October 15, 2014
DPMine/P: язык построения моделей извлечения и анализа процессов и плагины для ProM
Shershakov S., В кн.: Proceedings of the 9th Central & Eastern European Software Engineering Conference in Russia.: NY: ACM, 2013.
Process-aware information systems (PAIS) enable developing models for interaction of processes, monitoring accuracy of their execution and checking if they interact with each other properly. PAIS can generate large data logs that contain the information about the interaction of processes in time. Studying PAIS logs with the purpose of data mining and modeling lies within ...
Added: December 21, 2013
  • 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