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

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

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

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

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

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

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

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

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

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

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

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

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

-----
Чтобы юзер в нэте не делал,его всё равно жалко..

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

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


После упрощения становится:

А после перевода в асм код (если далее нет уловных переходов):


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

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

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

Illuzion пишет:
Половина условных dead-jump'ов и небольшая часть мёртвого кода убирается ещё до статического анализа.
странно звучит, что в снятой трассе, есть мёртвый код, допускаю что это просто выделено в буфер и скормлено солверу.
наличие в буфере эмуляции безусловного прыга, как бы это подтверждает, лапшу из прыгов можно в трассу ваще не писать.
если известны границы блоков в морфе, то сам код для эмуляции прыга, отлетает как щепки, ещё до солвера.
то есть ключевое это деление на блоки. я не знаю что солвер отрыгивает, не пробывал.
Illuzion пишет:
А как вы предложите?
я исхожу из простого, если пром код, позволяет упростить синтаксис инструкции, и готовый парсер покрывает весь набор интела или амд, то этим стоит по развлекаться.
если парсер мутить самому, то ну его нах.
многое опирается в память, пох на диске или оператива.
к примеру выхлоп слегка подрезанного капстона, с дитейлом 1 инструкции требует 0х300 байт памяти, остальные дизы требуют больше памяти.
но вся оптимизация упирается в шаблоны, но есть 2 плюса, результ под осмысленным контролем, и не надо заморачиваться, на линкование в асм. .

-----
Чтобы юзер в нэте не делал,его всё равно жалко..

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

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

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



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



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

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

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

на выходе

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