Использование доказательств теорем для поиска атак

Question

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

Мой вопрос: кто-нибудь работал над использованием инструментов, аналогичных обнаружению уязвимостей в существующих или предлагаемых системах?

---

Eidt: I'm НЕ с просьбой доказать, что программная система безопасна.Я спрашиваю о нахождении (в идеале неизвестных ранее) уязвимостей (или даже их классов).Я думаю, что здесь (но не как) черная шляпа: опишите формальную семантику системы, опишите, что я хочу атаковать, а затем дайте компьютеру понять, какую цепочку действий мне нужно использовать, чтобы захватить вашу систему.

Answer 1

Да, в этой области проделана большая работа. Решатели удовлетворенности (SAT и SMT) регулярно используются для поиска уязвимостей в безопасности. Например, в Microsoft инструмент SAGE используется для устранения ошибок переполнения буфера в Windows. SAGE использует проверку теоремы Z3 в качестве средства проверки ее соответствия. Если вы будете искать в Интернете ключевые слова, такие как «интеллектуальное фаззинг» или «фаззинг белого ящика», вы найдете несколько других проектов, использующих контролеры удовлетворенности для поиска уязвимостей в безопасности. Идея высокого уровня заключается в следующем: собрать пути выполнения в вашей программе (которые вам не удалось выполнить, т. Е. Вы не нашли вход, который заставил программу выполнить его), преобразовать эти пути в математические формулы, и передать эти формулы для решателя выполнимости. Идея состоит в том, чтобы создать формулу, которая будет выполнимой / выполнимой, только если есть входные данные, которые заставят программу выполнить данный путь. Если полученная формула является выполнимой (то есть выполнимой), тогда решатель выполнимости будет производить присваивание и требуемые входные значения. Белые ящики используют разные стратегии для выбора путей исполнения. Основная цель состоит в том, чтобы найти входные данные, которые заставят программу выполнить путь, который приводит к сбою.

Answer 2

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

И как минимум два видео на 9 канале. Вот один из них

Его исследование, вероятно, станет хорошей отправной точкой для изучения этой чрезвычайно интересной области исследований.

Такие проекты, как Spec # иTyped-Assembly-Language тоже связаны между собой.В своем стремлении перенести возможность проверок безопасности со времени выполнения обратно на время компиляции, они позволяют компилятору обнаруживать многие пути неверного кода как ошибки компиляции.Строго говоря, они не помогают вашим заявленным намерениям, но теория, которую они используют, может быть полезной для вас.

Answer 3

STACK и KINT использовали решатели ограничений для поиска уязвимостей во многих проектах OSS, таких как ядро ​​linux и ffmpeg.Страницы проекта указывают на документы и код.

Answer 4

Я сейчас пишу парсер PDF в Coq вместе с кем-то еще. Хотя в данном случае цель состоит в том, чтобы создать безопасный кусок кода, выполнение чего-то подобного может определенно помочь в поиске фатальных ошибок логики.

После того, как вы ознакомитесь с инструментом, большинство доказательств станет легким. Более сложные доказательства приводят к интересным тестам, которые иногда могут вызывать ошибки в реальных существующих программах. (А для поиска ошибок вы можете просто принять теоремы в качестве аксиом, если вы уверены, что ошибок нет, серьезных доказательств не требуется.)

Около месяца назад мы столкнулись с проблемой разбора PDF-файлов с несколькими / более старыми таблицами XREF. Мы не смогли доказать, что разбор прекращается. Размышляя об этом, я создал PDF-файл с зацикленными / предыдущими указателями в трейлере (кто бы мог подумать об этом ?:-P), что, естественно, заставило некоторых зрителей зацикливаться вечно. (В частности, почти любой попплер-зритель на Ubuntu. Заставил меня смеяться и проклинать Gnome / evince-thumbnailer за то, что он съел весь мой процессор. Думаю, они исправили это сейчас, хотя.)

---

Использование Coq для поиска ошибок низкого уровня будет трудным. Для того, чтобы что-то доказать, вам нужна модель поведения программы. Для проблем со стеком / кучей вам, вероятно, придется смоделировать выполнение на уровне процессора или, по крайней мере, на уровне C. Хотя технически это возможно, я бы сказал, что это не стоит усилий.

Использование SPLint для C или написание собственного средства проверки на выбранном вами языке должно быть более эффективным.

Answer 5

Существует проверенное ядро ​​ L4 , которое пытается это сделать. Однако, если вы посмотрите на историю эксплуатации, вы найдете совершенно новые шаблоны атак, а затем большое количество программного обеспечения, написанного до этого момента, будет очень уязвимо для атак. Например, уязвимости форматной строки не были обнаружены до 1999 года. Около месяца назад H.D. Мур выпустил DLL Hijacking и буквально все под windows уязвимо .

Я не думаю, что можно доказать, что часть программного обеспечения защищена от неизвестной атаки. По крайней мере, пока теорема не сможет обнаружить такую ​​атаку, и, насколько я знаю, этого не произошло.

Answer 6

Это на самом деле не связано с доказательством теорем, но нечеткое тестирование - это распространенный метод автоматического поиска уязвимостей.

Answer 7

Да. Многие проекты по доказательству теорем показывают качество своего программного обеспечения, демонстрируя дыры или дефекты в программном обеспечении. Чтобы связать это с безопасностью, просто представьте, что нашли дыру в протоколе безопасности. Доктор философии Карлос Оларте В диссертации Уго Монтанари есть один такой пример.

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

Answer 8

Отказ от ответственности: у меня практически нет опыта работы с автоматизированными средствами проверки теорем

Несколько наблюдений

• Такие вещи, как криптография, редко когда-либо "доказывались", просто считались безопасными.Если ваша программа использует что-то подобное, она будет такой же сильной, как и криптография.
• Теоретики теорем не могут анализировать все (или они могут решить проблему остановки)
• Выпришлось бы очень четко определить, что небезопасно означает для прувера.Само по себе это огромная проблема