Akceleracja obliczeń kryptograficznych z wykorzystaniem procesorów GPU

• Autorzy: Bęza P. , Gocławski J. , Mral P. , Sapiecha P.

Warianty tytułu

EN

Acceleration of cryptographic calculations using GPUS

• Języki publikacji: PL

Abstrakty

PL

Problem spełnialności formuł rachunku zdań SAT jest jednym z fundamentalnych oraz otwartych zadań we współczesnej informatyce. Jest on problemem NP-zupełnym. To znaczy, że wszystkie problemy z klasy NP możemy sprowadzić do problemu SAT w czasie wielomianowym. Co ciekawe, wśród problemów z klasy NP istnieje wiele takich, które są ściśle związanych z kryptologią, na przykład: faktoryzacja liczb – ważna dla RSA, łamanie kluczy szyfrów symetrycznych, znajdowanie kolizji funkcji skrótu i wiele innych. Odkrycie wielomianowego algorytmu dla SAT skutkowałoby rozwiązaniem problemu milenijnego: P vs. NP. Cel ten wydaje się bardzo trudny do osiągnięcia – nie wiadomo nawet czy jest możliwy. Mając nieco mniejsze aspiracje możemy projektować algorytmy heurystyczne lub losowe dla SAT. W związku z tym, głównym celem autorów pracy jest przedstawienie projektu równoległego SAT Solvera bazującego na algorytmie WalkSAT, w tym procesu jego implementacji z wykorzystaniem środowiska programistycznego OpenCL oraz komputera wyposażonego w karty graficzne NVIDIA Tesla. Wraz z dynamicznym rozwojem technologii procesorów typu GPU oraz układów FPGA, jak również przenośnością rozwiązań stworzonych w Open CL, kierunek takich prac staje się interesujący ze względu na uzyskiwaną efektywność obliczeniową, jak również szybkość prototypowania rozwiązań.

EN

The Boolean satisfiability problem SAT is one of the fundamental and open tasks in present-day information science. This problem is NP-complete. It means that all NP problems can be reduced to SAT in polynomial time. Interestingly, among NP problems, there are many closely related to cryptology, for example: factorization of numbers – important for RSA, breaking keys of symmetric ciphers, finding collisions of hash functions and many others. The discovery of the polynomial algorithm for SAT would result in resolving one of Millennium Prize Problems: P vs. NP. This objective seems to be hard to achieve – it’s unknown if it is even possible. With slightly lower aspirations, we can design heuristic or random algorithms for SAT. Therefore, the main goal of our study is to present a project of parallel SAT Solver based on WalkSAT algorithm, including its implementation using the OpenCL programming environment and a computer equipped with NVIDIA Tesla graphics cards. With the rapid development of GPU technology and FPGAs, as well as portability of solutions created in OpenCL, the direction of such works becomes interesting because of computational efficiency gained, as well as solution prototyping rate.

Słowa kluczowe

PL

spełnialność; formuły logiczne; SAT Solver; WalkSAT; karta graficzna; kryptoanaliza; OpenC; obliczenia równoległe

EN

satisfiability; SAT Solver; WalkSAT; graphics processing unit; cryptoanalysis; OpenCL; parallel computing

• Wydawca: Wojskowa Akademia Techniczna im. Jarosława Dąbrowskiego
• Czasopismo: Studia Bezpieczeństwa Narodowego
• Rocznik: 2014
• Tom: R. 4, Nr 6
• Strony: 341--357
• Opis fizyczny: Bibliogr. 30 poz., schem., tab.

Twórcy

autor

Bęza P.

• Politechnika Warszawska, Wydział Matematyki i Nauk Informacyjnych

autor

Gocławski J.

• Politechnika Warszawska, Wydział Matematyki i Nauk Informacyjnych

autor

Mral P.

• Politechnika Warszawska, Wydział Matematyki i Nauk Informacyjnych

autor

Sapiecha P.

• Politechnika Warszawska, Wydział Elektroniki i Technik Informacyjnych

Bibliografia

• [1] T. Eibach, E. Pilz, and G. Völkel, Attacking Bivium Using SAT Solvers, University of Ulm, Institute of Theoretical Computer Science http://www.uni-ulm.de/fileadmin/website_uni_ulm/iui.inst.190/Mitarbeiter/eibach/Attacking-Bivium-Using-SAT-Solvers.pdf, 01.02.2014.
• [2] M. Luisier, A. Schenk, IEEE TRANSACTIONS ON ELECTRON DEVICES, http://www.iis.ee.ethz.ch/schenk/04495122.pdf, 24.04.2014.
• [3] S. Anthony, 7nm, 5nm, 3nm: The new materials and transistors that will take us to the limits of Moores law, http://www.extremetech.com/computing/162376-7nm-5nm-3nm-the-new-materials-and-transistors-that-will-take-us-to-the-limits-of-moores-law, 24.04.2014.
• [4] NVIDIA Website, http://www.nvidia.pl/object/cuda-parallel-computing-pl.html, 24.04.2014.
• [5] SAT Competition, Strona internetowa konkursu SAT Competition, http://www.satcompetition.org/, 01.05.2014.
• [6] N. Een, N. Sörensson, An Extensible SAT-solver, [W:] SAT, pod red. Enrico Giunchiglia, Armando Tacchella, Springer, 2003, s. 502–518.
• [7] C. F. Madigan, S. Malik, M. W. Moskewicz, L. Zhang, Y. Zhao, Chaff: Engineering an Efficient SAT Solver, 39th Design Automation Conference (DAC 2001), ACM, 2001.
• [8] Glucose, The Glucose SAT Solver. http://www.labri.fr/perso/lsimon/glucose/, 17.04.2014.
• [9] WalkSAT, WalkSAT Home Page, http://www.cs.rochester.edu/u/kautz/walksat/, 17.04.2014.
• [10] H. H. Hoos, D. A. D. Tompkins, Novelty+ and Adaptive Novelty+, https://cs.uwaterloo.ca/dtompkin/papers/satcomp04-novp.pdf, University of British Columbia, 2004.
• [11] H. Deleau, Ch. Jaillet, M. Krajecki, GPU4SAT: solving the SAT problem on GPU, CReSTIC SysCom, Universitae de Reims Champagne-Ardenne, 2008.
• [12] V. W. Marek, Introduction to Mathematics of Satisfiability, CRC Press, 2008.
• [13] G. V. Bard, Algorithms for Solving Linear and Polynomial Systems of Equations over Finite Fields with Applications to Cryptanalysis, Rozprawa doktorska, 2007.
• [14] S. Cook, The complexity of theorem proving procedures, Proceedings of the Third Annual ACM Symposium on Theory of Computing, 1971, s. 151–158.
• [15] W. Chrabakh, R. Wolski, GrADSAT: A Parallel SAT Solver for the Grid, University of California Santa Barbara, 2003.
• [16] D.N. Pham, C. Gretton, gNovelty+ (v.2) [W:] Solver description, SAT competition, 2009.
• [17] Y. Hamadi, S. Jabbour, L. Sais, ManySAT: A Parallel SAT Solver, Journal on Satisfiability, Boolean Modeling and Computation, JSAT 6, 2009, s. 245–262
• [18] A. Roli, Criticality and Parallelism in Structured SAT Instances, [W:] CP’02. Volume 2470 of LNCS., pod red. P. V. Hentenryck, 2002, s.714–719.
• [19] Instytut Matematyczny Claya http://www.claymath.org/millennium, 07.05.2014.
• [20] top500.org, Titan – Cray XK7 , Opteron 6274 16C 2.200GHz, Cray Gemini interconnect, NVIDIA K20x, http://www.top500.org/system/177975, 05.02.2014.
• [21] top500.org, Oak Ridge Claims No. 1 Position on Latest TOP500 List with Titan, http://www.top500.org/blog/lists/2012/11/press-release/, 05.02.2014.
• [22] amazon.com, http://www.amazon.com/nVidia-K20X-NVIDIA-Tesla/dp/B00CX35KU2, 28.04.2014.
• [23] Oak Ridge Computing Facility, https://www.olcf.ornl.gov/support/, 24.04.2014.
• [24] computer store – newegg.com, http://www.newegg.com/Product/Product.aspx?Item= N82E16814132015, 24.04.2014.
• [25] Texas Advanced Computing Center, https://www.tacc.utexas.edu/news/press-releases/2013/tacc-to-deploy-maverick, 28.04.2014.
• [26] M. Vörös, Algebraic attack on stream ciphers, praca magisterska, Bratislava, 2007.
• [27] Khronos Group – OpenCL, http://www.khronos.org/opencl/, 28.04.2014.
• [28] CUDA Examples, http://www.nvidia.pl/object/gpu-computing-applications-pl.html, 28.04.2014.
• [29] VirtualCL, http://www.mosix.org/txt vcl.html/, 28.04.2014.
• [30] Timo Stich, OpenCL on NVIDIA GPUs, http://sa09.idav.ucdavis.edu/docs/SA09_NVIDIA_IHV_talk.pdf, 09.02.2014.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2021).