Хабр Курсы для всех
РЕКЛАМА
Практикум, Хекслет, SkyPro, авторские курсы — собрали всех и попросили скидки. Осталось выбрать!
Хабр доступен 24/7 благодаря поддержке друзей
Комментарии 31
if ((x*x & 1) == 0)
good_code
else
мусор
А разве подобные вещи компилятор не должен оптимизировать? Или в данном случае (.NET) вы полностью или частично компилируете в байт-код сами?
Вроде проблема именно в том, чтобы подставить в ((x*x & 1) == 0) достаточно сложное условие, чтобы понять, что оно всегда true — «сложно» для взломщика и невозможно для компилятора.
Невозможно всегда с уверенностью на 100% узнать, будет ли условие всегда true или она всегда false или могут быть разные варианты, без того, чтобы собственно выполнить программу («проблема останова»)
Невозможно всегда с уверенностью на 100% узнать, будет ли условие всегда true или она всегда false или могут быть разные варианты, без того, чтобы собственно выполнить программу («проблема останова»)
Откуда кстати взяли, что ((x*x & 1) == 0) всегда истинно?
Берем x=1, получаем ложное. Для любого нечетного x выражение будет ложное.
Берем x=1, получаем ложное. Для любого нечетного x выражение будет ложное.
Наверное, имелось ввиду, что это оптимизируется до (x & 1) == 0
В примере if ((x*x & 1) == 0) надо заменить на if ((x+x & 1) == 0) я опечатался и вместо плюс написал умножить
Не забывайте что программа, кроме непосредственно обеспечения самой защиты, должна еще продолжать работать :) Приложение, которое сплошь покрыто предикатами по 20..50 операций умножения\деления\возведения в степень каждый, вряд ли будет приемлемо в использовании.
На самом деле, очень перспективной на будущее, видится реализация Opaque Predicates на базе указателей. В статье упоминается, что эта задача считается неразрешимой, что еще лучше NP полноты :) Думаю в ближайшее время мы продолжим наши исследования в этом направлении.
На самом деле, очень перспективной на будущее, видится реализация Opaque Predicates на базе указателей. В статье упоминается, что эта задача считается неразрешимой, что еще лучше NP полноты :) Думаю в ближайшее время мы продолжим наши исследования в этом направлении.
Если x, y и z типа float, я бы не был так спокоен за диск C.
На сколько в среднем падает производительность зашифрованного кода и вырастает потребление памяти?
Так говорите, для решения надо все инты перебрать?
у меня для вас плохие новости
github.com/omgtehlion/randomstuff/blob/master/xops.cs
у меня для вас плохие новости
(Not(x) != x) : is always True (((x + -x) & 1) == 0) : is always True (Convert(Not(x)) != ((Convert(x) * 4) >> 2)) : is always True ((-x & 1) == (x & 1)) : is always True (((-x ^ x) & 1) == 0) : is always True (((x * 128) & 86) == 0) : is always True (Not((-x * 64)) != (x << 6)) : is always True ((Not((x * 128)) & 61) == 61) : is always False
github.com/omgtehlion/randomstuff/blob/master/xops.cs
в последнем тоже True, там код недописан конечно же, но имея достаточно времени можно решить всё.
В статье говориться
Мы не претендуем на NP-полноту задачи распознавания наших предикатов (именно поэтому не показываем реализацию). Но например, если бы генерировали тождественно истинные 3-КНФ (коньюктивные нормальные формы с тремя операндами в коньюнктах, типа: x==null & y!=null & z==null || x!= null & y==null в таком духе), то гарантировано не получилось бы написать распознаватель. Но когда мы реализовали это на практике, то оказалось, что в программе вставленный код сразу сильно бросается в глаза. Тогда мы задумались о скрытности предикатов, и в качестве временного решения, создали данный генератор. С учетом Control Flow обфускации выявление и удаление таких предикатов из кода будет достаточно затруднительно.
Статья же, охватывает тему Opaque Predicates намного более широко. Здесь поднимается вопрос о видах предикатов и разработке NP полного генератора. Мы планируем продолжать двигаться в эту сторону.
Наша реализация генератора, к сожалению, не совсем идеальна
Мы не претендуем на NP-полноту задачи распознавания наших предикатов (именно поэтому не показываем реализацию). Но например, если бы генерировали тождественно истинные 3-КНФ (коньюктивные нормальные формы с тремя операндами в коньюнктах, типа: x==null & y!=null & z==null || x!= null & y==null в таком духе), то гарантировано не получилось бы написать распознаватель. Но когда мы реализовали это на практике, то оказалось, что в программе вставленный код сразу сильно бросается в глаза. Тогда мы задумались о скрытности предикатов, и в качестве временного решения, создали данный генератор. С учетом Control Flow обфускации выявление и удаление таких предикатов из кода будет достаточно затруднительно.
Статья же, охватывает тему Opaque Predicates намного более широко. Здесь поднимается вопрос о видах предикатов и разработке NP полного генератора. Мы планируем продолжать двигаться в эту сторону.
Первым делом подумал про Пролог. Но потом понял, что выражения из примера не булевы, а битовые. ОК, определяем x как массив из 32 бит (b31, b30, ..., b0). Далее для каждого бита тупо выполняем операции, и смотрим, что получилось. Если переменная исчезла и остались лишь константы — все, выражение вычислено.
Например, (x + x & 1) == 0
Можно определить логические правила для каждого бита. Тупо идти по операциям и определять:
1) Изначально имеем b32 b31… b1 b0
2) Применяем x+x: тут сложно, правила переноса и т.д. Нулевой бит: b0 ^ b0 — что сокращается до 0, первый бит: b1 ^ (b0 & b0) = b1 ^ b0 и т.д.
3) Применяем &1: сложное дерево сокращается до 0. Предикат доказан.
В целом, основная идея — уменьшить число битов, от которых зависит результат. Прототип писать лень, но, думаю, все выражения в конце статьи можно таким образом прорешать.
UPD Товарищ atd уже написал :) habrahabr.ru/post/202162/#comment_6980848
Например, (x + x & 1) == 0
Можно определить логические правила для каждого бита. Тупо идти по операциям и определять:
1) Изначально имеем b32 b31… b1 b0
2) Применяем x+x: тут сложно, правила переноса и т.д. Нулевой бит: b0 ^ b0 — что сокращается до 0, первый бит: b1 ^ (b0 & b0) = b1 ^ b0 и т.д.
3) Применяем &1: сложное дерево сокращается до 0. Предикат доказан.
В целом, основная идея — уменьшить число битов, от которых зависит результат. Прототип писать лень, но, думаю, все выражения в конце статьи можно таким образом прорешать.
UPD Товарищ atd уже написал :) habrahabr.ru/post/202162/#comment_6980848
Спасибо за Ваш комментарий, ответил на вопрос atd чуть выше
Давайте посмотрим, сколько секунд понадобится SAT-солверу для того, чтобы доказать или опровергнуть ваши последние четыре предиката:
Дайте что-ли ради интереса что-нибудь из прошлого варианта, для чего «гарантировано не получилось бы написать распознаватель».
*Main> prove $ forAll_ test1 Falsifiable. Counter-example: s0 = 420228064 :: SInt32 (0.02 secs, 1032876 bytes)
*Main> prove $ forAll_ test2 Q.E.D. (0.01 secs, 1151920 bytes)
*Main> prove $ forAll_ test3 Q.E.D. (0.01 secs, 1128176 bytes)
*Main> prove $ forAll_ test4 Q.E.D. (0.01 secs, 1092956 bytes)
Дайте что-ли ради интереса что-нибудь из прошлого варианта, для чего «гарантировано не получилось бы написать распознаватель».
Некоторые примеры предикатов из первой версии генератора:
"(x3 | x2 | !x0) & (x3 | x2 | x1) & (x3 | x2 | x4) & (x3 | !x0 | x1) & (x3 | !x0 | x4) & (x3 | x1 | x4) & (x2 | !x0 | x1) & (x2 | !x0 | x4) & (x2 | x1 | x4) & (!x0 | x1 | x4) & (!x2 | !x1 | !x4) & (!x2 | !x1 | !x3) & (!x2 | !x1 | x0) & (!x2 | !x4 | !x3) & (!x2 | !x4 | x0) & (!x2 | !x3 | x0) & (!x1 | !x4 | !x3) & (!x1 | !x4 | x0) & (!x1 | !x3 | x0) & (!x4 | !x3 | x0)",
"(x2 | x1 | x0) & (x2 | x1 | x4) & (x2 | x1 | x3) & (x2 | x0 | x4) & (x2 | x0 | x3) & (x2 | x4 | x3) & (x1 | x0 | x4) & (x1 | x0 | x3) & (x1 | x4 | x3) & (x0 | x4 | x3) & (!x2 | !x4 | !x0) & (!x2 | !x4 | !x1) & (!x2 | !x4 | !x3) & (!x2 | !x0 | !x1) & (!x2 | !x0 | !x3) & (!x2 | !x1 | !x3) & (!x4 | !x0 | !x1) & (!x4 | !x0 | !x3) & (!x4 | !x1 | !x3) & (!x0 | !x1 | !x3)",
"(x1 | !x0 | !x2) & (x1 | !x0 | x4) & (x1 | !x0 | x3) & (x1 | !x2 | x4) & (x1 | !x2 | x3) & (x1 | x4 | x3) & (!x0 | !x2 | x4) & (!x0 | !x2 | x3) & (!x0 | x4 | x3) & (!x2 | x4 | x3) & (x0 | !x1 | !x4) & (x0 | !x1 | x2) & (x0 | !x1 | !x3) & (x0 | !x4 | x2) & (x0 | !x4 | !x3) & (x0 | x2 | !x3) & (!x1 | !x4 | x2) & (!x1 | !x4 | !x3) & (!x1 | x2 | !x3) & (!x4 | x2 | !x3)",
"(x0 | !x3 | x4) & (x0 | !x3 | x1) & (x0 | !x3 | x2) & (x0 | x4 | x1) & (x0 | x4 | x2) & (x0 | x1 | x2) & (!x3 | x4 | x1) & (!x3 | x4 | x2) & (!x3 | x1 | x2) & (x4 | x1 | x2) & (!x0 | !x2 | x3) & (!x0 | !x2 | !x1) & (!x0 | !x2 | !x4) & (!x0 | x3 | !x1) & (!x0 | x3 | !x4) & (!x0 | !x1 | !x4) & (!x2 | x3 | !x1) & (!x2 | x3 | !x4) & (!x2 | !x1 | !x4) & (x3 | !x1 | !x4)",
"(!x0 | !x3 | x1) & (!x0 | !x3 | x4) & (!x0 | !x3 | !x2) & (!x0 | x1 | x4) & (!x0 | x1 | !x2) & (!x0 | x4 | !x2) & (!x3 | x1 | x4) & (!x3 | x1 | !x2) & (!x3 | x4 | !x2) & (x1 | x4 | !x2) & (x0 | x2 | !x1) & (x0 | x2 | !x4) & (x0 | x2 | x3) & (x0 | !x1 | !x4) & (x0 | !x1 | x3) & (x0 | !x4 | x3) & (x2 | !x1 | !x4) & (x2 | !x1 | x3) & (x2 | !x4 | x3) & (!x1 | !x4 | x3)",
"(!x0 | x1 | x3) & (!x0 | x1 | x4) & (!x0 | x1 | x2) & (!x0 | x3 | x4) & (!x0 | x3 | x2) & (!x0 | x4 | x2) & (x1 | x3 | x4) & (x1 | x3 | x2) & (x1 | x4 | x2) & (x3 | x4 | x2) & (x0 | !x4 | !x3) & (x0 | !x4 | !x1) & (x0 | !x4 | !x2) & (x0 | !x3 | !x1) & (x0 | !x3 | !x2) & (x0 | !x1 | !x2) & (!x4 | !x3 | !x1) & (!x4 | !x3 | !x2) & (!x4 | !x1 | !x2) & (!x3 | !x1 | !x2)"Кстати, очень не советую встраивать предикат из картинки в начале поста в свою программу:
signed, 32 bit
signed, 64 bit
unsigned, 32 bit
unsigned, 64 bit
Я знаю, что в статье написано
но все равно решил предупредить невнимательных.
signed, 32 bit
*Main> prove $ forAll_ (fermat :: SInt32 -> SInt32 -> SInt32 -> SBool) Falsifiable. Counter-example: s0 = -655189642 :: SInt32 s1 = 125895093 :: SInt32 s2 = 1609826051 :: SInt32 (3.12 secs, 1094592 bytes)
signed, 64 bit
*Main> prove $ forAll_ (fermat :: SInt64 -> SInt64 -> SInt64 -> SBool) Falsifiable. Counter-example: s0 = -6515675963299228301 :: SInt64 s1 = 6034959013475051589 :: SInt64 s2 = 2466979131238012272 :: SInt64 (15.38 secs, 1939316 bytes)
unsigned, 32 bit
*Main> prove $ forAll_ (fermat :: SWord32 -> SWord32 -> SWord32 -> SBool) Falsifiable. Counter-example: s0 = 3639777654 :: SWord32 s1 = 125895093 :: SWord32 s2 = 1609826051 :: SWord32 (3.75 secs, 1095380 bytes)
unsigned, 64 bit
*Main> prove $ forAll_ (fermat :: SWord64 -> SWord64 -> SWord64 -> SBool) Falsifiable. Counter-example: s0 = 11931068110410323315 :: SWord64 s1 = 6034959013475051589 :: SWord64 s2 = 2466979131238012272 :: SWord64 (14.82 secs, 1159580 bytes)
Я знаю, что в статье написано
Но не спешите. Диофантово уравнение – это вовсе не набор сумм и произведений интов со значениями от 0 до 4 млрд, а набор сумм и произведений целых чисел со значениями от 0 до бесконечности.
но все равно решил предупредить невнимательных.
Упс, уже написали выше. Да ещё и с примером попроще (и в самом деле, 2566 = 0).
В коде таких предикатов сотни тысяч, 3-5 секунд на штуку — заведомо не приемлимое время (в случае реального применения).
Кроме того, предикат еще надо выявить в размазанном коде и, при этом, не зарезать реальные if'ы (даже с 99% вероятностью невыполнимые).
Кроме того, предикат еще надо выявить в размазанном коде и, при этом, не зарезать реальные if'ы (даже с 99% вероятностью невыполнимые).
В коде таких предикатов сотни тысяч, 3-5 секунд на штуку — заведомо не приемлимое время (в случае реального применения).
Шесть дней на приведение кода в читабельное состояние. Копейки, нет?
Так поэтому-то и интересно узнать, как генерировать такие вот сложные предикаты (заранее зная, выполнимый или невыполнимый предикат требуется).
А в случае реального применения, 100000 × 3 секунды (учтите, что у меня старенький нетбук) = 3.5 дня. Несколько недель на взлом программы — не так уж и плохо.
А в случае реального применения, 100000 × 3 секунды (учтите, что у меня старенький нетбук) = 3.5 дня. Несколько недель на взлом программы — не так уж и плохо.
По три секунды тратится только на те, которые недоказуемы формальными методами.
Для всех остальных отрабатывает за доли миллисекунды.
Для всех остальных отрабатывает за доли миллисекунды.
Имхо нет особого смысла гнаться за «неявностью» предикатов. Ведь очень сложно (если вообще возможно) объеденить неявность и непросчитываемость условия.
А что мешает пересыпать код большим количеством явных но не просчитываемых условий, сформулированным таким образом чтобы мусор был то then, то в else ветке? Деобфускатор будет понимать что весь код обфусцирован/инструментирован и для каждого конкретного ветвления не сможет определить тру там или фолс. В мусоре будете генерировать дальнейшие ветвления которые будутт похожи на настоящие в абсолютной степени (так как нет требований по просчитываемости).
Если мусор будет не очевидно рандомным, а слегка модифицированным оригинальным кодом + оригинальный код также будет разбавлен мусорными включениями (нейтральными с точки зрения выполнения конечной функции), то деобфусцировать такой код, не будучи уверенным какие части графа достижимы а какие нет, будет весьма сложно
А что мешает пересыпать код большим количеством явных но не просчитываемых условий, сформулированным таким образом чтобы мусор был то then, то в else ветке? Деобфускатор будет понимать что весь код обфусцирован/инструментирован и для каждого конкретного ветвления не сможет определить тру там или фолс. В мусоре будете генерировать дальнейшие ветвления которые будутт похожи на настоящие в абсолютной степени (так как нет требований по просчитываемости).
Если мусор будет не очевидно рандомным, а слегка модифицированным оригинальным кодом + оригинальный код также будет разбавлен мусорными включениями (нейтральными с точки зрения выполнения конечной функции), то деобфусцировать такой код, не будучи уверенным какие части графа достижимы а какие нет, будет весьма сложно
Кстати, я думаю, что генерация мусора вообще не обязательна. В не выполняемых ветках предиката можно просто вставить переход на непредсказуемый участок пользовательского кода (точнее передвинуть этот участок под предикат, чтобы скрытно было). Это также убережёт от раздувания екзешника. В текущей реализации мы так и делаем: выглядит очень ествественно как на уровне IL так и в декомпилированном виде.
Не забывайте что программа, кроме обеспечения непосредственно защиты, должна еще продолжать полноценно работать. Приложение сплошь покрытое предикатами по 20..50 операций умножения\деления\возведения в степень каждый, вряд ли будет приемлемо в использовании.
На самом деле, очень перспективной на будущее, видится реализация Opaque Predicates на базе указателей. В статье говориться о том, что эта задача, как и проблема останова, в общем случае, является неразрешимой. А неразрешимая задача всегда лучше NP полной :) Думаю что в ближайшее время мы продолжим наши исследования в этом направлении.
На самом деле, очень перспективной на будущее, видится реализация Opaque Predicates на базе указателей. В статье говориться о том, что эта задача, как и проблема останова, в общем случае, является неразрешимой. А неразрешимая задача всегда лучше NP полной :) Думаю что в ближайшее время мы продолжим наши исследования в этом направлении.
Неразрешимость будет, если память бесконечна. Понятное дело, перебирать все состояния памяти не вариант. Но ведь и выделять много памяти для этих предикатов в программу вряд ли захочется. Получается, что неразрешимость тут вообще никаким боком не стоит.
Что более важно, если выбирать произвольный предикат (будь то 3SAT-формула или предикат из любой другой NP-полной задачи), нет никаких гарантий, что данный экземпляр будет сложно решить. Я уверен, что подавляющее большинство случайных предикатов решается на ура. Выше уже писали, что те же 3SAT-формулы (особенно случайные) отлично решаются для достаточно больших размеров.
Я бы предложил попробовать использовать известные считающиеся сложными задачи — например взять какой-нибудь криптографический хэш и его код размазать (т.е. размазать проверку вида sha1(x) = y). Навскидку сложности: придумать, как замаскировать константы хэша; как сделать, чтобы все раунды хэширования выглядели по разному; плюс размер кода может получиться слишком большим для маленькой программы — а что если надо еще и несколько предикатов? (хотя можно попытаться использовать результаты одного и того же хэша).
Что более важно, если выбирать произвольный предикат (будь то 3SAT-формула или предикат из любой другой NP-полной задачи), нет никаких гарантий, что данный экземпляр будет сложно решить. Я уверен, что подавляющее большинство случайных предикатов решается на ура. Выше уже писали, что те же 3SAT-формулы (особенно случайные) отлично решаются для достаточно больших размеров.
Я бы предложил попробовать использовать известные считающиеся сложными задачи — например взять какой-нибудь криптографический хэш и его код размазать (т.е. размазать проверку вида sha1(x) = y). Навскидку сложности: придумать, как замаскировать константы хэша; как сделать, чтобы все раунды хэширования выглядели по разному; плюс размер кода может получиться слишком большим для маленькой программы — а что если надо еще и несколько предикатов? (хотя можно попытаться использовать результаты одного и того же хэша).
Неразрешимость будет, если память бесконечна.
Неразрешимость будет даже тогда, когда память потенциально бесконечна. Если генерировать ту самую динамическую структуру в памяти, то, из-за того, что эмуляция локальны, в каждом конкретном участке кода нельзя будет предугадать реальный объём занимаемый структурой. Естественно структура должна быть скрытной, чтобы не было априори известно, что в реальности не так много памяти она занимает.
Если встроить длинную арифметику и Диофантовы уравнения, то так же будет неразрешимость, так как параметры уравнения берутся из случайных даже потенциально сколь угодно больших участков в памяти, например. Но тут нет скрытности и хакер просто вырежет все неявные предикаты.
Я уверен, что подавляющее большинство случайных предикатов решается на ура.
Если сделать генератор, который создаёт предикаты и отсеивает те, которые решились на ура, то уже большинство предикатов не будут так просты.
Возможно я не совсем правильно понял Ваш вариант с хэшом. Как мне кажется эмулятор как раз сделан для того, чтобы проэмулировать вычисление sha1 и понять, что значение всегда такое-то. В этом предложении отсутствует элемент псевдослучайности входных параметров без которого задача решается эмуляцией.
Зарегистрируйтесь на Хабре, чтобы оставить комментарий
Неявные предикаты