eXeLab
eXeL@B ВИДЕОКУРС !

Курс видеоуроков «Программирование и взлом 2O18»
Обновлен 13 сентября 2O18 года
Свежие инструменты, новые видеоуроки!

  • 300+ видеоуроков
  • 800 инструментов
  • 100+ свежих книг и статей

УЗНАТЬ БОЛЬШЕ >>
Домой | Статьи | RAR-cтатьи | FAQ | Форум | Скачать | Видеокурс
Новичку | Ссылки | Программирование | Интервью | Архив | Связь

Русский / Russian English / Английский

Сейчас на форуме: 3ton, moreno410, rmn, ursula3030 (+4 невидимых)
 · Начало · Статистика · Регистрация · Поиск · ПРАВИЛА ФОРУМА · Язык · RSS · SVN ·

 eXeL@B —› Основной форум —› Решение набора уравнений
Посл.ответ Сообщение

Ранг: 15.4 (новичок)
Статус: Участник

Создано: 18 июня 2018 19:10 New!
Цитата · Личное сообщение · #1

Всем привет!

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

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.

Ранг: 49.2 (посетитель)
Статус: Участник

Создано: 18 июня 2018 19:20 · Поправил: kunix New!
Цитата · Личное сообщение · #2

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

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

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

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


Ранг: 313.9 (мудрец)
Статус: Участник
born to be evil

Создано: 18 июня 2018 19:24 · Поправил: ajax New!
Цитата · Личное сообщение · #3

Ранг: 220.9 (наставник)
Статус: Участник

Создано: 18 июня 2018 19:27 New!
Цитата · Личное сообщение · #4

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

Ранг: 15.4 (новичок)
Статус: Участник

Создано: 18 июня 2018 19:57 New!
Цитата · Личное сообщение · #5

kunix пишет:

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

[i]kunix пишет:

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

Ранг: 380.7 (мудрец)
Статус: Участник

Создано: 18 июня 2018 19:57 · Поправил: dosprog New!
Цитата · Личное сообщение · #6

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

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


Ранг: 49.2 (посетитель)
Статус: Участник

Создано: 18 июня 2018 20:03 · Поправил: kunix New!
Цитата · Личное сообщение · #7

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

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

Ранг: 361.7 (мудрец)
Статус: Участник
"Тибериумный реверсинг"

Создано: 18 июня 2018 20:23 New!
Цитата · Личное сообщение · #8

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


Ранг: 513.9 (!)
Статус: Участник
Победитель турнира 2010

Создано: 18 июня 2018 20:26 New!
Цитата · Личное сообщение · #9

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


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


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


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

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

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

Ранг: 361.7 (мудрец)
Статус: Участник
"Тибериумный реверсинг"

Создано: 18 июня 2018 20:32 New!
Цитата · Личное сообщение · #10

OKOB пишет:
j * v - d = 0xffffd9be слабо верится

Значит там явно разброс шире, чем цифры 0-9 или ошибка в уравнениях


Ранг: 513.9 (!)
Статус: Участник
Победитель турнира 2010

Создано: 18 июня 2018 20:42 New!
Цитата · Личное сообщение · #11

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

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

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

Ранг: 49.2 (посетитель)
Статус: Участник

Создано: 18 июня 2018 21:47 · Поправил: kunix New!
Цитата · Личное сообщение · #12

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

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

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


Ранг: 513.9 (!)
Статус: Участник
Победитель турнира 2010

Создано: 18 июня 2018 22:07 · Поправил: OKOB New!
Цитата · Личное сообщение · #13

Code:
  1. from z3 import *
  2.  
  3. = BitVec('a', 8)
  4. = BitVec('b', 8)
  5. = BitVec('c', 8)
  6.  
  7. = Solver()
  8.  
  9. s.add(0x34F8FD3D == a * b + c)
  10. s.add(0x129D3A06 == (- c) ^ b)
  11. s.add(0x404B8F9A == a ^ b ^ c + a*b*c)
  12.  
  13. print s.check()
  14. print s.model()


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

Ранг: 15.3 (новичок)
Статус: Участник

Создано: 18 июня 2018 22:07 · Поправил: RevCred New!
Цитата · Личное сообщение · #14

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

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

Code:
  1. import time
  2. from z3 import *
  3.  
  4. = Solver()
  5.  
  6. a, b, c = BitVecs("a b c", 32)
  7.  
  8. s.add( 0x34F8FD3D == a * b + c )
  9. s.add( 0x129D3A06 == (- c) ^ b )
  10. s.add( 0x404B8F9A == a ^ b ^ c + a*b*)
  11.  
  12. = 0
  13. start_time = time.time()
  14. while s.check() == sat:
  15.   r = s.model() # result
  16.   _a, _b, _c = r[a].as_long(), r[b].as_long(), r[c].as_long()
  17.  
  18.   print _a, _b, _c
  19.  
  20.   s.add(Or( _a != a, _b != b, _c != c )) # anticollision
  21.   i += 1
  22.  
  23. print('--- %.2f second(s) && %d answer(s) ---' % ((time.time() - start_time), i) )


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

Ранг: 49.2 (посетитель)
Статус: Участник

Создано: 18 июня 2018 23:04 · Поправил: kunix New!
Цитата · Личное сообщение · #15

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



{ Атач доступен только для участников форума } - solver19vars.cpp

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


Ранг: 380.7 (мудрец)
Статус: Участник

Создано: 18 июня 2018 23:50 · Поправил: dosprog New!
Цитата · Личное сообщение · #16

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


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

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



Ранг: 248.2 (наставник)
Статус: Участник

Создано: 19 июня 2018 01:12 New!
Цитата · Личное сообщение · #17

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

Ранг: 15.3 (новичок)
Статус: Участник

Создано: 19 июня 2018 14:23 · Поправил: RevCred New!
Цитата · Личное сообщение · #18

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

kunix пишет:
и решение для младших бит при этом "не испортится".

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

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

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

Ранг: 49.2 (посетитель)
Статус: Участник

Создано: 19 июня 2018 15:13 New!
Цитата · Личное сообщение · #19

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

Ранг: 15.4 (новичок)
Статус: Участник

Создано: 20 июня 2018 07:23 New!
Цитата · Личное сообщение · #20

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

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


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

Ранг: 15.3 (новичок)
Статус: Участник

Создано: 20 июня 2018 08:00 · Поправил: RevCred New!
Цитата · Личное сообщение · #21

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 очень и очень хорошо и шустро решает практически все уравнения, и ему не важно линейные они или нет.

Ранг: 15.4 (новичок)
Статус: Участник

Создано: 2 июля 2018 21:42 New!
Цитата · Личное сообщение · #22

Всем спасибо, z3 и ,правда, очень быстро нашел правильную последовательность из 19 символов (ps система уравнений из первого сообщения была отвлечением внимания и похоже она не имеет решения)
 eXeL@B —› Основной форум —› Решение набора уравнений
Эта тема закрыта. Ответы больше не принимаются.

Оригинальный DVD-ROM: eXeL@B DVD !

Вы находитесь на форуме сайта EXELAB.RU
Проект ReactOS