Safety-critical systems require additional effort to comply with specifications. One of the required specification is correct memory usage. The article describes an efficient method for static verification against memory safety errors as a combination of Symbolic Memory Graphs and predicate abstraction on symbolic values used in graph. In this article, we introduce an extension of Symbolic Memory Graphs. In addition to symbolic values, the graph stores predicates over symbolic values, which allow to track the relationship between symbolic values in the graph. We also expand existing vertex types to support arbitrary abstract regions, which allow us to represent such dynamic data structures as lists and trees. One of the types of abstract regions is also the ODM region, which presents a special kind of on-demand memory that occurs when analyzing incomplete programs. For this memory, the size and structure of the contents are not known in advance, but it is believed that such memory can be operated safely. The method is implemented in CPAchecker tool. Practical usage is demonstrated on Linux kernel modules. The practical contribution of our work is to reduce false error messages by constructing more accurate abstractions using predicates over symbolic values.
An automatic program defect detection is extremely important direction of current research and development in the field of program reliability and security assurance. There were performed research of different ways of application for combined analysis methods which mix static source code analysis and dynamic symbolic execution, fuzz testing and dynamic symbolic execution as part of previous period of two years for project 17-07-00702 of the Russian Foundation for Basic Research. This paper presents elaboration of previously presented methods in form of formal model of program symbolic execution applied for program defect detection and implementation of analyzer of memory buffer bounds violation based on this model. The common theorem for program defect detection based on model of symbolic program execution and violation of definitional domain for computation system operation is formulated and proved. A special case theorem for buffer bounds violation detection is formulated and proved basing on common theorem and shadow memory model. As a practical application for theoretical basis an implementation of the analysis tool prototype description provided. Experimental results are received on the set of command line utilities of Debian Linux distribution, which shows applicability of proposed theoretical basis for solving practical tasks in the field of program reliability and security assurance.
One of the main problem of a binary code security analysis is a revealing of malicious behavior in an untrusted program. This task is hard to automate, and it requires a participation of a cybersecurity expert. Existing solutions are aimed on the analyst manual work; automation they provide does not demonstrate a system approach. In case where needed analysis tools are absent, the analyst loses the proper support and he is forced to develop tools on one's own. This greatly slows down him from obtaining the practical results. The paper presents a software complex to solve a revealing of malicious behavior problem as a whole: from creating a controlled execution environment to man guided preparing a high-level description of an analyzed algorithm. A QEMU Developer Toolkit (QDT) is introduced, offering support for the domain specific development life cycle. QDT is especially suited for QEMU virtual machine development, including specialized testing and debugging technologies and tools. A high-level hierarchical flowchart-based representation of a program algorithm is presented, as well as an algorithm for its construction. The proposed representation is based on a hypergraph and it allows both automatic and manual data flow analysis at various detail levels. The developed representation is suitable for automatic analysis algorithms implementation. An approach to improve the quality of the resulting representation of the algorithm is proposed. The approach combines individual data streams into the one that links separate logical modules of the algorithm. A test set based on real programs and model examples has been developed to evaluate the result of constructing the proposed high-level algorithm representation.
Not only developers require tools that work with binary code: it is impossible to achieve sufficient security in contemporary software without inspecting its properties at this level. A key component of binary code analysis toolset is the instruction decoder. Different instruction set architectures give rise to decoders that are differently structured, the decoding results are incompatible, and maintenance is hindered because of the ubiquitous practice of implementing decoders as cascades of conditional operators. Further binary code analysis (control and data flows, symbolic interpretation, etc.) cannot easily be ported from one target architecture to another because of limitations and peculiarities of decoder implementations. In this paper, we propose an approach to decoding machine instructions that is based on external specifications. The main distinction is an original way of representing the decoder instruction universally, i.e. in a way that does not differ from one architecture to another. The decoding process is handled by an abstract stack machine we have developed. Despite the inevitable overhead stemming from the approach’s universality, an implementation prototype displays only 1.5-2.5 times slowdown compared to traditional decoders; the measurements include time required to parse the specification and build the required data structures. The proposed approach to organizing decoding would allow, in the long run, to establish a unified stack of binary code analysis tools that would be applicable to different instruction set architectures. The paper further discusses questions of translating the decoded instructions into a machine-neutral internal representation for analyzing their operational semantics and carrying out abstract interpretation. We give examples of practically useful interpretations: the concrete interpretation and a “directing” interpretation that allows to tie the idea of abstract interpretation with the problem of deeper automatic analysis of individual paths in a program.
Recently, more and more software companies are interested in tools to improve the stability and security of their product. The closed libraries and third-party applications used by developers may contain defects, the use of which by an attacker or by a user may lead to a violation of the stability and security of the application. In some cases, the source code of the problem areas may be missing. At the moment, static methods for finding defects in code are gaining popularity, which allow finding defects that are unattainable for dynamic methods. Static methods are algorithms for studying a static model of a program, including a call graph, control flow, data flow. Studying binary code involves restoring a static model of a program from a binary file by disassembling, restoring function boundaries, translating it into an intermediate representation, and restoring a call graph. Defects in modern code bases, as a rule, appear only on a certain set of paths in the call graph, which requires interprocedural algorithms for finding defects. The aim of this work is to develop methods of interprocedural algorithms for finding defects in binary code that have good scalability, a set of supported architectures, and acceptable accuracy. Algorithms are developed based on ISP RAS Binside tool.
This paper provides a survey of methods and tools for automated code-reuse exploit generation. Such exploits use code that already contains in a vulnerable program. The code-reuse approach, e.g., return-oriented programming, allows one to exploit vulnerabilities in the presence of operating system protection that prohibits execution of code in memory pages marked as data. We define fundamental terms such as gadget, gadget frame, gadget catalog. Moreover, we show that a gadget is, in fact, an instruction, and a set of gadgets defines a virtual machine. We can reduce an exploit creation problem to code generation for this virtual machine. Each particular executable file defines a virtual machine instruction set. We provide a survey of methods for gadgets searching and determining their semantics (creating a gadget catalog). These methods allow one to get the virtual machine instruction set. If a set of gadgets is Turing-complete, then a compiler can use a gadget catalog as a target architecture. However, some instructions can be absent. Hence we discuss several approaches to replace missing instructions with multiple gadgets. An exploit generation tool can chain gadgets by pattern searching (regular expressions) or taking gadgets semantics into consideration. Furthermore, some chaining methods use genetic algorithms, while others use SMTsolvers. We compare existing open source tools and propose a testing system rop-benchmark that can be used to verify whether a generated chain successfully opens a shell.
Today, virtualization is a key technology for cloud computing and modern data centers, providing scalability and security, managing the global IT infrastructure and reducing costs. Among the methods of virtualization, the most popular was containerization, that is the isolation of related groups of linux processes that share a common Linux kernel. Containerization is more profitable that classical hardware virtualization because of compactness of containers and lower overhead costs of memory, disk, CPU. However, in comparison with classical architectures without process isolation containers can cost more, and in any case, the industry is waiting for additional optimization – the speed of launch, saving memory and disk space and other resources. Different caching techniques can help in this, because Caching is the oldest mechanism of increasing software productivity without radical modification of algorithms and hardware. However, there are a lot of architectural and engineering tradeoffs. Here we will consider modern scientific and technical approaches to their solution in different aspects – acceleration of launch, optimization of shared usage, acceleration of building container images, as well as some security problems caused by aggressive caching in modern processor architectures. And in some use cases for multi-container systems performance and latency are not important, but we have to ensure the maximum load of physical servers. In these cases, the algorithms of planning and placement of containers are relevant, and we give an overview of theoretical work on this topic.
In this paper we study the possibility of using a certain cloud computing model supplied with cryptoservers to obfuscate software programs. Earlier, we proposed this cloud computing model in our study of some information security problems for multi-client distributed computing over encrypted data. Based on this model, we proposed a new approach involving the use of threshold homomorphic cryptosystems for program obfuscation. The main result of this paper is a new definition of the resistance of obfuscation of programs in the cloud computing model and a theorem proving the cryptographic strength of the proposed algorithm of obfuscation of programs under the assumption of the existence of cryptographically strong threshold homomorphic encryption systems. The paper is organized as follows. In the introducing section we discuss the main aspects of the information security problems for cloud computing systems. Section 2 provides a description of the obfuscation program objectives, as well as a brief overview of the main achievements in its study. The next section provides general information about homomorphic cryptosystems. Section 4 describes a more special class of homomorphic cryptosystems - threshold homomorphic encryption systems. Section 5 introduces the cloud computing model, which is used as framework for our program obfuscation techniques. For this computing environment, in Section 6, the definition of the cryptographic strength of program obfuscation is formulated, a new method of program obfuscation using threshold homomorphic cryptosystems is described, and the cryptographic strength of the proposed obfuscation algorithm is proved.
Wind energy is one of the most important directions in the development of renewable energy sources in the Russian Federation. The most important trends in the wind industry are objectives for the design of new wind farms, the tasks of maintenance and monitoring of wind farm design challenges of wind turbines, the development of Russian software, etc. A number of topical basic and applied problems are appeared in connection with the construction of new wind farms on the territory of the Russian Federation. In this paper, one of these tasks is considered: the study of the wind situation in the area of Tiksi village, due to the installation of a new wind farm there. The wind forecast is based on the Advanced Research WRF (Weather Research and Forecasting) mesoscale model using the Global Forecast System data. The presented results are obtained on a series of nested grids with spatial resolution of 1, 3 and 9 km. A method for wind farm study and monitoring of a near the village of Tiksi is proposed, which is based on interpolation the results obtained from WRF-ARW to a smaller scale model within the future use of Simulator fOr Wind Farm Applications (SOWFA) library in OpenFOAM platform.
Currently, Russia is actively building new wind farms. The issues of studying physical processes are relevant, as the existing wind farms have an impact on the microclimate and ecology. In wind farms, the appearance and movement of liquid and solid particles is possible. In the study of two-phase flows containing a suspension of aerosol particles (dispersed phase) in the carrier medium (dispersion medium) in the atmosphere, it is important to choose the main parameters that determine the system correctly and adequately describe the real process using the formulated mathematical model. The work is devoted to the development of new solvers based on the SOWFA library as part of the open-source OpenFOAM 2.4.0 package for the study of particle dynamics modeling in the atmospheric boundary layer and in the model wind farm. The Euler-Lagrangian approach is used to describe particle dynamics. Two new solvers based on ABLSolver and pisoTurbineFoam.ALM have been developed to simulate particle dynamics. The calculation results for the case of a neutral boundary layer and a model wind farm with 14 model wind turbines are presented. Graphs for the distribution of particles with different diameters in height are given. Between 72 and 96 cores were used to calculate one example.
The effect of numerical dissipation on the predictive accuracy of wall-modelled large-eddy simulation is investigated via systematic simulations of fully-developed turbulent channel flow. A total of 16 simulations are conducted using the open-source computational fluid dynamics software OpenFOAM®. Four densities of the computational mesh are considered, with four simulations performed on each, in turn varying in the amount of numerical dissipation introduced by the numerical scheme used for interpolating the convective fluxes. The results are compared to publicly-available data from direct numerical simulation of the same flow. Computed error profiles of all the considered flow quantities are shown to vary monotonically with the amount of dissipation introduced by the numerical schemes. As expected, increased dissipation leads to damping of high-frequency motions, which is clearly observed in the computed energy spectra. But it also results in increased energy of the large-scale motions, and a significant over-prediction of the turbulent kinetic energy in the inner region of the boundary layer. On the other hand, dissipation benefits the accuracy of the mean velocity profile, which in turn improves the prediction of the wall shear stress given by the wall model. Thus, in the current framework, the optimal choice for the dissipation of the numerical schemes may depend on the primary quantity of interest for the conducted simulation. With respect to the resolution of the grid, the change in the accuracy is much less predictable, and the optimal resolution depends on the considered quantity and the amount of dissipation introduced by the numerical schemes.
The performance of the airfoil is strongly dependent on the development of the boundary layer on the surface and therefore an accurate prediction of the laminar to turbulent transition onset is essential. A grid independence study is performed, turbulence variables values have been changed frequently, regularly, and carefully so that they cover the entire range of acceptable values reported by previous researches. Effects of turbulent variating at far stream on turbulent boundary layer structure and on transition stage characteristics at moderate Reynolds number have been studied over a full range of angles of attack of NACA0012. numerical results have been post-processed, analyzed and found that far stream turbulence variables have a significant effect on transition characteristic, their effects on skin friction is limited to small extent along wing surface where transition take place, increasing turbulence intensity or eddy viscosity ratio at far boundary shifts transition onset towards leading edge and increase transition length.
Now it is no doubt that there are large-scale magnetic fields in the spiral galaxies. Their evolution is described by the dynamo mechanism which is based on joint action of differential rotation and alpha-effect. For galaxies usually the no-z approximation is used, which takes into account that the galaxy disk is quite thin. It is necessary to study so-called outer rings of galaxies. Studying the magnetic fields there is quite difficult. Firstly, we cannot say that the outer ring is thinner than the radial lengthscale. Secondly, it is necessary to take into account the influence of the magnetic field on the turbulent motions. In this work we present the results of the magnetic field modeling, and also demonstrate the influence of the magnetic field on the turbulent motions of the interstellar medium.
The possibilities of numerical modeling of the motion of hydrodynamic flows around objects of complex shape allow us to consider the results of calculations as one of the ways to understand the mechanisms of wind removal of sand particles. To study the conditions for the occurrence of microrelief, a number of numerical experiments are carried out using the open package OpenFOAM. Over inhomogeneities of the surface, determined by the features of the mutual arrangement of particles, there are areas of pressure reduction, near which the wind removal of particles is more likely. The reason for this decrease in pressure is a different kind of rarefaction of the spatial arrangement of surface elements: a change in distance, a change in the orientation of the structure in space, a change in the angle between planes containing particles. Due to the decrease in pressure, an increase in the air velocity at the surface and the occurrence of microvortices occur.
The paper considers the application of various modern technologies of high-performance computing to accelerate the numerical solution of the problems of propagation of dynamic wave disturbances using the grid-characteristic method. Technologies are considered both for central processing units (CPUs) and for graphic processors (GPUs). Comparative results of applying MPI, OpenMP, CUDA technologies are presented. As examples of the work of the developed software package, a number of examples of calculating the problems of seismic and geophysics are given. Separately, the issue of parallelizing problems with the presence of contacts of many grids and the topography of the day surface using curvilinear grids is considered.
ISSN 2220-6426 (Online)
