Comments 31
if ((x*x & 1) == 0)
good_code
else
мусор
А разве подобные вещи компилятор не должен оптимизировать? Или в данном случае (.NET) вы полностью или частично компилируете в байт-код сами?
0
Вроде проблема именно в том, чтобы подставить в ((x*x & 1) == 0) достаточно сложное условие, чтобы понять, что оно всегда true — «сложно» для взломщика и невозможно для компилятора.
Невозможно всегда с уверенностью на 100% узнать, будет ли условие всегда true или она всегда false или могут быть разные варианты, без того, чтобы собственно выполнить программу («проблема останова»)
Невозможно всегда с уверенностью на 100% узнать, будет ли условие всегда true или она всегда false или могут быть разные варианты, без того, чтобы собственно выполнить программу («проблема останова»)
+2
Откуда кстати взяли, что ((x*x & 1) == 0) всегда истинно?
Берем x=1, получаем ложное. Для любого нечетного x выражение будет ложное.
Берем x=1, получаем ложное. Для любого нечетного x выражение будет ложное.
+1
Наверное, имелось ввиду, что это оптимизируется до (x & 1) == 0
0
В примере if ((x*x & 1) == 0) надо заменить на if ((x+x & 1) == 0) я опечатался и вместо плюс написал умножить
0
Не забывайте что программа, кроме непосредственно обеспечения самой защиты, должна еще продолжать работать :) Приложение, которое сплошь покрыто предикатами по 20..50 операций умножения\деления\возведения в степень каждый, вряд ли будет приемлемо в использовании.
На самом деле, очень перспективной на будущее, видится реализация Opaque Predicates на базе указателей. В статье упоминается, что эта задача считается неразрешимой, что еще лучше NP полноты :) Думаю в ближайшее время мы продолжим наши исследования в этом направлении.
На самом деле, очень перспективной на будущее, видится реализация Opaque Predicates на базе указателей. В статье упоминается, что эта задача считается неразрешимой, что еще лучше NP полноты :) Думаю в ближайшее время мы продолжим наши исследования в этом направлении.
0
Если x, y и z типа float, я бы не был так спокоен за диск C.
+4
На сколько в среднем падает производительность зашифрованного кода и вырастает потребление памяти?
+1
Так говорите, для решения надо все инты перебрать?
у меня для вас плохие новости
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
+3
в последнем тоже True, там код недописан конечно же, но имея достаточно времени можно решить всё.
0
В статье говориться
Мы не претендуем на 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 полного генератора. Мы планируем продолжать двигаться в эту сторону.
+1
Первым делом подумал про Пролог. Но потом понял, что выражения из примера не булевы, а битовые. ОК, определяем 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
+1
Давайте посмотрим, сколько секунд понадобится 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)
Дайте что-ли ради интереса что-нибудь из прошлого варианта, для чего «гарантировано не получилось бы написать распознаватель».
+3
Некоторые примеры предикатов из первой версии генератора:
"(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)"
0
Кстати, очень не советую встраивать предикат из картинки в начале поста в свою программу:
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 до бесконечности.
но все равно решил предупредить невнимательных.
0
Упс, уже написали выше. Да ещё и с примером попроще (и в самом деле, 2566 = 0).
+1
В коде таких предикатов сотни тысяч, 3-5 секунд на штуку — заведомо не приемлимое время (в случае реального применения).
Кроме того, предикат еще надо выявить в размазанном коде и, при этом, не зарезать реальные if'ы (даже с 99% вероятностью невыполнимые).
Кроме того, предикат еще надо выявить в размазанном коде и, при этом, не зарезать реальные if'ы (даже с 99% вероятностью невыполнимые).
0
В коде таких предикатов сотни тысяч, 3-5 секунд на штуку — заведомо не приемлимое время (в случае реального применения).
Шесть дней на приведение кода в читабельное состояние. Копейки, нет?
+1
Так поэтому-то и интересно узнать, как генерировать такие вот сложные предикаты (заранее зная, выполнимый или невыполнимый предикат требуется).
А в случае реального применения, 100000 × 3 секунды (учтите, что у меня старенький нетбук) = 3.5 дня. Несколько недель на взлом программы — не так уж и плохо.
А в случае реального применения, 100000 × 3 секунды (учтите, что у меня старенький нетбук) = 3.5 дня. Несколько недель на взлом программы — не так уж и плохо.
0
По три секунды тратится только на те, которые недоказуемы формальными методами.
Для всех остальных отрабатывает за доли миллисекунды.
Для всех остальных отрабатывает за доли миллисекунды.
+1
Имхо нет особого смысла гнаться за «неявностью» предикатов. Ведь очень сложно (если вообще возможно) объеденить неявность и непросчитываемость условия.
А что мешает пересыпать код большим количеством явных но не просчитываемых условий, сформулированным таким образом чтобы мусор был то then, то в else ветке? Деобфускатор будет понимать что весь код обфусцирован/инструментирован и для каждого конкретного ветвления не сможет определить тру там или фолс. В мусоре будете генерировать дальнейшие ветвления которые будутт похожи на настоящие в абсолютной степени (так как нет требований по просчитываемости).
Если мусор будет не очевидно рандомным, а слегка модифицированным оригинальным кодом + оригинальный код также будет разбавлен мусорными включениями (нейтральными с точки зрения выполнения конечной функции), то деобфусцировать такой код, не будучи уверенным какие части графа достижимы а какие нет, будет весьма сложно
А что мешает пересыпать код большим количеством явных но не просчитываемых условий, сформулированным таким образом чтобы мусор был то then, то в else ветке? Деобфускатор будет понимать что весь код обфусцирован/инструментирован и для каждого конкретного ветвления не сможет определить тру там или фолс. В мусоре будете генерировать дальнейшие ветвления которые будутт похожи на настоящие в абсолютной степени (так как нет требований по просчитываемости).
Если мусор будет не очевидно рандомным, а слегка модифицированным оригинальным кодом + оригинальный код также будет разбавлен мусорными включениями (нейтральными с точки зрения выполнения конечной функции), то деобфусцировать такой код, не будучи уверенным какие части графа достижимы а какие нет, будет весьма сложно
+6
Кстати, я думаю, что генерация мусора вообще не обязательна. В не выполняемых ветках предиката можно просто вставить переход на непредсказуемый участок пользовательского кода (точнее передвинуть этот участок под предикат, чтобы скрытно было). Это также убережёт от раздувания екзешника. В текущей реализации мы так и делаем: выглядит очень ествественно как на уровне IL так и в декомпилированном виде.
0
Не забывайте что программа, кроме обеспечения непосредственно защиты, должна еще продолжать полноценно работать. Приложение сплошь покрытое предикатами по 20..50 операций умножения\деления\возведения в степень каждый, вряд ли будет приемлемо в использовании.
На самом деле, очень перспективной на будущее, видится реализация Opaque Predicates на базе указателей. В статье говориться о том, что эта задача, как и проблема останова, в общем случае, является неразрешимой. А неразрешимая задача всегда лучше NP полной :) Думаю что в ближайшее время мы продолжим наши исследования в этом направлении.
На самом деле, очень перспективной на будущее, видится реализация Opaque Predicates на базе указателей. В статье говориться о том, что эта задача, как и проблема останова, в общем случае, является неразрешимой. А неразрешимая задача всегда лучше NP полной :) Думаю что в ближайшее время мы продолжим наши исследования в этом направлении.
0
Неразрешимость будет, если память бесконечна. Понятное дело, перебирать все состояния памяти не вариант. Но ведь и выделять много памяти для этих предикатов в программу вряд ли захочется. Получается, что неразрешимость тут вообще никаким боком не стоит.
Что более важно, если выбирать произвольный предикат (будь то 3SAT-формула или предикат из любой другой NP-полной задачи), нет никаких гарантий, что данный экземпляр будет сложно решить. Я уверен, что подавляющее большинство случайных предикатов решается на ура. Выше уже писали, что те же 3SAT-формулы (особенно случайные) отлично решаются для достаточно больших размеров.
Я бы предложил попробовать использовать известные считающиеся сложными задачи — например взять какой-нибудь криптографический хэш и его код размазать (т.е. размазать проверку вида sha1(x) = y). Навскидку сложности: придумать, как замаскировать константы хэша; как сделать, чтобы все раунды хэширования выглядели по разному; плюс размер кода может получиться слишком большим для маленькой программы — а что если надо еще и несколько предикатов? (хотя можно попытаться использовать результаты одного и того же хэша).
Что более важно, если выбирать произвольный предикат (будь то 3SAT-формула или предикат из любой другой NP-полной задачи), нет никаких гарантий, что данный экземпляр будет сложно решить. Я уверен, что подавляющее большинство случайных предикатов решается на ура. Выше уже писали, что те же 3SAT-формулы (особенно случайные) отлично решаются для достаточно больших размеров.
Я бы предложил попробовать использовать известные считающиеся сложными задачи — например взять какой-нибудь криптографический хэш и его код размазать (т.е. размазать проверку вида sha1(x) = y). Навскидку сложности: придумать, как замаскировать константы хэша; как сделать, чтобы все раунды хэширования выглядели по разному; плюс размер кода может получиться слишком большим для маленькой программы — а что если надо еще и несколько предикатов? (хотя можно попытаться использовать результаты одного и того же хэша).
0
Неразрешимость будет, если память бесконечна.
Неразрешимость будет даже тогда, когда память потенциально бесконечна. Если генерировать ту самую динамическую структуру в памяти, то, из-за того, что эмуляция локальны, в каждом конкретном участке кода нельзя будет предугадать реальный объём занимаемый структурой. Естественно структура должна быть скрытной, чтобы не было априори известно, что в реальности не так много памяти она занимает.
Если встроить длинную арифметику и Диофантовы уравнения, то так же будет неразрешимость, так как параметры уравнения берутся из случайных даже потенциально сколь угодно больших участков в памяти, например. Но тут нет скрытности и хакер просто вырежет все неявные предикаты.
Я уверен, что подавляющее большинство случайных предикатов решается на ура.
Если сделать генератор, который создаёт предикаты и отсеивает те, которые решились на ура, то уже большинство предикатов не будут так просты.
Возможно я не совсем правильно понял Ваш вариант с хэшом. Как мне кажется эмулятор как раз сделан для того, чтобы проэмулировать вычисление sha1 и понять, что значение всегда такое-то. В этом предложении отсутствует элемент псевдослучайности входных параметров без которого задача решается эмуляцией.
+1
Sign up to leave a comment.
Неявные предикаты