В комментариях к моей предыдущей статье amarao задал мне очень хороший вопрос. Он спрашивал, как именно, пользуясь какими правилами, мы ищем уязвимости в программном обеспечении. Приведу часть этого вопроса:
Этим вопросом amarao, вольно или невольно, привлекает внимание к проблеме объективности при оценке уязвимости программного обеспечения, насколько эта оценка зависит, или не зависит, от эксперта, ее проводящего. Вопрос является очень важным, и поэтому часто возникает как у специалистов по безопасности, так и у наших клиентов.
Действительно, если мы не имеем возможности объективно оценить безопасность предлагаемых нам продуктов, то как мы можем выбрать из них один, наилучшим образом удовлетворяющий нашим потребностям? Все производители, естественно, будут клясться, что именно их продукт — самый безопасный из когда-либо созданных. Более того, каждый из них, возможно, будет в это верить, причем, верить с полным на то основанием.
Кажется, что оценка программного обеспечения независимыми компаниями — например, сертификация — может решить эту проблему. Но если не существует объективного средства анализа, то, как мы можем проверить качество самой оценки? Ведь оценка программного продукта в этом случае — сама по себе продукт, услуга.
Несмотря на то, что эти вопросы обсуждаются достаточно часто, я не видел однозначного ответа на них. Но за время моей работы в этой области у меня сложились определенные представления о возможностях современных методик.
В этой статье я хочу проиллюстрировать следующую свою мысль: сегодня не существует алгоритма поиска уязвимостей, который бы гарантировал объективную оценку безопасности. Поэтому доверие к продукту может основываться только на репутации экспертов, проводивших его оценку, и на опыте его эксплуатации (по сути, на репутации взломщиков, которые пытались преодолеть защиту).
Все существующие методы поиска уязвимостей можно условно разделить на две категории: формальные и экспертные.
Формальные методы поиска уязвимостей в программном обеспечении очень тесно связаны с формальными методами разработки. Они основаны на использовании языков с точно определенным смыслом для спецификации проектируемого продукта; математических методах проверки корректности полученного проекта; автоматизированном создании кода программы. В ходе проверки корректности происходит и оценка возможных уязвимостей.
Экспертные методы, как следует из самого названия, основываются на знаниях и опыте специалистов, проводящих оценку. Несмотря на то, что, по определению, эти методы сложно назвать полностью объективными, я начну именно с них.
Экспертные методики основываются на том, что информационные системы создаются по более или менее известным шаблонам. Существуют шаблоны архитектуры, шаблоны проектирования, кода. Разработчики используют известные средства и методы защиты. Программы пишутся на известных языках программирования, работают под управлением распространенных операционных систем, используют доступные библиотеки, обращаются к доступным сервисам. И использование каждого из таких шаблонов открывает возможность для возникновения тех или иных уязвимостей.
Так, например, если программа написана на языке C, C++, можно попробовать найти в ней «exploitable» переполнение буфера. Если язык запросов к программе достаточно сложен, возможно, она будет уязвима для атаки методами API abuse. Если программа использует пароль для аутентификации пользователя, есть шанс его подобрать. Программы, работающие с СУБД, часто бывают уязвимы для SQL injection. Этот список, как вы можете догадаться, огромен.
Более сложная система раскладывается на составные части. Далее анализируются эти части и их взаимодействие.
Так в системе, состоящей из серверной и клиентской части, надо проанализировать сервер, клиента и протокол взаимодействия между ними. При этом может оказаться полезным отдельные части также разложить на составляющие. Например, серверная часть часто состоит из СУБД, и сервера приложений. В свою очередь сервер приложений может быть реализован в виде нескольких процессов в операционной системе; каждый процесс — использовать те или иные библиотеки.
Собственно, методика сводится к нахождению некоторого представления программы или системы в виде взаимодействующих частей. Это представление должно позволять на основании имеющейся у нас исторической информации проанализировать уязвимость каждой части и уязвимости, связанные с их взаимодействием.
Хорошим примером экспертного подхода является метод, разработанный и используемый в Microsoft. Метод описан, в частности, в книге “ThreatModeling” [1]. В нем для анализа архитектуры программы используются диаграммы потоков информации, для представления полученных результатов используются деревья атак.
Таким образом, экспертные методы основываются на способности специалиста грамотно провести декомпозицию программы и на его знании уязвимостей различных типов программ и протоколов.
По моему опыту, «использование математики» иногда воспринимается с благоговением, почти как магическое действие. Именно математические, формальные методы, в понимании многих, являются кандидатами на звание «серебряной пули», и результаты, полученные с их использованием, воспринимаются недостаточно критически.
Конечно, формальные методы действительно позволяют создавать более качественное программное обеспечение. Они уже нашли свое применение в тех областях, где к программам предъявляются повышенные требования по надежности или/и по безопасности. Постепенно области их использования расширяются, возможно, читающие эту статью уже используют хотя бы элементы таких методов, или будут использовать их в будущем. Думаю, со временем, использование формальных средств позволит как повысить качество получаемого продукта, так и снизить расходы на его разработку и поддержку*.
С другой стороны, хотя формальные методы позволяют получать великолепные результаты, необходимо понимать и их ограничения. Каждый, кто занимался построением и изучением математических моделей, скажет вам, что любая модель может дать не больше того, что в нее изначально заложено.
Давайте в качестве примера рассмотрим очень простую модель очень простой программы, которая реализует очень простой протокол.
Программа, после запуска и инициализации, должна ожидать установление соединения от пользователя. После того, как соединение установлено, программа должна получить от пользователя его имя и пароль. Если они окажутся корректными, программа может перейти к передаче пользователю некой информации, документа. После окончания передачи, программа должна разорвать соединение, и перейти к ожиданию нового соединения.
Мы хотим убедиться, что с использованием этой программы незарегистрированный пользователь не сможет получить доступ к информации.
Один из возможных вариантов сделать это — построить автоматную модель и исследовать ее.
Схема автомата, моделирующего данную программу, представлена на следующем рисунке.
В данной модели возможны всего два маршрута: I→II→III→I и I→II→I
Рассмотрев все возможные маршруты, мы приходим к выводу, что попасть в состояние, в котором происходит чтение документа, можно, только успешно пройдя аутентификацию. Полученный вывод является подтверждением корректности нашего проекта. Конечно, для нашей простой системы это было очевидно, в более сложной ситуации мы, возможно, нашли бы «неправильные» пути.
Если бы мы смогли найти маршруты, проходя по которым, система попадает в состояние чтения документа без аутентификации, это означало бы, что мы нашли уязвимость. Более того, поскольку мы знали бы, какие запросы должны быть сделаны в каждом состоянии для осуществления соответствующего перехода, мы сразу знали бы метод, которым система может быть атакована.
Казалось бы, вот он — алгоритм анализа уязвимостей. Мы создали модель, изучили ее; на выходе получили либо методы атаки, либо вывод о безопасности системы. Но заметим, что каждая модель может помочь нам найти уязвимости только некоторых типов, в данном случае, это ошибки в последовательности сообщений, которыми обменивается пользователь с программой. И мы строим ту или иную модель, поскольку ожидаем найти уязвимости определенного типа.
При утверждении о безопасности программы на основании изучения математической модели, мы опираемся на целый ряд предположений о свойствах моделируемой программы, окружения, в котором она работает.
Давайте обсудим некоторые предположения, сделанные нами при построении нашей простой модели.
Вероятно, самым очевидным нашим предположением является то, что пользователь, представивший корректный пароль, является зарегистрированным. Модель никак не рассматривает проблемы перехвата, подбора, кражи у пользователя его пароля. Для того чтобы оценить программу с этой точки зрения понадобились бы дополнительные исследования.
Существуют и менее очевидные предположения. Например, то, что пользователь, получающий документ, будет тем же пользователем, который ввел имя и пароль. Это исключает из рассмотрения все атаки, связанные с перехватом сессии.
Как мы увидели, даже при исследовании очень простой программы, мы вынуждены опираться на множество допущений. Для более сложных систем это справедливо в еще большей степени. Каждый раз, когда мы делаем заключение о безопасности того или иного программного продукта, системы, мы опираемся на целый ряд предположений об ограниченности возможностей атакующего.
Часть из предположений может быть проверена. Например, в некоторых случаях мы могли бы утверждать, что сессия не будет перехвачена. Это выглядит вполне правдоподобно, если пользователь работает с локальной клавиатурой и монитором, а операционная система поддерживает «trusted path». Да, чуть не забыл, вероятно, мы еще должны предположить, что сессия автоматически прерывается, если пользователь встает со стула…
Другие предположения проверены быть не могут. Некоторые из них не могут быть проверены, поскольку мы не знаем границ физических возможностей атакующего. Например, его возможности по перехвату электромагнитного излучения компьютера. Мы можем предполагать, какими средствами обладает нападающий, у нас даже могут быть основания для уверенности в этом знании. Но мы не можем быть уверенными до конца. Возможно, ситуация изменится завтра существенным образом. Возможно, что средства атаки уже есть в относительно свободном доступе, но мы пока об этом не знаем.
Некоторые логические предположения также не могут быть проверены. Примером такого предположения является безопасность алгоритма RSA. Строгих формальных доказательств его невзламываемости, насколько мне известно, не существует. Это означает, что завтра может появиться методика взлома, и все системы, основанные на использовании этого алгоритма, станут незащищенными. Более того, мы не можем быть абсолютно уверенными, что никто до сих пор не знает, как атаковать этот алгоритм. Конечно, существуют веские основания верить, что сейчас RSA безопасен, но задайте себе вопрос: если бы у вас был бизнес, ценою в пару-тройку миллиардов долларов (что делало бы его интересной мишенью), поставили бы вы его полностью в зависимость от RSA?
Интересно, что все эти предположения связаны не с тем, что мы что-то знаем — как решить ту или иную задачу, — а с тем, что мы чего-то не знаем. Каждый раз, когда мы должны проверить то или иное наше утверждение, встает вопрос: мы не можем решить эту задачу, и никто не умеет этого делать, или метод решения известен, но мы его не знаем?
Любой, кто хотя бы немного помнит школьный курс математики, легко заметит, что все математические модели основываются на аксиомах — недоказываемых в рамках самой модели предположений. И разница между «хорошей» и «плохой» моделью может быть только в надежности сделанных предположений. Проверить утверждение типа «никто этого не умеет» намного сложнее утверждения «мы умеем это делать». В этом мы вынуждены доверять экспертам.
И мы приходим к парадоксальному, казалось бы, выводу о субъективности формальных моделей в области безопасности, об их зависимости от наличия опыта у эксперта.
Отсутствие уязвимостей не может быть продемонстрировано, в противоположность тому, как может быть продемонстрирована, например, функциональность программы или ее быстродействие. Мы вынуждены доверять мнению эксперта.
Даже если тот или иной эксперт не знает, как атаковать данную систему, это еще не значит, что она безопасна. Даже если ни один эксперт не знает этого, все равно, мы не можем быть до конца уверены, что такие способы отсутствуют.
При этом только эксперт — или экспертное сообщество — может определить, какие проверки необходимо сделать, какие усилия достаточно приложить для поиска уязвимостей в анализируемой программе. Сделать это он может на основании своих знаний о методах атак на подобные системы. И доверие к результатам проверки может быть основано только на репутации проводивших ее экспертов.
А закончить мне хочется в рамках логики всей статьи.
Могу ли я утверждать, что завтра не будет сделано Большое Открытие, в результате которого, все, что было сказано в этой статье, окажется неверным? Нет, не могу.
Уверен ли я, что это Большое Открытие еще никем не сделано? У меня есть основания верить, что этого еще не произошло. Но я не могу быть окончательно уверенным.
* Если вы заинтересуетесь формальными подходами вообще, без относительно безопасности, то, возможно, вам будет интересно почитать книгу «Understanding formal methods» [2].
Другая книга «Computer Security. Art and Science» [3] содержит множество сведений о математических моделях в информационной безопасности, в том числе отдельная глава посвящена формальным методам анализа защищенности программного обеспечения.
1. Frank Swiderski, Window Snyder “Threat Modeling”, Microsoft Press 2004, ISBN 978-0-7356-1991-3
2. Jean Francois Monin, Michal G. Hichey (editor) “Understanding Formal Methods”, Springer-Verlag 2003, ISBN 1-85233-247-6
3. Matt Bishop “Computer Security. Art and Science”, Addison-Wesley 2003, ISBN 0-201-44099-7
По каким алгоритмам, по каким правилам? Или это всё на наитии «а я знаю что такое mim!»? В этом случае метод не описывает ровным случаем ничего где-то — подумал, где-то нет.
Этим вопросом amarao, вольно или невольно, привлекает внимание к проблеме объективности при оценке уязвимости программного обеспечения, насколько эта оценка зависит, или не зависит, от эксперта, ее проводящего. Вопрос является очень важным, и поэтому часто возникает как у специалистов по безопасности, так и у наших клиентов.
Действительно, если мы не имеем возможности объективно оценить безопасность предлагаемых нам продуктов, то как мы можем выбрать из них один, наилучшим образом удовлетворяющий нашим потребностям? Все производители, естественно, будут клясться, что именно их продукт — самый безопасный из когда-либо созданных. Более того, каждый из них, возможно, будет в это верить, причем, верить с полным на то основанием.
Кажется, что оценка программного обеспечения независимыми компаниями — например, сертификация — может решить эту проблему. Но если не существует объективного средства анализа, то, как мы можем проверить качество самой оценки? Ведь оценка программного продукта в этом случае — сама по себе продукт, услуга.
Несмотря на то, что эти вопросы обсуждаются достаточно часто, я не видел однозначного ответа на них. Но за время моей работы в этой области у меня сложились определенные представления о возможностях современных методик.
В этой статье я хочу проиллюстрировать следующую свою мысль: сегодня не существует алгоритма поиска уязвимостей, который бы гарантировал объективную оценку безопасности. Поэтому доверие к продукту может основываться только на репутации экспертов, проводивших его оценку, и на опыте его эксплуатации (по сути, на репутации взломщиков, которые пытались преодолеть защиту).
Все существующие методы поиска уязвимостей можно условно разделить на две категории: формальные и экспертные.
Формальные методы поиска уязвимостей в программном обеспечении очень тесно связаны с формальными методами разработки. Они основаны на использовании языков с точно определенным смыслом для спецификации проектируемого продукта; математических методах проверки корректности полученного проекта; автоматизированном создании кода программы. В ходе проверки корректности происходит и оценка возможных уязвимостей.
Экспертные методы, как следует из самого названия, основываются на знаниях и опыте специалистов, проводящих оценку. Несмотря на то, что, по определению, эти методы сложно назвать полностью объективными, я начну именно с них.
Экспертные методы
Экспертные методики основываются на том, что информационные системы создаются по более или менее известным шаблонам. Существуют шаблоны архитектуры, шаблоны проектирования, кода. Разработчики используют известные средства и методы защиты. Программы пишутся на известных языках программирования, работают под управлением распространенных операционных систем, используют доступные библиотеки, обращаются к доступным сервисам. И использование каждого из таких шаблонов открывает возможность для возникновения тех или иных уязвимостей.
Так, например, если программа написана на языке C, C++, можно попробовать найти в ней «exploitable» переполнение буфера. Если язык запросов к программе достаточно сложен, возможно, она будет уязвима для атаки методами API abuse. Если программа использует пароль для аутентификации пользователя, есть шанс его подобрать. Программы, работающие с СУБД, часто бывают уязвимы для SQL injection. Этот список, как вы можете догадаться, огромен.
Более сложная система раскладывается на составные части. Далее анализируются эти части и их взаимодействие.
Так в системе, состоящей из серверной и клиентской части, надо проанализировать сервер, клиента и протокол взаимодействия между ними. При этом может оказаться полезным отдельные части также разложить на составляющие. Например, серверная часть часто состоит из СУБД, и сервера приложений. В свою очередь сервер приложений может быть реализован в виде нескольких процессов в операционной системе; каждый процесс — использовать те или иные библиотеки.
Собственно, методика сводится к нахождению некоторого представления программы или системы в виде взаимодействующих частей. Это представление должно позволять на основании имеющейся у нас исторической информации проанализировать уязвимость каждой части и уязвимости, связанные с их взаимодействием.
Хорошим примером экспертного подхода является метод, разработанный и используемый в Microsoft. Метод описан, в частности, в книге “ThreatModeling” [1]. В нем для анализа архитектуры программы используются диаграммы потоков информации, для представления полученных результатов используются деревья атак.
Таким образом, экспертные методы основываются на способности специалиста грамотно провести декомпозицию программы и на его знании уязвимостей различных типов программ и протоколов.
Формальные методы
По моему опыту, «использование математики» иногда воспринимается с благоговением, почти как магическое действие. Именно математические, формальные методы, в понимании многих, являются кандидатами на звание «серебряной пули», и результаты, полученные с их использованием, воспринимаются недостаточно критически.
Конечно, формальные методы действительно позволяют создавать более качественное программное обеспечение. Они уже нашли свое применение в тех областях, где к программам предъявляются повышенные требования по надежности или/и по безопасности. Постепенно области их использования расширяются, возможно, читающие эту статью уже используют хотя бы элементы таких методов, или будут использовать их в будущем. Думаю, со временем, использование формальных средств позволит как повысить качество получаемого продукта, так и снизить расходы на его разработку и поддержку*.
С другой стороны, хотя формальные методы позволяют получать великолепные результаты, необходимо понимать и их ограничения. Каждый, кто занимался построением и изучением математических моделей, скажет вам, что любая модель может дать не больше того, что в нее изначально заложено.
Давайте в качестве примера рассмотрим очень простую модель очень простой программы, которая реализует очень простой протокол.
Простой пример
Программа, после запуска и инициализации, должна ожидать установление соединения от пользователя. После того, как соединение установлено, программа должна получить от пользователя его имя и пароль. Если они окажутся корректными, программа может перейти к передаче пользователю некой информации, документа. После окончания передачи, программа должна разорвать соединение, и перейти к ожиданию нового соединения.
Мы хотим убедиться, что с использованием этой программы незарегистрированный пользователь не сможет получить доступ к информации.
Один из возможных вариантов сделать это — построить автоматную модель и исследовать ее.
Схема автомата, моделирующего данную программу, представлена на следующем рисунке.
В данной модели возможны всего два маршрута: I→II→III→I и I→II→I
Рассмотрев все возможные маршруты, мы приходим к выводу, что попасть в состояние, в котором происходит чтение документа, можно, только успешно пройдя аутентификацию. Полученный вывод является подтверждением корректности нашего проекта. Конечно, для нашей простой системы это было очевидно, в более сложной ситуации мы, возможно, нашли бы «неправильные» пути.
Если бы мы смогли найти маршруты, проходя по которым, система попадает в состояние чтения документа без аутентификации, это означало бы, что мы нашли уязвимость. Более того, поскольку мы знали бы, какие запросы должны быть сделаны в каждом состоянии для осуществления соответствующего перехода, мы сразу знали бы метод, которым система может быть атакована.
Казалось бы, вот он — алгоритм анализа уязвимостей. Мы создали модель, изучили ее; на выходе получили либо методы атаки, либо вывод о безопасности системы. Но заметим, что каждая модель может помочь нам найти уязвимости только некоторых типов, в данном случае, это ошибки в последовательности сообщений, которыми обменивается пользователь с программой. И мы строим ту или иную модель, поскольку ожидаем найти уязвимости определенного типа.
При утверждении о безопасности программы на основании изучения математической модели, мы опираемся на целый ряд предположений о свойствах моделируемой программы, окружения, в котором она работает.
Предположения в модели
Давайте обсудим некоторые предположения, сделанные нами при построении нашей простой модели.
Вероятно, самым очевидным нашим предположением является то, что пользователь, представивший корректный пароль, является зарегистрированным. Модель никак не рассматривает проблемы перехвата, подбора, кражи у пользователя его пароля. Для того чтобы оценить программу с этой точки зрения понадобились бы дополнительные исследования.
Существуют и менее очевидные предположения. Например, то, что пользователь, получающий документ, будет тем же пользователем, который ввел имя и пароль. Это исключает из рассмотрения все атаки, связанные с перехватом сессии.
Как мы увидели, даже при исследовании очень простой программы, мы вынуждены опираться на множество допущений. Для более сложных систем это справедливо в еще большей степени. Каждый раз, когда мы делаем заключение о безопасности того или иного программного продукта, системы, мы опираемся на целый ряд предположений об ограниченности возможностей атакующего.
Часть из предположений может быть проверена. Например, в некоторых случаях мы могли бы утверждать, что сессия не будет перехвачена. Это выглядит вполне правдоподобно, если пользователь работает с локальной клавиатурой и монитором, а операционная система поддерживает «trusted path». Да, чуть не забыл, вероятно, мы еще должны предположить, что сессия автоматически прерывается, если пользователь встает со стула…
Другие предположения проверены быть не могут. Некоторые из них не могут быть проверены, поскольку мы не знаем границ физических возможностей атакующего. Например, его возможности по перехвату электромагнитного излучения компьютера. Мы можем предполагать, какими средствами обладает нападающий, у нас даже могут быть основания для уверенности в этом знании. Но мы не можем быть уверенными до конца. Возможно, ситуация изменится завтра существенным образом. Возможно, что средства атаки уже есть в относительно свободном доступе, но мы пока об этом не знаем.
Некоторые логические предположения также не могут быть проверены. Примером такого предположения является безопасность алгоритма RSA. Строгих формальных доказательств его невзламываемости, насколько мне известно, не существует. Это означает, что завтра может появиться методика взлома, и все системы, основанные на использовании этого алгоритма, станут незащищенными. Более того, мы не можем быть абсолютно уверенными, что никто до сих пор не знает, как атаковать этот алгоритм. Конечно, существуют веские основания верить, что сейчас RSA безопасен, но задайте себе вопрос: если бы у вас был бизнес, ценою в пару-тройку миллиардов долларов (что делало бы его интересной мишенью), поставили бы вы его полностью в зависимость от RSA?
Интересно, что все эти предположения связаны не с тем, что мы что-то знаем — как решить ту или иную задачу, — а с тем, что мы чего-то не знаем. Каждый раз, когда мы должны проверить то или иное наше утверждение, встает вопрос: мы не можем решить эту задачу, и никто не умеет этого делать, или метод решения известен, но мы его не знаем?
Любой, кто хотя бы немного помнит школьный курс математики, легко заметит, что все математические модели основываются на аксиомах — недоказываемых в рамках самой модели предположений. И разница между «хорошей» и «плохой» моделью может быть только в надежности сделанных предположений. Проверить утверждение типа «никто этого не умеет» намного сложнее утверждения «мы умеем это делать». В этом мы вынуждены доверять экспертам.
И мы приходим к парадоксальному, казалось бы, выводу о субъективности формальных моделей в области безопасности, об их зависимости от наличия опыта у эксперта.
Выводы
Отсутствие уязвимостей не может быть продемонстрировано, в противоположность тому, как может быть продемонстрирована, например, функциональность программы или ее быстродействие. Мы вынуждены доверять мнению эксперта.
Даже если тот или иной эксперт не знает, как атаковать данную систему, это еще не значит, что она безопасна. Даже если ни один эксперт не знает этого, все равно, мы не можем быть до конца уверены, что такие способы отсутствуют.
При этом только эксперт — или экспертное сообщество — может определить, какие проверки необходимо сделать, какие усилия достаточно приложить для поиска уязвимостей в анализируемой программе. Сделать это он может на основании своих знаний о методах атак на подобные системы. И доверие к результатам проверки может быть основано только на репутации проводивших ее экспертов.
А закончить мне хочется в рамках логики всей статьи.
Могу ли я утверждать, что завтра не будет сделано Большое Открытие, в результате которого, все, что было сказано в этой статье, окажется неверным? Нет, не могу.
Уверен ли я, что это Большое Открытие еще никем не сделано? У меня есть основания верить, что этого еще не произошло. Но я не могу быть окончательно уверенным.
Примечание
* Если вы заинтересуетесь формальными подходами вообще, без относительно безопасности, то, возможно, вам будет интересно почитать книгу «Understanding formal methods» [2].
Другая книга «Computer Security. Art and Science» [3] содержит множество сведений о математических моделях в информационной безопасности, в том числе отдельная глава посвящена формальным методам анализа защищенности программного обеспечения.
Литература
1. Frank Swiderski, Window Snyder “Threat Modeling”, Microsoft Press 2004, ISBN 978-0-7356-1991-3
2. Jean Francois Monin, Michal G. Hichey (editor) “Understanding Formal Methods”, Springer-Verlag 2003, ISBN 1-85233-247-6
3. Matt Bishop “Computer Security. Art and Science”, Addison-Wesley 2003, ISBN 0-201-44099-7
