Глава 1. Формальные методы в разработке и сертификации средств защиты информации
По мере развития и широкого проникновения информационных технологий во все сферы жизни все более острыми становятся проблемы обеспечения информационной безопасности. Гражданам, бизнесу, государственным учреждениям, обществу в целом все труднее защититься от угроз, связанных с отказами или взломом в результате преднамеренных атак разнообразных информационных систем.
Современный уровень науки и техники не предлагает никакого универсального средства для выявления и парирования всех возможных угроз информационной безопасности. Скорее всего, такое универсальное средство не удастся изобрести и в будущем. Вместе с тем за последние 50 лет было немало попыток создания технологий разработки «идеального» программного обеспечения (ПО), отвечающего всем предъявляемым к нему требованиям, в том числе и требованиям информационной безопасности, использование которого позволило бы обеспечить безопасное и надежное функционирование информационных систем. В частности, предлагались концепции «разработки программ, правильных по построению», методы строгого и формального анализа программ, методы математического доказательства корректности программ и многие другие.
Хотя «идеальное» ПО создавать до сих пор не удается, прогресс в этом направлении компьютерных наук значителен. Если еще 10–15 лет назад потенциал инновационных технологий был понятен только небольшим группам ученых, то в последнее время возможности новых методов разработки и анализа программ становятся доступны практикам. Современное состояние этой области отличается от состояния пятнадцатилетней давности по многим характеристикам. Во-первых, разработаны новые методы и инструменты анализа программ, которые (при современных, существенно возросших возможностях компьютеров) позволяют анализировать на предмет защищенности не только «учебные» примеры длиной до 100 строк программного кода, но и реальные сложные программы и даже программные комплексы объемом в миллионы строк кода.
Во-вторых, за это время в рассматриваемой области был выработан систематический подход к оценке информационной безопасности в целом. Общая идеология повышения уровня информационной безопасности сводится к тому, что защита целевой системы обеспечивается совокупностью мер, реализованных по протяжении всего жизненного цикла разрабатываемой, а потом эксплуатируемой системы. То есть, начиная с определения требований к системе, выбора архитектуры и проектирования, выбора инструментов разработки и поддержки жизненного цикла, должны выполняться работы, направленные на повышение уровня защищенности, уровня доверия к целевой системы. При этом важно, что качество и полнота работ, предписанных в соответствующих регламентах, должны быть проверяемы на соответствие объективным критериям, желательно при помощи программных инструментов, чтобы минимизировать влияние субъективных человеческих факторов на оценку достигнутого уровня доверия.
Основным стандартом в этой области является ГОСТ Р ИСО/МЭК 15408 «Информационная технология. Методы и средства обеспечения безопасности. Критерии оценки безопасности информационных технологий», состоящий из трех частей:
- Часть 1. Введение и общая модель [4].
- Часть 2. Функциональные компоненты безопасности [5].
- Часть 3. Компоненты доверия к безопасности [6].
С ростом уровня требований к надежности и безопасности системы естественным образом расширяется и набор техник ее защиты, и сложность аргументации, необходимой для достижения нужной степени доверия к ним. Набор требований к мерам защиты и подтверждению их корректности в части 3 ГОСТ Р ИСО/МЭК 15408 разбит на так называемые оценочные уровни доверия (ОУД). Минимальный набор требований, базирующийся на самых общих, неформальных подходах к подтверждению безопасности оцениваемой системы, содержится в первом оценочном уровне доверия (ОУД1), а наиболее широкий и строгий набор требований к удостоверению безопасности систем изложен в седьмом оценочном уровне доверия (ОУД7). Он, в частности, предусматривает формальное (в некоторых случаях полуформальное) обоснование корректности реализации механизма управления доступом, важнейшей части средств защиты информации (СЗИ), в рамках объекта оценки (ОО).
Данная монография посвящена вопросам моделирования и верификации политики безопасности в ОС. Операционные системы, в которых имеются дополнительные средства защиты информации по сравнению со стандартными версиями ОС, будем называть «защищенными ОС» (понимая, что разные защищенные ОС могут существенно отличаться друг от друга по степени защиты). ОС служит базовым слоем ПО, предоставляя для остальных программ среду выполнения и интерфейсы для взаимодействия с аппаратной платформой и другими программами и определяя тем самым множество элементов архитектуры и технологий разработки приложений, работающих на данной ОС. Уровень защищенности ОС не может быть ниже, чем уровень защищенности всей системы в целом. Политика безопасности ОС определяет правила управления доступом субъектов — пользователей и работающих от их имени программ к различным объектам — информационным ресурсам, файлам, каталогам, устройствам и т. д. При этом для систем, отвечающих самым высоким требованиям по защите информации, например соответствующим ОУД6 или ОУД7, требования стандарта ГОСТ Р ИСО/МЭК 15408 предписывают необходимость формального описания политики безопасности (в виде модели политики безопасности) и формального доказательства ее корректности.
Моделирование безопасности управления доступом и информационными потоками можно считать исторически первым научным направлением в современной теории компьютерной безопасности [7–9]. В рамках этого направления разработаны десятки, если не сотни формальных моделей, а наиболее известная из них модель Белла-ЛаПадулы [7] более 40 лет назад была реализована в механизме управления доступом ОС Multics. Вместе с тем до сих пор научным сообществом и практиками в области информационной безопасности в полной мере не определен ни сам термин «формальная модель политики безопасности», ни тем более не сформировано четких критериев наличия представления такой модели, ее верификации при сертификации средств защиты информации [10].
Впервые требование представления формальной модели механизма управления доступом было включено в 1985 г. в требования классов защиты, начиная с B2, стандарта Trusted Computer System Evaluation Criteria (TCSEC, «Оранжевая книга») [11]. Тогда в качестве примера такой модели в TCSEC была указана модель Белла-ЛаПадулы. В 1992 г. аналогичное требование вошло в раздел «Гарантии проектирования», начиная с третьего класса защищенности по Руководящим документам (РД) Гостехкомиссии (ныне ФСТЭК) России «Средства вычислительной техники. Защита от несанкционированного доступа к информации. Показатели защищенности от несанкционированного доступа к информации» [12]. Однако в доступных источниках авторами не найдено свидетельств применения этого требования по существу.
Ситуация существенно изменилась с февраля 2017 года, когда ФСТЭК России были утверждены профили защиты ОС общего назначения (типа «А») [13, 14], основанные на «Требованиях безопасности информации к операционным системам» [15] и ГОСТ Р ИСО/МЭК 15408. Эти профили включают требования доверия (например, содержащиеся в компонентах доверия ADV_FSP.6 «Полная полуформальная функциональная спецификация с дополнительной формальной спецификацией», ADV_SPM.1 «Формальная модель политики безопасности», AVA_CCA_EXT.1 «Анализ скрытых каналов» и др.), которые ставят перед научным сообществом задачи по разработке соответствующих технологий их реализации, без чего успешное применение новых профилей защиты будет крайне затруднено. Кроме того, ожидается утверждение ФСТЭК России профилей защиты СУБД, содержащих аналогичные требования.
Разработка модели политики безопасности и ее верификация это только часть сложного процесса оценки защищенности операционной системы и представления ее на сертификацию. В данной монографии авторы описывают опыт проведения работ по подготовке к сертификации на соответствие требованиям профиля защиты ОС общего назначения (типа «А») второго класса защиты ОССН Astra Linux Special Edition [1-3]. Представленный материал не описывает весь процесс такой подготовки, а концентрируется на вопросах систематического, строгого анализа, построения модели политики безопасности управления доступом и информационными потоками, верификации механизмов управления доступом, которые реализованы в конкретной ОССН. Тем не менее представленная схема процесса моделирования и верификации дает достаточно полную картину проблем и арсенала средств верификации, которые позволяют подготовить все необходимые материалы (свидетельства) для сертификации на соответствие профилям защиты, включающим соответствующие требования доверия.
Хотя в монографии описывается модель политики безопасности управления доступом Linux, собственно Linux не вносит существенной специфики (за исключением учета некоторых конкретных особенностей Linux, например наличия «жестких» ссылок на файлы и др.). Практически любая ОС может брать предложенную модель за основу без значительной доработки. Например, для пополнения модели описанием дискреционного управления доступом можно ввести соответствующие роли на основе уже описанного ролевого управления доступом. Привязка к Linux позволяет дать конкретные примеры и показать, как процесс моделирования и верификации может выполняться в реальных условиях.
Содержание монографии выстроено в соответствии с этапами подготовки ОССН к сертификации. Сначала описывается фаза разработки модели политики безопасности в строгой математической нотации, затем описывается схема ее перевода на формальный язык моделирования и разработки спецификации формальной модели, после чего излагается подход к верификации полученной модели, а также верификации и тестирования ее реализации непосредственно в программном коде ОССН.
В реальности, конечно, на каждой фазе этой работы могут встречаться проблемы, в частности могут обнаруживаться некоторые ошибки в спецификациях, что вызывает необходимость менять отдельные решения или даже возвращаться и пересматривать спецификации или доказательства корректности, которые были сделаны на предыдущих фазах процесса. Важно отметить, что в данном случае приходится работать как минимум с тремя различными нотациями: математической, формальной (в нашем случае Event-B) и на языке программирования Си (его диалектом, который используется при программировании компонентов ядра ОС Linux). Переход от одной нотации к другой это непростая работа, которая не всегда может быть полностью формализована и, соответственно, автоматизирована. Кроме того, нужно понимать, что, двигаясь от модели к реализации ядра ОС Linux, мы переходим от описания модели в математической нотации (около 300 страниц текста) к формальной на Event-B (около 5 тысяч строк кода) и далее к спецификации поведения реализации ядра, размер которого приближается к 20 млн строк кода на Си, из которых значительная часть явно или косвенно связана с реализацией механизма управления доступом ОССН. Последний «переход» самый трудный в плане его формализации и автоматизации.
Цель формализации требований к механизму управления доступом и систематической верификации как моделей, так и его реализации в ОССН — это повышение уровня доверия к данному механизму в ОО. Элементы технологической цепочки процесса верификации, представленные в данной книге, различаются по степени точности и гарантиям обеспечения информационной безопасности. Для такой большой и сложной системы, как ОССН, современный уровень технологий не позволяет дать гарантии полной защищенности, тем не менее систематичный и, по возможности, строгий или даже формальный подход к верификации моделей и программ существенно повышает уровень уверенности в обеспечении информационной безопасности, именно этого и требуют регламенты и стандарты, на которые опираются процедура сертификации операционных систем, «работающих» с государственной тайной.
Все фазы процесса представлены и описаны в данной монографии. Конечно, ее нельзя рассматривать как учебное пособие, изучения которого достаточно для того, чтобы специалист по информационной безопасности смог без каких-либо затруднений выполнить аналогичный проект применительно к собственному программному продукту.
Цель авторов состоит в том, чтобы показать пример использования современных достижений компьютерных наук для решения практической задачи, с которой все больше приходится сталкиваться специалистам по информационной безопасности и другим разработчикам, которые планируют сертификацию своих продуктов на соответствие требованиям с высоким уровнем доверия к их безопасности. Вместе с тем технологии верификации, которые описываются в книге, постоянно развиваются и уже сейчас являются достаточно зрелыми, чтобы ими могли пользоваться не только математики, но и инженеры, и программисты, а это значит, что эти технологии уже можно использовать в крупных программных проектах.
Модели и спецификации, о которых пойдет речь далее, а также используемые для их создания и верификации инструменты выложены в открытом доступе на сайте ИСП РАН1 и могут быть скачаны для подробного изучения.