Как Sha256 може да бъде редуциран до SAT?

[electroweakk]

Здравейте, искам да попитам, дали някой е наясно как Sha256 може да бъде редуциран до SAT? Постоянно попадам в нета на специалисти, които говорят, че това е възможно, но не виждам как може да се случи това.

[mnogoznaiko]

Какво е Sha256 и какво е SAT?

[scaner]

Преди 30 минути, electroweakk said:

Здравейте, искам да попитам, дали някой е наясно как Sha256 може да бъде редуциран до SAT? Постоянно попадам в нета на специалисти, които говорят, че това е възможно, но не виждам как може да се случи това.

Попитай ChatGPT.

Ето какво казва тя на въпроса дали може да се направи такава редукция (може да попиташ и за алгоритъм):

---------

Редуцирането на SHA-256 хеш функция до SAT (Boolean Satisfiability Problem) е предизвикателен процес, който изисква изразяването на алгоритъма на SHA-256 като логическа формула от булеви променливи. Ето основните стъпки за извършване на това:

---

1. Разбиране на SHA-256

SHA-256 е криптографска хеш функция, която работи по следния начин:

• Входът (съобщението) се обработва в блокове от 512 бита.
• Всеки блок преминава през редица операции, включително побитови ротации, побитови XOR, AND и OR операции, както и математически операции като добавяне по модул $2^{32}$.
• Изходът е фиксиран хеш от 256 бита.

---

2. Булеви променливи

За да преобразувате SHA-256 в SAT:

• Разделете всеки бит от входа, вътрешните променливи и изхода на отделна булева променлива.
• Например, ако входното съобщение е 512-битово, ще имате поне 512 булеви променливи, плюс допълнителни за вътрешните стойности и крайния хеш.

---

3. Изразяване на операциите в булеви формули

SHA-256 използва операции, които трябва да бъдат изразени като булеви формули:

• AND: $a \land b$ остава директно.
• OR: $a \lor b$ остава директно.
• XOR: $a \oplus b$ може да бъде изразено като $(a \lor b) \land \neg(a \land b)$.
• NOT: $\neg a$ остава директно.
• Ротации и побитови операции: Тези операции трябва да бъдат описани с комбинация от логически променливи, представляващи позициите на битовете.
• Добавяне по модул $2^{32}$: Това е по-сложно и изисква булеви вериги, описващи сумата, като се включват и преносите на битове.

---

4. Добавяне на ограниченията

След като всички операции на SHA-256 са описани като булеви формули:

• Формулирайте входните ограничения, като зададете конкретни булеви стойности за входното съобщение.
• Определете очаквания изход (хеш) като булеви формули, които са свързани с вътрешните променливи.

---

5. Формулиране като SAT проблем

Целта е да се генерира логическа формула, която да е удовлетворима (satisfiable), ако и само ако съществува вход, който води до желания изходен хеш:

• Булевата формула трябва да обхваща всички логически зависимости между входа, вътрешните стойности и изхода.
• Например, ако искате да "обръщате" SHA-256 (да намерите вход, който дава конкретен хеш), формулата ще включва този хеш като изходна стойност.

---

6. Практически аспекти

• SAT Solver: След като формулата бъде изградена, тя може да бъде предадена на SAT solver (например MiniSAT, Glucose, или Z3) за решаване.
• Оптимизация: Размерът на формулата може да бъде огромен, тъй като SHA-256 използва сложни операции. Могат да се използват техники за оптимизация, за да се намали броят на булевите променливи и клаузи.

---

Примерна ситуация

Ако искате да намерите сблъсък (collision) или да обърнете хеша (да намерите вход за даден изход):

1. Дефинирайте формулата на SHA-256 като булеви ограничения.
2. Добавете условия за изходния хеш.
3. Нека SAT solver търси вход, който удовлетворява формулата.

---

Предизвикателства

• Мащаб: SHA-256 е сложен алгоритъм, което означава, че SAT формулата може да има милиони булеви променливи и клаузи.
• Изчислителна сложност: Намаляването на сложността изисква специфични оптимизации и симплификации.

SHA-256 може успешно да бъде редуциран до SAT, но това изисква прецизно моделиране и мощни изчислителни ресурси.

[electroweakk]

Аз търся реална практика, където можеш да видиш как се прави. Тук има някви стъпки, но не е ясно какво се случва. Пък не се зн дали е редовно това дето снася.

[gmladenov]

Преди 2 минути, electroweakk said:

Аз търся реална практика, където можеш да видиш как се прави.

По каквото чета, принципно е възможно, но не е практично. Затова никъде не намириш реална
практика. Явно никой не е успял да го направи.

[scaner]

Преди 4 минути, electroweakk said:

Аз търся реална практика, където можеш да видиш как се прави. Тук има някви стъпки, но не е ясно какво се случва. Пък не се зн дали е редовно това дето снася.

Ами попитай ИИ за примерен алгоритъм на съответния език. Бълва много неща, не са за тука, ще задръстим форума.

Формулирай си ясно въпроса, и е добре да ползваш платената версия, макар че и безплатната е доста словоохотлива. И в диалог ще си изясниш напълно всичко. Програмирането вече до това се свежда.

[gmladenov]

Преди 5 минути, electroweakk said:

Аз търся реална практика, където можеш да видиш как се прави.

Нещо друго: ако някой успее да измисли надеждно редуциране на sha256 до SAT - и това стане
обществено достояние - тоагва sha256 ще трябва да бъде изоставен и да се потърси алтернатива.
Щом това не се е случило, значи засега никой не измислил надеждно редуциране (или поне не го
е обявил).

[scaner]

Преди 1 минута, gmladenov said:

Нещо друго: ако някой успее да измисли надеждно редуциране на sha256 до SAT - и това стане
обществено достояние - тоагва sha256 ще трябва да бъде изоставен и да се потърси алтернатива.
Щом това не се е случило, значи засега никой не измислил надеждно редуциране (или поне не го
е обявил).

Има надеждни методи за редуциране. Просто те изискват много голяма изчислителна мощност. Затова и се ползват тези алгоритми, обръщането им струва много повече от сметките в права посока.

А сега като дойдат квантовите компютри, тези кодове ще умрат. И биткойните също Само стой и гледай катастрофата тогава...