Неявные предикаты

    Речь здесь пойдёт о некоторых аспектах компьютерной безопасности, связанных с запутыванием кода программы. Именно это мне было интересно в связи с разработкой обфускатора .NET приложений – программы для защиты .NET кода от взлома. Есть и другая – тёмная сторона: запутыванием кода очень интересуются разработчики вирусов и других нехороших штук, но нам они неинтересны.


    Эмуляторы


    Итак, Вы придумали супер алгоритм для запутывания кода программы. При декомпиляции код выглядит просто вырвиглазно и никто точно такое анализировать не будет. Казалось: победа! Но нет. Естественно обфусцированный код никто анализировать не будет… руками. Хакер поймёт как вы код запутывали и напишет «распутывалку». Если Ваш алгоритм был достаточно силён, то хакеру придётся писать собственный эмулятор, но и это не такая проблема как может показаться на первый взгляд – в сети есть доступные эмуляторы и даже специально написанные именно для целей взлома.

    Из теории компьютерных наук известно, что не существует и никогда не будет существовать алгоритма, определяющего остановится ли программа или будет работать вечно – так называемая «проблема останова». Это гарантирует, что хакерский эмулятор, распутывающий обфусцированную программу, будет делать это как бы «локально»: он не сможет узнать состояние и значение всех переменных, задействованных в каждом участке кода и поэтому в точках условного ветвления часто будет полагать, что возможны все варианты хода программы. Вот тут-то на ум и приходит решение: запутанный код будет наполнен переходами по условиям, которые будут всегда истинны, но проэмулировать и понять это будет трудно. Примерно вот так:

    if ((x+x & 1) == 0)
      good_code
    else
      мусор
    


    «Но это же как раз одна из тех запутывалок, которые хакер и собирается обходить с помощью эмулятора» — скажете Вы и будете правы. А что если придумать тысячу подобных фокусов? О, это решение, если у Вас есть легион программистов, каждый из которых придумывает трюки не похожие на трюки других. В реальности это не так. В реальности Вы думаете неделю и придумываете тридцать трюков, а хакер смотрит на код один день и находит все тридцать трюков, потому что тридцать – это не так уж много.


    В области, связанной с запутыванием кода, тождественно истинные условные выражения называются «неявными предикатами» (оригинальный термин «opaque predicates»). Далее буду использовать слова «предикат» и «условие» как синонимы. Тема эта придумана давно и я, честно, не знаю кто исходный автор, должно быть фольклор. Несколько видных статей по предикатам:



    Идеальный генератор неявных предикатов


    Сформулируем как должен выглядеть эдакий идеальный супер генератор неявных предикатов. Он создаёт предикаты P(x1,x2,…,xn), зависящие от переменных x1,x2,…,xn, причём может создавать как тождественно истинные, так и не всегда истинные предикаты в зависимости от желания пользователя генератора. И генератор обладает следующими фантастическими характеристиками:

    1. предикат генерируется за линейное время от длины;
    2. предикат очень похож на обычное условие из обычной программы (скрытность);
    3. не существует и не может существовать (!) алгоритма, который определял бы, что предикат сгенерирован нашим генератором;
    4. не существует и не может существовать (!) алгоритма, который по сгенерированному предикату мог бы определить всегда он истинный или существуют входные параметры на которых он ложный;
    5. не существует вероятностного алгоритма, который верно определял бы в среднем по меньшей мере в 80% случаев (цифра найдена методом научного тыка), является ли созданный генератором предикат тождественно истинным.

    Теперь надо понять возможна ли хотя бы теоретически такая штука.

    Пункт 4, похоже, возможен. Напомню, что Диофантово уравнение – это уравнение вида f(x1, x2, …, xn) = 0, где f — многочлен с целочисленными коэффициентами, а иксы — целые неотрицательные числа. Опять обращаясь к теории компьютерных наук, вспоминаем, что не существует и не может существовать алгоритма, который по любому Диофантову уравнению определял бы имеет оно решение или нет. В частности, по великой теореме Ферма, Диофантово уравнение (x+1)*(x+1)*(x+1) + (y+1)*(y+1)*(y+1) — (z+1)*(z+1)*(z+1) = 0 не имеет решений. Казалось: вот куда надо копать! Но не спешите. Диофантово уравнение – это вовсе не набор сумм и произведений интов со значениями от 0 до 4 млрд, а набор сумм и произведений целых чисел со значениями от 0 до бесконечности. Вам придётся записывать их с помощью так называемой «длинной арифметики» и выглядеть они будут в коде весьма странно.

    Пункт 2 всем мешает. Интуитивно скрытным мы называем предикат, который не выделяется в толпе настоящих, «ненеявных» предикатов из настоящих программ. Умные люди уже проанализировали много типичных приложений и нашли, что большая часть предикатов в них совсем незамысловата: x == 0, x == y, x > 0 и т.д., где x, y – интовые переменные (во второй из приведённых выше статей умные люди как раз между делом анализируют условия типичных java программ). Не нужно долго гадать, чтобы понять, что условие скрытности очень важно для предикатов. Действительно, хакер может просто найти все «странные» предикаты и как-то обособить их или вообще удалить, что нам совсем не нужно.

    Пункт 4 невозможен из-за пункта 2… хотя. Итак, если предикат является арифметическим и он «скрытен», то в нём скорее всего задействована только арифметика с интами, а значит существует алгоритм, который проверит является ли предикат всегда истинным: достаточно просто перебрать все значения интов, входящих в предикат. Но и это неплохо, ведь в лучшем случае для анализа предиката придётся перебрать 4 миллиарда значений! А если переменных в предикате две? Значит мы с чистой совестью, полагая, что P<NP, ослабим четвёртую характеристику генератора: задача выявления того факта, что созданный генератором предикат всегда истинен, должна быть NP-полной. Конечно, если окажется, что P=NP, то это тоже вряд ли вариант, но пока можно спать спокойно. Тут вспоминается 3-SAT – известная NP-полная задача, которую сам Бог велел вспомнить на этом моменте. Но предикаты, получающиеся на этом пути, едва ли можно назвать скрытыми.

    Пункты 1, 3 и 5 обойдём молчанием – слишком тонкий вопрос для короткой статьи.

    Граф выполнения программы


    Арифметическими предикатами будем называть предикаты, вида f(x1,…,xn) < g(x1,…xn) или f(x1,…,xn) == g(x1,…,xn), где все иксы имеют тип инт, а f и g – обычные арифметические выражения. Почему же предикат должен быть обязательно арифметическим? Нет, не должен и даже не утверждаю, что в тексте ниже я смогу Вас убедить, что должен. Тем не менее приведу соображения, которые привели меня к мысли, что арифметические предикаты наиболее реальны.

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

    Является ли арифметический предикат неявным (то есть всегда истинным)? Это NP-полная задача. На что указывает данный указатель в данном месте программы? Это неразрешимая задача, то есть нет общего алгоритма для решения такого вопроса, как и в случае проблемы останова. Вот и прекрасно: неразрешимая лучше, чем NP-полная. Следующая идея способа построения неявных предикатов почерпнута из второй статьи, приведённой выше (Collberg, Clark, Low).

    Давайте, раз мы обладаем графом выполнения, раскидаем по программе незаметный код, строящий и модифицирующий где-то в памяти какую-то достаточно сложную динамическую структуру. Это действительно может быть незаметно: кто знает, что там потребовалось записать в память?
    И мы будем знать в каждой конкретной точке программы каково состояние структуры и на что указывают содержащиеся в ней указатели.
    На основе этих знаний мы втыкаем неявные предикаты и мёртвый код под неявными предикатами, который вызывает какие-то части программы, которые модифицируют нашу скрытую структуру.
    В итоге хакер уже не обладает нашими знаниями о структуре, если только он не решит неразрешимую проблему разрешения указателей.
    Рассмотрим игрушечный пример. Пусть часть исходного графа выполнения программы имеет вид:

    В обфусцированной программе мы формируем в памяти дико сложную структуру, состоящую из одного четырёхбайтового числа и указателя на это число. Пусть p – это указатель. Пусть при входе в левый нарисованный кусок графа (*p) гарантированно равно 1. Граф модифицируется так:

    Если и раньше выяснение того, что *p == 1 могло быть сопряжено с трудностями, то теперь дополнительно можно сделать неверное предположение по этому куску, что иногда *p == 7 и в левой части рисунка.

    Это хороший метод и он лучше, чем арифметические предикаты. Но есть одно большое НО: в реальности мы как и хакер не знаем граф выполнения. Всё этот подлый рефлекшн, коллбэки/делегаты и прочие непредсказуемые пути выполнения кода. А если код генерируется в памяти? Да, такое тоже бывает и особенно в .NET. Тем не менее мы знаем граф выполнения локально. В .NET, как минимум, можно быть уверенным в графе выполнения кода внутри каждого конкретного метода. Но если Вы вставите создание и построение некой структуры в памяти в каждый метод, то едва ли это будет скрытным. Вот так скрытность, а точнее её отсутствие, мешает нам использовать этот метод.

    Есть и иные методы построения неявных предикатов, но все они (те, что я слышал краем уха) завязаны на графе выполнения всей программы и выглядят громоздко в контексте одного метода. Другое дело арифметические предикаты.

    Реализация


    В идеальном генераторе неявных предикатов есть ещё один большой плюс: алгоритм работы Вашего генератора не должен быть секретным! Наша реализация генератора, к сожалению, не совсем идеальна, и раскрывать всех деталей реализации нашего алгоритма мы пока не будем. Впрочем, я не нашёл у кого-то даже близкого к идеальному генератора. Тема очень интересная, и я был бы рад продолжить ее обсуждение в комментариях.

    Ниже приведены некоторые результаты работы нашего генератора неявных предикатов. Выдержки из начала, середины и конца списка предикатов (3000 штук; приоритет операций как в с# ~; * / %; + -; « »; &; ^; |; все переменные int):

    			~x != x
    			(x + x & 1) == 0
    			(x + -x & 1) == 0
    			~x != x * 4u >> 2
    			(-x & 1) == (x & 1)
    			((-x ^ x) & 1) == 0
    			(x * 0x80 & 0x56) == 0
    			(x << 1 ^ 0x1765) != 0
    			~(-x * 0x40) != x << 6
    			(~(x * 0x80) & 0x3d) == 0x3d
    			x - 0x9d227fa9 != x - 0x699c945e
    			(y ^ y - 0x35f5f4d2) != 0x42a26409
    			(x * 0x20000000 & 0x19a27923) == 0
    			(int)(y * 9u + y * 0xf7u >> 3) >= 0
    			(x * 4 & 8) == (x + x * 3 - 0x1fef9d8f & 8)
    			(x | 0xffffdbe8) - 0x1baa != x || (x & 0x10) == 0x10
    			(x ^ 0x1145f) != 0 || (x | 0xfffeffff) == 0xffffffff
    			(uint)x / 0x59d7e3 != 0x90298cf9 || (x * 3 + x & 3) == 0
    			((uint)x % 0x38 + 0xe4df62c8 & 0x6d755e00) == 0x64554200
    			(x ^ 0x770363c6) != 0 || ((uint)x >> 0x19 ^ 0x926797eb) != 0
    			(uint)y / 0x2369af8 - 0x78400000 != (uint)x / 0x1f2ce * 0x10
    			(x & 0x8e3ef800) != 0x70641deb && (uint)x / 0x9388ea != 0x3ab6921c
    


    Автор публикации: Дмитрий Косолобов, разработчик Appfuscator.
    AdBlock похитил этот баннер, но баннеры не зубы — отрастут

    Подробнее
    Реклама

    Комментарии 31

      0
      if ((x*x & 1) == 0)
        good_code
      else
        мусор
      

      А разве подобные вещи компилятор не должен оптимизировать? Или в данном случае (.NET) вы полностью или частично компилируете в байт-код сами?
        +2
        Вроде проблема именно в том, чтобы подставить в ((x*x & 1) == 0) достаточно сложное условие, чтобы понять, что оно всегда true — «сложно» для взломщика и невозможно для компилятора.
        Невозможно всегда с уверенностью на 100% узнать, будет ли условие всегда true или она всегда false или могут быть разные варианты, без того, чтобы собственно выполнить программу («проблема останова»)
          +1
          Откуда кстати взяли, что ((x*x & 1) == 0) всегда истинно?
          Берем x=1, получаем ложное. Для любого нечетного x выражение будет ложное.
            0
            Наверное, имелось ввиду, что это оптимизируется до (x & 1) == 0
              0
              В примере if ((x*x & 1) == 0) надо заменить на if ((x+x & 1) == 0) я опечатался и вместо плюс написал умножить
                0
                Не забывайте что программа, кроме непосредственно обеспечения самой защиты, должна еще продолжать работать :) Приложение, которое сплошь покрыто предикатами по 20..50 операций умножения\деления\возведения в степень каждый, вряд ли будет приемлемо в использовании.

                На самом деле, очень перспективной на будущее, видится реализация Opaque Predicates на базе указателей. В статье упоминается, что эта задача считается неразрешимой, что еще лучше NP полноты :) Думаю в ближайшее время мы продолжим наши исследования в этом направлении.
              +4
              Если x, y и z типа float, я бы не был так спокоен за диск C.
                +1
                В статье подчеркивается, что уравнения целочисленные.
                  0
                  Если ограничиться unsigned int, сойдут и x=y=z=256. Но да, в статье говорится, что нужно юзать bignum
                    0
                    bignum в неявном виде, т.е. логику частей большого целого числа можно замаскировать в большой динамической куче данных и распределить по коду.
                +1
                На сколько в среднем падает производительность зашифрованного кода и вырастает потребление памяти?
                  +1
                  Замедление на нашем синтетическом тесте с большим объемом кода примерно в 1.2 раза, в реальной программе должно получиться еще меньше. Потребление памяти фактически никак не меняется, т.к. в предикатах используются переменные из пользовательского кода.
                  +3
                  Так говорите, для решения надо все инты перебрать?
                  у меня для вас плохие новости
                  (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
                    0
                    в последнем тоже True, там код недописан конечно же, но имея достаточно времени можно решить всё.
                      +1
                      В статье говориться
                      Наша реализация генератора, к сожалению, не совсем идеальна

                      Мы не претендуем на 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
                        0
                        Спасибо за Ваш комментарий, ответил на вопрос atd чуть выше
                        +3
                        Давайте посмотрим, сколько секунд понадобится 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)

                        Дайте что-ли ради интереса что-нибудь из прошлого варианта, для чего «гарантировано не получилось бы написать распознаватель».
                          0
                          Некоторые примеры предикатов из первой версии генератора:

                          "(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)"
                            +1
                            Это же 3SAT. Если не ошибаюсь, его уже давно научились решать для сотен, если не тысяч, переменных (с вероятностью решения более 80%). Так что текущее направление более перспективное.
                          0
                          Кстати, очень не советую встраивать предикат из картинки в начале поста в свою программу:

                          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 до бесконечности.

                          но все равно решил предупредить невнимательных.
                            +1
                            Упс, уже написали выше. Да ещё и с примером попроще (и в самом деле, 2566 = 0).
                              0
                              В коде таких предикатов сотни тысяч, 3-5 секунд на штуку — заведомо не приемлимое время (в случае реального применения).

                              Кроме того, предикат еще надо выявить в размазанном коде и, при этом, не зарезать реальные if'ы (даже с 99% вероятностью невыполнимые).
                                +1
                                В коде таких предикатов сотни тысяч, 3-5 секунд на штуку — заведомо не приемлимое время (в случае реального применения).

                                Шесть дней на приведение кода в читабельное состояние. Копейки, нет?
                                  0
                                  Так поэтому-то и интересно узнать, как генерировать такие вот сложные предикаты (заранее зная, выполнимый или невыполнимый предикат требуется).

                                  А в случае реального применения, 100000 × 3 секунды (учтите, что у меня старенький нетбук) = 3.5 дня. Несколько недель на взлом программы — не так уж и плохо.
                                    +1
                                    По три секунды тратится только на те, которые недоказуемы формальными методами.
                                    Для всех остальных отрабатывает за доли миллисекунды.
                                  +6
                                  Имхо нет особого смысла гнаться за «неявностью» предикатов. Ведь очень сложно (если вообще возможно) объеденить неявность и непросчитываемость условия.

                                  А что мешает пересыпать код большим количеством явных но не просчитываемых условий, сформулированным таким образом чтобы мусор был то then, то в else ветке? Деобфускатор будет понимать что весь код обфусцирован/инструментирован и для каждого конкретного ветвления не сможет определить тру там или фолс. В мусоре будете генерировать дальнейшие ветвления которые будутт похожи на настоящие в абсолютной степени (так как нет требований по просчитываемости).

                                  Если мусор будет не очевидно рандомным, а слегка модифицированным оригинальным кодом + оригинальный код также будет разбавлен мусорными включениями (нейтральными с точки зрения выполнения конечной функции), то деобфусцировать такой код, не будучи уверенным какие части графа достижимы а какие нет, будет весьма сложно
                                    0
                                    Кстати, я думаю, что генерация мусора вообще не обязательна. В не выполняемых ветках предиката можно просто вставить переход на непредсказуемый участок пользовательского кода (точнее передвинуть этот участок под предикат, чтобы скрытно было). Это также убережёт от раздувания екзешника. В текущей реализации мы так и делаем: выглядит очень ествественно как на уровне IL так и в декомпилированном виде.
                                    0
                                    Не забывайте что программа, кроме обеспечения непосредственно защиты, должна еще продолжать полноценно работать. Приложение сплошь покрытое предикатами по 20..50 операций умножения\деления\возведения в степень каждый, вряд ли будет приемлемо в использовании.

                                    На самом деле, очень перспективной на будущее, видится реализация Opaque Predicates на базе указателей. В статье говориться о том, что эта задача, как и проблема останова, в общем случае, является неразрешимой. А неразрешимая задача всегда лучше NP полной :) Думаю что в ближайшее время мы продолжим наши исследования в этом направлении.
                                      0
                                      Неразрешимость будет, если память бесконечна. Понятное дело, перебирать все состояния памяти не вариант. Но ведь и выделять много памяти для этих предикатов в программу вряд ли захочется. Получается, что неразрешимость тут вообще никаким боком не стоит.

                                      Что более важно, если выбирать произвольный предикат (будь то 3SAT-формула или предикат из любой другой NP-полной задачи), нет никаких гарантий, что данный экземпляр будет сложно решить. Я уверен, что подавляющее большинство случайных предикатов решается на ура. Выше уже писали, что те же 3SAT-формулы (особенно случайные) отлично решаются для достаточно больших размеров.

                                      Я бы предложил попробовать использовать известные считающиеся сложными задачи — например взять какой-нибудь криптографический хэш и его код размазать (т.е. размазать проверку вида sha1(x) = y). Навскидку сложности: придумать, как замаскировать константы хэша; как сделать, чтобы все раунды хэширования выглядели по разному; плюс размер кода может получиться слишком большим для маленькой программы — а что если надо еще и несколько предикатов? (хотя можно попытаться использовать результаты одного и того же хэша).
                                        +1
                                        Неразрешимость будет, если память бесконечна.

                                        Неразрешимость будет даже тогда, когда память потенциально бесконечна. Если генерировать ту самую динамическую структуру в памяти, то, из-за того, что эмуляция локальны, в каждом конкретном участке кода нельзя будет предугадать реальный объём занимаемый структурой. Естественно структура должна быть скрытной, чтобы не было априори известно, что в реальности не так много памяти она занимает.

                                        Если встроить длинную арифметику и Диофантовы уравнения, то так же будет неразрешимость, так как параметры уравнения берутся из случайных даже потенциально сколь угодно больших участков в памяти, например. Но тут нет скрытности и хакер просто вырежет все неявные предикаты.

                                        Я уверен, что подавляющее большинство случайных предикатов решается на ура.

                                        Если сделать генератор, который создаёт предикаты и отсеивает те, которые решились на ура, то уже большинство предикатов не будут так просты.

                                        Возможно я не совсем правильно понял Ваш вариант с хэшом. Как мне кажется эмулятор как раз сделан для того, чтобы проэмулировать вычисление sha1 и понять, что значение всегда такое-то. В этом предложении отсутствует элемент псевдослучайности входных параметров без которого задача решается эмуляцией.

                                    Только полноправные пользователи могут оставлять комментарии. Войдите, пожалуйста.

                                    Самое читаемое