• 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 6, 2026
Ancient Craniiform Brachiopod: A Newly Discovered Species with a Unique Shell Shape and Lifestyle
Scientists from HSE University, MSU, and Tallinn University of Technology have studied a fossil species of ancient brachiopods that lived in a warm sea in what is now northern Estonia more than 445 million years ago. These ancient brachiopods developed a cup-shaped shell with a protective 'cap' that shielded them from overgrowth by other marine organisms. The study has been published in Palaeogeography, Palaeoclimatology, Palaeoecology.
July 2, 2026
Researchers Discover How Spelling Errors Slow Down Reading in Russian
Psycholinguists from the Centre for Language and Brain at HSE University–St Petersburg have shown that words that are frequently misspelled are processed more slowly by readers, even when presented with the correct spelling. The researchers confirmed this effect for the first time using Russian-language materials and found that response speed is most strongly linked to how confidently individuals can distinguish the correct spelling of a word from an incorrect one. The study has been published in The Mental Lexicon.
July 2, 2026
HSE Develops App for Assessing Phonological Processing in Children
Researchers at the HSE Centre for Language and Brain have developed a new digital tool for assessing children's phonological processing skills—the ZARYA (Sound Analysis of the Russian Language) test battery. It is the first standardised application in Russia designed to provide a fast and reliable assessment of children's ability to distinguish speech sounds, retain them in working memory, and perform phonemic analysis. The app runs on Android tablets and smartphones and is available for download from RuStore. Details of the test validation have been published in the Journal of Speech, Language, and Hearing Research.

 

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