• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site
Of all publications in the section: 114
Sort:
by name
by year
Article
С.Д, Кузнецов, Мендкович Н. А. Труды Института системного программирования РАН. 2013. Т. 25. С. 113-130.

This paper describes enhanced algorisms of lexical optimization query. These algorisms detect and remove redundant conditions from query restriction to simplify it. The paper also presents results of implementation of these optimization techniques and those effects on query processing speed. The paper includes four sections. The first section (Introduction) provides general context of the paper. The second section describes three proposed algorithms of lexical query optimization. The first one is the algorithm of absorption. This algorithm allows to find and remove a wide set of conditions that are redundant but are not equal textually even after standardization of whole restriction expression. The second algorithm is an adaptation of well-known Quin-McCluskey algorithm initially designed for minimization of Boolean functions. The last algorithm of lexical query optimization is based on techniques for optimization of systems of linear inequalities. The third section of the paper discusses results of efficiency evaluation of the proposed algorithms. The forth section concludes the paper.

Added: Jan 30, 2018
Article
С.Д. Кузнецов, Мендкович Н. А. Труды Института системного программирования РАН. 2013. Т. 25. С. 113-130.

This paper describes enhanced algorisms of lexical optimization query. These algorisms detect and remove redundant conditions from query restriction to simplify it. The paper also presents results of implementation of these optimization techniques and those effects on query processing speed. The paper includes four sections. The first section (Introduction) provides general context of the paper. The second section describes three proposed algorithms of lexical query optimization. The first one is the algorithm of absorption. This algorithm allows to find and remove a wide set of conditions that are redundant but are not equal textually even after standardization of whole restriction expression. The second algorithm is an adaptation of well-known Quin-McCluskey algorithm initially designed for minimization of Boolean functions. The last algorithm of lexical query optimization is based on techniques for optimization of systems of linear inequalities. The third section of the paper discusses results of efficiency evaluation of the proposed algorithms. The forth section concludes the paper.

Added: Nov 6, 2017
Article
Дробышевский М., Коршунов А., Turdakov D. Y. Proceedings of the Institute for System Programming of the RAS. 2016. Vol. 28. No. 6. P. 153-170.
Added: Aug 28, 2017
Article
Трофимович Ю., Козлов И., Турдаков Д. Ю. Труды Института системного программирования РАН. 2016. Т. 28. № 6. С. 185-196.
Added: Aug 28, 2017
Article
Подымов В. В., Захаров В. А. Труды Института системного программирования РАН. 2014. Т. 26. № 3. С. 145-166.
Added: Sep 29, 2015
Article
Захаров В. А., Новикова Т. А. Труды Института системного программирования РАН. 2012. Т. 22. С. 435-455.
Strong (logic&term) equivalence of programs is the weakest decidable equivalence relation which approximates the functional equivalence of programs. In this paper we develop a new variant of the algorithm for checking strong equivalence of programs. A distinguished feature of our algorithm is that it relies completely on the algebra of finite substitutions which includes the operations of composition and antiunification. The paper begins with a short introduction to the theory of first-order substitutions. In the next section the formal first-order model of sequential programs and strong equivalence are defined. We also describe a preliminary variant of equivalence checking algorithm. This algorithm deals with composition and antiunification operations on finite substitutions. Since the complexity of these operations depends on data structures that represent substitutions, we consider in Section 4 graph-theoretic representations of substitutions as well as upper and lower bounds on the complexity of basic operations on substitutions. To reduce the complexity of equivalence checking algorithm for sequential programs we introduce in Section 5 a new class of truncated substitutions and study the basic algebraic properties of composition and antiunification operations on truncated substitutions. In Section 6 we showed that both operations on truncated substitutions can be performed in time O(n^2) . Finally, in Section 7 using the properties of truncated substitutions we introduced an improved version of the equivalence checking algorithm and proved that its time complexity is O(n^6 ) on the size of programs to be checked.
Added: Sep 30, 2015
Article
Федотов А., Каушан В., Гайсарян С. С. и др. Труды Института системного программирования РАН. 2017. Т. 29. № 6. С. 151-162.

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.

Added: Feb 12, 2018
Article
Гуськова М. С., Бараш Л. Ю., Щур Л. Н. Труды Института системного программирования РАН. 2018. Т. 30. № 1. С. 115-126.

The generation of uniformly distributed random numbers is necessary for computer simulation by Monte Carlo methods and molecular dynamics. Generators of pseudo-random numbers (GPRS) are used to generate random numbers. GPRS uses deterministic algorithms to calculate numbers, but the sequence obtained in this way has the properties of a random sequence. For a number of problems using Monte Carlo methods, random number generation takes up a significant amount of computational time, and increasing the generation capacity is an important task. This paper describes applying SIMD instructions (Single Instruction Multiple Data) to parallelize generation of pseudorandom numbers. We review SIMD instruction set extensions such as MMX, SSE, AVX2, AVX512. The example of AVX512 implementation is given for the LFSR113 pseudorandom number generator. Performance is compared for different algorithm implementations.

Added: Mar 26, 2018
Article
Захаров В. А., Новикова Т. А. Труды Института системного программирования РАН. 2011. Т. 21. С. 141-166.
Many problems in software engineering such as program refactoring, deobfuscation, vulnerability detection, require an efficient toolset for detecting pieces of code that have similar behavior. Current state of art in software clone detection makes it possible to find out only those pieces of code which have the same syntactic structure since. A more profound analysis of functional properties of programs encounters with undecidability of equivalence checking problem for Turing-complete models of computation. To overcome this principal deficiency of modern clone detection techniques we suggest to use equivalence relations on programs that are more strong than functional equivalence. One of such equivalences is a so called logic&term program equivalence introduced by V.E. Itkin in 1972 г. In this paper we build a new algorithm for checking logic&term equivalence of programs. This algorithm is based on the operations for computing the least upper bound and the greatest upper bound in the lattice of finite substitutions. Using this algorithm we also develop a procedure for solving the unification problem for sequential programs, i.e. the problem of computing the most general common instance (specialization) of a given pair of programs (pieces of code).
Added: Sep 30, 2015
Article
Захаров В. А., Подымов В. В. Труды Института системного программирования РАН. 2015. Т. 27. № 4.

Equivalence checking algorithms found vast applications in system programming; they are used in software refactoring, security checking, malware detection, program integration, regression verification, compiler verification and validation. In this paper we show that equivalence checking procedures can be utilized for the development of global optimization transformation of programs. We consider minimization problem for two formal models of programs: deterministic finite state transducers over finitely generated decidable groups that are used as a model of sequential reactive programs, and deterministic program schemata that are used as a model of sequential imperative programs. Minimization problem for both models of programs can be solved following the same approach that is used for minimization of finite state automata by means of two basic optimizing transformations, namely, removing of useless states and joining equivalent states. The main results of the paper are Theorems 1 and 2. Theorems 1. If G is a finitely generated group and the word problem in G is decidable in polynomial time then minimization problem for finite state deterministic transducers over G is decidable in polynomial time as well. Theorem 2. If S is a decidable left-contracted ordered semigroup of basic program statements and the word problem in S is decidable in polynomial time then minimization problem for program schemata operating on the interpretation over S is decidable in polynomial time as well.

Added: Oct 13, 2015
Article
С.С.Гайсарян, Нурмухаметов А., Курмангалеев Ш. и др. Труды Института системного программирования РАН. 2014. Т. 26. № 3. С. 113-126.
Added: Sep 13, 2016
Article
С.С.Гайсарян, Курмангалеев Ш., Долгорукова К. и др. Труды Института системного программирования РАН. 2014. Т. 26. № 1. С. 315-326.
Added: Sep 13, 2016
Article
Массобрио Р., Несмачнов С., Черных А. и др. Труды Института системного программирования РАН. 2016. Т. 28. № 6. С. 121-140.
Added: Aug 28, 2017
Article
Семакин А. Н. Труды Института системного программирования РАН. 2017. Т. 29. № 5. С. 311-328.
Added: Dec 25, 2017
Article
Кузнецов С. Д., Турдаков Д. Ю., Борисенко О. Д. и др. Труды Института системного программирования РАН. 2014. Т. 26. № 4. С. 45-54.

This article is an overview of scalable infrastructure for storage and processing of genome data in genetics problems. The overview covers used technologies descriptions, the organization of unified access to genome processing API of different underlying services. The article also covers methods for scalable and cloud computing technologies support. The first service in virtual genome processing laboratory is provided and presented. The service solves transcription factors bindning sites prediction problem. The main principles of service construction are provided. Basic requirements for underlying comptutaion software in virtual laboratory environments are provided. Overview describes the implemented web-service (https://api.ispras.ru/demo/gen) for transcription factors binding site prediction. Provided solution is based on ISPRAS API project as an API gateway and load-balancer; the middle-ware task-manager software for pool of workers support and for communications with Openstack infrastructure; OpenZFS as an intermediate storage with transparent compression support. The described solution is easy to extend with new services fitting the basic requirements.

Added: Nov 26, 2017
Article
С.Д. Кузнецов, Посконин А. В. Труды Института системного программирования РАН. 2013. Т. 24. С. 327-258.

Many modern applications (such as large-scale Web-sites, social networks, research projects, business analytics, etc.) have to deal with very large data volumes (also referred to as “big data”) and high read/write loads. These applications require underlying data management systems to scale well in order to accommodate data growth and increasing workloads. High throughput, low latencies and data availability are also very important, as well as data consistency guarantees. Traditional SQL-oriented DBMSs, despite their popularity, ACID transactions and rich features, do not scale well and thus are not suitable in certain cases. A number of new data management systems and approaches have emerged over the last decade intended to resolve scalability issues. This paper reviews several classes of such systems and key problems they are able to solve. A large variety of systems and approaches due to the general trend toward specialization in the field of SMS: every data management system has been adapted to solve a certain class of problems. Thus, the selection of specific solutions due to the specific problem to be solved: the expected load, the intensity ratio of read and write, the form of data storage and query types, the desired level of consistency, reliability requirements, the availability of client libraries for the selected language, etc.

Added: Jan 30, 2018
Article
Иванников В. П., Курмангалеев Ш. Ф., Белеванцев А. А. и др. Труды Института системного программирования РАН. 2014. Т. 26. № 1. С. 327-342.

Actual task is protecting programs from reverse engineering. The best choice to implement a resistant obfuscation is to create obfuscating compiler based on one of the existing compiler infrastructures. On the one hand, it will produce obfuscated program, with full information about it at all stages of compilation, and the other allows you to focus on the development of protection, rather than on creating the infrastructure required. In addition, this approach provides support for multiple architectures, as well as introduces watermarks for binary images of the program for each user depending from a unique key. The paper describes the methods for obfuscating C/C++ programs to prevent applying static analyzers to them. Paper observes existing obfuscating compilers. The proposed transformations are based on well-known obfuscation algorithms (including constant string protection, fake cycle insertion, control flow graph flattening, functions merge, function call encapsulation, control flow graph structure obfuscation, opaque predicate insertion and other) and they are specifically improved to resist better to static analysis deobfuscation techniques. The methods are implemented within the LLVM (low level virtual machine) compiler infrastructure. Experimental results presenting resulting program slowdown and used memory growth are given.

Added: Mar 22, 2017
Article
S. Kuznetsov, Борисенко О. Д., Алексиянц А. В. et al. Proceedings of the Institute for System Programming of the RAS. 2015. Vol. 27. No. 5. P. 35-48.

In this paper the problem of creating virtual clusters in clouds for big data analysis with Apache Hadoop and Apache Spark is discussed. Existing methods for Apache Spark clusters creation are described in this work. Also the implemented solution for building Apache Spark clusters and Apache Spark jobs execution in Openstack environment is described. The implemented solution is a modification for OpenStack Sahara project and it was featured in Openstack Liberty release.

Added: Jan 23, 2018
Article
Захаров В. А., Варновский Н. П., Кузюрин Н. Н. и др. Труды Института системного программирования РАН. 2014. Т. 26. № 3. С. 167-198.
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.
Added: Sep 30, 2015
Article
Борисенко О. Д., Пастухов Р. К., С.Д. Кузнецов Труды Института системного программирования РАН. 2016. Т. 28. № 6. С. 111-120.

Apache Spark is a framework providing fast computations on Big Data using MapReduce model. With cloud environments Big Data processing becomes more flexible since they allow to create virtual clusters on-demand. One of the most powerful open-source cloud environments is Openstack. The main goal of this project is to provide an ability to create virtual clusters with Apache Spark and other Big Data tools in Openstack. There exist three approaches to do it. The first one is to use Openstack REST APIs to create instances and then deploy the environment. This approach is used by Apache Spark core team to create clusters in propriatary Amazon EC2 cloud. Almost the same method has been implemented for Openstack environments. Although since Openstack API changes frequently this solution is deprecated since Kilo release. The second approach is to integrate virtual clusters creation as a built-in service for Openstack. ISP RAS has provided several patches implementing universal Spark Job engine for Openstack Sahara and Openstack Swift integration with Apache Spark as a drop-in replacement for Apache Hadoop. This approach allows to use Spark clusters as a service in PaaS service model. Since Openstack releases are less frequent than Apache Spark this approach may be not convenient for developers using the latest releases. The third solution implemented uses Ansible for orchestration purposes. We implement the solution in loosely coupled way and provide an ability to add any auxiliary tool or even to use another cloud environment. Also, it provides an ability to choose any Apache Spark and Apache Hadoop versions to deploy in virtual clusters. All the listed approaches are available under Apache 2.0 license.

Added: Jan 25, 2018
Article
Татарников А. Д., Камкин А. С., Чупилко М. М. и др. Труды Института системного программирования РАН. 2014. Т. 26. № 1. С. 149-200.

Ensuring the correctness of microprocessors and other microelectronic equipment is a fundamental problem. To deal with it, various tools for functional verification are used. Unlike bugs in software programs which are relatively easy to fix (it does not apply to their consequences), defects in integrated circuits (both design and manufacturing ones) cannot be removed. In spite of continuous development of computer-aided design (CAD) systems, test generation tools and approaches to analysis of circuits, verification remains the bottleneck of the microprocessor design cycle (it accounts for approximately 70 percent of total design resources). The article gives a brief overview of microprocessor verification tools, describes issues that commonly occur in industrial practice and analyzes possible ways to solve them. The main part of the article is dedicated to research in the field of unit- and system-level hardware verification conducted at ISPRAS. It describes such approaches as contract specification of pipeline, event-driven hardware specification, parallel/distributed testing, combinatorial test program generation and template-based test program generation. The article also summarizes the outcomes of accomplished projects, describes the present works and formulates the directions of further research.

Added: Dec 11, 2017