• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • A
  • A
  • A
  • A
  • A
Обычная версия сайта
  • RU
  • EN
  • HSE University
  • Publications
  • Articles
  • Configurable toolset for static verification of operating systems kernel modules
  • 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 30, 2026
‘This Format Turned Each Presentation Into a Collaborative Effort to Assess the Robustness of the Study
On October 16, 2026, HSE ICEF hosted the Eighth International Conference on Applied Economics. Held fully on-site, the conference brought researchers from HSE University, the New Economic School, Wuhan University, and Shandong University together in Moscow. The programme was organised around three overarching themes— ‘Environment, Resources and Policy,’ ‘Migration, Labour, and Communication,’ and ‘Consumption, Behaviour, and Climate—offering an opportunity to see how similar economic mechanisms operate in China, Pakistan, the United States, and Russia.
October 23, 2026
‘I Always Conduct Research on Topics That Genuinely Matter to Me
Anastasiia Deeva studies the socio-economic consequences of excess weight in Russia. In an interview for the Young Scientists of HSE University project, she spoke about why beauty cannot be measured, her desire to write a novel, ‘Dostoevskian’ burnout, and working at the hotel where The Shining was filmed.
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.

 

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

?

Configurable toolset for static verification of operating systems kernel modules

Programming and Computer Software. 2015. Vol. 41. No. 1. P. 49–64.
Khoroshilov A. V., Мандрыкин М. У., Мутилин В. С., Новиков Е. М., Petrenko A. K., Захаров И. С.

An operating system (OS) kernel is a critical software regarding to reliability and efficiency. Quality of modern OS kernels is already high enough. However, this is not the case for kernel modules, like, for example, device drivers that, due to various reasons, have a significantly lower level of quality. One of the most critical and widespread bugs in kernel modules are violations of rules for correct usage of a kernel API. One can find all such violations in modules or can prove their correctness using static verification tools that need contract specifications describing obligations of a kernel and modules relative to each other. This paper considers present methods and toolsets for static verification of kernel modules for different OSs. A new method for static verification of Linux kernel modules is proposed. This method allows one to configure the verification process at all its stages. It is shown how it can be adapted for checking kernel components of other OSs. An architecture of a configurable toolset for static verification of Linux kernel modules that implements the proposed method is described, and results of its practical application are presented. Directions for further development of the proposed method are discussed in conclusion.

Research target: Computer Science
Priority areas: IT and mathematics
Language: English
DOI
Text on another site
Keywords: Static Verificationoperating system kernel
Similar publications
Кластеризация услуг распределенной системы, в которой хосты могут выполнять функцию коммутации сообщений
Бурдонов И. Б., Evtushenko N. V., Косачев А. С. et al., Труды Института системного программирования РАН 2025 Т. 37 № 5 С. 7–32
Статья является продолжением предыдущей статьи авторов, в которой строится абстрактная модель распределенной сети, содержащей только хосты и коммутаторы. Хосты предлагают пользователям пакеты определенных услуг (сервисов), сообщения (запросы) между хостами пересылаются через промежуточные узлы по правилам коммутации, и настройка узлов определяет множество путей от хоста к хосту, по которым будут пересылаться пакеты. Ситуация моделируется с использованием ...
Added: October 30, 2026
Модель распределенной системы, в которой хосты могут выполнять функцию коммутации сообщений.
Бурдонов И. Б., Evtushenko N. V., Косачев А. С. et al., Труды Института системного программирования РАН 2025 Т. 37 № 4-1 С. 7–30
В работе строится абстрактная модель распределенной сети, содержащей только хосты и коммутаторы, которая позволяет оценить классы задач, которые необходимо решать в такой сети, принимая во внимание, в том числе, нефункциональные параметры. Предполагается, что хосты предлагают пакеты определенных услуг (сервисов) и сообщения (запросы) между хостами пересылаются через промежуточные узлы по правилам коммутации. Правило определяет, каким соседним ...
Added: October 30, 2026
Improving system survivability by path duplication
Бурдонов И. Б., Evtushenko N. V., Косачев А. С., PROGRAMMING AND COMPUTER SOFTWARE 2025 Vol. 51 No. 4 P. 224–241
In this paper, the problem of distributed network survivability is investigated. A distributed system is modeled by a finite connected undirected graph the nodes of which are divided into two types: hosts and switches. Hosts perform computational functions, while switches are used for message passing between hosts. The survivability of the system is understood as ...
Added: October 30, 2026
Улучшение живучести системы с помощью дублирования путей
Бурдонов И. Б., Evtushenko N. V., Косачев А. С., Программирование 2025 № 4 С. 11–32
Исследуется проблема живучести распределенных сетей. Распределенная система моделируется конечным связным неориентированным графом, вершины которого делятся на два типа: хосты и коммутаторы. Хосты выполняют вычислительные функции, а коммутаторы обеспечивают доставку сообщений между хостами. Под живучестью системы понимается ее способность выполнять свои основные функции по передаче сообщений после выхода из строя некоторых ребер графа. Решение проблемы живучести ...
Added: October 30, 2026
Programming and Computer Software
M.: Pleiades Publishing, Ltd. (Плеадес Паблишинг, Лтд), 2025.
Programming and Computer Software is a peer-reviewed journal devoted to various problems in all areas of computer science: operating systems, compiler technology, software engineering, artificial intelligence, etc. The journal publishes original manuscripts submitted in English, as well as works translated from several other journals. The sources of content are indicated at the article level. The ...
Added: October 30, 2026
Методология создания информационных систем
Karminsky A. M., Chernikov B. V., М.: НИЦ Инфра-М, 2026.
Рассмотрены методологические вопросы создания финансово-экономических информационных систем, проблемы информатизации производственной и дистрибьютерской деятельности, темы адаптации типовых систем в бизнес-структурах, в том числе систем поддержки офисной деятельности. Для студентов учреждений среднего профессионального образования, обучающихся по укрупненным группам специальностей 09.02.00 «Информатика и вычислительная техника», 38.02.00 «Экономика и управление», экономистов, юристов, предпринимателей и финансистов, а также специалистов и ...
Added: October 30, 2026
Mean-field reduction of networks of bursting neurons
Guerreiro I., Sergey Skorokhod, di Volo M. et al., Communications in Nonlinear Science and Numerical Simulation 2027 Vol. 164 Article 110954
The collective dynamics of spiking networks of neurons has been of central interest to both computational neuroscience and network science. Over the past years, a new generation of neural population models based on exact reductions (ER) of spiking networks have been developed. However, most of these efforts have been limited to networks of neurons with simple dynamics (e.g. the ...
Added: October 29, 2026
Proceedings of the 11th Workshop on Automated Knowledge Base Construction (AKBC 2026)
Association for Computational Linguistics, 2026.
While Large Language Models (LLMs) have revolutionized NLP, they remain prone to hallucinations, reasoning “mode-collapse” in open-ended generation, and a lack of factual provenance. The Automated Knowledge Base Construction (AKBC) workshop addresses a key missing piece of the generative era: structured knowledge. Knowledge Bases (KBs) serve as ground truth for fact verification, the semantic backbone ...
Added: October 28, 2026
Molecular dynamics and machine learning insights into oil-brine interfacial tension: Uncovering roles of dissolved gases and salinity
Nikitiuk B., Lenev D., Pisarev V. et al., Journal of Colloid and Interface Science 2026 Vol. 718 Article 140444
Hypothesis:Accurate determination of interfacial tension values is crucial for many modeling applications in the oil and gas industry. However, many of the presently used empirical and theoretical models show poor prediction accuracy and do not allow for direct consideration of the concentrations of gases and salts dissolved in the system as well as the specific ...
Added: October 28, 2026
Predicting multi-component oil viscosity using machine learning methods
Deshchenya V., Nikolay D. Kondratyuk, Sivakova A. et al., Chemical Engineering Sciences 2027 Vol. 337 Article 124616
Accurate prediction of complex formulation viscosity is crucial for the lubricant industry and engineering processes. However, developing generalizable models remains challenging due to the complexity of industrial mixtures and the scarcity of public experimental data, often resulting from corporate proprietary restrictions. This study presents a machine-learning workflow for viscosity estimation from a proprietary pseudonymized dataset, ...
Added: October 28, 2026
PARSE: Physical attribute representativity and stationarity evaluator open-source library for 3D images using scalar and vector metrics
Zubov A., Zubov A., Малявко, Я. et al., Computer Physics Communications 2025 Vol. 317 Article 109860
The concept of representative volume (REV, or RVE in material sciences) is the cornerstone of continuum scale models – one needs to get the volume big enough so that it could be represented with an averaged value (scalar, vector or tensorial, etc.). While REV should be established in all larger scale simulations, this is rarely ...
Added: October 28, 2026
Amplifying Latent Safety in Large Language Models via Gated Activation Steering
Roman Prosvirnin, Suslov A., Aleksei Soldatov et al., Computation 2026 Vol. 14 No. 10 Article 261
Abstract Safety-aligned language models often encode that a request is harmful yet still comply with it. We turn this gap between internal recognition and observable behavior into an inference-time defense. The proposed activation-steering method uses a multiplicative operator that amplifies the residual-stream component along a harm-recognition direction. Intervention strength scales with the model’s own assessment of ...
Added: October 27, 2026
PACTraD: Multi-Task Benchmark and Domain-Specific Attention Mechanism for Wildlife Classification, Detection, and Segmentation in Protected Area Camera Trap Data
Aleksei Samarin, Nazarenko A., Nazarenko D. et al., Big Data and Cognitive Computing 2026 Vol. 10 No. 11 P. 1–52
Camera traps are a key tool for non-invasive wildlife monitoring, yet models trained on existing benchmarks often generalize poorly to new regions due to domain shift, class imbalance, and natural variability in illumination, season, and background. We introduce PACTraD, a benchmark of 116,973 annotated camera trap images collected in a protected area of the Baikal ...
Added: October 27, 2026
2026 10th Scientific School Dynamics of Complex Networks and their Applications
IEEE, 2026.
Proceedings of the X Scientific School "Dynamics of Complex Networks and their Applications" (DCNA'2026) contain papers of reports of scientists and specialists in the field of intelligent technologies, engineering education, research and design of complex networks. DCNA'2026 was held from 10 to 12 September 2026 in Moscow, Russia, as a part of the International Forum on Artificial Intelligence and ...
Added: October 26, 2026
A Curated Dataset for Chemical Characterization of Heated Tobacco Product Aerosol
Maddalena L., Yildiz B., Del Vecchio Blanco F. et al., Scientific data 2026 P. 1–20
We addressed the task of chemical characterization of the aerosol emitted by heated tobacco products (HTPs) and of the smoke emitted by conventional/commercial cigarettes, usually adopted as a reference. Emphasis was placed on quantifying constituents for enabling the identification of novel compounds through targeted and untargeted analyses, and the evaluation of reductions in toxicant exposure under ...
Added: October 26, 2026
A Multi-Feature Fusion Deep Neural Network with Attention for Multi-Task Crop Monitoring
Obsie E. Y., Zhan Y., Liu Y., Engineering Research Express 2026 Article 7
Maintaining plant health is crucial for crop quality, food security, and agricultural productivity. Although deep learning methods have shown strong potential for species, disease, and severity classification, most existing approaches tackle these tasks separately, failing to exploit shared representations and interdependencies among them. Furthermore, the variability of disease symptoms, such as subtle differences in size, ...
Added: October 22, 2026
A Neural Network Approach for Generating Libration Point Orbits
Lev Pyatko, Sergey Aksenov, Regular and Chaotic Dynamics 2026 Vol. 31 No. 5 P. 794–813
In the circular restricted three-body problem, families of periodic and quasi-periodic orbits exist in the vicinity of the libration points and are of significant interest for practical applications. This work presents a neural network-based algorithm for orbit construction and station-keeping, applicable to both periodic and quasi-periodic orbits near collinear libration points. The method employs a ...
Added: October 19, 2026
Основы теории информации
Vorontsova T., М.: Академия, 2025.
The textbook has been prepared in accordance with the requirements of the federal state educational standards for secondary vocational education and is intended for studying the professional modules “Information Security in Information and Telecommunication Systems and Networks Using Software and Hardware‑Software Tools, Including Cryptographic Protection Tools” and “Information Security in Automated Systems Using Software and ...
Added: October 19, 2026
A Reproducible Microscopy Acquisition Pipeline and Microscopy-Aware Attention for Classification, Detection, and Segmentation of Microorganisms
Aleksei Samarin, Nazarenko A., Nazarenko D. et al., Machine Learning and Knowledge Extraction 2026 Vol. 8 No. 10 Article 330
Automated microscopic image analysis is essential for quantitative microbiology, yet manual acquisition and generic recognition models struggle with morphological variability and scene artifacts. We address both ends of this pipeline. First, we present a low-cost, open-source acquisition system, based on an Arduino UNO R3 microcontroller and NEMA 17 stepper motors, that automates focusing, magnification, and ...
Added: October 14, 2026
Studies in Computational Intelligence
Springer, 2026.
This book highlights cutting-edge research in the field of network science, offering scientists, researchers, students and practitioners a unique update on the latest advances in theory and a multitude of applications. It presents the peer-reviewed proceedings of the XIV International Conference on Complex Networks and their Applications (COMPLEX NETWORKS 2025). The carefully selected papers cover ...
Added: October 13, 2026
Proceedings of the 3rd International Conference on Sustainability: Developments and Innovations. Proceedings of ICSDI 2026, Volume 4. Lecture Notes in Civil Engineering (LNCE, volume 886)
Springer, 2026.
This book offers a comprehensive overview of the latest research, innovations, and practical applications in the field of sustainability, with a focus on construction materials and their use in building and civil engineering structures. As an outcome of the 3rd International Conference on Sustainability: Developments and Innovations (ICSDI 2026), this book presents a selection of ...
Added: October 13, 2026
A Three-Party W-State Quantum Secret Sharing Protocol with X-Gate Encoding and Forbidden-Outcome Detection
Timur Teregulov, Elena R. Loubenets, / Series Quantum Physics "arXiv". 2026. No. 2609.31472.
We develop a new three-party quantum secret-sharing (QSS) protocol based on a three-qubit W state. This protocol encodes the secret-sequence bits using X gates and employs randomly selected Hadamard operations and measurement bases to generate information and security-test rounds. We evaluate the efficiency of the proposed protocol and analyze its security against an internal adversary ...
Added: September 28, 2026
On calibration of remote sensing retrievals of ecosystem respiration (Reco) with tower measurements over,Russian forests and wetlands
Shabanov N., Kuricheva O., Kurbatova J. et al., / Series Working Papers SSRN "Department of Economics Ca’ Foscari University of Venice". 2026.
The carbon balance of an ecosystem is the difference between Gross Primary Productivity (GPP) and Ecosystem Respiration (Reco) as expressed by Net Ecosystem Exchange (NEE). While remote sensing retrievals of GPP have reached maturity, Reco estimation remains underexplored and ultimately cast bias on NEE. Here we present an end-to-end multi-scale analysis of the mechanism of ...
Added: August 21, 2026
Three Algorithms for Merging Hierarchical Navigable Small World Graphs
Ponomarenko A., / Series Computer Science "arxiv.org". 2025.
This paper addresses the challenge of merging hierarchical navigable small world (HNSW) graphs, a critical operation for distributed systems, incremental indexing, and database compaction. We propose three algorithms for this task: Naive Graph Merge (NGM), Intra Graph Traversal Merge (IGTM), and Cross Graph Traversal Merge (CGTM). These algorithms differ in their approach to vertex selection ...
Added: July 30, 2026
  • 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