Search

The search and classification of text documents are used in many practical applications. These are the key tasks of information retrieval. Methods of text searching and classifying are used in search engines, electronic libraries and catalogs, systems for collecting and processing information, online education and many others. There are a large number of particular applications of these methods, but each such practical task is characterized, as a rule, by weak formalizability and narrow objectivity. Therefore, it requires individual study and its own approach to the solution. This paper discusses the task of automatically searching and typing text fragments containing biographical information. The key problem in solving this problem is to conduct a multi-class classification of text fragments, depending on the presence and type of biographical information contained in them. After reviewing the related works, the author concluded that the use of neural network methods is promising and widespread for solving such problems. Based on this conclusion, the paper compares various architectures of neural network models, as well as basic text presentation methods (Bag-Of-Words, TF-IDF, Word2Vec) on a pre-assembled and marked corpus of biographical texts. The article describes the steps involved in preparing a training set of text fragments for teaching models, methods for text representation and classification methods chosen for solving the problem. The results of the multi-class classification of text fragments are also presented. The examples of automatic search for fragments containing biographical information are shown for the texts that did not participate in the model learning process.

Visual domain-specific languages usually have low entry barrier. Sometimes even children can program on such languages by working with visual representations. This is widely used in educational robotics domain, where most commonly used programming environments are visual. The paper describes a novel dataflow visual programming environment for embedded robotic platforms. Obviously, complex dataflow languages are not simple for understanding. The purpose of our tool is to "bridge" between lightweight educational robotic programming tools (commonly these tools provide languages which are based on control flow model) and complex industrial tools (which provide languages based on more complex dataflow execution model). We compare programming environments mostly used by robotics community with our tool. After brief review of behavioural robotic architectures, some thoughts on expressing them in terms of our dataflow language are given. Visual language, which is described here, provides opportunity to mix dataflow and control flow models for robotics programming. We believe that it is important for educational purposes. Program on our language consists of different blocks (visual representation of data transformation processes) and "links" which presents data flow between them. Domain-specific modelling approach was used to develop our language. Also, this paper provides the examples of solving two typical robot control tasks in our language.

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.

Existing research analyzing evolution of the Linux kernel considers the kernel together with loadable modules delivered with it or some specific subsystems of the kernel. The aim of this paper is to evaluate evolution of the kernel without loadable modules. It proposes a method for determining boundaries between them and evaluates evolution for all versions of the Linux kernel, released over the past 7.5 years. Also the paper presents a classification and a distribution of typical bugs that were fixed in the kernel, based on analysis of changes that have been made to stable branches of the kernel during the last 2 months of 2015. One can use the obtained results for evaluation of applicability of various methods and tools for software quality assurance.

High quality labeled corpora play a key role to elaborate machine learning systems. Generally, creating of such corpora requires human efforts. So, annotation process is expensive and time-consuming. Two approaches that optimize the annotation are active learning and crowdsourcing. Methods of active learning are aimed at finding the most informative examples for the classifier. At each iteration from the unplaced set, one algorithm is chosen by an algorithm, it is provided to the oracle (expert) for the markup and the classifier is newly trained on the updated set of training examples. Crowdsourcing is widely used in solving problems that can not be automated and require human effort. To get the most out of using crowdplatforms one needs to to solve three problems. The first of these is quality, that is, algorithms are needed that will best determine the real labels from the available ones. Of course, it is necessary to remember the cost of markup - to solve the problem by increasing the number of annotators for one example is not always reasonable - this is the second problem. And, thirdly, sometimes the immediate factor is the rapid receipt of the marked corpus, then it is necessary to minimize the time delays when the participants perform the task. This paper aims to survey existing methods based on this approaches and techniques to combine them. Also, the paper describes the systems that help to reduce the cost of annotation.

Reverse debugging is software development technique that effectively helps to fix bugs caused by nondeterministic program behavior. It allows inspecting past program’s state without rerun. The paper describes implementation of software reverse debugging using deterministic replay based on the QEMU emulator. We present ways to improve debugging performance by reducing saved data, using copy-on-write snapshots’ format and indexing/compressing of replay log. QEMU supports a common user interface for reverse debugging in GDB debugger which allows using reverse-continue, reverse-nexti, reverse-stepi and reverse-finish commands. Time required for these commands’ execution depends on taking snapshots frequency in recording replay log. This paper also presents assessment of snapshots frequency for better performance.

Jolie is the first language for microservices and it is currently dynamically type checked. This paper considers the opportunity to integrate dynamic and static type checking with the introduction of refinement types, verified via an SMT solver. The integration of the two aspects allows a scenario where the static verification of internal services and the dynamic verification of (potentially malicious) external services cooperate in order to reduce testing effort and enhance security. Refinement types are well-known technique for numeric, array and algebraic data types. They rely on corresponding SMT-theories. Recently SMT solvers got support for a theory of strings and regular expressions. In the paper, we describe possible application of the theory to string refinement types. We use Jolie programming language to illustrate feasibility and usefulness of such extension. First, because Jolie already has syntax extension to support string refinements. We build on top of that extension to provide static type checking. Second, because in the realm of microservices the need for improved checking of string data is much higher as most of external communication goes through text-based protocols. We present simplified but real-world example from the domain of web-development. We intentionally introduce a bug in the example demonstrating how easily it can slip a conventional type system. Proposed solution is feasible, as it do not accept program with the bug. Complete solution will need enhancements in precision and error reporting.

In the last few years there has been a growing interest in route building oriented mobile applications with the following features of navigation and sending timely notifications about arrival. Despite the large body of existing knowledge on navigational services, there has been an important issue relative to positioning accuracy. The paper discusses a possible solution to comparison problem, which is linked to the determination of the closeness to destination metro station through finding a difference between user’s current coordinates and fixed-point coordinates. With this end in view, fuzzy logic approach is used to develop Routes Recommender System (RRS) that utilizes linguistic variables to express the vague and uncertain term ‘closeness to…’. The paper provides detailed explanation of each variable considered in the fuzzy inference system (FIS), set of fuzzy rules in line with graphical representation of system’s output. Based on Mamdani model, we propose a set of test cases to check maintainability of the model and provide a description about received results. At a later time, an Android-based mobile application aimed at public transport route building will be developed whose notification system will be based on our model`s implementation presented. It should be emphasized that the paper examines potentials of the modeling approach based on interval type-2 fuzzy sets (IT2FS) that attract much attention these days in various research studies and conventional Mamdani fuzzy inference system (MFIS) as applied to real and rather topical problem. The significance of developing such models may be of a high demand for appropriate representation of factors that are inherently vague and uncertain. Hence, this study may also contribute to future research on similar topics.

Relational programming is an approach that allows you to execute programs in different "directions" to get different behaviors from one relational specification. The direct development of relational programs is a complex task, requiring the developer to have certain skills. However, in many cases, the required relational program can be obtained from a certain functional program automatically. In this paper, the problem of automatic conversion of functional programs into relational ones is considered. The main contribution of the paper is the method of converting typed functions into a relational form, as well as proving its static and dynamic correctness. This method can be applied to typed programs of a general kind. To describe these programs, a compact ML-like language (a subset of OCaml) is used, equipped with a Hindley-Milner type system with let-polymorphism Also, the paper discusses the limitations of the proposed method, presents an implementation for a subset of the OCaml language, and evaluates the method on a number of realistic examples.

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.

When developing programs in high-level languages, developers have to make assumptions about the correctness of the compiler. However, this may be unacceptable for critical systems. As long as there are no full-fledged formally verified compilers, the author proposes to solve this problem by proving the correctness of the generated machine code by deductive verification. To achieve this goal, it is required to combine the pre- and postcondition specifications with the machine code behavior model. The paper presents an approach how to combine them for the case of C functions without loops. The essence of the approach is to build models, both machine code and its specifications in a single logical language, and use target processor ABI to bind machine registers with the parameters of the high-level function. For the successful implementation of this approach, you have to take a number of measures to ensure the compatibility of the high-level specification model with the machine code behavior model. Such measures include the use of a register type in the high-level specifications and the translation of the pre- and postconditions into the abstract predicates. Also in the paper the choice of logical language for building models is made and justified, the most suitable tools for implementing the approach of merging specifications are selected and the evaluation of the system of deductive verification of machine code built on the basis of the proposed approach is made using test examples obtained by compiling C programs without loops.

This paper provides an overview of program analysis techniques and describes practical implementation of these techniques for automatic software defect detection. The paper focuses on program dynamic analysis technique based on tainted data flow tracing, instrumentation and constraint set construction for automatic input generation. An overview of practical considerations for developing a dynamic analysis tool for Java applications is given. It is complemented by a detailed description of actual prototype implementation created within the scope of this project. Finally, the paper features an overview of practical results obtained on a number of Java applications and provides an evaluation of these results.

The paper is devoted to the works performed within the Svace static analysis tool to support Java language. First, the approach to intercept compilation process for transparently building the analyzer internal representation should be extended to cover usage of the Java compiler API that is popular in Ant and Maven tools. We achieve this goal with implementing our custom Java agent that instruments all calls to the compiler API and notifies the analyzer with the actual compilation parameters. Second, the modified Javac compiler builds the analyzer IR. The changes we made to the compiler include avoiding unnecessary bytecode duplication for easier mapping of bytecode instructions to source code and properly marking the code added by the compiler itself. Third, we discuss the process of bytecode translation to the Svace IR proper (which is a low-level 3-address IR akin to the LLVM IR). It is a straightforward code generation algorithm with further code cleanups that treats stack locations as local variables made possible by the fact that we know the maximum stack size consumed by the method. Finally, we discuss the devirtualization heuristics that assume we know the full class hierarchy and specific Java checkers including synchronization issue checkers. Experimental results obtained on Android 5 source code show that the checkers have high quality (more than 80% true positives). It can be seen that the general infrastructure for analysis and checkers implemented in Svace works well for the Java programming language with the adaptations described in the paper.

The paper is addressed to an analysis of object-oriented data models specified at EXPRESS language and widely used in industrial applications. These models play important role for achievement of software interoperability and system integration in accordance with STEP standard family (ISO 10303). The examples of such models are STEP application protocols for machinery construction, automobile industry, shipbuiling, electronics, electrical engineering, systems engineering, furniture production as well as IFC (ISO 16739) model for architecture, engineering and construction, CIS/2 model for manufacturing using constructional steel work, POSC Caesar (ISO 15296) model for oil and gas producing industry. The purpose of the performed analysis is to unify representation of data integrity constraints typically used in the models by means of identification of constraint patterns. The identified patterns are specified at EXPRESS language as an unified constraint library that can be applied both on refactoring of the existing models and on development of new ones. Utilizing the constraint library users can improve clearness of the specifications, to simplify their maintenance and evolution and, on the whole, to accelerate their development. Besides, CASE tools can be effectively applied to analyze the specifications in highly automatic way. Possibility to apply the library for verification of the data models is also discussed in the paper. Rules for resolving the appropriate constraints have been proposed for each pattern. The constraint library can be recommended to industrial consortiums and technical committees that are engaged in development and standardization of the data models. The work is supported by RFBR (grant 13-07-00390).

The paper considers the problems of developing and analysis of cloud database systems. We determine the requrments for encryption to be usable in practical applications. A new notion - a non-derandomizable encryption - allows to do this and we explain the practical value of this notion as well as links between it and classical notions of cryptosystem’s security, practical security of whole cloud computing system. We show the examples of simple algebraically homomorphic cryptosystems - both derandomizable and not non-derandomizable. The paper finally concludes about usability of considered cryptosystems for practical cloud systems.

In this paper, we explore the possibilities of applying dynamic symbolic execution (or concolic testing) methods to applications with graphical user interfaces. Such applications inherently feature interactive user input processing and multithreaded execution. These features typically decrease the effectiveness of dynamic symbolic execution by increasing the volume of processed code not related to actual application functionality. We present a hybrid approach that combines commonly used GUI test automation methods based on GUI model excavation with dynamic symbolic execution methods to construct test cases for checking internal application logic. We have implemented this approach using two open-source tools - test automation framework GUITAR and Java byte-code static instrumentation framework Coffee Machine. GUI model extracted automatically by GUITAR tool is extended with symbolic traces relevant to application GUI event handlers. Our test generation module for GUITAR combines these symbolic traces into complex queries to be processed by SMT solver. The resulting test cases are valid within automatically extracted GUI structure model and allow to check different execution paths in GUI event handler code. We have checked our hybrid approach on a set of small open-source applications and identified several bugs caused by uncaught exceptions. The paper is concluded with an overview of current limitations and possible improvements of the hybrid approach.

The paper describes static analysis techniques that are used for defect detection in C# programs. The goal of proposed analysis approaches is to catch more defects within an acceptable amount of time. Although the paper contains a description of full analysis cycle, it mainly focuses on special aspects that distinguish C# analysis approaches from well-known Java and C++ techniques. The paper illustrates methods that allow taking into account C# specialties of all analysis stages: call graph and control flow graph construction, data flow analysis, context- and path-sensitive interprocedural analysis. We propose an adaptation of symbolic execution methods inspired by Bounded Model Checking and Saturn Software Analysis Project. The paper also explains the organization of memory model, which is suitable for both a precise intraprocedural analysis and a creation of compact function-bound conditions used for interprocedural analysis. Special attention is paid to optimization of condition size and simplicity during a path sensitive-analysis. The conditions produced by a path-sensitive analysis are supposed to be solved by modern SMT solvers like Microsoft Z3 Prover. Different approaches to external functions modeling are covered. All proposed approaches are implemented in the SharpChecker static analysis tool and, as evaluated on several open source C# projects of varying size (1K - 1.35M lines of code), display good results and scalability.

The paper deals with keyphrase extraction problem for single documents, e.g. scientific abstracts. Keyphrase extraction task is important and its results could be used in a variety of applications: data indexing, clustering and classification of documents, meta-information extraction, automatic ontologies creation etc. In the paper we discuss an approach to keyphrase extraction, itsтАЩ first step is building of candidate phrases which are then ranked and the best are selected as keyphrases. The paper is focused on the evaluation of weighting approaches to candidate phrases in the unsupervised ex-traction methods. A number of in-phrase word weighting procedures is evaluated. Unsuitable approaches to weighting are identified. Testing of some approaches shows their equivalence as applied to keyphrase extraction. A feature, which allows to increase the quality of extracted keyphrases and shows better results in comparison to the state of the art, is proposed. Experiments are based on Inspec dataset.

Embedded platforms with heterogeneous architecture, considered in this paper, consist of one primary and one or more secondary processors. Development of software systems for these platforms poses substantial difficulties, requiring a distinct set of tools for each constituent of the heterogeneous system. It also makes achieving high efficiency the more difficult task. Moreover, many use cases of embedded systems require runtime configuration, that cannot be easily achieved with usual approaches. This work presents a C-like metaprogramming DSL and a library that provides a unified interface for programming secondary processors of heterogeneous systems with this DSL. Together they help to resolve aforementioned problems. The DSL is embedded in C++ and allows to freely manipulate its expressions and thus embodies the idea of generative programming, when the expressive power of high-level C++ language is used to compose pieces of low-level DSL code. Together with other features, such as generic DSL functions, it makes the DSL a flexible and powerful tool for dynamic code generation. The approach behind the library is dynamic compilation: the DSL is translated to LLVM IR and then compiled to native executable code at runtime. It opens a possibility of dynamic code optimizations, e.g. runtime function specialization for specific parameters known only at runtime. Flexible library architecture allows simple extensibility to any target platform supported by LLVM. At the end of the paper a system approbation on different platforms and a demonstration of dynamic optimizations capability are presented.

This paper gives a survey of existing methods and tools for test program generation for microprocessors. Test program generation and analysis of their execution traces is the main approach to functional verification of microprocessors. This approach is also known as testing. Despite continuous progress in test program generation methods, testing remains an extremely laborious process. One of the main reasons is that test program generation tools are unable to quickly enough adapt to changes. In the majority of cases, they are created for specific microprocessor types and are designed to solve specific tasks. For this reason, support for new microprocessors types and generation methods requires a significant effort. Often, in such situations, tools have to be implemented from scratch. Inability to reuse existing implementations of generation methods complicates evolution of test generation tools and, consequently, prevents improvement of testing quality. The present situation creates motivation to search for solutions to developing more flexible tools which could be easily adapted to testing new microprocessor types and applying new generation methods. The goal of the present work is to summarize existing experience in test program generation, which could serve as a basis for creating such tools. The paper considers strengths and weaknesses of popular generation methods, their application domains and cases of their combined use. It also makes a comparative analysis of facilities of existing generation tools implementing these methods. Based on the analysis, it gives recommendations on creating a unified methodology to develop tools for test program generation for microprocessors.

Nowadays static verification is one of the most promising methods for finding bugs in programs. To apply successfully existing tools for the Linux kernel one needs to perform componentwise verification. Such verification needs an environment model that reflects a real environment of components rather accurately. Development of the complete environment model for Linux kernel components is a very time-consuming task since there are too many programming interfaces in the kernel and they are not stable. The given paper suggests a new approach for building programming interface specifications. This approach allows one to apply static verification tools efficiently (with small number of false alarms but without missed bugs) for checking rules of programming interfaces usage under conditions of the incomplete environment model, if component developers obey a specific coding style. Two implementations of the suggested approach were developed. The first one extended the BLAST static verification tool while the second one utilized C Instrumentation Framework – an aspect-oriented programming implementation for the C programming language. The latter allowed to use various static verification tools, like BLAST, CPAchecker, CBMC, etc., for checking specifications. In practice that implementation helped to reduce the number of false alarms on more than 70% for some rules of programming interfaces usage. The paper shows that to avoid left false alarms one needs to develop more precise environment models and to use more accurate static verification tools. Besides the Linux kernel the suggested approach can be applied for componentwise verification in projects where developers obey the specific coding style.

Linux driver verification is a large application area for software verification methods, in particular, for functional, safety, and security verification. Linux driver software is industrial production code — IT infrastructures rely on its stability, and thus, there are strong requirements for correctness and reliability. Linux driver software is complex, low-level systems code, and its characteristics make it necessary to bring to bear techniques from program analysis, SMT solvers, model checking, and other areas of software verification. These areas have recently made a significant progress in terms of precision and performance, and the complex task of verifying Linux driver software can be successful if the conceptual state-of-the-art becomes available in tool implementations.The paper is based on experience of the research groups led by authors in verification of industrial software. It is important to develop verification tools that are efficient and effective enough to successfully check software components that are as complex as device drivers. In this area verifiers/researchers and Linux society find mutual benefits in cooperation because: for the society it is important to get such crucial software verified; for the verification community it is important to get realistic verification tasks in order to tune and further develop the technology. The paper provides an overview of the state-of-the-art and pointed out research directions in which further progress is essential. In particularly the paper considers most promising verification techniques and tools, including predicate abstraction, counter example generation, explicit-state verification, termination and concurrency analysis. One of main topic of Linux driver verification research is combination of verification techniques.

Querying source code helps developers to discover code fragments of interest and to determine their interrelations with each other. Different approaches exist to execute source code queries automatically. Some of them are based on a rather simple text pattern matching. More advanced approaches provide abilities to use natural languages for queries and perform matching on the basis of a formal program representation. We suggest using aspect-oriented programming for querying source code and consider advantages and disadvantages of this approach. The paper introduces main conceptions of aspect-oriented programming and briefly presents C Instrumentation Framework – an aspect-oriented programming implementation for the C programming language. We slightly extended C Instrumentation Framework so that it could execute source code queries written in form of aspects. The paper gives several examples of utilization of the suggested approach in particular for collecting information required for generating environment models for device drivers in the Linux Driver Verification project. The suggested approach is inferior to special querying tools in making queries by control and data flows. But it is simple in implementation and allows one to use traditional means of aspect-oriented programming for developing and executing source code queries.

Topic modeling is a method for building a model of a collection of text documents. The model is able to determine topics for each of documents. Shifting from term space to space of extracted topics helps resolving synonymy and polysemy of terms. Besides, it allows for more efficient topic-sensitive search, classification, summarization, and annotation of document collections and news feeds. The paper shows an evolution of topic modeling techniques. The earlier methods are based on clustering. These algorithms use some similarity function defined on two documents. The next generation of topic modeling techniques is based on Latent Semantic Indexing (LSA). Words co-occurrences in documents are analyzed here. Currently, the most popular are approaches based on Bayesian networks — directed probabilistic graphical models which incorporate different kinds of entities and metadata: document authorship, connections between words, topics, documents, and authors, etc. The paper contains a comparative survey of different models along with methods for parameter estimation and accuracy measurement. The following topic models are considered in the paper: Probabilistic Latent Semantic Indexing, Latent Dirichlet Allocation, non-parametric models, dynamic models, and semi-supervised models. The paper describes well-known quality evaluation metrics: perplexity and topic coherence. Freely available implementations are listed as well.

Big data challenged traditional storage and analysis systems in several new ways. In this paper we try to figure out how to overcome this challenges, why it's not possible to make it efficiently and describe three modern approaches to big data handling: NoSQL, MapReduce and real-time stream processing. The first section of the paper is the introduction. The second section discuss main issues of Big Data: volume, diversity, velocity, and value. The third section describes different approaches to solving the problem of Big Data. Traditionally one might use a relational DBMS. The paper propose some steps that allow to continue RDBMS using when it’s capacity becomes not enough. Another way is to use a NoSQL approach. The basic ideas of the NoSQL approach are: simplification, high throughput, and unlimited scaling out. Different kinds of NoSQL stores allow to use such systems in different applications of Big Data. MapReduce and it’s free implementation Hadoop may be used to provide scaling out Big Data analytics. Finally, several data management products support real time stream processing under Big Data. The paper briefly overviews these products. The final section of the paper is the conclusion.

The paper presents a unified model for testing tools for object-oriented application development. Based the available papers were identified shortcomings of existing work and identified the following optimal criteria, which shall comply the resulting model: 1. To deep inheritance hierarchies 2. To presents of multiple inheritance hierarchies 3. To presents of abstract classes in the hierarchy 4. To presents of multiple (n-ary) associations 5. To presents of associations with attributes 6. To presents of a composition between classes 7. To presents of recursive associations 8. To presents of associations between classes belonging to the same inheritance hierarchy 9. To presents of association classes 10. To presents between the association class and other classes 11 To presents enumerations in model With a unified graphical language UML class diagram unified model testing. The paper we verified compliance with the resulting implementation of the selected criteria was presented. Currentlythe implementation of applications using object-oriented programming languages and relational databases. To overcome the object-relational mismatch it is necessary to implement object-related mapping patterns presents. The paper presents three methods used to represent the class hierarchy highlighted the advantages and disadvantages of each method. For test the feasibility a unified model chosen development environment SharpArchitect RAD Studio which is designed object applications in C# and are implementing a relational database. The paper presents the developed object model in the form a class diagram showing the interfaces and inheritance relations diagram containing all the tables and columns the resulting database. In the conclusion recommendations on the areas for further development work and identified the need of implement a unified model with other approaches proposed by the authors was used.

Due to huge amounts of code in modern software products, there is always a variety of subtle errors or flaws in programs, which are hard to discover during everyday use or through conventional testing. A lot of such errors could be used as a potential attack vector if they could be exploited by a remote user via manipulation of program input. This paper presents the approach for automatic detection of security vulnerabilities using interprocedural static taint analysis. The goal of this study is to develop the infrastructure for taint analysis applicable for detection of vulnerabilities in C and C++ programs and extensible with separate detectors. This tool is based on the Interprocedural Finite Distributive Subset (IFDS) algorithm and is able to perform interprocedural, context-sensitive, path-insensitive analysis of programs represented in LLVM form. According to our research it is not possible to achieve good results using pure taint analysis, so together with several enhancements of existing techniques we propose to supplement it with additional static symbolic execution based analysis stage, which has path-sensitivity and considers memory region sizes for filtering results found by the first stage. The evaluation of results was made on Juliet Test Suite and open-source projects with publicly known vulnerabilities from CVE database.

The existing tools of deductive verification allow us to successfully prove the correctness of functions written in high-level languages such as C or Java. However, this may not be enough for critical software because even fully verified code cannot guarantee the correct generation of machine code by the compiler. At the moment, developers of such systems have to accept the compiler correctness assumption, which, however, is extremely undesirable, but inevitable due to the lack of full-fledged systems of formal verification of machine code. It is also worth noting that the verification of machine code by a person directly is an extremely time-consuming task due to the high complexity and large amounts of machine code. One of the approaches to simplify the verification of machine code is automatic deductive verification reusing the formal specification of the high-level language function. The formal specification of the function consists of the specification of the pre- and postcondition, as well as loop invariants, which specify conditions that are satified at each iteration of the loop. When compiling a program into machine code, pre- and postconditions are preserved, which, however, cannot be said about loop invariants. This fact is one of the main problems of automatic verification of machine code with loops. Another important problem is that high-level function variables often have ‘projections' to both registers and memory at the machine code level, and the verification procedure requires that invariants be described for each variable, and therefore the missing invariants must be generated. This paper presents an approach to solving these problems, based on the analysis of the control flow graph, and intelligent search of the locations of variables.

The subject of this paper is development of software framework for real-time management of intelligent devices. The framework enables intelligent management of IoT devices in cyber-physical systems using models based on recurrence relations and differential equations. The platform was developed using Python programming language, Django framework and wide corpus of modules and libraries that supports continuous simulation. The software framework incorporates application programming interface as well, for specification of system behaviour, transmission of input parameters and output results, sending control actions via web services to the IoT system.

Cyber security standards are often used to ensure the security of industrial control systems. Nowadays, these systems are becoming more decentralized, making them more vulnerable to cyber attacks. One of the challenges of implementing cyber security standards for industrial control systems is the inability to verify early that they are compliant with the relevant standards. Cyber security standard compliance is also only validated and not formally verified, often not providing strong proofs of correct use of cyber security standard. In this paper, we propose an approach that uses formal analysis to achieve this. We formally define building blocks necessary to define the system formally in order to enable formal modeling of the system and carry out the analysis using the Alloy Analyzer. Our approach can be used at an early design stage, where problems are less expensive to correct, to ensure that the system has the desired security properties. We show the applicability of our approach by modeling two distinct cyber attacks and mitigations strategies used to defend against these attacks and also evaluate our approach based on its flexibility to handle and combine different aspects of the cyber security standards. We discuss the future directions of our research.

Today the development cycle of many application classes requires a security analysis stage. Taint analysis is widely used to check programs for different security vulnerabilities. This paper describes static interprocedural flow, context, and object-sensitive taint analysis approach for C/C++ applications. Our taint analysis algorithm is based on the Flowdroid project’s approach, but in contrast to Flowdroid, which aims to analyze Java bytecode, our approach handles LLVM bitcode and pointer arithmetic. Primary drawback of the Flowdroid approach is a memory usage issue which arises during analysis of medium size applications (around 10 000 edges in the call graph). To achieve scalability of the approach, we suggest a set of heuristics which helps to significantly decrease memory usage of the algorithm. The testing of real-world applications shows that such heuristics make precise taint analysis suitable for the medium size programs. Using our approach, we implemented general taint analysis framework as an LLVM pass. Additional security checks (e.g. Use of Hard-coded Password, Information Exposure, etc.) can be implemented on top of this framework. We have also developed auxiliary passes which resolve targets of virtual calls and build interprocedural control flow graph according to the results.

In this paper search method for format string vulnerabilities is presented. The method is based on dynamic analysis and symbolic execution. It is applied to program binaries, without requiring debug information. We present a tool implementing this method. We have used this tool to detect known vulnerabilities in Linux programs.

The deterministic replay technique can be used for debugging, improving reliability and robustness, software development and incident investigation (including reverse engineering of malware). The paper describes the implementation of deterministic replay of IA-32 based boards in QEMU. Another implementation of this technique in QEMU had been previously published, but it uses a significantly different approach. Deterministic replay implementation details and features substantially depend on deterministic area - the part of virtual machine which execution is being replayed. For replay to be deterministic the implementation must ensure that (1) all information flows across deterministic area borders should be logged and then replayed, and (2) there is no non-determinism inside deterministic area. The proposed approach is called «Min VM» because it’s based on the minimal deterministic area while the former one should be called «Max VM» as it attempts to stretch deterministic area to cover whole virtual machine. The proposed approach shows the advantages of lower time overhead for logging phase and easier support (because it is much easier to ensure determinism of small deterministic area). On the other side the shortcoming is larger log size mostly because deterministic area doesn’t include hard disks so all data flows from disks are being logged. It makes the self-sufficient replay log: image of the original HDD is not needed to replay the execution. The implementation has been tested on popular operating systems: Windows XP, Windows 7 and GNU/Linux 3.12. The current implementation shows 6 - 42% slowdown depending on application code that exceeds previous approach slowdown (17 - 79%).

In recent years, as performance and capacity of main and external memory grow, performance of database management systems (DBMSes) on certain kinds of queries is more determined by raw CPU speed. Currently, PostgreSQL uses the interpreter to execute SQL queries. This yields an overhead caused by indirect calls to handler functions and runtime checks, which could be avoided if the query were compiled into native code "on-the-fly", i.e. just-in-time (JIT) compiled: at run time the specific table structure is known as well as data types and built-in functions used in the query as well as the query itself. This is especially important for complex queries, performance of which is CPU-bound. We’ve developed a PostgreSQL extension that implements SQL query JIT compilation using LLVM compiler infrastructure. In this paper we show how to implement JIT compilation to speed up sequential scan operator (SeqScan) as well as expressions in WHERE clauses. We describe some important optimizations that are possible only with dynamic compilation, such as precomputing tuple attributes offsets only for attributes used by the query. We also discuss the maintainability of our extension, i.e. the automation for translating PostgreSQL backend functions into LLVM IR, using the same source code both for our JIT compiler and the existing interpreter. Currently, with LLVM JIT we achieve up to 5x speedup on synthetic tests as compared to original PostgreSQL interpreter.

It is generally considered that object-oriented (OO) languages provide weaker support for generic programming (GP) as compared with functional languages such as Haskell or SML. There were several comparative studies which showed this. But many new object-oriented languages have appeared in recent years. Have they improved the support for generic programming? And if not, is there a reason why OO languages yield to functional ones in this respect? In the earlier comparative studies object-oriented languages were usually not treated in any special way. However, the OO features affect language facilities for GP and a style people write generic programs in such languages. In this paper we compare ten modern object-oriented languages and language extensions with respect to their support for generic programming. It has been discovered that every of these languages strictly follows one of the two approaches to constraining type parameters. So the first design challenge we consider is “which approach is better”. It turns out that most of the explored OO languages use the less powerful one. The second thing that has a big impact on the expressive power of a programming language is language support for multiple models. We discuss pros and cons of this feature and its relation to other language facilities for generic programming.

The paper discusses an optimization approach for external calls in position-independent code that is based on loading the callee address immediately at the call site from the Global Offset Table (GOT), avoiding the use of the Procedure Linkage Table (PLT). Normally the Linux toolchain creates the PLT both in the main executable (which comprises position-dependent code and has to rely on the PLT mechanism to make external calls) and in shared libraries, where the PLT serves to implement lazy binding of dynamic symbols, but is not required otherwise. However, calls via the PLT have some overhead due to an extra jump instruction and poorer instruction cache locality. On some architectures, binary interface of PLT calls constrains compiler optimization at the call site. It is possible to avoid the overhead of PLT calls by loading the callee address from the GOT at the call site and performing an indirect call, although it prevents lazy symbol resolution and may cause increase in code size. We implement this code generation variant in GCC compiler for x86 and ARM architectures. On ARM, loading the callee address from the GOT at call site normally needs a complex sequence with three load instructions. To improve that, we propose new relocation types that allow to build a PC-relative address of a given GOT slot with a pair of movt, movw instructions, and implement these relocation types in GCC and Binutils (assembler and linker) for both ARM and Thumb-2 modes. Our evaluation results show that proposed optimization yields performance improvements on both x86 (up to 12% improvement with Clang/LLVM built with multiple shared libraries, on big translation units) and ARM (up to 7% improvement with SQLite, average over several tests), even though code size on ARM also grows by 13-15%.

This paper introduces a method for scalable verification of cache coherence protocols described in the Promela language. Scalability means that resources spent on verification (first of all, machine time and memory) do not depend on the number of processors in the system under verification. The method is comprised of three main steps. First, a Promela model written for a certain configuration of the system is generalized to the model being parameterized with the number of processors. To do it, some assumptions on the protocol are used as well as simple induction rules. Second, the parameterized model is abstracted from the number of processors. It is done by syntactical transformations of the model assignments, expressions, and communication actions. Finally, the abstract model is verified with the Spin model checker in a usual way. The method description is accompanied by the proof of its correctness. It is stated that the suggested abstraction is conservative in a sense that every invariant (a property that is true in all reachable states) of the abstract model is an invariant of the original model (invariant properties are the properties of interest during verification of cache coherence protocols). The method has been automated by a tool prototype that, given a Promela model, parses the code, builds the abstract syntax tree, transforms it according to the rules, and maps it back to Promela. The tool (and the method in general) has been successfully applied to verification of the MOSI protocols implemented in the Elbrus computer systems.

This paper proposes an analysis of various distributed data storage systems and possible solutions to basic problems of the subject area, in particular, the issue of system scaling, data consistency, availability and partition tolerance. Performed analysis has allowed to reveal consistent patterns with an attempt to classify systems based on various parameters, in particular, the presence or absence of specific functions and mechanisms. The choices of the distributed data storage systems are based on data analysis and classification.

Market surveillance systems, used for monitoring and analysis of all transactions in the financial market, have gained importance since the latest financial crisis. Such systems are designed to detect market abuse behavior and prevent it. The latest approach to the development of such systems is to use machine learning methods that largely improve the accuracy of market abuse predictions. These intelligent market surveillance systems are based on data mining methods, which build their own dependencies between the variables. It makes the application of standard user-logic-based testing methodologies difficult. Therefore, in the context of intelligent surveillance systems, we built our own model for classifying the transactions. To test it, it is important to be able to create a set of test cases that will generate obvious and predictable output. We propose scenarios that allow to test the model more thoroughly, compared to the standard testing methods. These scenarios consist of several types of test cases which are based on the equivalence classes methodology. The division into equivalence classes is performed after the analysis of the real data used by real surveillance systems. We tested the created model and discovered how this approach allows to define its weaknesses. This paper describes our findings from using this method to test a market surveillance system that is based on machine learning techniques.

This article is based on a thesis “Techniques of organizations shared access to distributed memory pages in cloud computing systems”, defensed in Igor Sikorsky Kyiv Polytechnic Institute in 2017. The paper describes distributed pages processing in Oracle Real Application Clusters (Oracle RAC) and compares it with other known processing methods. The comparison comprises analysis of different architectures (including shared nothing, shared disk and “based on a replication” architecture) in the context of SQL query processing and asserts reasonableness of distributed pages approach (also known as Global Cache Fusion) choice for cloud DBMS. As a result researching the Global Cache Fusion approach there was revealed main drawback of Oracle RAC systems - “increasing queue problem”: impossibility process requests after intensity of requests exceeds threshold intensity, which is inversely proportional packet sent time between nodes. To eliminate “increasing queue problem” during distributed page access the new access method is proposed, which is based on the initiation of one more page state - the "unloading" state, which increases the efficiency of processing distributed pages by reducing the number of transfers between nodes during hot page processing. The considered method can be used not only in cloud DBMS but also in other cloud systems in a case if they use page-organized distributed memory architecture.

The paper presents an approach to specify constraints on AADL models in Python-based language and a toolset allowing to verify that constraints. The goal of the approach is to enable reusing of existing rich facilities of Python language, tools, and libraries as well as to reduce learning curve of engineers. Constraints must be placed into component annexes. These constraints must be written in Python programming language as functions with one argument (an object to be checked), Boolean result, and special decorator. A plugin for a modeling environment generates a program in Python from the model components declarations. While it is executing this program creates an object with the model instance and checks the object by functions from annexes. This approach is implemented in MASIW Framework that allows checking constraints on model instance. The implementation is made upon PyDev, a well-known Eclipse-plugin for Python developing in Eclipse and reuses integration of Eclipse with Python from PyDev.

This paper describes the static analysis tool for finding program entities, their metrics, and relations between entities. Program entities are files/directories (physical structure) and classes/functions/methods/global variables (logical structure). Relations are connections between entities, such as calls, inheritance, aggregation, reading/writing, inclusion. We describe the methods for developing such a tool for C/C++ languages based on open source components: LLVM/Clang compiler infrastructure, GNU Binutils linker and archiver. We are sketching the changes that were required to be made in the Clang compiler, and we discuss the analysis methods implemented in the LLVM analyzer. We briefly present the results of testing our tool on Android OS.

The paper proposes an approach to introspection of virtual machines using the applications binary interface. The purpose of ​​the method is to get information about the system, while having a minimum knowledge about its internal structure. Our system is based on QEMU emulator and has a modular structure. Existing approaches (RTKDSM, DECAF) receive data from the operating system using the kernel structures. Those instruments have to store a large number of data profiles, because all addresses and offsets in the kernel structures vary from version to version. We offer the use of the rarely changing application binary interfaces, such as calling conventions and the numbers and parameters of system calls. The idea of ​​the method is to intercept system functions and read parameters and return values. Processor uses a special instruction to implement a system call. We expand QEMU with instrumentation engine, so we are able to monitor each executing instruction and to filter desired ones. In the event of a system call, we pass the control to the detector of system calls, that checks the number of occurred call and according to it decides to which plugin the job should be redirected to. In the mechanism of system calls interception, it is important not only to determine that the call occurred, but also to correctly determine its completion. That is needed to obtain the values ​​of output parameters and return values. To determine the end of the system call, the system also has special instructions, but we need to collate the beginning of the call to its end correctly. And to do so we are using the current context. Thus, we have implemented monitoring of file operations and processes, and created a prototype of API functions monitor. We plan to expand the set of plugins for analysis and monitoring.

Specialization is a program optimization approach that implies the use of a priori information about values of some variables. Specialization methods are being developed since 1970s (mixed computations, partial evaluation, supercompilation). However, it is surprising, that even after three decades, these promising methods have not been put into the wide programming practice. One may wonder: What is the reason? Our hypothesis is that the task of specialization requires much greater human involvement into the specialization process, the analysis of its results and conducting computer experiments than in the case of common program optimization in compilers. Hence, specializers should be embedded into integrated development environments (IDE) familiar to programmers and appropriate interactive tools should be developed. In this paper we provide a work-in-progress report on results of development of an interactive specializer based on partial evaluation for a subset of the Java programming language. The specializer has been implemented within the popular Eclipse IDE. Scenarios of the human-machine dialogue with the specializer and interactive tools to compose the specialization task and to control the process of specialization are under development. An example of application of the current version of the specializer is shown. The residual program runs several times faster than the source one.

In this paper, we present a Big Data analysis paradigm related to smart cities using cloud computing infrastructures. The proposed architecture follows the MapReduce parallel model implemented using the Hadoop framework. We analyse two case studies: a quality-of-service assessment of public transportation system using historical bus location data, and a passenger-mobility estimation using ticket sales data from smartcards. Both case studies use real data from the transportation system of Montevideo, Uruguay. The experimental evaluation demonstrates that the proposed model allows processing large volumes of data efficiently.

In recent years, as performance and capacity of main and external memory grow, performance of database management systems (DBMSes) on certain kinds of queries is more determined by raw CPU speed. Currently, PostgreSQL uses the interpreter to execute SQL queries. This yields an overhead caused by indirect calls to handler functions and runtime checks, which could be avoided if the query were compiled into native code "on-the-fly", i.e. just-in-time (JIT) compiled: at run time the specific table structure is known as well as data types and built-in functions used in the query as well as the query itself. This is especially important for complex queries, performance of which is CPU-bound. We have developed a PostgreSQL extension that implements SQL query JIT compilation using LLVM compiler infrastructure. In this paper we show how to implement LLVM-analogues of the main operators of the PostgreSQL, how to replace Volcano iterator model abstraction (open(), next(), close()) by the abstraction that is more suitable to generate code for a particular query. Currently, with LLVM JIT we achieve up to 4.3x speedup on TPC-H Q1 query as compared to original PostgreSQL interpreter.

The goal of finding unreachable code is to report warnings about possible bugs in the source code and an increase of other analyses accuracy. The paper describes unreachable code classification and approaches for finding unreachable code in C/C++ programs. We described three data-flow analysis problems: value interval analysis, excluded value analysis, predicate analysis. Solutions for these problems are used to detect redundant expressions in conditional statements. We described common occurrences of useless warnings. The algorithms are implemented in the Svace tool that is developed by ISP RAS. The results are evaluated for open source projects Android-5.02 and Tizen-2.3. They represent the number of found warnings and its intersection.

Static verification proves correctness of the software against checked requirements, but it requires a lot of resources for that and its task is undecidable in general case. At present there is no universal static verification method, which could efficiently check any software. That is why one should choose more appropriate method and set its parameters for checking correctness of the given requirements in a given program. This paper suggests to combine different static verification methods in order to increase efficiency and effectiveness of verification, which is the first step in creating universal method for static verification. The suggested methods were implemented as combination of actively developing static verification methods for checking requirements composition. Implementation of the suggested methods showed their advantages on Linux kernel modules in comparison with using of each verification method separately.

Nowadays, web applications are one of the most popular types of target of evaluation within the framework of the information security certification. The relevance of the study of web applications vulnerabilities during information security certification is due to the fact that web technologies are actively used while producing modern information systems, including information systems critical from the information security point of view, and on the other hand carrying out basic attacks on such information systems do not require violators of high technical competence, since data on typical vulnerabilities and attacks, including the attacking tools are heavily represented in publicly available sources of information, and the information systems themselves are usually available from public communication networks. The paper presents the results of a study of the security of web applications that are target of evaluation within the framework of certification for information security requirements against cross-site requests forgery attacks. The results of systematization and generalization of information about the cross-site requests forgery attacks and security controls used by web application developers are presented. The results of experimental studies of 10 web applications that have passed certification tests against information security requirements are presented. The results of experimental studies have shown that most developers do not pay enough attention to protection from cross-site request forgery attack - 7 out of 10 web applications tested have been vulnerable to this type of attack. Based on the results of processing the results of experimental studies, the distribution of security controls used in web applications and identified vulnerabilities by programming languages were obtained. Recommendations regarding the protection of web applications against cross-site request forgery attack for developers planning to certify their software are formulated.

Extracting various valuable medical information from head MRI and CT series is one of the most important and challenging tasks in the area of medical image analysis. Due to the lack of automation for many of these tasks, they require meticulous preprocessing from the medical experts. Nevertheless, some of these problems may have semi-automatic solutions, but they are still dependent on the person's competence. The main goal of our research project is to create an instrument that maximizes series processing automation degree. Our project consists of two parts: a set of algorithms for medical image processing and tools for its results interpretation. In this paper we present an overview of the best existing approaches in this field, as well the description of our own algorithms developed for similar tissue segmentation problems such as eye bony orbit and brain tumor segmentation based on convolutional neural networks. The investigation of performance of different neural network models for both tasks as well as neural ensembles applied to brain tumor segmentation is presented. We also introduce our software named "MISO Tool" which is created specifically for this type of problems. It allows tissues segmentation using pre-trained neural networks, DICOM pixel data manipulation and 3D reconstruction of segmented areas.