Introduction

The most detailed provisions of the similarity theory were developed concerning the processes, described by the homogeneous power polynomial systems [1,3]. There are three main theorems in the similarity theory: the direct, inverse, and π-theorem. The similarity theorem, known as "π-theorem", allows identifying the functional relationship between variable processes in relative form. The deductions form the direct theorem and the "π-theorem" of similarity allowed formulating invariant informative fea-Introducing a passport system for programs

Let us consider two processes of p1 and p2, which complete equations have the following form:

, u = 1, 2, …, r;

, u = 1, 2, …, r;

Where and -homogeneous functions of their parameters. The direct similarity theorem states that if the processes are homogeneously similar, then the following system takes place: ,

u = 1,2, …, r; s = 1,2, …, (q-1).

Expressions ,

u = 1,2, …, r; s = 1,2, …, (q-1)

are called criteria or similarity invariants and, as a theorem deduction, are numerically equal to all processes belonging to the same subclass of mutually similar processes.

Thus, the direct theorem formulates the necessary conditions for the correlation of the analyzed process with one of the subclasses. Sufficient conditions for the homogeneous similarity of two processes are given in the inverse similarity theorem: if it is possible to reduce the complete processes equations to an isostructural relative form with the numerically equal similarity invariants, then such processes are homogeneously similar [6,7].

The similarity theorem, known as "π-theorem", allows identifying the functional relationship between variable processes in relative form. The deductions form the direct theorem and the "π-theorem" of similarity allowed formulating invariant informative features for the correct behavior of some critical information infrastructure software [9,11].

   q 1 i ui 0     q 1 i ui 0 Ф    n 1 j j u 1 u x      n 1 j j u 1 u X Ф  uq ui uq ui Ф Ф    uq ui us    

3

Mathematical problem formulation

Imagine the computational process (СP) in the following form ((5), table 1):

CP=<T,X,Y,Z,F,Ф>

Table 1. Mathematical problem formulation of a computational process 1 T The set of times t at which a computational process is observed 2 X, Y Sets of input and output parameters of the computational process 3 Z Set of states of the computing process. Every state of the computational process is characterized at each moment of time by the sequence of arithmetic operations at the selected control point k.

F

The set of transition operators fi, reflecting the mechanism of changing the states of the computing process during its execution, including arithmetic operations 5 Ф The set of output operators фi, describing the mechanism of the formation of the result during the calculation We introduce the following notation: λ -Violation mapping of an arithmetic operation at a specific time ti for given input parameters;

ψ -Mapping of the computational process regular invariants formation; μ -Comparative mapping of standard and reference invariants of the computational process; υ -Mapping of the signal generation about incorrect calculations; ξ -Mapping of the arithmetic operations recovery, based on reference similarity invariants;

χ -Performed calculation correctness mapping, based on the recovered arithmetic operations.

In order to exclude the possibility of discreet modification, made by the calculation program, it is necessary to perform dynamic control of the executed computational process (Figure 1). Under the dynamic control of the computational program correctness, we will understand the correctness control of the performed arithmetic operations semantics, while their actual execution. Data for dynamic control must first be obtained as a program passport, resulting from its additional static analysis [8,10]. In order to form the passport program the following actions are required:

1. Solving the observative problem (the computational process simulation by an oriented program control graph). 2. Solving the problem of presenting calculations by similarity equations on linear graph parts, i.e. to transform the arithmetic operations of the form:

To dimensionless form:

1. Solving the problem of managing the computational process by comparing the semantic invariants with the program passport that means that it is necessary to find the maps:

ψ: Z'→П' μ: П'→П(8)2 1 2 1 m il m ij x x x z x x x z  p , 1 l , j 

Solving these problems allowed developing a new method to control the computational program semantic correctness, which complemented the known method capabilities to ensure the required cyber resilience of the secured critical information infrastructure [9,12].

In order to control the software correctness, it was necessary to construct a program control graph.

Let us imagine some computational process in the form of a program control graph: G(B.D).

Where B = {Bi}is set of vertices (linear program part and D = {BxB} set of arcs (control connections) between them.

Here, each linear graph part has its own arithmetic operator sequence, i.e.

An ordered vertex sequence corresponds to each elementary (without cycles) route of the graph input vertex to output vertex:

where and form a sequence of the executed arithmetic operators called a program implementation or a computational process. The arithmetic expression sequence data is the potentially dangerous program fragments.

The computational process algorithm was reduced to the graph representation form to derive the arithmetic expression operators from the control operators (conditional transitions, branching, cycles). As a result, in the control graph, all arithmetic expression operators were grouped on a set of linear program partsthe graph vertices, into which checkpoints (CP) were entered. Here, checkpoints were needed to determine the routing context within which the calculations take place. Moreover, the special systems of defining relations were constructed in the form of similarity equations at each checkpoint for arithmetic operators. The equation system solution allowed to form the matrices of similarity invariants to control the computational process semantics.

A similarity equations system development

The studies have shown that the most effective way to control the computation semantics is to test relations, based on theoretically based relations and computation features. Here the key relationships in the approach for detecting the parameters of the incorrect computational process functioning are some invariant, which is understood as the auto modeling (constant) presentation of program execution in the actual operating secured infrastructure conditions. The invariant generation problem, from the different program representations, is non-trivial and poorly formalized. In the program execution dynamics, only semantic invariants remain fully computable (repro-

B B i  ). ,..., , ( 2 1 il i i i b b b B  ), ,..., , ( 2 1 k t k k k B B B B  B B k  ), ,..., , ( 2 1 k il k i k i k i b b b B  p i , 1  

ducible) (since they do not depend on the specific values of the program variables) [7,13].

Let us imagine the implementation of B k of the program control graph as an ordered primary relation sequence, corresponding to arithmetic operators: (11) Having performed the superposition {yi} on X on the right relation sides, we obtain a relation invariant system according to the displacement: (12) The relation can be presented as: (13) where -a power monomial. In accordance with the Fourier rule, the summands (13) should be homogeneous in dimensions, i.e.

[yi] = [ ] = [ ],

or

[ ] = [ ],(14)

System ( 16) is a defining relations system or a similarity equation system.

Using the function ρ = X→[X], we associate each with some abstract dimension . Then the summand dimensions (13) will be expressed as

, (15)            ) y ,..., y , y , x ,..., x , x ( f y ... ), y , x ,..., x , x ( f y ), x ,..., x , x ( f y 1 M 2 1 N 2 1 k M M 1 N 2 1 k 2 2 N 2 1 k 1 1           ).1 ij i    ) x ,..., x , x ( z N 2 1 ij ) x ,..., x , x ( z N 2 1 ij ) x ,..., x , x ( z N 2 1 il i p , 1 l , j  ) x ,..., x , x ( z N 2 1 ij ) x ,..., x , x ( z N 2 1 il i p , 1 l , j  X x j      X x j      jn N 1 n n n 2 1 ij x x ,..., x , x ( z     i p , 1 j  164

Using ( 14) and (15), we develop a system of defining relations:

(16) which is transformed into the following form:

(17)

Using the logarithm method, as it is usually done, when analyzing the similarity relations we obtain a homogeneous system of linear equations from the system (17)

, (18)

Expression ( 16) is a criterion for semantic correctness.

Having performed a similar development for , we obtain a system of homogeneous linear equations for k-implementation:

А к ω = 0 (19)

Generally, we can assume that the function ρ = X→[X] is surjective and, therefore, the B k implementation is represented by a matrix of size mk × nk, which a number of columns are not less than the number of rows, i.e. . We say that the implementation of B k is representative if it corresponds to the matrix А k with , i.e. the implementation allows developing at least one similarity criterion.

Usually, a program corresponds to a separate functional module or consists of an interconnected group of those and describes the general solution of a certain task. Each of the implementations describes a particular solution of the same problem, corresponding to the certain X components values. Since then the mathematical dependencies structure should be preserved during the transition from one implementation to another, i.e. similarity criteria should be common. Then the matrices {A k }, corresponding to the implementations {B k }, can be combined into one system.

Let the program have q implementations. Denote by A the union of the matrices {A k } corresponding to the implementations {B k }, i.e.

(20)

    , x x ln jn N 1 n n N 1 n n        i p , 1 l , j    , 1 x ln jn N 1 n n       i p , 1 l , j        N n n n l n j x 1 0 ] ln[   i p , 1 l , j  k k i B B   ij k a A  k k m n  1 m k  B B k     l k B B B B , B l k              q 1 A ... A A 165

The A Development can be carried out using selective vertices covering the implementations.

Thus, the matrices A union is part of the program passport and is a database of semantic standards {A k } for the linear program {B k } sections.

The similarity equation example.

Let us consider an assignment operator:

p = a*b + c/(d-e)(21)

Here, the correct expression must be generated by some selected grammar, which depends on both the possible terms meanings and the chosen operations set. For a context-free grammar, each expression can be matched to an output tree in a unique way. Thus, an output tree can be used as an alternative expression representation.

When constructing a tree by the expression, the order of the calculations plays its role. Obviously, the vertex descendant values are calculated earlier than the ancestor vertex value. Therefore, the operation last performed will take place at the treetop. In order to construct a tree unambiguously, it is necessary to determine the operation calculation order in the expression, taking into account their priorities and the operation order with the same priority, including the case when calculating the same operation (associativity property). Usually, such expressions are calculated from left to right.

Fig. 2. Arithmetic expression generation tree

The constructed tree will definitely correspond to the specified expression taking into account the calculation order.

We formalize the arithmetic expressions: Let Op {+,-,*,/} be an arithmetic operations set under consideration.

Terms is a set of terms, consisting of possible objects that can be operation arguments.

Expr is a set of all possible expressions, and .

-many other elements, and . Thus, an arithmetic expression is either a term or an operation connecting several expressions.

The expression (20) with the set of terms Terms = {p,a,b,c,d,e} and the binary operations set Op {,-,*,/} will be represented as: elem: (=,p,(,(*,a,b),(/,c,(-,d,e)))).

The arithmetic operator execution correctness can be assessed using the appropriate semantic function. When applied to expressions, the semantic function assigns to each argument some abstract entity or dimension [a]. Thus, the arithmetic operations, performed on program variables during the program execution are in fact operations on physical dimensions, and the semantics reflections, performed at runtime, are linear mappings. The axiomatic of extended semantic algebra, which defines operations on the variable dimensions, is presented in Table 2. 1 [P] -1 = 1 0 1 -1 where Rthe operation result; L, Rleft and right operands; [ ]dimension.

[L] = [P] [R] 0 [L] 1 [P] -1 = 1 0 1 -1 Subtraction R = L -P [L] = [P] [R] 0 [L] 1 [P] -1 = 1 0 1 -1 Multiplication R = L * P [R] = [L][P] [R] 1 [L] -1 [P] -1 = 1 1 -1 -1 Division R = L / P [R] = [L][P] -1 [R] 1 [L] -1 [P] 1 = 1 1 -1 1 Exponentiation R = L s [R] = [L] s [R] 1 [L] -s [P] 0 = 1 1 -s 0 Assignment L = P [L] = [P] [R] 0 [L]

For a correctly running program in the context of this operator, the following relations between the physical dimensions of the terms {p, a,b,c,d,e} should be fulfilled:

[p] = [a * b] = [a][b], [d] = [e], [p] = [c / (d-e)] = [c][d] −1 = [c][e] −1 ,(22)

Where [X]is a physical object X dimension. a starting symbol. The terminal symbols include arithmetic coprocessor command lexical tokens, including addition, subtraction, multiplication, division, assignment (data transfer) commands. A non-terminal symbol set is a set of lexical tokens, united by a generalizing feature, as well as their combinations, using products. An example of nonterminal symbols is given in the Table 3. The output rule represented by expression (21) determines the use of the "fadd" command. Thus, we will present all possible inference rules in assembly language.

Expr

(24)

Where Addition -a non-terminal set of coprocessor addition commands; Register -a non-terminal set of coprocessor stack registers; Address -a memory identifier set or actual memory addresses. Each output in a context-free grammar, starting with a non-terminal symbol, is uniquely associated with a directed graph, which is a tree and is called an output (parse) tree. An output tree example related to the disassembled expression code, as well as its representation as to the similarity equations in terms of the dimension theory, is shown in figure 3.

 , S , R , N , G     register ... address , t tan cons , identifier     e Appropriat Division tion Multiplica n Subtractio Addition N , , , ,    DivCommand ..., , MulCommand SubCommand , AddCommand R    S N    ...

Fig. 3. Calculations representation by similarity equations

The solution to this equation system is a similarity coefficient matrix, constructed as follows:

[ebp+p] = [ebp+a][ebp+b] [ebp+d] = [ebp+e] [ebp+p] = [ebp+c][ebp+d]- 1=[ebp+c][ebp+e]-1 [ebp+p]1[ebp+a]-1[ebp+b]- 1[ebp+c]0[ebp+d]0[ebp+e]0=1 [ebp+p]0[ebp+a]0[ebp+b]0[ebp+c]0[ebp+d]1 [ebp+e]-1=1 [ebp+p]0[ebp+a]0[ebp+b]0[ebp+c]- 1[ebp+d]1[ebp+e]0=1  169

By taking a logarithm we obtain a homogeneous linear equation system with a coefficients matrix:

(25)

In order to organize the similarity relations development, it is necessary to construct a translation grammar for assignment operators of the arithmetic type. The translational (attribute) grammar in addition to the syntax allows describing the action characters, which are implemented as functions, procedures, and algorithms. According to dimensions, these functions should implement algorithmic calculations and the similarity relation development, power monomials, equations and solutions.

Thus, the observation problem solution (control graph) and the computations representation (similarity equation) made it possible to form the image of a system for monitoring destructive software actions on the secured infrastructure, and restoring computation processes based on similarity invariants.

The plan of destructive software impacts control and the computational processes recovery includes preparatory and main stages (Figure 4). The preparatory stage includes the program passport formation in similarity invariants, the main ones are the stages of: A general representation of the information infrastructure that implements correct calculations under the hidden intruder program actions is reflected in Figure 5. We will reveal the stages of the destructive software impacts control and the computation processes recovery in more detail. At the stage of a static verification using the disassembled correct calculation code, the program control graph is constructed.

At each checkpoint for each arithmetic operator, a production tree of an arithmetic expression is generated to develop a linear homogeneous equation system in the dimension terms. The result of solving the equation systems for each linear program part is a similarity invariant matrix. The semantic standard database is made up of reference matrices of similarity invariants for each checkpoint (Figure 6). The similarity invariants formation of the computational process, which is subjected to the hidden arithmetic operations impacts, runs according to the same algorithm as the computational process reference invariant formation.

For a given program, a set of checkpoints (CT) is formed, which are embedded in the studied program. The initial program model is the control graph of the computation process in terms of linear program sections. The similarity equations are analyzed and a coefficient matrix is developed in embedded CT for each linear program section, where the calculations take place (Figure 7). Incorrect calculations will differ in the state set of the computational process Z, i.e. in arithmetic operator sequence. The incorrect calculations scheme is presented in Figure 8. At this stage, the similarity invariant matrices constructed for each checkpoint form a similarity invariants database. The scheme of adding matrices to the database is presented in Figure 9. In order to control the semantic correctness of the performed calculations, it is necessary to check the semantic correctness criterion by the formula (18) applying the reference and standard invariants matrix (Figure 9).

If the validation of this checkpoint has been completed, then proceed to check the criteria in the next CT until the program ends.

Stage 5. The signal generation of the computation semantics violation and the partial calculations recovery according to the program passport.

If the semantic correctness violation of the program execution is detected, that is, if for a given checkpoint , then a signal is formed and an attempt is made to recover the calculations from the inverse transformation of the reference matrix invariants (Figure 10).