DOI: https://doi.org/10.26089/NumMet.v20r106

Дубликаты конфликтных ограничений в CDCL-выводе и их использование в задачах обращения некоторых криптографических функций

Авторы

  • В.С. Кондратьев
  • А.А. Семенов
  • О.С. Заикин

Ключевые слова:

задача о булевой выполнимости (SAT)
алгоритм CDCL
конфликтные дизъюнкты
криптографические хеш-функции

Аннотация

Изучен феномен повторного порождения конфликтных ограничений SAT-решателями в процессе работы с трудными экземплярами задачи о булевой выполнимости. Данный феномен является следствием применения эвристических механизмов чистки конфликтных баз, которые реализованы во всех современных SAT-решателях, основанных на алгоритме CDCL (Conflict Driven Clause Learning). Описана новая техника, которая позволяет отслеживать повторно порождаемые дизъюнкты и запрещать их последующее удаление. На базе предложенных технических решений построен новый многопоточный SAT-решатель (SAT, SATisfiability), который на ряде SAT-задач, кодирующих обращение криптографических хеш-функций, существенно превзошел по эффективности многопоточные решатели, занимавшие в последние годы высокие места на специализированных соревнованиях.

Новые вычислительные технологии

Загрузки

Опубликован

2019-02-24

Выпуск

Том 20 (2019): Выпуск 1.

Раздел

Раздел 1. Вычислительные методы и приложения

Авторы

В.С. Кондратьев

Иркутский национальный исследовательский технический университет
ул. Лермонтова 83, 664074, Иркутск
• магистрант

А.А. Семенов

Институт динамики систем и теории управления имени В.М. Матросова СО РАН (ИДСТУ СО РАН)
ул. Лермонтова, 134, 664033, Иркутск
• заведующий лабораторией

О.С. Заикин

Институт динамики систем и теории управления имени В.М. Матросова СО РАН (ИДСТУ СО РАН)
ул. Лермонтова, 134, 664033, Иркутск
• старший научный сотрудник

Библиографические ссылки

  1. S. A. Cook, “The Complexity of Theorem-Proving Procedures,” in Proc. 3rd Annu. ACM Symp. on Theory of Computing, Shaker Heights, USA, May 3-5, 1971 (ACM Press, New York, 1971), pp. 151-158.
  2. L. A. Levin, “Universal Sequential Search Problems,” Probl. Peredachi Inf. 9 (3), 115-116 (1973) [Problems Inform. Transmission 9 (3), 265-266 (1973)].
  3. J. P. Marques-Silva and K. A. Sakallah, “GRASP: A Search Algorithm for Propositional Satisfiability,” IEEE Trans. Comput. 48 (5), 506-521 (1999).
  4. J. Marques-Silva, I. Lynce, and S. Malik, “Conflict-Driven Clause Learning SAT Solvers,” in Handbook of Satisfiability (IOS Press, Amsterdam, 2009), pp. 131-153.
  5. B. Selman, H. A. Kautz, and B. Cohen, “Noise Strategies for Improving Local Search,” in Proc. 12th National Conf. on Artificial Intelligence (AAAI’94), Seattle, USA, July 31-August 4, 1994 (MIT Press, Cambridge, 1994), pp. 337-343.
  6. U. Schöning, “A Probabilistic Algorithm for k-SAT and Constraint Satisfaction Problems,” in Proc. 40th Annual Symp. on Foundations of Computer Science, New York, USA, October 17-19, 1999 (IEEE Press, Washington, DC, 1999), pp. 410-414.
  7. M. J. H. Heule and H. van Maaren, “Look-Ahead Based SAT Solvers,” in Handbook of Satisfiability (IOS Press, Amsterdam, 2009), pp. 155-184.
  8. M. J. H. Heule, O. Kullmann, S. Wieringa, and A. Biere, “Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads,” in Lecture Notes in Computer Science (Springer, Heidelberg, 2011), Vol. 7261, pp. 50-65.
  9. M. J. H. Heule, O. Kullmann, and V. W. Marek, “Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer,” in Lecture Notes in Computer Science (Springer, Heidelberg, 2016), Vol. 9710, pp. 228-245.
  10. I. Mironov and L. Zhang, “Applications of SAT Solvers to Cryptanalysis of Hash Functions,” in Lecture Notes in Computer Science (Springer, Heidelberg, 2006), Vol. 4121, pp. 102-115.
  11. A. Semenov, O. Zaikin, D. Bespalov, and M. Posypkin, “Parallel Logical Cryptanalysis of the Generator A5/1 in BNB-Grid System,” in Lecture Notes in Computer Science (Springer, Heidelberg, 2011), Vol. 6873, pp. 473-483.
  12. E. Mendelson, Introduction to Mathematical Logic (Van Nostrand, Princeton, 1964; Nauka, Moscow, 1971).
  13. S. V. Yablonskii, Introduction to Discrete Mathematics (Nauka, Moscow, 1986) [in Russian].
  14. M. R. Garey and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness (Freeman, New York, 1979; Mir, Moscow, 1982).
  15. A. Biere, M. Heule, H. van Maaren, and T. Walsh, Handbook of Satisfiability (IOS Press, Amsterdam, 2009).
  16. A. Biere, “Bounded Model Checking,” in Handbook of Satisfiability (IOS Press, Amsterdam, 2009), pp. 457-481.
  17. D. Kröning, “Software Verification,” in Handbook of Satisfiability (IOS Press, Amsterdam, 2009), pp. 505-532.
  18. I. Lynce and J. Marques-Silva, “SAT in Bioinformatics: Making the Case with Haplotype Inference,” in Lecture Notes in Computer Science (Springer, Heidelberg, 2006), Vol. 4121, pp. 136-141.
  19. S. Kochemazov and A. Semenov, “Using Synchronous Boolean Networks to Model Several Phenomena of Collective Behavior,” PLoS ONE 9 (2014).
    doi 10.1371/journal.pone.0115156
  20. H. Zhang, “Combinatorial Designs by SAT Solvers,” in Handbook of Satisfiability (IOS Press, Amsterdam, 2009), pp. 533-568.
  21. G. V. Bard, Algebraic Cryptanalysis (Springer, Berlin, 2009).
  22. T. Gendrullis, M. Novotný, and A. Rupp, “A Real-World Attack Breaking A5/1 within Hours,” in Lecture Notes in Computer Science (Springer, Heidelberg, 2008), Vol. 5154, pp. 266-282.
  23. M. A. Posypkin, O. S. Zaikin, D. V. Bespalov, and A. A. Semenov, “Solving the Cryptanalysis Problems for Stream Ciphers in Distributed Computing Environments,” Tr. Inst. Sistem. Analiza, No. 46, 119-137 (2009).
  24. K. Nohl, “Attacking Phone Privacy,”
    https://media.blackhat.com/bh-us-10/whitepapers/Nohl/BlackHat-USA-2010-Nohl-Attacking.Phone.
    Privacy-wp.pdf . Cited February 15, 2019.
  25. V. Bulavintsev, A. Semenov, O. Zaikin, and S. Kochemazov, “A Bitslice Implementation of Anderson’s Attack on A5/1,” Open Eng. 8 (1), 7-16 (2018).
  26. J. C. King, “Symbolic Execution and Program Testing,” Commun. ACM 19 (7), 385-394 (1976).
  27. L. Erkök and J. Matthews, “Pragmatic Equivalence and Safety Checking in Cryptol,” in Proc. 3rd Workshop on Programming Languages Meets Program Verification, Savannah, USA, January 20, 2009 (ACM Press, New York, 2009), pp. 73-82.
  28. L. Erkök, M. Carlsson, and A. Wick, “Hardware/Software Co-Verification of Cryptographic Algorithms Using Cryptol,” in Proc. 9th Int. Conf. on Formal Methods in Computer-Aided Design, Austin, USA, November 15-18, 2009 (IEEE Press, New York, 2009), pp. 188-191.
  29. P. Janicic, “URSA: A System for Uniform Reduction to SAT,” Log. Meth. Comput. Sci. 8 (3), 1-39 (2012).
  30. I. V. Otpushchennikov and A. A. Semenov, “Technology for Translating Combinatorial Problems into Boolean Equations,” Prikl. Diskr. Mat., No. 1, 96-115 (2011).
  31. I. Otpuschennikov, A. Semenov, I. Gribanova, et al., “Encoding Cryptographic Functions to SAT Using TRANSALG System,” in Frontiers in Artificial Intelligence and Applications (IOS Press, Amsterdam, 2016), Vol. 285, 1594-1595.
  32. M. Davis and H. Putnam, “A Computing Procedure for Quantification Theory,” J. ACM 7 (3), 201-215 (1960).
  33. M. Davis, G. Logemann, and D. Loveland, “A Machine Program for Theorem-Proving,” Commun. ACM 5 (7), 394-397 (1962).
  34. J. P. Marques-Silva and K. A. Sakallah, “GRASP - a New Search Algorithm for Satisfiability,” in Proc. 1996 IEEE/ACM Int. Con. on Computer-Aided Design, San Jose, USA, November 10-14, 1996 (IEEE Press, Piscataway, 1996), pp. 220-227.
  35. M. W. Moskewicz, C. F. Madigan, Y. Zhao, et al., “Chaff: Engineering an Efficient SAT Solver,” in Proc. 38th Annual Design Automation Conference, Las Vegas, USA, June 22-22, 2001 (IEEE Press, New York, 2001), pp. 530-535.
  36. L. Zhang, C. F. Madigan, M. H. Moskewicz, and S. Malik, “Efficient Conflict Driven Learning in a Boolean Satisfiability Solver,” in Proc. 2001 IEEE/ACM Int. Conf. on Computer-Aided Design, San Jose, USA, November 4-8, 2001 (IEEE Press, Piscataway, 2001), pp. 279-285.
  37. N. Eén and N. Sörensson, “An Extensible SAT-Solver,” in Lecture Notes in Computer Science (Springer, Heidelberg, 2004), Vol. 2919, pp. 502-518.
  38. G. Audemard and L. Simon, “Predicting Learnt Clauses Quality in Modern SAT Solvers,” in Proc. 21st Int. Joint Conf. on Artificial Intelligence. Pasadena, USA, July 11-17, 2009 (Morgan Kaufmann, San Francisco, 2009), pp. 399-404.
  39. W. F. Dowling and J. H. Gallier, “Linear-Time Algorithms for Testing the Satisfiability of Propositional Horn Formulae,” J. Logic Programm. 1 (3), 267-284 (1984).
  40. J. H. Liang, V. Ganesh, P. Poupart, and K. Czarnecki, “Learning Rate Based Branching Heuristic for SAT Solvers,” in Lecture Notes in Computer Science (Springer, Heidelberg, 2016), Vol. 9710, pp. 123-140.
  41. S. A. Cook and R. A. Reckhow, “The Relative Efficiency of Propositional Proof Systems,” J. Symbolic Logic 44 (1), 36-50 (1979).
  42. A. Haken, “The Intractability of Resolution,” Theor. Comp. Sci. 39, 297-308 (1985).
  43. P. Beame, H. Kautz, and A. Sabharwal, “Understanding the Power of Clause Learning,” in Proc. 18th Int. Joint Conf. on Artificial Intelligence. Acapulco, Mexico, August 9-15, 2003 (Morgan Kaufmann, San Francisco, 2003), pp. 1194-1201.
  44. A. E. J. Hyv854rinen, Grid Based Propositional Satisfiability Solving , Ph.D. Thesis (Aalto Univ., Aalto, 2011).
  45. O. Zaikin, “A Parallel SAT Solving Algorithm Based on Improved Handling of Conflict Clauses,” Procedia Comput. Sci. 119, 103-111 (2017).
  46. S. Nejati, Z. Newsham, J. Scott, et al., “A Propagation Rate Based Splitting Heuristic for Divide-and-Conquer Solvers,” in Lecture Notes in Computer Science (Springer, Heidelberg, 2017), Vol. 10491, pp. 251-260.
  47. S. Nejati, J. H. Liang, C. Gebotys, et al., “Adaptive Restart and CEGAR-Based Solver for Inverting Cryptographic Hash Functions,” in Lecture Notes in Computer Science (Springer, Heidelberg, 2017), Vol. 10712, pp. 120-131.
  48. X. Wang and H. Yu, “How to Break MD5 and Other Hash Functions,” in Lecture Notes in Computer Science (Springer, Heidelberg, 2005), Vol. 3494, pp. 19-35.
  49. I. A. Bogachkova, O. S. Zaikin, S. E. Kochemazov, et al., “Problems of Search for Collisions of Cryptographic Hash Functions of the MD Family as Variants of Boolean Satisfiability Problem,” Vychisl. Metody Programm. 16, 61-77 (2015).
  50. A. Biere, “CaDiCaL, Lingeling, Plingeling, Treengeling and YalSAT Entering the SAT Competition 2017,”
    http://fmv.jku.at/papers/Biere-SAT-Competition-2017-solvers.pdf . Cited February 15, 2019.
  51. L. Le Frioux, S. Baarir, J. Sopena, and F. Kordon, “PaInleSS: A Framework for Parallel SAT Solving,” in Lecture Notes in Computer Science (Springer, Heidelberg, 2017), Vol. 10491, pp. 233-250.
  52. Irkutsk Supercomputing Center, Siberian Branch of the Russian Academy of Sciences.
    http://hpc.icc.ru . Cited February 15, 2019.