The article suggests a new object model of data for in-depth analysis of network traffic. In contrast to the model used by most existing network analyzers, such as Wireshark or Snort, the core of our model supports data streams reassembling and next processing. The model also provides a convenient universal mechanism for binding parsers. So one can develop parsers independently at all. Our model also provides processing of modified, e.g. compressed or encrypted, data. It forms the basis of the infrastructure for in-depth analysis of network traffic.

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.

False cache sharing happens when different parallel execution threads update the variables that reside in the same cache line. We suggest in this paper to evaluate the number of cache misses using code instrumentation and post-mortem trace analysis: the probability of the false sharing cache miss (defined as a memory write issued by one thread between two consecutive memory accesses issued by another thread) is calculated based on the gathered event trace, where each event is a memory access with a timestamp. The tracer tool is implemented as a GCC compiler pass, whereas the post-mortem analyzer is a separate application that gets the trace collection gathered on a sample application input data as its own input. Program slowdown in our approach is ~10 times, and it is dependent on a sampling probability but it does not depend on a cache line size.

The paper takes a look at the problem of deductive verification of Linux kernel code that is concurrent and accesses shared data. The presence of shared data does not allow to apply traditional deductive verification techniques, so we consider how to verify such code using proof of its compliance to a specification of a synchronization discipline. The approach is demonstrated on examples of spinlock specification and a simplified specification of RCU (Read-copy-update) API.

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).

This paper describes an approach to problem phrase extraction from texts that contain user experience with products. User reviews from online resources, that describe actual difficulties in use of products in addition to sentiment-oriented phrases, affect on other people's purpose decisions. In this paper we present two probabilistic graphical models which aims to extract problems with products from online reviews. We incorporate information about problem phrases with words’ sentiment polarities (negative, neutral or positive). The proposed models learn a distribution over words, associated with topics, both sentiment and problem labels. The algorithms achieve a better performance in comparison to several state-of-the-art models in terms of the likelihood of a held-out test and in terms of an accuracy of classification results, evaluated on reviews from several different domains in English and Russian. Our contribution is that summarizing sentiment and problem information about words with reviews’ topics by the model's asymmetric priors gives an improvement for problem phrase extraction from user reviews.

The paper is devoted to methods for construction of socio-demographic profile of Internet users. Gender, age, political and religion views, region, relationship status are demographic attributes. This work is a survey of methods that detect demographic attributes from user’s profile and messages. The most of observed works are devoted to gender detection. Age, political views and region are also interested researches. The most of solutions are based on supervised machine learning. Each step of solution is observed in this work: data collection, feature extraction, feature selection, classifiers, evaluation of methods

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.