Всем привет!

Какие подходы существуют для решения следующей задачи:

a * b + c - d = 0x2fa5
e ^ f - g = 0x6c
h + j - k = 0x63
z * x + v + n + m = 0x314a
q + w + r = 0x14d
w ^ h ^ k * g = 0x2e05
c + a + x = 0x143
m ^ d * q - 0x31 * v = 0x1ff
e ^ r + n = 0xb7
f * b - j ^ z = 0x325f
c + x - h = 0x5d
m ^ e - z + q + 0x31 = 0xb4
w * g - n - f + k = 0x36d1
j * v - d = 0xffffd9be
a ^ b - r = 0xffffff90
f ^ j - k * m + a = 0xffffd8c3
0x31 * h - v ^ r * e = 0x898
c ^ z ^ d + q = 0xdb
w + b = 0xe3
n * g - x = 0x30e6

где буквы предположительно принимают значения от 0x30 до 0x39.

| Сообщение посчитали полезным:

Во-первых, задачу надо бы уточнить, а то нихера не ясно.
Мне кажется, переменных сильно дофига.

Во-вторых, я бы сказал, что задача удобна для перебора.
Можно заметить, что старшие биты во всех вычислениях не влияют на младшие.
Например, можно решить задачу для 4 младших бит перебором, потом зафиксировать их и перебрать еще 4 бита постарше, и решение для младших бит при этом "не испортится".

Например, если бы нам нужно было перебрать одно 32-битное значение, то сложность перебора была бы (32/4)*2^4 вместо 2^32, что дофига меньше.

Чтобы такого не было, умные люди вставляют в шифры sbox-ы и перемешивание бит.

| Сообщение посчитали полезным:

gggeorggge
--> Методы_решения_систем_уравнений <-- + брут?

-----
От многой мудрости много скорби, и умножающий знание умножает печаль

| Сообщение посчитали полезным:

Использовать x в уравнении и в записи чисел - это просто гениально.

| Сообщение посчитали полезным:

kunix пишет:

Во-первых, задачу надо бы уточнить, а то нихера не ясно.
Мне кажется, переменных сильно дофига
[i]kunix пишет:

Буквы это печатные символы. Этими уравнениями, как я понимаю, проверяется 19 символьная строка.

| Сообщение посчитали полезным:

kunix пишет:
Мне кажется, переменных сильно дофига.

Ну, получит, значит, множество решений.



| Сообщение посчитали полезным:

Ну короче, если 19 переменных, то по 4 бита перебирать затратно.
Перебираете по 1 биту все 19 переменных, начиная с младшего.
То есть, сначала перебор a{0}...z{0}.
Если нашли подходящие, фиксируем, и рекурсивно переходим к перебору a{1}...z{1}.
В противном случае - return на предыдущий шаг перебора.
И так далее, пока рекурсивно не переберем a{7}...z{7}.
На самом деле, только до a{3}...z{3} надо, остальное типа уже известно.

Можно запилить фреймворк для общего решения задач подобного вида.
Задал формулки текстом - получил решение.

| Сообщение посчитали полезным:

Я конечно не шибко математик, но на многочлен больше похоже с несколькими неизвестными - возможно суть сводится к подстановке и решению матрицы методом Крамера или Гаусса.
Единственный вопрос, примеру:
v ^ r
j ^ z
Буквы r и z в 0x30 (48 степени) сложно представить при целочисленном вычислении. Может оно как-то сокращается или числа там не более 5.

| Сообщение посчитали полезным:

kunix пишет:
Мне кажется, переменных сильно дофига.

Наоборот, избыточное число уравнений. Переменных 18, а уравнений 20.


gggeorggge пишет:
где буквы предположительно принимают значения от 0x30 до 0x39

Исходя из уравнения j * v - d = 0xffffd9be слабо верится (если уравнения записаны без ошибок).
0xffffd9be наверняка в дополнительном коде -0x2642 и тогда произведение двух значений и вычитание третьего в этом диапазоне врядли даст такой результат.

По другим уравнениям тоже есть вопросы, например
q + w + r = 0x14d (3*0x39 = 0xab)
ну и т.д.

SMT solver Z3 решения не находит.

-----
127.0.0.1, sweet 127.0.0.1

| Сообщение посчитали полезным:

OKOB пишет:
j * v - d = 0xffffd9be слабо верится
Значит там явно разброс шире, чем цифры 0-9 или ошибка в уравнениях

| Сообщение посчитали полезным:

ELF_7719116 пишет:
Значит там явно разброс шире, чем цифры 0-9 или ошибка в уравнениях
Я пробовал 8-битные и 32-битные значения для переменных, без задания диапазона.

ЗЫ: ^ - брал как xor, а не как power.

-----
127.0.0.1, sweet 127.0.0.1

| Сообщение посчитали полезным:

gggeorggge, Проверяйте уравнения. Как минимум, нужно расставить скобки.
Мой побитовый солвер дальше 0 бита решения не видит в вашей системе.

Хотя вот подобную хуету решает сходу:
0x34F8FD3D == a * b + c;
0x129D3A06 == (a - c) ^ b;
0x404B8F9A == a ^ b ^ c + a*b*c;

OKOB, можете в Z3 проверить мою системку? Все вычисления unsigned 32-bit. Интересно сравнить...

| Сообщение посчитали полезным:

sat
[b = 180, a = 147, c = 225]

не увидел про 32-битные
sat
[b = 3959353012, a = 3177889939, c = 3288787937]

тоже будет коллизия
s.add(a != 3177889939)

sat
[b = 889005009, a = 3740983034, c = 3097150755]

s.add(a != 3177889939)
s.add(a != 3740983034)
unsat

-----
127.0.0.1, sweet 127.0.0.1

| Сообщение посчитали полезным:

Ваша система уравнений имеет 2 решения для 8битных значений
[147, 180, 225]
[250, 209, 35]

а так же z3 выдаёт 2 и для 32битных
[3177889939, 3959353012, 3288787937]
[3740983034, 889005009, 3097150755]



PS C:\Users\PC\Desktop> python sol.py
3177889939 3959353012 3288787937
3740983034 889005009 3097150755
--- 0.12 second(s) && 2 answer(s) ---

| Сообщение посчитали полезным:

Хех, а он хорош, этот Z3 Я думал, намного хуже будет это все...
Ладно, вот мой говносолвер, для истории.
Писал на коленке, сильно не пинать...



6b4a_19.06.2018_EXELAB.rU.tgz - solver19vars.cpp

| Сообщение посчитали полезным: RevCred

ELF_7719116 пишет:
возможно суть сводится к подстановке и решению матрицы методом Крамера или Гаусса.

Уравнения нелинейные.

Только перебор.



| Сообщение посчитали полезным:

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

-----
vx

| Сообщение посчитали полезным:

kunix пишет:
Ладно, вот мой говносолвер, для истории.
Писал на коленке, сильно не пинать...

kunix пишет:
и решение для младших бит при этом "не испортится".
переписал ваш солвер на Rust с использованием 128битных векторов, получил такие результаты для вашей системы из трёх уравнений.

https://pastebin.com/raw/9C2HSfxi

если вкратце - то видно побайтовый подбор, и работает очень шустро: 1_000_000 итераций сделал по 2 мс;
три 128битные числа за 2 мс!!!)
буду тестировать дальше.

| Сообщение посчитали полезным:

Ну солвер норм работет для такого примитивного алгоритма.
Однако, если уравнение неудачное, можно заставить его перебрать очень много вариантов, полное пространство.
Вы бы свою задачу решали

| Сообщение посчитали полезным:

OKOB пишет:
Я пробовал 8-битные и 32-битные значения для переменных, без задания диапазона.

ЗЫ: ^ - брал как xor, а не как power.

^ - Это xor. А разве Z3 позволяет перебрать 19 переменных за приемлемое время?

| Сообщение посчитали полезным:

gggeorggge пишет:
А разве Z3 позволяет перебрать 19 переменных за приемлемое время?
как показывает мой опыт - и не только 19 переменных.
вот какой-то скрипт c какого-то цтф - https://pastebin.com/9ZvCftqU - 31 переменная.

PS C:\!CTF> python re300_z3.py
MSKCTF_R34LLY_TR1CKY_C0ND1T1ON5
--- 0.41 second(s) ---

или ещё один таск, где 45 переменных

PS C:\!CTF> python YSNP_solver.py
VolgaCTF{D1$guis3_y0ur_code_and_y0u_@re_s@fe}
--- 1.33 second(s) && 1 answer(s) ---

правда раз пробовал решить самописную криптографию, получилось 200+ уравнений, и 400+ переменных - за полчаса не сделало, а дальше было лень.

но в общем z3 очень и очень хорошо и шустро решает практически все уравнения, и ему не важно линейные они или нет.

| Сообщение посчитали полезным:

Всем спасибо, z3 и ,правда, очень быстро нашел правильную последовательность из 19 символов (ps система уравнений из первого сообщения была отвлечением внимания и похоже она не имеет решения)

| Сообщение посчитали полезным: