• 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
October 19, 2026
'Cultural Studies Seeks to Understand What Lies Beneath the Surface of Everyday Things'
Maxim Zhiganov has been exploring different aspects of sound for many years—first in relation to his native Perm and then on a broader, global scale. In this interview for the HSE Young Scientists project, he talks about sound maps, the special issue of the journal Logos, and why it is important to make the familiar less clear and obvious.
October 14, 2026
At HSE University–St Petersburg, Experts Discuss How AI Changes Tourist Routes and Cultural Heritage
Neural networks are no longer simple travel assistants; now they decide what to include on the route and what to skip. Artificial intelligence changes how people perceive a place and shapes the image of tourist centres. At the II International Scientific and Practical Conference ’Information Technologies in the Preservation and Promotion of Cultural Heritage,’ researchers discussed who controls algorithmic solutions and in what ways, and whether authentic traditions get lost in them.
October 12, 2026
Road Injuries Leading Cause of Death Among Men Aged 10 to 39
Worldwide, road injuries are the leading cause of death among males aged 10–39. An international team of researchers reached this conclusion as part of the Global Burden of Disease Study 2023, analysing data from 204 countries between 1990 and 2023. Their findings have been published in The Lancet Public Health, with HSE University Professor Vasily Vlassov listed among the collaborators.

 

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