Любую ли уязвимость можно устранить?

Спросили тут, какие мои доказательства, что любая уязвимость приложения поддается устранению. И, вроде бы очевидная хрень, но ведь «очевидная хрень» ≠ «доказательство». Да и уязвимости можно же по-разному трактовать. Устранить ту же уязвимость бизнес-логики, не поломав при этом саму бизнес-логику, возможно далеко не всегда. Но, тогда, какие уязвимости поддаются устранению, а какие — нет? Хорошо бы в этом разобраться.

А, значит, пора вспомнить теорию вычислений.

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

1. Определения

Программа P — частично-рекурсивная функция φ_P : Σ* ⇀ Σ* над конечным алфавитом Σ. Расширенная модель (для анализа состояний и трасс): P порождает множество бесконечных последовательностей состояний Executions(P) ⊆ Σ\_ω.

Уязвимость (определение A, поточечное) есть разрешимый предикат Bad ⊆ Σ* × Σ*, где Bad(x, y) истинно, если выход y на входе x составляет «нежелательное поведение» в терминах модели угроз (аварийное завершение, выход за границы буфера, запуск вредоносного кода и т.д.). Предикат Bad фиксирован моделью угроз и не зависит от текста программы — он определяет, какие пары вход-выход считаются опасными, безотносительно того, какая именно программа этот выход произвела.

Уязвимость (определение B, трассовое): нарушение свойства безопасности (safety property) в смысле Алперна и Шнайдера: множество «плохих» конечных префиксов, таких что если префикс содержит «плохое событие», то любое продолжение также его содержит. Формально: свойство Φ является safety-свойством, если ∀σ ∉ Φ, ∃i < |σ| : ∀τ, σ|\_i · τ ∉ Φ.

Уязвимость (определение C, семантическое): нарушение произвольного нетривиального семантического свойства S программ (т.е. S зависит только от вычисляемой функции, а не от текста программы). По теореме Райса, такие свойства неразрешимы — не существует алгоритма, определяющего по тексту программы, обладает ли она свойством S. Однако неразрешимость распознавания свойства и невозможность конструирования программы с заданным свойством — это разные утверждения, и второе требует отдельного доказательства.

Устранение уязвимости. Говорим, что в программе Q устранена уязвимость программы P, если:

• ∀x ∉ Vuln\_P : φ\_Q(x) ≃ φ\_P(x) — идентичное поведение на безопасных входах (включая расхождение: если φ_P(x) не определено и x ∉ Vuln_P, то φ_Q(x) тоже не определено);
• ∀x ∈ Vuln_P : φ_Q(x) определено ∧ ¬Bad(x, φ_Q(x)) — на уязвимых входах Q останавливается с безопасным выходом;

где Vuln_P = {x | φ_P(x) определено ∧ Bad(x, φ_P(x))}.

Символ ≃ означает совпадение частичных функций (по Клини): обе стороны одновременно определены и равны, или обе не определены.

2. Теорема 1 (о поточечных уязвимостях)

Поточечные уязвимости всегда устранимы

Формулировка. Пусть уязвимость задана разрешимым предикатом Bad(x, y), и пусть safe : Σ* → Σ* — вычислимая тотальная функция «безопасного ответа», удовлетворяющая условию ∀x : ¬Bad(x, safe(x)). Тогда существует вычислимая программа Q такая, что в Q устранена уязвимость P.

Доказательство. Определим Q следующим алгоритмом:

Q(x):
  y ← P(x)
  if Bad(x, y):
    return safe(x)
  else:
    return y

Поскольку P вычислима (частично-рекурсивна) и Bad разрешим, композиция этих операций также вычислима. Покажем, что Q удовлетворяет определению устранения уязвимости:

• Вычислимость: Q — частично-рекурсивная функция как композиция вычислимых операций.
• Совпадение с P на безопасных входах: если x ∉ Vuln_P, то либо φ_P(x) не определено (тогда Q(x) расходится на шаге y ← P(x), т.е. φ_Q(x) тоже не определено), либо φ_P(x) = y и ¬Bad(x, y) (тогда Q возвращает y). В обоих случаях φ_Q(x) ≃ φ_P(x).
• Безопасность на уязвимых входах: если x ∈ Vuln_P, то φ_P(x) определено, значит y ← P(x) завершается. Далее Bad(x, y) истинно, и Q возвращает safe(x). По условию на safe: ¬Bad(x, safe(x)), значит ¬Bad(x, φ_Q(x)). ∎

Замечание о существовании safe. Условие ∀x : ¬Bad(x, safe(x)) не является ограничительным на практике: поскольку Bad разрешим и нетривиален (существуют безопасные выходы), для большинства моделей угроз такую safe можно предъявить явно — например, safe(x) = ε (пустая строка) или safe(x) = сообщение об ошибке, если модель угроз не считает аварийное завершение уязвимостью.

3. Теорема 2 (о трассовых уязвимостях)

Трассовые уязвимости устранимы через программу-монитор

Формулировка. Пусть уязвимость определена как нарушение safety-свойства Φ (в смысле Алперна–Шнайдера) на трассах исполнения, и пусть автомат безопасности A_Φ для данного свойства имеет вычислимое отношение перехода. Тогда существует вычислимое преобразование программ Rewrite : β → β такое, что для любой программы P, Rewrite(P) удовлетворяет Φ и согласуется с P на всех трассах, где P не нарушает Φ.

Автомат безопасности. Свойство безопасности Φ характеризуется автоматом безопасности — автоматом A_Φ со счётным (потенциально бесконечным) множеством состояний Q, алфавитом событий исполнения Σ_ev и вычислимой функцией перехода δ : Q × Σ_ev → Q ∪ {reject}. Автомат переходит в отвергающее состояние при наблюдении «плохого» события. Ключевое требование — вычислимость δ (по паре (состояние, событие) за конечное время получаем следующее состояние или reject), а не конечность Q.

В отличие от классических DFA, автоматы безопасности (по Шнайдеру и Хамлену и др.) допускают счётно-бесконечное множество состояний. Это позволяет представлять safety-свойства, не являющиеся ω-регулярными (например, «количество открытых файлов никогда не превышает n» для произвольных n).

Доказательство. Преобразование Rewrite работает следующим образом:

1. Встраивание: в код P вставляется симуляция автомата A_Φ — переменная текущего состояния q, инициализированная начальным состоянием q₀.
2. Перехват: перед каждым событием e ∈ Σ_ev (системный вызов, запись в память, и т.д.) вставляется проверка: вычисляется δ(q, e).
3. Ветвление: если δ(q, e) = reject, программа выполняет безопасную альтернативу (аварийное завершение или подмену действия). Если δ(q, e) = q', то действие e исполняется и q обновляется на q'.

Это определение предполагает, что все события из Σ_ev наблюдаемы и перехватываемы на уровне инструментации. В модели, где программа — это последовательность наблюдаемых действий (что стандартно для анализа безопасности), данное предположение выполняется.

Результирующая программа Rewrite(P):

• Вычислима: P вычислима, δ вычислима, добавление конечного числа вычислимых операций перед каждым шагом сохраняет вычислимость.
• Удовлетворяет Φ: по построению, ни один «плохой» префикс не может возникнуть — автомат отвергает его до исполнения.
• Согласуется с P на безопасных трассах: до первого момента, когда P нарушила бы Φ, программы Rewrite(P) и P производят одинаковую последовательность событий (в проекции на Σ_ev). Дополнительные вычисления (симуляция автомата) не влияют на наблюдаемое поведение, а лишь на внутреннее состояние. ∎

Связь с EM-принудимостью. Шнайдер доказал: все EM-принудимые (enforceable via execution monitoring) свойства являются safety-свойствами. Однако обратное неверно: Базин и др. показали, что класс EM-принудимых свойств — собственное подмножество safety в обобщённой модели с различением контролируемых и наблюдаемых действий. Конструкция program rewriting покрывает более широкий класс, чем чистый EM, поскольку допускает не только прерывание исполнения, но и подмену действий. Хамлен, Моррисетт и Шнайдер показали, что RW-принудимые свойства включают некоторые Π₂-трудные свойства, выходящие за пределы coRE-класса EM.

4. Теорема 3 (о неустранимых уязвимостях)

Существуют уязвимости, неустранимые вычислимыми средствами

Формулировка. Существует частично-рекурсивная функция φ_P и нетривиальное семантическое свойство S, такие что не существует вычислимой программы Q, одновременно удовлетворяющей S и согласующейся с P на всех входах из dom(φ_P), где P не нарушает S.

Доказательство. Пусть S = «тотальность»: программа Q удовлетворяет S тогда и только тогда, когда φ_Q — всюду определённая (тотальная) функция. Тотальность — нетривиальное семантическое свойство (существуют тотальные и нетотальные программы), неразрешимое по теореме Райса.

Определим программу P следующим образом:

P(n):
  simulate TM_n on input n
  if TM_n(n) halts with output k then
    return k + 1
  else
    diverge

Здесь {TM_i} — стандартная гёделева нумерация всех машин Тьюринга. Программа P частично-рекурсивна: φ_P(n) = φ_n(n) + 1, если φ_n(n) определено; иначе φ_P(n) не определено.

P не удовлетворяет S (P нетотальна — расходится на входах n, где TM_n(n) не останавливается). «Уязвимость» здесь — нетотальность: программа обязана давать ответ на всех входах, но на некоторых расходится.

Покажем, что не существует тотальной вычислимой Q, согласующейся с P на dom(φ_P).

Предположим от противного, что такая Q существует. Тогда:

1. φ_Q — тотальная вычислимая функция;
2. Для всех n, где φ_P(n) определено (т.е. где TM_n(n) останавливается): φ_Q(n) = φ\_P(n) = φ\_n(n) + 1.

Поскольку Q — программа, она имеет номер в стандартной нумерации: Q = TM_k для некоторого k. Рассмотрим вход n = k:

• TM_k — тотальная функция (по предположению), значит TM_k(k) определено, значит k ∈ dom(φ_P);
• Из согласованности: φ_Q(k) = φ_P(k) = φ_k(k) + 1;
• Но φ_Q(k) = φ_k(k) (поскольку Q = TM_k);
• Получаем: φ_k(k) = φ_k(k) + 1 — противоречие. ∎

Замечание о связи с теоремой Райса. Теорема Райса мотивирует постановку задачи: она говорит, что нельзя алгоритмически распознать, обладает ли программа нетривиальным семантическим свойством. Однако Теорема 3 — более сильное утверждение: она показывает, что для некоторых программ вообще не существует вычислимой замены с нужными свойствами, независимо от того, можем ли мы это распознать.

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

5. Заключение

Доказано следующее:

• Теорема 1: уязвимости, заданные разрешимым предикатом на парах вход-выход, устранимы всегда — достаточно обернуть программу фильтром с безопасным ответом.
• Теорема 2: нарушения safety-свойств с вычислимым автоматом безопасности устранимы через встраивание монитора (program rewriting). Это покрывает широкий класс практических уязвимостей: переполнения буфера, нарушения контроля доступа, нарушения протоколов и т.д.
• Теорема 3: существуют семантические свойства, для которых устранение «уязвимости» (в смысле достижения этого свойства при сохранении согласованности) доказуемо невозможно.

Разделительная линия проходит в том, устранима ли уязвимость ограничением поведения (отсечь плохое, оставив хорошее неизменным) или требует расширения области определения программы (заставить программу осмысленно отвечать там, где она раньше расходилась). Первое всегда возможно; второе — нет.

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

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

Говоря ещё проще: существуют неустранимые узявимости, относящиеся к классу уязвимостей логики приложения.

Литература

1. B. Alpern, F. B. Schneider. Defining Liveness. Information Processing Letters, 21(4), 1985.
2. F. B. Schneider. Enforceable Security Policies. ACM TISSEC, 3(1), 2000.
3. K. W. Hamlen, G. Morrisett, F. B. Schneider. Computability Classes for Enforcement Mechanisms. ACM TOPLAS, 28(1), 2006.
4. D. Basin, V. Jugé, F. Klaedtke, E. Zălinescu. Enforceable Security Policies Revisited. ACM TISSEC, 16(1), 2013.
5. H. G. Rice. Classes of Recursively Enumerable Sets and Their Decision Problems. Trans. AMS, 74, 1953.