Vol 26, No 3 (2014)
View or download the full issue
PDF (Russian)
5-50
Abstract
The paper is addressed the important problem of systematization and conceptualization of scheduling theory. Scheduling is widely applied in such subject areas as production management, traffic flow organization, planning of projects and resource management into computing systems. However, a diversity of mathematical models and methods of scheduling poses usually the problem of design of fast algorithm as well as the problem of efficient software implementation taking into account specificity of subject area. A usage of typical solvers from shared mathematical libraries is exceedingly limited. A usage of object-oriented frameworks for software implementations is more perspective. In the paper we make an attempt to systematize and to generalize models and methods of scheduling theory with the aim of construction of such a framework. The main attention is paid to resource-constrained project scheduling problems. These problems are widely used in practice on the one hand and bring together different mathematical statements arising in related subject areas and disciplines on the other hand.
51-68
Abstract
The software platform for mathematical modeling support Temetos is decribed. The Temetos platform is the integrated graphical tool environment for the study of mathematical models of physical processes and technical systems. Temetos platform provides opportunities for preparation of geometric and physical models of the object; external or built-in problem-oriented modules configuration, including numerical method parameters configuration; computational module launch and executing control; calculations results visualization and analysis. The platform consists of three subsystems: the mathematical subsystem, including command-line utilities for the computational domain discretization and triangulation and software modules for the numerical solution of the mathematical model differntial equation systems; instrumental graphics subsystem, including tools for the 3D geometric design of the investigated object model; subject libraries subsystem containing structured knowledgebase for the simulated structures, constructions and physical processes (elements of the libraries are: 3D object models, meshes, material physical models and others.). The subject libraries subsystem is the base of platform information structure. It contains of free format XML files decribing knowledgebase elements. Hierarchical library architecture and universal data interfaces leads the platform to grow and to implement the new subject areas and mathematical models in easy way. As examples of platform implementation the simulation of plasma flow instability in astrophysical conditions and model of brittle material failure under heat load are considered.
69-90
Abstract
Most applications consist of separated modules. Optimization of such applications during building in the traditional way “compiling-linking” is reduced to a single module optimization. However, in spite of support of cross-module optimizations by many compilers full optimizations are often unacceptable for large applications because of significant time and memory consumption. Compiler frameworks that could solve these problems with regard to hardware capabilities and user demands are called scalable cross-module optimization frameworks. In this article, we aim to consider all the different approaches to the problem of scalability of with respect to resources consumed rather than inter-procedural or cross-module optimizations or their effectivenesses because of their independence of used framework. The possibility of parallelization of various stages of whole program compilation as well as ways to save memory consumed by cross-module analysis are of interest. This overview observes several compiler frameworks for general-purpose programming languages like C, C++ and Fortran. Although, quite often these frameworks are able to optimize other languages in case of existence of corresponding front-ends.
91-102
Abstract
We describe an implementation of conjugate gradient method on heterogeneous platforms (multiple nodes with GPU accelerators) to be used in OpenFOAM. Several optimizations are described. For conjugate gradient itself, we suggest using device memory for scalars used only on the GPU and pinned memory for scalars used in MPI reductions. For preconditioning, we choose AINV as a suitable preconditioner for GPUs and describe ways to make it more efficient, such as storing in it single precision, laying out factors in upper-left triangular form and computing it on the CPU asynchronously. We describe how multi-GPU computing can be supported together with arbitrary boundary conditions by copying only boundary coefficients from the accelerator to host memory and then using existing OpenFOAM methods on the CPU. To improve overlap of computations and communications, we suggest using a pipelined variant of the conjugate gradient method and describe GPU-specific adjustments. In experimental evaluation, we obtain a 1.75x speedup in the linear solver by using a Tesla K20X accelerator in addition to a 10-core Xeon CPU, but only for sufficiently large problem sizes: below 1 million cells per accelerator the efficiency of GPU computations dimishes.
103-112
Abstract
This paper describes algorithm for static search for error of double locking of mutex. The algorithm allows emitting warnings with low level of false positives. We considered finding errors for abstract library containing functions of mutex lock, unlock and conditional locking. We defined a set of regular languages, which models locks and unlocks during concrete execution of a program. We have defined a domain approximated set of regular languages. The algorithm is implemented in terms of data flow analysis. In the analysis elements of the domain are used as the data flow properties. The algorithm is described for a program that has only one mutex and does not contain any aliases. In that case every emitted warning will correspond to a real error which may occur during program execution. The algorithm is implemented in system of static analysis Svace developed in Institute for System Programming of the Russian Academy of Sciences. Svace performs alias analysis and matching of formal and actual function parameters. This makes it possible to apply the algorithm to search for double locking of a program containing only one mutex, and the rest of the work will be executed by Svace. The search algorithm of the double lock implemented in Svace can emit some number of false positives because Svace performs nonconservative analysis.
113-126
Abstract
Software vulnerabilities are critical for security. All C/C++ programs contain significant amount of vulnerabilities. Some of them can be successfully exploitable by attacker to gain control of the execution flow. In this article we propose several compiler protection techniques against vulnerability exploitation: function reordering, insertion of additional dummy variables into stack, local variables permutation on the stack. These transformations were implemented in GCC. It successfully diversifies whole operational system including Linux kernel. We suggest to generate diversified population of binary application files with these transformations. Diversified applications can be easily distributed via the application stores. Every client downloads the unique copy of application. The proposed method complicates and increases the cost of ROP-attacks. After downloading of the binary copy attacker can create ROP-exploit for this copy but it would not be exploitable for another application copy. The diversified transformations decrease application performance about 15% and increase code size about 5%.
127-144
Abstract
In this paper automated method for exploit generation is presented. This method allows to construct exploits for stack buffer overflow vulnerabilities and also to prioritize software bugs. It is applied to program binaries, without requiring debug information. The method is based on dynamic analysis and symbolic execution. We present a tool implementing the method. We used this tool to generate exploits for 8 vulnerabilities in both Linux and Windows programs, 3 of which were undocumented at the time this paper was written.
145-166
Abstract
In this paper we study the equivalence problem in the model of sequential programs which assumes that some instructions are commutative and absorbing. Two instructions are commutative if the result of their executions does not depend on an order of their execution. An instruction b absorbs an instruction a if the sequential composition a;b yields the same result as the single instruction b. A.A. Letichevskij in 1971 proved the decidability of equivalence checking problem in this model of programs. Nevertheless a possibility of building polynomial time equivalence checking procedures remains an open problem till nowadays. The main result of this paper is the description of a polynomial time algorithm for checking the equivalence of sequential programs with commutative and absorbing instructions. The paper includes 9 sections. In Section 1 we introduce informally the model of programs under consideration, the equivalence checking problem, and give a brief overview of the preceding results in the study of equivalence checking problem for this model. In Sections 2 and 3 the syntax and a semigroup-based semantics of propositional model of sequential programs are formally defined. The algebraic properties of semigroups of commutative and absorbing program instructions are studied in Section 4. In Section 5 we introduce a graph of joined computations which is the key structure in designing our equivalence checking techniques. In Section 6 and 7 we show that the cumulative absorbing effect of finite sequences of commutative instructions can be specified by means of finite automata; this is another key step in building the decision procedure. In Section 8 we show that equivalence checking of two programs is reducible to a traversal of a bounded fragment of the graph of joint computations of these programs; the latter can be performed in time polynomial of the size of programs to be checked.
167-198
Abstract
Program obfuscation is a semantic-preserving transformation aimed at bringing a program into such a form, which impedes the understanding of its algorithm and data structures or prevents extracting of some valuable information from the text of a program. Since obfuscation could find wide use in computer security, information hiding and cryptography, security requirements to program obfuscators became a major focus of interests for pioneers of theory of software obfuscation. In this paper we give a survey of various definitions of obfuscation security and main results that establish possibility or impossibility of secure program obfuscation under certain cryptographic assumptions. We begin with a short retrospective survey on the origin and development of program obfuscation concept in software engineering and mathematical cryptography. In the introduction we also point out on the main difficulties in the development of practical and secure obfuscation techniques. In the next section we discuss the main line of research in the application of program obfuscation to the solution of various problems in system programming and software security. Finally, in section 3 we present and discuss a compendium of formal definitions of the program obfuscation concept developed so far in mathematical cryptography - black-box obfuscation, gray-box obfuscation, the best possible obfuscation, obfuscation with auxiliary inputs, etc.. We also make a comparative analysis of these definitions and present the main results on the (im)possibility of secure program obfuscation w.r.t. every such definition.
ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)
ISSN 2220-6426 (Online)