The information is prepared on the basis of data from the information-analytical system RSF, informative part is represented in the author's edition. All rights belong to the authors, the use or reprinting of materials is permitted only with the prior consent of the authors.

Project titleEvolution strategies for hard SAT-instances decomposition with application to cryptographic functions inversion.

Research area 01 - MATHEMATICS, INFORMATICS, AND SYSTEM SCIENCES, 01-201 - Artificial intelligence and decision-making

KeywordsArtificial Intelligence, cryptanalysis, cryptographic function inversion, Boolean Satisfiability (SAT), evolution algorithms, genetic algorithms, SAT-solver, SAT-partitioning

Annotation
The level of systems security and data communication protocols depends critically on the resistance of cryptographic algorithms used to protect these data. Due to a wide variety of approaches used for data protection, automatic methods are considered as the most valuable ones, which reasonably allow comparing resistance of different cryptographic algorithms. Such methods should be based on a combinatorial problem with powerful and well-developed algorithmics. A number of recent studies show that one of the most promising ones is the Boolean satisfiability problem (SAT). In this research it is planned to develop new methods for constructing decomposition representations of difficult instances of the Boolean satisfiability problem and to apply the developed algorithms to a number of cryptanalysis problems of modern ciphers. Specifically, it is expected that new algorithms based on evolutionary principles will be constructed, which will allow to find decomposition representations of SAT instances (so-called "SAT Partitioning") with a better estimate of the solution complexity than in the known methods. It should be emphasized that evolutionary algorithms will be used only on the decomposition step of difficult instances of the SAT problem, but not for the SAT formulae solving process itself. It is assumed that the developed algorithms for a number of ciphers will allow building new "guess-and-determine" attacks, which will be more effective than the known ones. It is planned to develop new SAT-solver parameterization strategies, which allow to use these solvers in SAT-based cryptanalysis problems. It is also planned to conduct a detailed analysis of possibilities of using evolutionary strategies for this purpose. The research actuality is based on the fact that cryptanalysis methods are an important part of the new encryption systems development. In recent years modern SAT solving algorithms were very successfully used in the cryptanalysis, which allows considering them as a basis for constructing a number of attacks on the known and developing cryptographic primitives and ciphers. Thus, such algorithms can be seemed as expert systems, giving resistance estimates of considered cryptographic structures. In the future, the most resistant structures can be used in the development of real ciphers. The scientific novelty of this study lies in the development of methods based on new principles, for constructing decomposition representations of difficult SAT instances. Also, new methods will be proposed for selecting optimal parameters of SAT-solvers for solving the considered SAT formulae class. It is assumed that the developed methods will allow building new, more efficient cryptographic attacks than the ones currently known. It is also proposed to use the developed methods for comparison of different cryptographic systems among themselves.

Expected results
Expected that during the project implementation new methods of constructing decomposition representations of Boolean formulas will be developed and implemented in the context of solving the Boolean satisfiability problem (SAT). Each such decomposition corresponds to some cryptographic attack that belongs to the guess-and-determine class. The novelty of developed algorithms is the use of evolutionary strategies for evaluating the effectiveness of a particular decomposition (and, as consequence, the complexity of corresponding "guess-and-determine" attack) through optimization of special evaluation functions of the black-box type. Relatively recent works demonstrate that using SAT in conjunction with black-box optimization allows creating record attacks of "guess-and-determine" class for a number of ciphers. It is assumed that the use of new evolutionary strategies will significantly improve these results. It is also assumed that software environment created in the scope of the project for testing the resistance of different cryptographic primitives to "guess-and-determine" attacks will be useful for developing new high-speed cryptographic algorithms. Developed and implemented algorithms for constructing "guess-and-determine" attacks will be tested on a number of cryptographic keystream generators (Bivium, Toy-Trivium, Trivium, Grain, etc.) in parallel and distributed computing environments.

Annotation of the results obtained in 2019
The second and the final stage of the project continues its work on the development of new methods for analyzing stream encryption algorithms based on evolutionary algorithms and SAT-solvers. 1. The evolutionary optimization algorithms for evaluating Monte-Carlo functions of black-box type that evaluate the effectiveness of SAT decompositions in SAT-based cryptanalysis tasks were significantly improved. The major improvement implies modification of the fitness function (FF) through the use of statistical tests. During the evaluation, the optimization algorithm checks a great number of SAT decompositions, the effectiveness of which is worse than the current solution. For such decompositions, it is possible to interrupt the calculations at the earlier stages of computing the FF, which is calculated iteratively and requires a large number of computational resources. To decide on the interruption, the current sample of the results of SAT-solvers launches is evaluated at each iteration using the Wilcoxon test. 2. The EvoGuess software framework (https://github.com/ctlab/EvoGuess) was implemented for cryptanalysis of streaming encryption algorithms to SAT-based attacks. This framework consists of four modules and includes previously developed methods and their improvements. It includes the possibility of using both parametrizable and non-parameterizable SAT solvers ROKK, Lingeling, Treengeling, MiniSat, CryptoMiniSAT, PaInleSS, Glucose, Maple, and Minicard. The framework is available at the public domain, and can be used both for cryptanalysis of encryption algorithms and for the implementation of similar research projects, involving the parallel solution of many SAT formulas during the process of optimization algorithm. 3. With the implemented EvoGuess framework, some experimental studies were conducted. It was confirmed that using statistical tests and parameterized SAT solvers in SAT cryptanalysis tasks was efficient. In this series of experiments, the algorithms of stream encryption A5/1, Bivium, Trivium-64 and Trivium-96 were investigated on five identical nodes of the Irkutsk computing cluster “Akademik V.M. Matrosov”. The obtained results showed that the developed improvements made it possible to use the same resources to consider at times a larger number of potential decomposition sets: by 4.31 times for A5/1; 1.48 times for Bivium; 2.56 times for Trivium-64 and 1.92 times for Trivium-96. There have been constructed new decomposition sets with the improved estimates. Based on the results of the second stage, a paper (doi.org/10.1145/3321707.3321847) was published in the proceedings of the GECCO 2019 conference (rank A), which is the most famous in the field of evolutionary computing. A paper describing the framework (doi.org/10.23919/MIPRO.2019.8757214) was published in the proceedings of the MIPRO conference. Several talks were given in Prague, Czech Republic; Opatija, Croatia; and at the Congress of Young Scientists in St. Petersburg (presentations are available on the personal page of the project’s lead http://rain.ifmo.ru/~ulyantsev/papers.html).

Publications

1. Pavlenko A., Buzdalov M., Ulyantsev V. Fitness Comparison by Statistical Testing in Construction of SAT-Based Guess-and-Determine Cryptographic Attacks GECCO 2019 - Proceedings of the 2019 Genetic and Evolutionary Computation Conference, ACM, P. 312-320 (year - 2019) https://doi.org/10.1145/3321707.3321847

2. Pavlenko A., Semenov A., Ulyantsev V., Zaikin O. Parallel framework for evolutionary black-box optimization with application to algebraic cryptanalysis 2019 42nd International Convention on Information and Communication Technology, Electronics and Microelectronics, MIPRO 2019 - Proceedings, IEEE, P. 1144-1149 (year - 2019) https://doi.org/10.23919/MIPRO.2019.8757214

3. - Ученые Университета ИТМО представили рекордное количество работ на конференции по эволюционным вычислениям GECCO-2019 в Праге ITMO.NEWS, - (year - )

Annotation of the results obtained in 2018
In modern information security, cryptographic methods takes one of the central roles. Expanding the scope of information security practices and the emergence of new threats leads to increasing the number of cryptographic structures. The problem of choosing a cipher to solve a specific problem on a specific type of device and platform becomes nontrivial. Thus, the problem of using intellectual methods to assess the strength of stream ciphers to various cryptographic attacks, compare the strength of various ciphers and finally choose the best cipher for a particular situation is relevant. This project aims to develop a new approach to estimate the cryptographic strength of a given stream cipher algorithm. The project develops (with active joint collaboration) the results of a research group led by A. Semenov in ISDCT SB RAS. In their recent works, the tasks of constructing attacks of a single class are reduced to the pseudo-Boolean black-box functions minimization problem. More accurately, defined in [Semenov et al. 2016, 2018] functions allow a comparative analysis of the strength of various ciphers to algebraic attacks, which related to the class of guess-and-determine and presented as a Boolean SAT-formula. In most cases, the search of guessed bits set is based on the manual analysis of the cipher features and the corresponding SAT-formula. In mentioned papers was proposed a method, in which decomposition search task is solved as the task of optimization problem for a special pseudo-Boolean black-box function. The values of this function stochastically estimate the complexity of the corresponding guess-and-determine attack. Previously Tabu Search and Simulated Annealing algorithms was used. In this project we apply evolutionary algorithms to search a guessed bit set. During the first year we achieved the next results. 1. New evolutionary algorithms (EA) to optimize black-box evaluation functions that evaluate the effectiveness of SAT-decomposition in SAT-based cryptanalysis tasks have been developed. After a series of preliminary studies, (1+1)-EA and a genetic algorithm (GA) with a population size of 10 were selected as strategies for directional search. The proposed modification of the fitness function (FF), called as an adaptive strategy, deserves special attention. At the initial stage of the algorithm launch, the smallest Monte Carlo sample size (М = 10) is used to calculate the FF. This significantly increases the algorithm’s speed at the initial stage, but leads to a loss of function accuracy. As we approach the local optimum, the sample size is gradually increased to M = 1000 to increase the FF calculation accuracy. 2. The developed algorithms are implemented as software applications that effectively work in parallel and distributed computing environments. Source codes and launchers are located in the open repository (https://github.com/lytr777/CryptoEv). The proposed algorithms were implemented as a parallel MPI program for a computing cluster. Our software was successfully used on ITMO University cluster and the cluster "Akademik V.М. Matrosov" (Irkutsk). 3. Experiments with developed algorithms have been performed. Detailed results are presented in the paper “Evolutionary Computation Techniques for Constructing SAT-Based Attacks in Algebraic Cryptanalysis”. Each experiment was conducted on 180 cores of a computing cluster equipped with Intel Xeon E5-2695 processors. The duration of one experiment was 12 hours. Using our algorithms we constructed new guess-and-determine attacks for four keystream ciphers. As a result, the proceedings paper (https://link.springer.com/chapter/10.1007/978-3-030-16692-2_16) have been published in LNCS EvoStar 2019 proceedings. A talk was given in Leipzig, Germany (the presentation and a poster are available online (http://rain.ifmo.ru/~ulyantsev/papers.html). However, from our point of view, we have only touched the potential of evolutionary computation in this area.

Publications

1. Pavlenko A., Semenov A., Ulyantsev V. Evolutionary Computation Techniques for Constructing SAT-Based Attacks in Algebraic Cryptanalysis Applications of Evolutionary Computation. EvoApplications 2019. Lecture Notes in Computer Science, Vol. 11454, P. 237-253 (year - 2019) https://doi.org/10.1007/978-3-030-16692-2_16