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

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

 eXeL@B —› Софт, инструменты —› Как применять солверы?
Посл.ответ Сообщение

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

Создано: 3 мая 2020 18:21 · Поправил: Illuzion New!
Цитата · Личное сообщение · #1

Добрый день.
Почитал про солверы и попробовал Z3 (--> Link <--). Хотелось бы понять основные варианты и алгоритмы их применения при исследовании программ.
Я пока увидел такие варианты:

1. Удаление "мёртвого" кода.
Алгоритм: Берём небольшой участок кода. Сохраняем/загружаем начальное состояние. Эмулируем/исполняем код, сохраняем конечное состояние. По-очереди убираем инструкции и снова эмулируем/исполняем код. Загружаем конечное состояние "с" и "без" инструкции в солвер и решаем. Если состояние с инструкцией и без инструкции равны, то можем её убирать.
Выглядит странно, не очень понятно зачем тут солвер нужен, если мы можем просто сравнить состояния. Из недостатков вижу скорость эмуляции/выполнения. Также не очень понятно с начальными состояниями. Их нужно много разных?

2. Упрощение кода.
Алгоритм: Берём небольшой участок кода. Переводим инструкции в нотацию солвера, регистры в переменные и "жмём" simplify. Результат переводим обратно в инструкции.

3. Для решения "opaque predicate" в статическом анализе.
Также эмулируем/исполняем/упрощаем инструкции и на условном переходе смотрим флаги.

4. Для подбора, скажем, серийника.
Алгоритм: например, если на выходе функции мы должны получить RAX==1, определили входы, загрузили инструкции и ждём пока солвер даст нам примерный вход. Мне кажется, что он может решать некоторые функции слишком долго.

Опять же не очень понятно, зачем солвер, мы ведь можем всегда снять трассу и в нужных местах, грубо говоря, если после 100 проходов RCX == 1, то и в 101-м он будет такой же. А если до этого идут xor/and/... то просто в нужном месте поставить "mov rcx, 1". Хотя, конечно, могут быть участки кода, на которые сложно попасть в run-time..

Верно ли это? Есть ли ещё варианты их применения?

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

Создано: 3 мая 2020 18:50 · Поправил: VOLKOFF New!
Цитата · Личное сообщение · #2

--> Тут <-- достаточно наглядно показано.

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


Ранг: -5.6 (нарушитель)
Статус: Участник

Создано: 4 мая 2020 00:28 New!
Цитата · Личное сообщение · #3

Интересная -> статья <- на эту тему.


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

Создано: 5 мая 2020 04:38 · Поправил: Bronco New!
Цитата · Личное сообщение · #4

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

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

Создано: 6 мая 2020 23:48 · Поправил: Illuzion New!
Цитата · Личное сообщение · #5

Подскажите, а есть ли какие-н штатные средства, чтобы SMT-LIB в асм код переделать? Например:

Code:
  1. (bvsub (bvnot (_ bve4 20)) (_ bv3099356b 20))

После упрощения становится:
Code:
  1. (_ bvcf66c9b0 20)

А после перевода в асм код (если далее нет уловных переходов):
Code:
  1. mov reg32, 0xcf66c9b0


VOLKOFF, попробовал тритон, очень приятно с ним работать (только PIN tracer на Ubuntu не получилось скомпилировать, там пишут что только 2.* поддерживается, а последний пин далеко уже ушёл, хотя мож я чего не так сделал).

Bronco пишет:
а кто и как определяет границы :небольшого участока кода ?

Я на 1-ой функции экспериментирую, которая около 2 кб. Хочу немного её упростить. Пока я вижу это в semi-automatic режиме, с подтверждением сомнительных(?) действий. Т.е. скажем простые упрощения xor/mov/or и т.п. можно на автоматике. Понятно, что есть side-effects, но не везде и не всегда. Также плюсом я попробовал сюда уже снятую в XML трассу подключить с разными входами. Половина условных dead-jump'ов и небольшая часть мёртвого кода убирается ещё до статического анализа. Интересно получилось, что некоторые cond-jmps выполняются, скажем 20 раз из 963-х, но код, который после них, мусорный. Т.е. вообще не важно - будет код выполнен или нет.
А как вы предложите?


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

Создано: 7 мая 2020 01:03 · Поправил: Bronco New!
Цитата · Личное сообщение · #6

Illuzion пишет:
Половина условных dead-jump'ов и небольшая часть мёртвого кода убирается ещё до статического анализа.

странно звучит, что в снятой трассе, есть мёртвый код, допускаю что это просто выделено в буфер и скормлено солверу.
наличие в буфере эмуляции безусловного прыга, как бы это подтверждает, лапшу из прыгов можно в трассу ваще не писать.
если известны границы блоков в морфе, то сам код для эмуляции прыга, отлетает как щепки, ещё до солвера.
то есть ключевое это деление на блоки. я не знаю что солвер отрыгивает, не пробывал.
Illuzion пишет:
А как вы предложите?

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

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

Создано: 7 мая 2020 01:32 · Поправил: Illuzion New!
Цитата · Личное сообщение · #7

Bronco пишет:
Половина условных dead-jump'ов и небольшая часть мёртвого кода убирается ещё до статического анализа.
странно звучит, что в снятой трассе, есть мёртвый код, допускаю что это просто выделено в буфер и скормлено солверу.


Почему странно? Трасса пин тулом была снята, но не полностью, а только все возможные переходы и +нужная функция. Пример мёртвого кода после jbe loc_7FA7001E:

Code:
  1. mfc:7FA70000                 push    0
  2. mfc:7FA70002                 push    esp
  3. mfc:7FA70003                 push    ebx
  4. mfc:7FA70004                 jbe     loc_7FA7001E   ;Taken="656" Total="963"; Total > Taken
  5.  
  6. ;Всё что ниже до 0х7FA7001E - мёртвый. Судя по логу он выполняется 307 раз. Там ebx ещё дальше меняется, не стал его приводить
  7.  
  8. mfc:7FA7000A                 push    edi
  9. mfc:7FA7000B                 not     bl
  10. mfc:7FA7000D                 jb      loc_7FA7001F    ; never taken
  11. mfc:7FA70013                 lea     esp, [esp+4]
  12. mfc:7FA70017                 push    eax
  13. mfc:7FA70018                 mov     eax, 0
  14. mfc:7FA7001D                 pop     eax
  15. mfc:7FA7001E
  16. mfc:7FA7001E loc_7FA7001E:                           ; CODE XREF: mfc+4&#8593;j
  17. mfc:7FA7001E                 push    edi
  18. mfc:7FA7001F
  19. mfc:7FA7001F loc_7FA7001F:                 


Переходы в таком формате снял (использовал, кстати, XED). Там где переходы вида "call reg32" просто добавляются <Dest>, а если код меняет уже сделанный переход и ещё раз на него возвращается, то просто добавляется новый адрес с другими <Bytes>:

Code:
  1.     <7fa70004 Taken="656" Total="963">
  2.         <Bytes>0F8614000000</Bytes>
  3.         <Dism>jbe 0xdbac762</Dism>
  4.         <Dest>
  5.             <7fa7001e Taken="656"/>
  6.         </Dest>
  7.     </7fa70004>


Bronco пишет:
но вся оптимизация упирается в шаблоны

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


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

Создано: 7 мая 2020 02:06 · Поправил: Bronco New!
Цитата · Личное сообщение · #8

Illuzion пишет:
Почему странно? Трасса пин тулом была снята

если код исполняется в динамике, он не может быть мёртвым.
хз может пин покрытие предугадывает, и ему не важно, где фейковый оператор флага, а где в цикле.
тогда это минус для жирного пина.
если это тупо левое ветвление обфускации, то при свёртке оно лесом.
у меня на входе, шлак подобный твоему, но я фильтрую трассу, почти всё писать глупо:
Code:
  1. PUSH RDX
  2. ADD EBX, 0x0
  3. NOT RDX
  4. AND QWORD PTR SS:[RSP], RDX
  5. MOV R9, 0xFFFFFFFF00000000
  6. POP RDX
  7. ADD RDX, 0x0
  8. PUSH R11
  9. NOT R11
  10. LEA RBP, QWORD PTR SS:[RSP]
  11. AND BYTE PTR SS:[RBP], R11B
  12. MOV R11, QWORD PTR SS:[RSP]
  13. SUB RSP, 0xFFFFFFFFFFFFFFF8
  14. MOV R14D, 0x1FFF
  15. LEA RAX, QWORD PTR DS:[R13 + 0x2D14DED3]
  16. ROL RDX, 0x20
  17. AND RDX, R9
  18. XOR RDX, R14
  19. LEA R14, QWORD PTR DS:[R13 - 0x3A584A5B]
  20. ADD R11B, BYTE PTR DS:[R14 + 0x3A58515B]
  21. ADD RCX, 0xFFFFFFFFFFFFFFA0
  22. MOVZX R11, R11B
  23. AND R11, RDX
  24. ROL R11, 0x33
  25. XOR ESI, ESI
  26. OR QWORD PTR DS:[RAX - 0x2D14DD0B], R11
  27. ROL EDI, CL
  28. PUSH R12
  29. LEA R12, QWORD PTR DS:[0x151881D08]
  30. XCHG QWORD PTR SS:[RSP], R12
  31. BTS R15D, 0x2
  32. RET 

на выходе
Code:
  1. MOVZX R11, BYTE PTR DS:[R13 + 0x700]
  2. AND R11D, 0x1FFF
  3. ROL R11, 0x33
  4. OR QWORD PTR DS:[R13 + 0x1C8], R11

Illuzion пишет:
<7fa70004 Taken="656" Total="963">
<Bytes>0F8614000000</Bytes>
<Dism>jbe 0xdbac762</Dism>
<Dest>
<7fa7001e Taken="656"/>
</Dest>
</7fa70004>

хз я такую трассу не приветствую, опкод условного +дист, это макси 6 байт. а тут 7 строк, по 10 символов в каждой.
в страницу влазит более 70 лямов строк асм кода в бинарном виде( это всего 256 мб).
не надо контекст за собой тянуть, всегда можно бинарь подгрузить к отладчику, по трассировать с любого места, засейвить правку и тп.

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

 eXeL@B —› Софт, инструменты —› Как применять солверы?

Видеокурс ВЗЛОМ