Home page

It has been a proven fact that the inclusion of more than one modality makes biometric recognition systems more robust and elevates its recognition accuracy. This paper aims to develop a strategic platform for the upcoming researchers in order to develop multimodal biometric recognition systems. The researchers in this fraternity would be able to design their own procedural strategy using the generalized workflow template depicted in this review. The selection of proper visually interpreted biometric identifiers and modalities, various fusion strategies, choice of performance metrics, formation of training and test sets from databases and the possible challenges in developing the workflow are purposefully portrayed in this article.

Ensuring trust in cryptographically secure algorithm implementations is a relevant task in modern programming. Because increased correctness requirements are imposed on such software systems, the proof of their correctness with respect to a certain formal specification is constructed via deductive verification. This article outlines the progress made towards the proof of correctness of the Streebog hash function implementation located in the Linux kernel with respect to the GOST R 34.11-2012 standard. The work began as part of the "Formal verification of a Streebog hash function implementation with the Astra Group" project during the 2025 Great Mathematical Workshop. As the result of our work we present a formalization of the GOST R 34.11-2012 algorithm in the Rocq proof assistant's Gallina language. This formalization can serve as a functional specification for any implementation of the Streebog hash function. We also present specifications for some of the basic functions present in the Streebog hash function implementation located in the Linux kernel and also methods of simplifying proofs of correctness of such functions by formulating lemmata that establish a correspondence between the data structures present in the implementation and the data structures outlined in the functional specification.

The article presents a comprehensive overview of modern near-Earth space geospatial monitoring systems aimed at providing protection from space debris and asteroid hazards. The review examines existing and promising technologies, including methods of surveillance, active threat removal, and the use of information systems. Special attention is paid to the role of artificial intelligence and automation in improving monitoring efficiency.

The article presents a new mathematical model of cryptographic protocols and provides examples of using this model to solve problems of verification of cryptographic protocols. Cryptographic protocols are communication protocols implemented using cryptographic algorithms to solve information security problems, within which participants in information interaction consistently perform certain actions and exchange messages. They are used, for example, in electronic payments, electronic voting procedures, systems of access to confidential data, etc. Errors in cryptographic protocols can lead to significant damage, so it is necessary to use mathematical methods to justify various properties of correctness and security of cryptographic protocols. The article presents new methods of formal verification of cryptographic protocols. To model cryptographic protocols, the concepts of sequential and distributed processes are introduced. The proposed approach is intended only to prove the correctness of cryptographic protocols. A feature of the protocol model is its simplicity in comparison with other protocol models based on logical formulas or algebraic expressions of processes. Protocol participants are represented as graphs, which are transition systems. The actions performed by the participants are labels of these transitions. The methods of proving the correctness of protocols considered in the article are associated with reasoning on graphs, which are simpler and more visual compared to methods based on constructing logical inference in logical-algebraic models of protocols.

This paper describes the experience of using an automated testing system to support the learning process in computer science and ICT lessons. The system is used to accumulate materials on certain thematic sections and verify the correctness of the solution based on selected tests. The test system is created taking into account the tracking of the effectiveness of the algorithms selected during the implementation for the tasks selected by the topic. The use of this mechanism has shown good effectiveness and efficiency both in the process of preparing for Olympiad competitions and in regular classes. The analysis of the experience of using it is given and the prospects for implementing the capabilities of an automated system to support the educational process are outlined. Task verification technologies supported by technical means are a promising and effective direction. The material can be useful for both school and university teachers for use in the educational process, as well as for independent training of students.