In connection with the process of implementation by the Federal Service for Technical and Export Control of Russia "Information Security Requirements for Operating Systems", the work analyzes the ways of fulfilling the requirements of the functional component ADV_SPM.1 "Formal Security Policy Model", including defining the language, depth and detail of the presentation of the access control policy and information flows. Among other things, proposals are given on the composition of the main elements of the model, the use of tools for its verification. The practical possibility of applying the proposed approaches is considered by the example of the presentation of the description and verification of the mandatory entity-role security model for logical access control and information flows as the basis of the access control mechanism in the special-purpose operating system Astra Linux Special Edition.

The article presented a set of algorithms that form the basis of the safe code execution system. The functional purpose of it is to investigate arbitrary executable files of the operating system in the absence of source codes in order to provide the ability to control the execution of the program code within the specified functional requirements. The set of algorithms presented in this work includes: the algorithm for the functioning of a system for the safe execution of the program code; the algorithm for constructing a program model suitable for verification, which accurately preserves the properties of the source program.

The paper discusses the problem of representation of algorithms extracted from binary code in course of reverse engineering: both representations for automatic analysis and final representations for the user. Two key subproblems of reverse engineering are focused on: automatic search for exploitable defects and discovery of undeclared capabilities. A principal scheme of system that allows automatically finding exploitable defects is described, along with key features of an internal representation employed by such system from the viewpoint of efficient generation of equations for an SMT solver. A sequence of steps for a system that reveals undeclared capabilities is enumerated: algorithm localization, its representation in a form suitable for analysis, and recovery of its properties. In order to automate the first step a static-dynamic representation is built which includes OS-level events and calls to library functions that serve as “anchor points” for the analyst in course of algorithm localization. Further support for localization is provided by means of code slicing and navigation algorithms. Once the algorithm is localized, further work goes in two directions: dialogue-based building of an annotated representation of the algorithm as a flowchart and automated research of characteristics of the algorithm in terms of declared and undeclared data flows. Flowchart representation of an algorithm is based on building simplified function models which describe input and output buffers, and automatic analysis of data flows between buffers of calls of different functions. The general scenario of interaction between an analyst and such a flowchart in context of the undeclared capability revealing problem is described, based on annotating declared data flows and automatically revealing undeclared ones. The paper concludes with an example of such a representation and an enumeration of further work directions.

The paper examines the ADV_SPM "Security policy modelling" assurance family, which is part of the ADV "Development" assurance class and defined by the ISO/IEC 15408-3-2013 "Information technology - Security techniques - Evaluation criteria for IT security - Part 3: Security assurance components" standard. We discuss the objective set by this family, which is to provide additional assurance from the development of a formal security policy model of the target of evaluation security functionality and establishing a correspondence between the functional specification and this security policy model by means of a mathematical proof. We propose an approach to the formalization and verification of security policies using the Event-B modelling notation and the Rodin platform, whose rigour is used to obtain the desired security properties by means of formal machine-checkable proofs. The approach helps to identify and eliminate ambiguous, inconsistent, contradictory, or unenforceable security policy elements. We illustrate this approach with a simplified example of a FRU_PRS "Priority of service" model (defined in the second part of the standard) in which we provide a formal proof that the model contains no inconsistencies, and that an insecure state cannot be reached. We conclude that the approach is applicable for solving practical problems and it can be used to fulfil the requirements of the ADV_SPM assurance family.

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.

In the present day, software development industry for different classes of computing devices grows at an extremely high speed. Continuously growing power of computational systems presents new opportunities to create powerful, often parallel, programs and software systems. This leads to the growth of complexity of software intended to manage these computational systems. The process of quality assurance calls for new approaches and methods both to check correctness and satisfiability of requirements for software as well as for check software for critical runtime defects and security vulnerabilities. Program analysis is one of the methods intended to assure software quality. The static and dynamic analysis tool industry has been evolving aggressively since the first decade of 2000^th. Nowadays there are many academic research and industrial tools for program analysis. But, due to fundamental limitations and engineering compromises for the sake of performance and scalability, static analysis tools cannot avoid false positive alarms. At the same time, reviewing static analysis tool alarms can take significant time of an experienced software engineer or a software quality assurance specialist. Hence, the task of automating refinement of static analysis tool results becomes more important. This survey covers approaches for static analysis tools result refinement. Approaches, which combine static and dynamic analysis of programs form the principal concern of this paper.

Currently, one of the most efficient ways to find software security problems is taint analysis. It can be based on static analysis and successfully detect errors that lead to vulnerabilities, such as code injection or leaks of private information. Several different ways exist for the implementation of the algorithm for the taint data propagation through the program intermediate representation: based on the dataflow analysis (IFDS) or symbolic execution. In this paper, we describe how to implement both approaches within the existing static analyzer infrastructure to find errors in C# programs, and compare these approaches in different aspects: the scope of application, practical completeness, results quality, performance and scalability. Since both approaches use a common infrastructure for accessing information about the program and are implemented by a single development team, the results of the comparison are significant and can be used to select the best option in the context of the task. Our experiments show that it’s possible to achieve the same completeness regardless of chosen approach. IFDS-based implementation has higher performance comparing with symbolic execution for detectors with small amount of taint data sources. In the case of multiple detectors and a large amount of sources the scalability of IFDS approach is worse than the scalability of symbolic execution.

The paper discusses the problem of network traffic classification: the characteristics that are used to solve it, existing approaches and their limitations. Applied tasks that require classification are listed, as well as additional requirements that arise from the main problem. Properties of network traffic that root in communication medium specifics are analyzed as well as the technology being used where they influence the classification process. Relevant directions in current approaches to analysis and the reasons for their development are discussed.

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.

JetOS is a prospective onboard real-time operating system (RTOS). Nowadays GosNIIAS develops JetOS in the scope of the research and development project. One of the most important tasks during JetOS development is to create the DO-178C certification kit, which will allow JetOS to be used for development and modification of avionics for civil aircraft. Today there is no operating system certified in accordance with DO-178C in Russia, therefore the JetOS creation is the matter of current importance. Using DO-178C requires the developer to have very strict development processes. The arrangement of processes that satisfy the DO-178C requirements is a very responsible and demanding task because of high expectations in the fields of safety and security. JetOS is being developed primarily for onboard equipment based on the integrated modular avionics (IMA). One of the key features of IMA is the ability to execute several functional applications on one target onboard module. The obvious consequence of this feature is a necessity to have a time and resource partitioning of applications. In avionics field application partition along with a host of other features is defined in ARINC 653 international standard, so its support is the significant requirement for JetOS. ARINC 653 defines application programming interface (API) and modes of operation for onboard functional software. JetOS supports the up-to-date version of ARINC 653 (2015) with supplementary services. JetOS also supports the safety-critical graphical library - OpenGL SC; the special implementation of the OpenGL SC library is being developed along with JetOS itself. OpenGL SC services are used to draw two-dimensional and three-dimensional pictures by onboard functional software. JetOS is a certifiable modular cyber-safe real-time operating system, which is designed in order to support several hardware architectures and to be easily adopted for different hardware boards. The scope of the JetOS project also includes creation of the tools necessary for functional software development, especially aircraft systems.

Data processing systems have been traditionally optimized for I/O, mainly because, until pretty recently, disk storage has been the most affordable type of storage and the most prevalent one. This is not necessarily the case today, particularly in the world of big data analytics. As the problems posed by data analytics become more commonplace, efficient CPU utilization becomes the new bottleneck. Just-in-time query compilation is a promising solution to this challenge that is currently being applied both in academic studies and across the industry. This paper is a survey of just-in-time query compilation methods sampled from the literature available on the subject. All methods are broadly categorized into expression compilation and hotspot methods, whole-query compilation methods, and specialization-based methods. A number of query processors are identified within confines of each category, various methods, architectures, and significant results are described. Finally, we conclude with an overview of most general approaches to query compilation that we identified.

In this paper, we consider the problem of finding large hidden clique in random graph and it’s analog for bipartite graphs.

In this paper, we continue our work that is devoted to the parallel composition of Timed Finite State Machines (TFSMs). We consider the composition of TFSMs with timeouts and output delays. We held experiments in order to estimate how often parallel composition of nondeterministic TFSMs (with and without timeouts) has infinite sets of output delays. To conduct these experiments we have created two tools: the first one for converting TFSMs into automata (this tool is integrated into BALM-II), the second one for converting the global automaton of the composition into TFSM. As it was suggested in earlier works, we describe the infinite sets of output delays by linear functions, and it is important to know how often these sets of linear functions appear to justify the importance of future investigations of the TFSM parallel compositions (especially for deriving cascade composition). Results of the experiments show significant amount (around 50 %) of TFSMs with infinite number of output delays. We also estimate the size of the global automaton and the composed TFSM. In the experiments, we do not consider global automata with the huge number of states (more then 10000).

Theory of scheduling and project planning is widely applied in diverse scientific and industrial areas. To effectively solve application-specific problems, it is necessary to state right objectives as well as to take into account a lot of factors, such as task execution models, precedence relationship between tasks, resource limitations, directive deadlines, working calendars, conditions for financial and logistics support of project tasks, specific spatio-temporal requirements, et al. Therefore, the development of scheduling applications becomes more and more complicated purposes, risky and costly ones. In this paper, we present an innovative object-oriented Scheduling Application Framework (SAF) designed to simplify and accelerate the software development processes. The presented SAF framework is a system of C++ classes that implement basic abstractions of the scheduling theory as well as provide ready-to-use components to build target applications of typical scheduling functionality. As a general-purpose mathematical library, the framework enables to set and solve so-called RCPSP problems (Resource-Constrained Project Scheduling Problem) in extended statements peculiar to popular project management systems. Branch and bound and linear dispatching algorithms have been implemented and included as a part of the framework. A dozen of heuristics has been implemented and has been provided by the framework too to solve large-scale problems more effectively. Thereby target application developers can adjust the application solver properly taking into account application-specific issues and making the search of suboptimum schedules more effective. As a software toolkit the framework enables developers to implement own components and to configure target applications in unified and flexible manner. Due to object-oriented paradigm, multi-layer architecture and class package organization, the application development takes relatively small efforts. The SAF framework has been successively validated during development of a software application intended for visual modeling and planning of projects under diverse spatial-temporal, resource and finance constraints. Due to achieved advantages, the framework looks promising for development of both sophisticated multi-disciplinary systems and effective domain-specific scheduling applications.