The article represented the technical implementation of the system of verified program code execution. The functional purpose of this system is to investigate arbitrary executable files of the operating system in the absence of source codes in order to provide the ability to control the execution of the program code within the specified functional requirements. The prerequisites for the creation of such a system are described, the user's operating procedure is given according to two typical usage scenarios. A general description of the architecture of the system and the software used for its implementation, the mechanism of interaction of the elements of the system are presented. The model example of implementation this system is presented. Demonstrating the flexible set of functional constraints, based on temporal attribute process action. At the end of the article given a brief comparison with the closest analogues.

Methods and tools for automated static verification aim at detecting all violations of checked requirements in target programs under certain assumptions even without complete models and formal specifications. The given feature form a basis of the suggested method for incremental development of environment model and requirement specifications for subsystems of operating system monolithic kernels. This method was implemented on top of static verification framework Klever. It was evaluated by checking the Linux kernel TTY subsystem. During this study some Klever components were improved. Besides, we fixed some existing and developed new environment model and requirement specifications. Almost all made changes also helps at static verification of loadable modules of the Linux kernel. Developers of automated static verification tool CPAchecker fixed several issues that we revealed and reported during the research. Overall developed specifications allowed to increase function coverage of the TTY subsystem from 5% to 83%. Moreover, we revealed 7 bugs in loadable modules verified together with the TTY subsystem.

The paper presents result of a study on deductive verification of 26 Linux kernel library functions with AstraVer toolset. The code includes primarily string-manipulating functions and is verified against contract specifications formalizing its functional correctness properties. The paper presents a brief review of the related earlier studies, discusses their results and indicates both the previous issues that were successfully solved in this study and the ones that remain and still prevent successful verification. The paper also presents several specification practices that were applied in the study, including some common specification patterns. The authors have successfully and fully proved functional correctness of 25 functions. The paper includes results of benchmarking 5 state-of-the-art SMT solvers on the resulting verification conditions.

Null pointer dereferencing remains one of the major issues in modern object-oriented languages. An obvious addition of keywords to distinguish between never null and possibly null references appears to be insufficient during object initialization when some fields declared as never null may be temporary null before the initialization completes. There are several proposals to solve the object initialization problem. How can they be compared in practice? Are the implementations sound? This work presents a set of examples distilling out the use cases from publications on the subject and open source libraries and explains the criteria behind. Then it discusses expected results for a selected set of tools performing null safety checks for Eiffel, Java, and Kotlin, and concludes with the actual outcomes demonstrating immaturity of the solutions.

Approaches for code execution using program vulnerabilities are considered in this paper. Particularly, ways of code execution using buffer overflow on stack and on heap, using use-after-free vulnerabilities and format string vulnerabilities are examined in section 2. Methods for automatic generation input data, leading to code execution are described in section 3. This methods are based on dynamic symbolic execution. Dynamic symbolic execution allows to gain input data, which leads program along the path of triggering vulnerability. The security predicate is an extra set of symbolic formulas, describing program's state in which code execution is possible. To get input data, leading to code execution, path and security predicates need to be united, and then the whole system should be solved. Security predicates for pointer overwrite, function pointer overwrite and format string vulnerability, that leads to stack buffer overflow are presented in the paper. Represented security predicates were used in method for software defect severity estimation. The method was applied to several binaries from Darpa Cyber Grand Challenge. Testing security predicate for format string vulnerability, that leads to buffer overflow was conducted on vulnerable version of Ollydbg. As a result of testing it was possible to obtain input data that leads to code execution.

Program vulnerabilities are a serious security threat. It is important to develop defenses preventing their exploitation, especially with a rapid increase of ROP attacks. State of the art defenses have some drawbacks that can be used by attackers. In this paper we propose fine-grained address space layout randomization on program load that is able to protect from such kind of attacks. During the static linking stage executable and library files are supplemented with information about function boundaries and relocations. A system dynamic linker/loader uses this information to perform functions permutation. The proposed method was implemented for 64-bit programs on CentOS 7 operating system. The implemented method has shown good resistance to ROP attacks based on two metrics: the number of survived gadgets and the exploitability estimation of ROP chain examples. The implementation presented in this article is applicable across the entire operating system and has shown 1.5 % time overhead. The working capacity of proposed approach was demonstrated on real programs. The further research can cover forking randomization and finer granularity than on the function level. It also makes sense to implement the randomization of short functions placement, taking into account the relationships between them. The close arrangement of functions that often call each other can improve the performance of individual programs.

The paper is dedicated to architecture and scalability principles for developed service intended to be a drop-in replace for Openstack Keystone. Openstack Keystone is the central identification and service catalogue service for clouds based on Openstack. Previous papers indicated problems of this service: it uses RDBMS (MariaDB/MySQL/PostgreSQL) as a data storage. Since each service and each user gets a token to have access to Openstack cloud and tokens are periodically revoked by the system, token generation is a critical function for the whole cloud. As soon as Keystone queries DBMS for getting user or service identification hashes and recomputes this hash upon the user-provided data, there is a bottleneck based on Keystone architecture. Each Keystone process has separate session with DBMS and since the recommended way is to use Galera cluster thus the DBMS part is limited to the slowest DBMS node since Galera provides High-Availability not the performance scale. Our approach is based on API Gateway Kong and its scalability through Apache Cassandra usage as a data store. Drop-in replacement is implemented as Lua plugin inside Kong API Gateway and implements Keystone V3 API.

Random networks are often described using Erdos-Renyi model of random graph . The concept of graph density is often used in random network analysis. In this article, the maximal size of c-dense subgraph almost surely included in random graph was evaluated. It was shown, that if , then is almost surely c-dense; the upper and lower bounds for the size of maximal -dense subgraph almost surely included in were determined; in case when , the upper bound for the maximal size of c-dense subgraph almost surely included in was attained.

In 2012 M.A. Trushnikov in [2] suggested a new online method for 2DSP Problem. The average case evaluation for a 2DSP algorithm equals the expected value of space of strip not filled with rectangles. In 2013 in [3] the average case evaluation for this method was attained and it equaled . The best known before evaluation was improved. In present article this evaluation was improved to . Also a new method was constructed for MSP Problem, where rectangles are packed in strips, , with average case evaluation equaling

MPI is a well-proven technology that is widely used in a high-performance computing environment. However, configuring an MPI cluster can be a difficult task. Containers are a new approach to virtualization and simple application packaging, which is becoming a popular tool for high-performance tasks (HPC). This approach is considered in this article. Packaging an MPI application as a container solves the problem of conflicting dependencies, simplifies the configuration and management of running applications. A typical queue system (for example, SLURM) or a container management system (Docker Swarm, Kubernetes, Mesos, etc.) can be used to manage cluster resources. Containers also provide more options for flexible management of running applications (stop, restart, pause, in some cases, migration between nodes), which allows you to gain an advantage optimizing the allocation of tasks to cluster nodes in comparison with the classic scheduler. The article discusses various ways to optimize the placement of containers when working with HPC-applications. A variant of launching MPI applications in Fanlight system is proposed, which simplifies the work of users. The optimization problem associated with this method is considered also.

Mixed convection over horizontal heated plate was simulated with four numerical models based on Reynolds stress, large eddy simulation (LES) and eddy viscosity approximations. Temperature distributions over plate and in adjacent volume of fluid were the main criteria of results assessment. Three-dimensional computational domain was considered with symmetry boundary conditions. Simulation was performed with Code_Saturne software package in unsteady formulation. Three orthogonal meshes were evaluated to validate initial guess about optimal cell size. u2-f and Smagorinsky LES models appeared to yield the most adequate results. However, temperature distribution in high-buoyancy region, located in the middle of heated plate, was reproduced much more accurate with classical LES and elliptic blending Reynolds stress models. Obtained results are suitable for industrial applications (e.g. cooling jackets) and might be a base ground for further research.

Due to the development of Wind Energy and construction of new wind farms in Russian Federation there is a need for the solution of application-oriented problems and development of effective methods for calculation of wind turbine’s elements. One of the directions for computational continuous mechanics is connected with problems in aeroelasticity (fluid-structure interaction). The possibility of solving one of the problem in aeroelasticity using a complex program approach on the basis of open source software OpenFOAM and Code_Aster is shown in this article. On the example of the blade for wind turbine, 61.5 meters long, the techniques of solving problem for a static and dynamic aeroelasticity in which calculation of flow of the blade with a subsonic air flow is done in OpenFOAM library (solvers simpleFOAM and pimpleFOAM) are considered. The calculation of the intense deformed status of the blade is done in Code_Aster code. The flowcharts for three different approaches for solving problems of aeroelasticity, examples of scripts and command files for data transfer between two codes in the course of calculation are provided in article. The control-volume mesh consisting their hexahedral elements, the total number is about 400000 elements, for calculation of flow around the blade is constructed in OpenFOAM library, the finite-element mesh consisting of triangular shell elements of first order, the total number is 7714, for calculation of the intense deformed status is constructed in Salome-Meca code. The results of calculation are provided in the form of fields for pressure and velocities; graphics for residuals of pressure, velocity, turbulent viscosity; projections of aerodynamic force from time; diagrams of displacement and stress; the values of pressure for two points for the surfaces and displacement of the tip of the blade from time. The calculations are run using resources of UniHUB web-laboratory ISPRAS.

The software package to calculate parameters of three-dimensional steady and unsteady gas flows in complex devices is presented. The mathematical flow model used in package is based on the Reynolds-averaged Navier Stokes equations for a two-component equilibrium turbulent medium and a two-parameter semiempirical turbulence model. A numerical implementation of the software package to modelling three complex flows in modern devices is described.

In this paper, we present techniques Surface Flow Image Velocimetry (SFIV) that is a practical extension of Particle Image Velocimetry method (PIV). In particular, this technique is to evaluate the behavior on the surface flow for complex flow. SFIV allows to measure complex surface velocity fields for engineering applications. The objective of this work was the application of the SFIV technique to determine the velocity fields and their hydraulic efficiency of grated inlet, making a comparison between the programs able to correlate images like Digiflow or PIVlab program.

The paper describes the development and testing processes of a modification of an existing solver for hypersonic reacting flow within the OpenFOAM numerical simulation framework. The modification is suited to simulate the interaction between the flow and the constant applied magnetic field. The purpose of the development is to create a simulation tool for the study of the concept of magnetohydrodynamical flow control and its possible technological applications. Resulting application utilizes Navier-Stokes-Fourier system of equations supplemented with appropriate auxiliary models for the accurate assessment of process-specific additional terms. Solver testing has been carried out using the cases that highlight solvers capabilities to model MHD high-speed flow in different regimes.

This paper presents a 3D numerical analysis of flow field patterns in a dam break laboratory scale by applying the numerical code based on Finite Volume Method (FVM), OpenFOAM. In the numerical model the turbulence is treated with RANS methodology and the VOF (Volume of Fluid) method is used to capture the free surface of the water. The numerical results of the code are assessed against experimental data. Water depth and pressure measures are used to validate the numerical model. The results demonstrate that the 3D numerical code satisfactorily reproduce the temporal variation of these variables.

In this paper, we describe the method, which is the composition of finite volume method (FVM) and adaptive mesh refinement (AMR). We use it to solve car final drive inner volume oil lubrication problem. The computational algorithm is implemented using OpenFOAM parallel library that provides data structures and routines to work with the finite volume method and adaptive mesh. This library supports parallelism through OpenMPI. The paper presents the results of numerical simulation.