Введение
Тема SAST (static application security testing) довольно актуальна: многие хотят выявлять проблемные и уязвимые места в приложении еще на этапе разработки, когда стоимость их правок и риски относительно скромны.
Для анализа исходного кода применяются разные технологии и алгоритмы: от менее точных, но быстрых, до всеобъемлющих, но длительных. Ниже мы будем рассматривать один из них — абстрактную интерпретацию, а если точнее, то символьное выполнение. Подробное описание технологий можно найти по ссылкам:
Symbolic Execution 17-355/17-665/17-8190: Program Analysis (Spring 2018)
Ищем уязвимости в коде: теория, практика и перспективы SAST
Abstract interpretation, Wikipedia
Если вкратце, под абстрактной интерпретацией кода подразумевают интерпретацию без его конкретного выполнения для сбора информации о семантике кода (потоках передачи данных, потоках передачи управления и т. д.). Если же при абстрактной интерпретации все входные данные — аргументы функции точек входа, обращение к файловой системе, к внешним сервисам и т. д. — считать неизвестными, помечая их как символьные значения, то полученная надстройка будет называться символьным выполнением. В качестве примера см. рис. 1, где в восьмой строчке у переменной указаны два возможных значения в зависимости от символьного значения входного аргумента.
Чтобы говорить на одном языке, введем следующие термины:
- Вариантом мы будем называть пару
где 
— некое значение, а 
— условие достижимости этого значения. Обозначать будем как 
- Вариативным множеством будем называть множество вариантов и обозначать как:
Применение этих терминов см. на рис. 2:
Скорость роста
В тот момент, когда формируется некоторое выражение языка, состоящее из подвыражений/переменных (например, конкатенация), которым соответствуют какие-то вариативные множества (рис. 3), количество вариантов итогового выражения растет с огромной скоростью. Если быть точнее, то скорость роста — не что иное, как экспоненциальная функция:
вариативные множества: 
мерная функция языка (например конкатенация, вызов функции от 
аргументов), в частности определенно 
Введем отображение 
, которое элемент декартового произведения вариативных множеств переводит в вариант, как показано на рисунке 4. Тогда все образы этого отображения формируют вариативное множество По построению следует, что количество элементов в множестве образов равно числу элементов в множестве декартового произведения вариативных множеств, коих экспоненциальное число:
Экспоненциальное количество вариантов сильно сказывается на времени выполнения алгоритма анализа, которое вместо желаемых минут может достигать нескольких часов, дней, недель или лет. В реальности мы не готовы так долго ждать завершения анализа и хотим получить результат как можно быстрее. Но, к сожалению, экспоненциальный рост— фундаментальная проблема такого алгоритма, и в общем случае с этим ничего нельзя поделать. Но это не значит, что мы совсем бессильны.
Пути решения
Давайте введем 
— функцию, фильтрующую ложные варианты, тогда
В дальнейшем для упрощения записи будем опускать написание :
«Совпадение»
Предположим, что все рассматриваемые вариативные множества совпали, как показано на рис. 5, то есть
Такие случаи будем называть «совпадение».
Тогда мы утверждаем, что количество выводимых вариантов, когда вариативные множества удовлетворяют случаю «совпадение», линейное, а не экспоненциальное:
Вариативному множеству 
соответствует некоторое выражение языка, которое в конкретный момент времени при реальном исполнении имеет ровно одно значение, тогда как при символьном выполнении оно имеет одно значение при конкретном условии. Это достигается за счет наличия операций присвоения/перезаписи (это касается переменных, а выражения, содержащие переменные, естественным образом это распространяют), в силу которых все предыдущие значения теряют смысл при текущем условии при символьном выполнении (но могут иметь место при отрицании условия присвоения). Если зафиксировать некоторый вариант из вариативного множества, то есть какое-то значение для соответствующего выражения языка, то каждая проекция кортежа 
может быть только этим зафиксированным вариантом. Всего можно зафиксировать 
штук таких вариантов, откуда и следует утверждение.
«Условность»
В предыдущем случае никак не использовалось совпадение значений вариантов; давайте попробуем от этого отказаться и будем считать, что вариативные множества не равны, но условные множества этих вариантов (множество условий всех вариантов в вариативном множестве 
) равны (см. рис. 6 и 7). То есть
Такие случаи будем называть «условность».
Для дальнейших формулировок нам потребуется следующее свойство, которое мы будем называть теоремой о вариантах:
Для 
— очевидно верно. Рассмотрим 
Вариативное множество из двух элементов получается двумя последовательными присвоениями в переменную под некоторыми условиями. Пусть, не умоляя общности, первое присвоение значения 
безусловное. После него вариативное множество будет 
Пусть второе присвоение значения 
будет под условием 
. Тогда при выполнении присвоения все предыдущие значения вариантов вариативного множества перестают иметь смысл при условии текущего присвоения и имеют место тогда и только тогда, когда текущее присвоение не свершилось (не наступило условие этого присвоения) ⇒ условия предыдущих вариантов дополняются отрицанием текущего 
где видно, что условия противоречивы.
Пусть 
Сделаем присвоение в соответствующую переменную значения 
при условии . Как было сказано ранее, при записи значения все предыдущие варианты вариативного множества имеют место тогда и только тогда, когда текущее присвоение не свершилось. Тогда получаем новое вариативное множество 
где первые элементов противоречивы по условию изначальному, а 
элемент противоречит всем остальным в силу перезаписи под условием , что и требовалось доказать (случай, когда вариативное множество есть комбинация других вариативных множеств как некое выражение языка с подвыражениями, естественным образом распространяется из доказательства выше и вида отображения ).
Теперь мы утверждаем, что количество выводимых вариантов, когда вариативные множества удовлетворяют случаю «условность», тоже линейное, а не экспоненциальное:
Будем
считать этот факт «звездочкой» в рамках текущего доказательства. По условию же имеем, что
Будем считать этот факт «двумя звездочками».
Возьмем некоторое вариативное множество 
и зафиксируем в нем некоторый вариант, как показано на рис. 8. Затем рассмотрим все образы отображения , где в конъюнкциях и в подстановке в функцию языка 
позициях будет зафиксированный вариант, как показано на все том же рис. 8.
По факту «звездочка» имеем, что любые два неравных варианта в любом вариативном множестве, в частности , имеют противоречивое условие (см. рис. 9). По факту «две звездочки» имеем, что зафиксированный вариант, точнее условие зафиксированного варианта, лежит в условных множествах любого рассматриваемого вариативного множества (см. рис. 10).
Тогда получаем, что зафиксированное условие будет противоречиво любому другому условию из условного множества любого вариативного множества и все конъюнкции будут заведомо ложными за исключением только одной, где все операнды — зафиксированное условие. Это равноценно взятию в каждом вариативном множестве варианта, условием которого является условие изначально зафиксированного варианта. Конечно, эта единственная конъюнкция будет выводима тогда и только тогда, когда зафиксированное условие само не ложно.
Изначально в вариативном множестве был зафиксирован один конкретный вариант; а таких вариантов можно зафиксировать ровно столько, сколько элементов в вариативном множестве, то есть штук, что и требовалось доказать.
«Черпак»
Теперь же предположим, что вариативные множества не равны, их условные множества тоже не равны, у них разное количество вариантов, но все условные множества имеют непустое пересечение, как показано на рис. 11 и 12. То есть
Такие случаи будем называть «черпак».
Тогда мы утверждаем, что количество выводимых вариантов, когда вариативные множества удовлетворяют случаю «черпак», тоже не экспоненциальное, но меньшее значение, что есть сумма:
Будем считать этот
факт «звездочкой». Дальнейшее доказательство этого
утверждения будем разбивать на два независимых случая, а после их объединять.
Давайте возьмем некоторое вариативное множество и зафиксируем в нем некоторый вариант, как показано на рисунке 13. Затем рассмотрим все образы отображения , где в конъюнкциях и в подстановке в функцию языка позициях будет зафиксированный вариант, как показано на все том же рисунке 13.
Пусть условие зафиксированного варианта лежит в общем множестве условий — будем считать это первым случаем доказательства.
Из того, что зафиксированный вариант, точнее условие зафиксированного варианта, лежит в общем множестве условий, следует, что это условие также будет лежать в условных множествах любого рассматриваемого вариативного множества по факту «звездочка», как показано на рис. 14.
Согласно теореме о вариантах имеем, что любые два условия неравных вариантов в любом вариативном множестве противоречивы. Учитывая это и ранее изложенный факт, что зафиксированное условие лежит в условных множествах любого рассматриваемого вариативного множества, получаем, что зафиксированное условие будет противоречиво любому другому условию из условного множества любого вариативного множества и все конъюнкции (см. рис. 15) будут заведомо ложными, за исключением только одной, где все операнды — зафиксированное условие. Это равноценно взятию в каждом вариативном множестве варианта, условием которого является изначально зафиксированный вариант. Конечно, эта единственная конъюнкция будет выводима тогда и только тогда, когда зафиксированное условие само не ложно.
Изначально в вариативном множестве был зафиксирован один конкретный вариант, условие которого лежит в общем множестве условий. Таких вариантов можно зафиксировать ровно столько, сколько элементов в общем множестве условий. Отсюда следует, что левое слагаемое суммы утверждения доказано.
Теперь рассмотрим второй случай, когда условие зафиксированного варианта в вариативном множестве не лежит в общем множестве условий. Все так же рассмотрим все образы отображения , где в конъюнкциях и в подстановке в функцию языка позициях будет наш зафиксированный вариант, как было в первом случае.
По факту «звездочка» имеем, что любое условие из общего множества условий лежит в условных множествах любого рассматриваемого вариативного множества, как показано на рисунке 16. А применив теорему о вариантах к зафиксированному варианту, получим, что условие зафиксированного варианта будет противоречиво любому другому условию неравного варианта в вариативном множестве .
Тогда по указанному выше следует, что условие зафиксированного варианта будет противоречиво любому условию из общего множества условий. Из этого вытекает, что все конъюнкции будут заведомо ложными тогда, когда во всех вариативных множествах, кроме вариативного множества , взяли вариант, условие которого лежит в общем множестве условий, как показано на рисунке 17.
Следовательно, возможно выводимые варианты можно получить тогда, когда во всех вариативных множествах, кроме вариативного множества , взяли варианты, чьи условия не лежат в общем множестве условий. Количество таких вариантов для каждого вариативного множества есть разность общего числа вариантов и числа элементов в общем множестве условий, когда общее количество комбинаций есть произведение этих разностей.
Изначально в вариативном множестве был зафиксирован один конкретный вариант, условие которого не лежит в общем множестве условий. Количество же таких вариантов, которые можно зафиксировать, есть разность общего количества элементов в вариативном множестве и количества элементов в общем множестве. Отсюда следует, что правое слагаемое суммы утверждения также доказано. Объединив два случая, получим ту самую сумму, которую требовалось доказать.
Результаты
Описанные выше утверждения были применены в анализаторе исходного кода PT Application Inspector от Positive Techologies. В таблице ниже время сканирования исходной версией PT Application Inspector без применения описанных случаев считается за 
Реализация описанных случаев ускорила работу алгоритма анализа в среднем в 2,5 раза за счет уменьшения количества перебираемых вариантов: мы исключили заведомо недостижимые и ложные. Соответственно, не тратили время и на их постобработку. Стоит отметить, что по ряду технических и исторических причин на момент реализации эти случаи не могли быть полностью покрыты в PT Application Inspector. Из-за этого показанные результаты не в полной мере отображают то, насколько можно ускорить алгоритм анализа за счет наших утверждений.
По определенным причинам мы не можем показать какие-то другие случаи, если они возможны, но скажем, что да, они возможны.
