Теория и практика формального моделирования уязвимостей

Краткая версия доклада

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

Построение прикладной модели на основе каких-либо свойств абстрактной модели позволяет, в некоторой степени, доказывать ее свойства на основе уже имеющихся теорем и утверждений. Количество моделей не ограничено, их можно разделить на такие виды, как логические, по предметной области (управление доступом, защищенность приложения, бизнес-логика, верификация), и вычислительные, такие как машина Тьюринга (МТ).

Рассмотрим применимость абстрактных моделей на практике на примере МТ. МТ - абстрактная модель, имеющая бесконечную ячеистую ленту в качестве источника входных и выходных данных, управляющего устройства с конечным числом состояний и таблицы переходов между состояниями. На каждой итерации МТ способна изменить текущую ячейку, перейти в другое состояние и переместиться в соседнюю ячейку. По этой схеме реализуется фильтрующая функция МТ.

Мы можем говорить об успешном окончании анализа и получении результата только после остановки анализатора. Лента МТ бесконечна, это означает существование бесконечного множества неуязвимых конфигураций программы. Однако при этом при анализе веток неуязвимых конфигураций анализатор никогда не достигнет начального состояния и никогда не остановится, если программа неуязвима.

В связи с этим ряд ведущих исследователей, в том числе Михал Залевски, даже пришли к мнению, что формальные модели, построенные на таких допущениях, практически бесполезны. С этим нельзя согласиться, потому что в любой ситуации модель можно упростить, привести ее к такому состоянию, когда она будет работать на реальном приложении. Наш подход был основан на предположении, что в каждый момент времени рассматривается конфигурация нашей машины (позиция считывателя на ленте, содержимое ленты и активное состояние, в котором находится вычислитель). Для реального приложения полным аналогом конфигурации МТ является состояние любых изменяемых потоков данных, доступных в каждой точке потока управления. Соответственно, эту модель можно будет применить к реальному коду, пытаясь таким образом перебирать состояния.

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

Модель потока вычисления позволяет разрешать элементы множества значений входных данных по заданному состоянию и определять состояние по заданному множеству значений входных данных. Для моделирования уязвимостей модели потока вычислений требуется конкретизация понятия "уязвимое состояние" в зависимости от рассматриваемого класса атак. Один из возможных подходов к конкретизации, применимый в МТ, заключается в сопоставлении аргументов опасных операций со множествами значений возможных эксплоитов.

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

Применяя сформулированный критерий инъекции мы рассмотрим технологию виртуального патчинга (virtual patching), позволяющую защитить веб-приложение от эксплуатации имеющихся в нем известных уязвимостей на уровне межсетевого экрана уровня веб-приложений (web application firewall (WAF) - выделенное решение, функционирующее на отдельном узле, между шлюзом во внешнюю сеть и веб-сервером), определяя атакующие HTTP-запросы. Дальнейшим развитием технологии стала идея runtime virtual patching - совмещение идей WAF и статанализатора, при которой последний строит полную модель потока вычисления приложения и передает ее WAF. WAF при обработке каждого HTTP-запроса подставляет его параметры в формулу модели, вычисляет значения ее состояний и анализирует их.

Кроме того, существует также библиотека LibProtection с открытым под MIT-лицензией кодом, позволяющая разработчикам полностью автоматизировать защиту от атак инъекций по достаточному критерию и реализовывать защиту по необходимому критерию. Библиотека может применяться для быстрого патчинга уязвимого кода, использующего форматные и интерполированные строки, а также для защиты кода там, где форматные строки или интерполяция неизбежны.