+ Reply to Thread
Page 2 of 2 FirstFirst 1 2
Results 21 to 25 of 25

Thread: Введение в reverse engineering для начинающих [Денис Юричев]

  1. #21
    0xAF50's Avatar

    Default Re: Введение в reverse engineering для начинающих [Денис Юричев]

    Форум на сайте приказал долго жить - "Closed due to inactivity." Может ответит кто тут по вопросу на Lite-версии книги? Раздел 6.1.2, листинг 6.2.

    1. Почему там команда "mov edx, 1", а не "mov rdx, 1" ?
    2. Зачем выделяется 88 байт, если аргументов всего 9 (8*9=72) ?
    3. Если первые четыре аргумента передаются через регистры, то почему пятый аргумент записывается по [rsp+32] ?
    4. Что хранится по адресам [rsp+72] до [rsp+88] ?

  2. Пользователь сказал cпасибо:
    Dark Koder (09-02-2016)
  3. #22
    Darwin's Avatar

    Default Re: Введение в reverse engineering для начинающих [Денис Юричев]

    1. Почему там команда "mov edx, 1", а не "mov rdx, 1" ?

    Это оптимизация. MOV EDX, 1 занимает 5 байтов, а MOV RDX, 1 занимает 10 байтов.

    2. Зачем выделяется 88 байт, если аргументов всего 9 (8*9=72) ?

    Специфика вызова функции printf, но два значения, т.е. 16 байт (2*8) там явно лишние.

    3. Если первые четыре аргумента передаются через регистры, то почему пятый аргумент записывается по [rsp+32] ?

    Потому что первые четыре аргумента (внутри функции printf), будут записаны в rsp+0, rsp+8, rsp+16, rsp+24. Вероятно это сделано для совместимости.

    4. Что хранится по адресам [rsp+72] до [rsp+88] ?

    Мусор. Эти данные никак не используются внутри функции printf.
    Last edited by Darwin; 12-02-2016 at 09:43.
    Счастлив кто отдал, а не взял. (с) Inception

  4. 6 пользователя(ей) сказали cпасибо:
    0xAF50 (13-02-2016) benedict (12-02-2016) dukeBarman (12-02-2016) gavz (16-02-2016) mikserok (10-03-2016) ximera (12-02-2016)
  5. #23
    mikserok's Avatar

    Default Re: Введение в reverse engineering для начинающих [Денис Юричев]

    Ух ты тут еще и на вопросы отвечают! :)
    Меня приятно удивила глава 77.2. Попробуем Z3 SMT-солвер про крякинг с использованием питона и автоматических решателей.
    Получается что можно заставить бездушную машину искать хотя бы 1 из целого множества вариантов решения системы уравнений причём в таких уравнениях можно использовать даже команды вроде циклического сдвига. А как насчёт md5 кто нить пробовал натравить Z3 солвер или другие решатели на обращение этого хеша?
    Вы пишите что криптографы вкурсе про сольверы. Получается что такую вот примитвную защиту Z3 не пробьёт?
    Code:
    if (md5(key + "Salt") != "449967E0F98744100CB480786856A0A3") ExitProcess();

    Или всё-таки пробьёт если дать хороший комп и достаточно времени (за разумный срок)?

    PHP Code:
    1 from z3 import *
    2
    3 C1
    =0x5D7E0D1F2E0F1F84
    4 C2
    =0x388D76AEE8CB1500
    5 C3
    =0xD2E9EE7E83C4285B
    6
    7 inp
    i1i2i3i4i5i6outp BitVecs('inp i1 i2 i3 i4 i5 i6 outp'64)
    8
    9 s 
    Solver()
    10 s.add(i1==inp*C1)
    11 s.add(i2==RotateRight (i1i1 0xF))
    12 s.add(i3==i2 C2)
    13 s.add(i4==RotateLeft(i3i3 0xF))
    14 s.add(i5==i4 C3)
    15 s.add(outp==RotateLeft (i5URem(i560)))
    16
    17 s
    .add(outp==10816636949158156260)
    18
    19 
    print s.check()
    20 m=s.model()
    21 print m
    22 
    print (" inp=0x%X" m[inp].as_long())
    23 print ("outp=0x%X" m[outp].as_long()) 
    Меня в этом коде смущают строки с s.add(...) Какого типа аргумент попадает на вход методу add? Разве в Питоне есть такой тип - алгебраическое уравнение или в нём есть ленивые вычисления? Обычно когда питон встречает выражение i1==inp*C1 он сначала попытается его вычислить. Очевидно раз последним встречается оператор == значит на вход add поступает либо True либо False. Но Питон не сможет вычислить это выражение так как не знает чему равны i1 и inp. Поэтому он должен ругнутся и сказать что я такой код выполнять не собираюсь. Но ведь этого не происходит. Почему?

    Есть что на русском почитать, помимо википедии, о том как устроены внутри (алгоритмы) эти SMT сольверы?
    Last edited by mikserok; 10-03-2016 at 14:26.

  6. #24

    Default Re: Введение в reverse engineering для начинающих [Денис Юричев]

    Quote Originally Posted by mikserok View Post
    Есть что на русском почитать, помимо википедии, о том как устроены внутри (алгоритмы) эти SMT сольверы?
    На русском не знаю, а вот на питоне и С++ почитать можно.
    Стартануть "под капот" можно с https://github.com/Z3Prover/z3, где в наличии все сырки, и ядра решателя и биндинги во все поддерживаемые языки.
    Дальше в \z3\src\api\python\z3.py и там ищем ответы на все свои вопросы.
    Code:
    class Solver(Z3PPObject):
    ....................................................
        def add(self, *args):
            self.assert_exprs(*args)
    ....................................................
        def assert_exprs(self, *args):
            args = _get_args(args)
            s    = BoolSort(self.ctx)
            for arg in args:
                if isinstance(arg, Goal) or isinstance(arg, AstVector):
                    for f in arg:
                        Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
                else:
                    arg = s.cast(arg)
                    Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
    ....................................................
    и т.д.

  7. 2 пользователя(ей) сказали cпасибо:
    dukeBarman (11-03-2016) ximera (11-03-2016)
  8. #25

    Default Re: Введение в reverse engineering для начинающих [Денис Юричев]

    Quote Originally Posted by mikserok View Post
    Ух ты тут еще и на вопросы отвечают! :)
    Меня приятно удивила глава 77.2. Попробуем Z3 SMT-солвер про крякинг с использованием питона и автоматических решателей.
    Получается что можно заставить бездушную машину искать хотя бы 1 из целого множества вариантов решения системы уравнений причём в таких уравнениях можно использовать даже команды вроде циклического сдвига. А как насчёт md5 кто нить пробовал натравить Z3 солвер или другие решатели на обращение этого хеша?
    Вы пишите что криптографы вкурсе про сольверы. Получается что такую вот примитвную защиту Z3 не пробьёт?
    Code:
    if (md5(key + "Salt") != "449967E0F98744100CB480786856A0A3") ExitProcess();

    Или всё-таки пробьёт если дать хороший комп и достаточно времени (за разумный срок)?
    В теории пробьет, но на практике нет, потому что MD5 разработана так, что уравнение в ней настолько большое, что с ним не справиться в реальности. Как и во всей остальной криптографии.

    Quote Originally Posted by mikserok View Post
    Меня в этом коде смущают строки с s.add(...) Какого типа аргумент попадает на вход методу add? Разве в Питоне есть такой тип - алгебраическое уравнение или в нём есть ленивые вычисления? Обычно когда питон встречает выражение i1==inp*C1 он сначала попытается его вычислить. Очевидно раз последним встречается оператор == значит на вход add поступает либо True либо False. Но Питон не сможет вычислить это выражение так как не знает чему равны i1 и inp. Поэтому он должен ругнутся и сказать что я такой код выполнять не собираюсь. Но ведь этого не происходит. Почему?
    Z3Py API это перегруженные операции (как в ООП), == в этом выражении это не питоновское, там дергается совсем другая ф-ция из недр Z3. Которая собирает все эти питоно-подобные выражения из s.add(...) и скармливает их в Z3.
    Например:
    https://github.com/Z3Prover/z3/blob/...hon/z3.py#L787

    Quote Originally Posted by mikserok View Post
    Есть что на русском почитать, помимо википедии, о том как устроены внутри (алгоритмы) эти SMT сольверы?
    На русском не знаю, а вообще вот, дописываю потихоньку:
    http://yurichev.com/tmp/SAT_SMT_DRAFT.pdf
    Постепенно переведу на русский... но не знаю, когда.

  9. 7 пользователя(ей) сказали cпасибо:
    Dark Koder (19-03-2016) Darwin (24-03-2016) Shizoid (09-11-2016) dukeBarman (12-03-2016) gavz (13-03-2016) mikserok (12-03-2016) ximera (12-03-2016)
+ Reply to Thread

Posting Permissions

  • You may not post new threads
  • You may not post replies
  • You may not post attachments
  • You may not edit your posts
All times are GMT. The time now is 10:43
vBulletin® Copyright ©2000 - 2017
www.reverse4you.org