Topic: SAT solving, или майнинг "наоборот" (Read 1468 times)

Solving Circuit Optimisation Problems in Cryptography and Cryptanalysis

Nicolas T. Courtois, Daniel Hulme and Theodosis Mourouzis

Abstract: One of the hardest problems in computer science is the problem of gate-eficient implementation. Such optimizations are particularly important in industrial hardware implementations of standard cryptographic algorithms. In this paper we focus on optimizing some small circuits such as S-boxes in cryptographic algorithms. We consider the notion of Multiplicative Complexity studied in 2008 by Boyar and Peralta and applied to find interesting optimizations for the S-box of the AES cipher. We applied this methodology to produce a compact implementation of several ciphers. In this short paper we report our results on PRESENT and GOST, two block ciphers known for their exceptionally low hardware cost. This kind of representation seems to be very promising in implementations aiming at preventing side channel attacks on cryptographic chips such as DPA. More importantly, we postulate that this kind of minimality is also an important and interesting tool in cryptanalysis.

Нормальные герои всегда идут в обход (c) Есть способ косвенно применить SAT-сольверы к майнингу, расскажу, но сначала - почему идти в лобовую атаку не надо. Одна из задач, на которых тренируют SAT - разложение на простые множители, из умножения двух длинных чисел и произведения генерируется система булевских уравнений, если произведением взять простое число - получается UNSAT задача. Это известный метод, никакого секрета тут нет, поэтому когда сольверы начнут всерьёз участвовать в RSA Challenge, только тогда и можно будет воспринимать их всерьёз как инструмент для майнинга, а сейчас ещё рано.

smolen, ура, наконец-то нашелся человек который хотя бы понимает о чем речь 

да я понимаю, что при наличии сложения в каждом раунде SAT-солвер против нашей задачи "в лоб" будет малоэффективен, иначе грош цена всем SHA2 вместе взятым 
но когда мы накладываем биткойновые ограничения, начинают закрадываться сомнения, а вдруг при низком target много нулей в нем дадут внятное преимущество против тупого брут-форса. и алгоритмы SAT кстати тоже разные бывают, и настройки тоже у них есть разные. Heusser показал что выигрыш в скорости только от настроек может достигать 500-1000%.

я аналогично плаваю сейчас в области домыслов и спекуляций, но кмк пора уже переводить эксперимент в практическое русло.
даже если результат будет отрицательным, это все равно результат. тем более что классический майнинг уже выоптимизирован дальше некуда, и нужно искать альтернативный подход.
к сожалению, пока моих познаний в этой области для реальной работы недостаточно, поэтому и создал тему для обмена опытом.

OZR, мы говорим не об изменении PoW, а о решении текущей задачи PoW (двойной SHA256 от заголовка блока+nonce < target) способом, отличным от повсеместно используемого, а именно брут-форса nonce.

Майнинг - способ обеспечения транзакций. Т.е должен соответствовать трём параметрам.

- Отсутствие возможности (теоретической) взлома.
- Скорость.
- Экономичность.

А что конкретно считать разницы нет. В чём конкретно преимущество данного метода?

----
У BTC

- PoW - в ближайшее время достигнет таких масштабов, на SHA-256. Что перебить его будет нереально почти никому. Для особо хитропопых увеличиться сложность настолько, что не взять даже 20% сети. Не то что 51%. Мы даже децентрализации достигнем. Будет 99% производителей чипов и 1% частных майнеров на всю сеть. Т.к сложность будет уже астрономическая. Каждый производитель будет работать на взаимовыгодных условиях с каким-либо конкретным регионом. Либо с конкретными частниками.

- Скорость очень даже приемлемая. (хотя лично я уже не раз сталкивался, когда перевод идёт больше суток, иногда это критично, хотя ничего страшного, привыкнут). Уменьшать время. На самом деле серьёзный вопрос в стабильности и безопасности. А потянет ли?

- Экономичность страдает. Не одна тонна железа и захламление окружающей среды. Но тут опять же спорно. Это в разы меньше затрат, нежели тратит нынешняя денежная система.

Забавно, но до сих пор выходит, что биткойн почти идеален. Мне нравится PoW, как концепт. Точно так же, как и PoS. (опять же не 100% PoS). Хотя PoS решает проблему 51% и экономичности. Это не нужно, 51% возьмётся в лоб, бараньим методом. Экономичность же вырастит не сильно.

Т.е реально, какие глобальные преимущества? Я их не вижу. Просто решать другую задачу ради фана?

А так ли нужен майнинг вообще? Это ведь всего лишь концепт.

Напрямую применить SAT-сольвер малореально, дело не только в размере функции (~120000 уравнений в базисе XOR/AND, ~80000 после фиксирования всего ввода, кроме 32 переменных nonce. После перехода в базис AND/OR, "родной" для сольверов,  будет ещё хуже), но и в её высоте, слишком много цепочек сложения.
Наверху при текущей сложности 64 уравнения, внизу - 32 свободные переменные, если позволить времени блока гулять часа три - 32+13. Примерно посередине, там где стыкуются два SHA-256, находится узкий "пояс" из 256 переменных, он сдвигается к началу после элиминации констант. Средняя ширина - 768 переменных. При таком раскладе ожидаю, что конфликт, найденный наверху не дойдёт вниз даже до "пояса" и сольвер будет работать как тупой переборщик. Это всё спекуляции и предположения, никак руки не дойдут попробовать на деле.
Вот тут Killerstorm пытался начать обсуждение, но заглохло.

Я не понял что чему противостоит ) ну или о чем ты раздумываешь.

тебя вынудят купить аккаунты

Вот еще вариант:

Сферических (в вакууме). 

Троянских коней?  

по теме есть что сказать, или твой заплечный унитаз только говно сливать и умеет? 

оппа, скамерок, тебя ещё не забанили? 

довольно давно раздумываю над этим подходом, почитал работы Jonathan Heusser, в целом внутренний голос подсказывает что SHA2 все же достаточно хорош чтобы противостоять SAT.

ссылки:

SAT solving
Proof of concept code
педивикия
дискуссия на reddit

основная идея - заменить традиционный brute-force майнинг (перебором возможных nonce) на обратную задачу: поиск с помощью SAT значения недетерменированной переменной nonce при которой условие sha256(sha256(block+nonce)) > target НЕ выполняется.
при этом открывается простор для оптимизации, кроме того, как ни парадоксально, чем выше сложность тем проще будет поиск (в теории), т.к. в детерменированной части выражения target будет больше нулей.

ну и еще идея на закуску - формирование структуры SAT solver-а средствами FPGA.
т.е. мы сначала медленно "запрягаем" формируя из исходных данных булевое выражение, затем загружаем его в FPGA и быстро "едем" решаем его получая на выходе ответ НЕТ  и искомый nonce или, увы, ответ ДА, не выполняется  

если у кого есть мысли на этот счет прошу высказываться.