- The article presents the development of the concept of cyber immunity to protect the Industry 4.0 critical information infrastructure and the theory of self-healing machine computing. The specified theory is based on the results of the scientific-applied sections of biological and cybernetic immunology. In the developed concept it was taken into account that the neutralization of malicious influences should not lead to a denial of service for the entire system and to a loss of the functional semantics of calculations. Using interrelated probative, verification and testing programming, a model for restoring functional program specifications was developed. It was developed with separation by levels: semantic (functional, logical and algebraic models are defined to determine the base of functionally-logic specifications of programs); syntactic (defined models to form automatic machines for the detection and neutralization of malicious influences); semantically syntactic (models are defined for applying the simplest forms of program calculation semantics based on graphical, schematic, and network representations). In order to prove the correctness of functional semantics of the "cleared" calculations, a mathematical apparatus of the similarity theory and calculation dimensions were developed. The п-converter was identified; this operator allows forming the required "passports" of trusted computations in the conditions of disturbances. Calculations with "antibodies" are represented by regular schemes in the system of algorithmic algebras of V. M. Glushkov. A semantically controlled translator based on formal automata with abstract memory was developed for the interpretation of the input program of the trusted computations and type of actions.
A fundamental contribution to the formation and development of the theoretical and system programming was made by the outstanding scientists from all over the world: A. • • • • • • •
However, in order to protect the critical information
infrastructure of the Industry 4.0 in the face of increasing threats
to information security, it was necessary to define the concept of
cyber immunity and develop a new theory of self-healing
machine computing [
Including under conditions of a priori uncertainty and obfuscation of programs (Figure 3).
In the mentioned theory, by analogy with classical immunology (Figure 1, Figure 2), the antigen is understood to be some destructive program code, and the antibody is a synthesized metaprogram of this code neutralization. Model of immune protection of Industry 4.0 describes the causal relationship between "antigens" and "antibodies". That is, between vulnerabilities and program defects (manifested in the form of structural violations), modes of functioning (distorting the properties of programs), security incidents, caused by the destructive program tabs (changing the given standard algorithms of calculations) and metaprograms for their neutralization.
Immune protection of Industry 4.0 includes three key subsystems: Recognizer, Planner and Executor. Here, the Recognizer is designed to recognize patterns (images) of malicious code by its structural, correlation and invariants features. The scheduler is intended for planning, i.e. creation of corresponding plans and metaprograms of malicious code neutralization. The executor is intended for execution of the specified plans and metaprograms. As a result of these three subsystems operation, the required "purification" and formation of a trusted environment for calculations in the conditions of heterogeneous mass cyber-attacks by malefactors takes place.
Whereas the classical immunology neutralizes antigens by
physically destroying them (absorbing them), this is
unacceptable in cybernetic immunology. As far as the loss of a
part of the functional program code can lead to denial of service
and impossibility to continue calculations as a whole. That is
why it was demanded that the functional semantics of
calculations during the neutralization of malicious influences be
invariable (constant) [
Taking into account the requirements set forth above, we present the main goals of the organization of self-recovering trusted computations C1, C2 and C3 by the following display 0 ÷ 6 system (Figure 4).
In order to reach these goals, a number of research objectives were achieved. In particular, the model of restoration of functional program specifications in the ideology of interrelated probative, verification and testing programming has been developed (Figure 4). Here, the probative programming allowed us to study the correctness of computational structures, correctness of computability properties and stability of calculations. These aspects were modelled by denotation, axiomatic and operational formal semantics of programs, respectively.
Thus for an establishment of conformity between their functionally-logic specifications and physical design the methods of annotated programs of N. Wirth, Ch. Hoare and E. Dixtra were involved.
In order to solve the specific problems of restoring the
functional specifications of programs, a corresponding model
basis was developed (Figure 5) [
Here, the level classification was made by analogy with the classification of formal languages by N. Khomsky. In the semantic class we chose models suitable for the construction of calculations, in the syntactic class we chose models that allow us to form automatic machines for the detection and neutralization of malicious influences. The class of semanticsyntactic models has allowed operating with the simplest forms of program calculation semantics in an effective basis of models types of graphical, schematic and network representation (Figure 6). At the same time, the control flow graph (CFG), Yanov schemata and Petri nets were chosen to specify the model basis.
As a result, the following architecture of the neutralization
system of malware and malicious software bookmarks was
proposed (Figure 7) [
In order to prove the correctness of functional semantics of the "cleared" calculations, a mathematical apparatus of the similarity theory and calculation dimensions were developed. In particular, the direct similarity theorem, which allows establishing the general scheme of representation of semantically correct calculations in the invariant (dimensionless) form, is formulated and proved ( 11 0 , 22 0 , … , 0 , П1 , П2 , … , П −1 = 0, where 1 , 2 , … , 0 - similarity invariants of calculations. 1 0 2 0
The direct similarity theorem allowed proving the statements about the necessary and sufficient similarity conditions of semantically correct calculations ( +1) = 1(П11, … , П( 1−1); 1 0 1 , … , 0) ⎧ ( +1) 0 ⎪ ( +2) = 2(П12, … , П( 2−1); 1 0 1 , … , 0) ⎨ ( +2) 0 ⎪ = (П1 , … , П( −1); 1 0 1 , … , 0) ⎩ 0 where П1 = 1 ⁄ 1 , П2 = 2 ⁄ 2 , … , П −1 = ⁄ similarity invariants, - multipliers of similarity ratios transformation, - functions of all or some relative data.
For the assignment operator A ≔ B ∗ C + DE + 1, the following relations must be performed between the abstract dimensions of the parameters (A, B, C, D, E, CONST_1): (1) (2) (3) (1) ∗ [ ] + (−1) ∗ [ ] + (−1) ∗ [ ] = 0, (1) ∗ [ ] + (−1) ∗ [ ] + (1) ∗ [ ] = 0, (1) ∗ [ ]1 + (−1) ∗ [ 1]1 = 0.
The received relations allow defining unequivocally the standard (or passport) of semantically correct calculation. The calculation is semantically correct if the corresponding system of dimension equations has at least one component consisting of all non-zero components among the set of vectors-solutions.
Let us suppose that this is not the case, and among these parameters there appeared a parameter identically equal to zero at any values of other parameters. This indicates that the new parameter is dimensionless. However, it is impossible because it contradicts the initial condition of semantic correctness of calculations, which was to be proved.
Also, a п-converter was identified; this operator allows forming the required "passports" of trusted computations in the conditions of disturbances.
Statement 1: Operator F is a п-converter if for each object ∈ and each element ∈ of the finite abelian subgroup the ratio of = ∗ −1, = 1, 2, … , (4)
Let F is п-converter and F* is corresponding mapping in the subgroup .
Let us assume that the objects to be compared are equivalent. ∗ is true.
Then
= , = 1, 2, … , or in terms of mapping ∗ = ∗ , = 1, 2, … , Apply now to the left and right parts of this equality the ∗ ( )−1, ∗ ( )−1 ∗ = = ∗ ( )−1 ∗ = , = 1, 2, … , based on the property of the existence of the group unit ∗ ( )−1 ∗ = , = 1, 2, … , multiplying on the left by ∗ ( ), get
∗ = ∗ , = 1, 2, … , multiplying on the right −1, find the required ratio ∗
= ∗ −1, = 1, 2, … ,
As a result, the following conclusions can be drawn: - п-converter is a mapping of a reference pair - Set of standards M0 represents a set of objects (similarity invariants), which do not change values of their information signs under the action of п-converter F, i.e.
- With the help of п-converter F and the corresponding mapping :
→ 0
= , ∗: → (5) (6) (7) (8) (9) (10) (11) (12) (13)
one can find the transformation g, which connects two equivalent objects 1 and 2so that = ( 2)−1 ( 1).
It is essential that a multi-model approach was proposed
solving the task of synthesizing programs of trusted
computations which allowes describing abstract programs of the
trusted computations in structural-functional, logical-semantic
and computational-operational aspects [
When choosing a meta-modeling apparatus, preference was given to the system of algorithmic algebras (SAA) proposed by academician V. M. Glushkov. This made it possible to create an algorithmic system equivalent in its visual capabilities to such classical algorithmic systems as Turing machines, Post products and Markov algorithms. Besides, the advantage of SAA is the possibility to express structures of abstract programs of trusted calculations in a strict basis of Dijkstra types (sequence, branching, cycle) in the form of corresponding algebraic formulas. This allowed developing a multi-faceted algebraic system of the form < , > with a signature of operations ∆, where A is a set of operators; L is a set of logical conditions taking values from a set of {true, false, uncertain}. Here, the signature ∆= ∆1 ∪ ∆2consists of a system of ∆1 logical operations that take on a value in a variety of conditions L and a system of ∆2 operations that take on values in a variety of operators A.
In SAA < , > the system of forming ∐ is fixed. It is the final functionally complete set of operators and logical conditions. With the help of this set and by means of superposition of operations included in ∆, arbitrary operators and logical conditions of the set A and L are generated. The logical operations of the system ∆1 include generalized Boolean operations of disjunctions, conjunctions, and negation, as well as the operation of left multiplication of the condition by the operator = and filtration. The following operations belong to the ∆2 set: composition of operators ∗ , sequential execution of operators A and L, α - disjunction of operators, alternative execution of operators A and L, i.e.
( ∨ ) = ̀ , = 1; ( ∨ ) = , = 0; ( ∨ ) = J , = . (14)
Here, the α-iteration of operator A under the condition { } consists in checking the condition α, if this condition is false, then the execution of operator A is performed.
It should be noted that such a representation < , > allows developing effective regularization procedures (reduction to a regular scheme (RS)) (∐) and prove the theorem, which defines the principal possibility of a formal description of an arbitrary and reconstructed algorithm and procedure of trusted calculations in RS.
Thus, it is possible to formally describe the declarative, technological and procedural knowledge of trusted computations in the form of regular schemes.
Statement 2. Calculations with "antibodies" are represented by regular schemes in the system of algorithmic algebras (SAA) of V. M. Glushkov.
The modified technique of a composite programming allowed determining the effective sequence of operations of trusted calculations. For each operator's construction there were given operations and operands that make up the program of trusted calculations. After checking the completeness of this program for compliance with the selected criteria, an executable program of trusted calculations was synthesized (Figure 8).
A semantically controlled translator based on formal automata with abstract memory (AAM) was developed for the interpretation of the input program of the trusted computations and type of actions (Figure 9). The AAM consists of four elastic belts (EB), which contain: • • •
Neutralization and countermeasures scenarios; • Information messages of the broadcast procedures’ completion.
The following significant results have been obtained in the course of the concept development. Theoretical results: 1. Scientific-methodological apparatus of computer immunology of cyber-security based on the mechanisms of "immune response" and "immune memory" of classical immunology.
2. Methodology of self-recovery of trusted machine calculations with the required functional semantics of calculations.
• • • •
Approach to deobfuscation and normalization of logical structures of calculations using a system of equivalent transformations of Janov's schemes.
Method of combined verification of semantics of calculations on the basis of similarity invariants and provocative load testing.
Methods of generating trusted program algorithms on the basis of synthesis of calculations in the system of algorithmic algebra and scenarios of permits.
Computer immunology technology for cybersecurity and private methods of detecting and neutralizing destructive software bookmarks and program vulnerabilities. [7] Biryukov D.N, Rostovtsev Yu.G. Approach to constructing a consistent theory of synthesis of scenarios of anticipatory behavior in a conflict // Proceedings of SPIIRAS. - 2015. - Issue. 1 (38). - P. 94-111. DOI: http://dx.doi.org/10.15622/sp.38.6