3.2 динамическая верификация: Вид тестирования на основе формальных моделей поведения систем.
Примечание - Результатом динамической верификации в случае верификации средства защиты информации являются данные, полученные на основе сопоставления входов, выходов, наблюдаемого поведения средства защиты информации в целом с ее формальной моделью, имеющей на входе соответствующие воздействия. Автоматический анализ поведения средства защиты информации, таким образом, сводится к построению отображения ее входов и выходов в интерфейсы модели и последующему анализу (или анимации) модели с полученными входными воздействиями и получению вердикта о том, нарушают ли полученные данные о поведении средства защиты информации требования модели или нет.
3.3 модульная верификация; верификация на модульном уровне: Верификация программного модуля или группы модулей методом погружения их в тестовое или модельное окружение, которое моделирует воздействия и реакции на обращения верифицируемого модуля.
3.4 модуль (обеспечения) безопасности: Программный модуль на некотором языке программирования, реализующий политики управления доступом в средстве защиты информации и имеющий явно заданный программный интерфейс.
Примечание - Часть функций по реализации политик управления доступом в средстве защиты информации может быть не локализована в виде программного модуля. В этом случае модуль безопасности выполняет не все функции по реализации таких политик, а только часть.
3.5 статическая верификация: Техники анализа программ, при которых проверка корректности не требует исполнения программы.
3.6
3.7
3.8
3.9 функциональная спецификация средства защиты информации: Описание, детализирующее внешний интерфейс средства защиты информации.
4.1 Рекомендации настоящего стандарта по верификации средств защиты информации, реализующих политики управления доступом на основе формализованного описания модели управления доступом, направлены на обеспечение соответствия функционирования средства защиты информации формальной модели управления доступом, разработанной и верифицированной в соответствии с критериями и рекомендациями ГОСТ Р 59453.1, ГОСТ Р 59453.2 и ГОСТ Р 59453.3.
4.2 Для верификации средств защиты информации, реализующих политики управления доступом, на основе формализованного описания модели управления доступом в качестве основной техники верификации предлагается динамическая верификация, частный случай тестирования на основе формальных моделей.
4.3 Статические методы верификации могут применяться для верификации средств защиты информации в случае, когда размер и сложность программного обеспечения средства защиты информации позволяют применить указанные методы верификации.
4.4 Динамическую верификацию средства защиты информации можно проводить на системном и на модульном уровне. Верификация на системном уровне обязательна. Верификация на модульном уровне может выполняться при наличии в средстве защиты информации выделенного модуля безопасности и технической возможности проведения модульного тестирования.
4.5 Рекомендуются следующие этапы верификации средства защиты информации, реализующего политики управления доступом, на основе формализованного описания модели управления доступом:
- проведение архитектурного анализа средства защиты информации и исследование наличия модуля безопасности или группы функций, которые могут рассматриваться как модуль безопасности (возможность определения интерфейсов взаимодействия такого модуля с его окружением);
- принятие решения о проведении модульной верификации или отказе от нее;
- выбор языков разработки формальных спецификации и инструментов разработки и верификации;
- выбор критериев и методики оценки полноты верификации (оценки верификационного покрытия).
Примечания
1 Критерии и методики оценки полноты верификации (оценки верификационного покрытия) разрабатываются и обосновываются разработчиками и специалистами по верификации с учетом технической возможности выбранных средств моделирования и верификации и с учетом общепринятой практики, описанной в приложении А.
2 Важно обращать внимание на способы обеспечения интеграции работ в ходе верификации, то есть способы организации переиспользования промежуточных результатов, созданных или полученных в ходе использования инструментов верификации. При выборе инструментов верификации нужно обращать внимание на наличие средств сбора и обработки информации о полноте покрытия;
- разработка формальной спецификации интерфейсов средства защиты информации, реализующих политики управления доступом, и ее верификация.
Примечание - Формальная спецификация разрабатывается с учетом требований формальной модели управления доступом, которая разрабатывается и верифицируется до данного этапа;
- верификация средства защиты информации, проверка соответствия поведения средства защиты информации формальной модели управления доступом.
Примечание - Вместо демонстрации соответствия поведения средства защиты информации модели управления доступом можно демонстрировать соответствие формальной спецификации средства защиты информации, если предварительно было доказано, что все требования безопасности, представленные в формальной модели управления доступом, аналогичным образом представлены и в формальной спецификации средства защиты информации;
- разработка формальной спецификации интерфейсов модуля безопасности (опционально, если ставится задача верификации модуля безопасности) и ее верификация (опционально);
- верификация модуля безопасности (опционально, если ставится задача верификации модуля безопасности).
4.6 В описании результатов верификации должны быть представлены:
- анализ архитектуры средства защиты информации, обоснование вывода о наличии или отсутствии возможности модульной верификации модуля безопасности;
- описание формальной спецификации интерфейсов средства защиты информации;
- сопоставление структуры формальной модели управления доступом и формальной спецификации средства защиты информации;
- обоснование выбора способа демонстрации того, что формальная спецификация соответствует формальной модели управления доступом;
- результаты проведения верификации в соответствии с рекомендациями разделов 6 и 7 настоящего стандарта.
При выборе инструментов для проведения верификации средства защиты информации, реализующего политики управления доступом, на основе формализованных описаний модели управления доступом следует руководствоваться следующими рекомендациями:
а) инструменты должны поддерживать статическую верификацию или динамическую верификацию;
б) в инструментах должна быть предусмотрена возможность использовать выбранные языки моделирования для описания формальной модели управления доступом и/или формальной спецификации интерфейсов средства защиты информации;
в) инструментами должна поддерживаться техника уточнения для перевода реализационного представления данных (определенного в терминах используемого языка программирования) в их модельное представление. В случае динамической верификации должен быть выделен слой адаптеров/медиаторов для конвертации данных;
г) в инструментах статической верификации должны быть средства анализа верификационного покрытия;
д) в инструментах динамической верификации должны быть средства для сбора и анализа тестового (верификационного) покрытия:
1) на основе структур формальной модели управления доступом и/или формальной спецификации средства защиты информации;
2) на основе структуры реализации средства защиты информации.
Примечания
1 Формальные модели управления доступом, формальные спецификации средства защиты информации и формальные спецификации модулей обеспечения безопасности могут создаваться при помощи различных инструментов, языков моделирования, языков формальных спецификаций или других формальных нотаций.
2 Для целей моделирования и верификации моделей управления доступом большое распространение получили языки (нотации) Event-B и TLA+. Первая поддерживается несколькими инструментами, наиболее известные Rodin и ProB. Наиболее известным набором инструментов для TLA+ является набор TLA+ Toolbox. Перечисленные инструменты распространяются под открытыми лицензиями.
3 Распространенных инструментов, которые разрабатывались специально для тестирования на основе моделей, мало. Большая часть из них плохо интегрируется с языками программирования, на которых разрабатываются средства защиты информации, и с языками, на которых описываются модели и спецификации. Однако для указанных выше нотаций такие инструменты есть. Пример для нотации Event-B приводится в приложении Б.
6 Рекомендации по верификации средства защиты информации, реализующего политики управления доступом, на основе формализованных описаний модели управления доступом на системном уровне
6.1 Для верификации средства защиты информации рекомендуется проведение динамической верификации на соответствие формальной модели управления доступом или формальной спецификации этого средства защиты информации.
Примечание - Верификация на системном уровне состоит в проверке соответствия поведения средства защиты информации требованиям модели управления доступом на уровне его внешних интерфейсов, то есть при этом средство защиты информации анализируется как система, и не анализируются его внутренние процессы и функциональность на уровне межмодульных связей.
6.2 Проведение верификации средства защиты информации начинается с анализа соответствия интерфейсов модели управления доступом и интерфейсов средства защиты информации. В случае, когда интерфейсы по структуре совпадают или близки, верификацию средства защиты информации можно проводить, проверяя соответствие поведения средства защиты информации формальной модели управления доступом. В случае, когда структуры интерфейсов различны, необходимо построить формальную спецификацию средства защиты информации и доказать (или продемонстрировать другим способом), что формальная спецификация средства защиты информации соответствует формальной модели управления доступом.
6.3 В случае наличия прямого соответствия между структурами интерфейсов формальной модели управления доступом и формальной спецификации средства защиты информации последняя может быть разработана как прямое уточнение формальной модели управления доступом.
6.4 Если интерфейс средства защиты информации не находится в прямом соответствии с интерфейсом формальной модели управления доступом, для установления соответствия между ними следует применять техники, доступные для разработчиков, включая формальную верификацию (верификацию, выполняемую при помощи формальных методов) или анализ вручную.
Примечание - Наиболее высокий уровень доверия к верификации соответствия формальной модели управления доступом и формальной спецификации средства защиты информации дает формальная верификация, которую можно выполнять при помощи процедуры установления уточнения по состояниям. Эта процедура включает построение так называемого абстрагирующего отображения состояний формальной спецификации средства защиты информации (СЗИ) в состояния формальной модели управления доступом. При этом выполнение условий безопасности в формальной спецификации СЗИ в некотором ее состоянии влечет выполнение условий безопасности формальной модели управления доступом в состоянии, полученном в результате применения абстрагирующего отображения к этому состоянию формальной спецификации СЗИ.
6.5 При проведении динамической верификации средства защиты информации, реализующего политики управления доступом, необходимо оценивать полноту верификации на соответствие формальной спецификации средства защиты информации с отслеживанием покрытия модели (см. приложение А). Если формальная спецификация средства защиты информации не является прямым уточнением формальной модели управления доступом, покрытие формальной модели управления доступом должно отслеживаться отдельно при помощи отображения отдельных событий или цепочек событий из формальной спецификации средства защиты информации в события формальной модели управления доступом.
6.6 В описании результатов верификации должны быть представлены:
- описание формальной спецификации средства защиты информации;
- обоснование того, что эта формальная спецификация соответствует формальной модели управления доступом;
- описание тестового (модельного) окружения и процесса верификации и обоснование выбора этого окружения;
- оценка полноты верификации на основе структуры формальной модели управления доступом и формальной спецификации средства защиты информации.
7 Рекомендации по верификации средства защиты информации, реализующего политики управления доступом, на основе формализованных описаний модели управления доступом на уровне интерфейсов модулей безопасности
7.1 Рекомендации данного раздела относятся к случаю, когда в средстве защиты информации явно выделен модуль безопасности и должна быть проведена его верификация. Такая верификация может проводиться, если есть техническая возможность отделить модуль безопасности от остальных составляющих средства защиты информации и организовать его модульное тестирование.
7.2 Верификация модуля безопасности в средстве защиты, реализующем политики управления доступа, должна основываться на формальной модели управления доступом. Для верификации модуля безопасности сначала необходимо разработать формальную спецификацию интерфейсов модуля.
Примечания
1 Разработка такой спецификации и проверка ее соответствия формальной модели управления доступом и формальной спецификации средства защиты информации в целом во многих случаях является сложной научно-технической задачей. В ряде случаев может быть использован подход на основе технической экспертизы, предполагающей последовательное построение формальной спецификации модуля с многократным и итеративным проведением ее обзоров (инспекций) несколькими специалистами.
2 Ситуация усложняется в тех случаях, когда модуль безопасности строится в виде обобщенного интерпретатора возможных политик, описываемых на некотором структурированном языке и поставляемых в виде отдельных конфигурационных файлов системы защиты информации. Примером такой реализации является модуль LSM SELinux. В этом случае нет какого-либо прямого соответствия между функциональностью модуля самого по себе и моделью управления доступом в целом. В этой ситуации верификация проводится для каждой политики безопасности или для каждого класса политик безопасности.
7.3 Оценку полноты верификации модуля безопасности следует проводить при помощи анализа покрытия модели (см. приложение А).
7.4 Кроме того, необходимо отслеживание покрытия кода модуля получаемыми тестами (не менее уровня покрытия всех ветвлений в программе). Непокрытые ветвления в программе должны анализироваться на предмет возможного существенного влияния на работу модуля в целом, при подтверждении этого влияния должны создаваться дополнительные тесты для покрытия таких ветвлений.
7.5 При проведении верификации конфигурируемого модуля безопасности необходимо использовать различные конфигурации и достигать покрытия структурных элементов языка описания конфигураций (правил и отдельных альтернатив грамматики, отдельных возможных операторов, используемых при описании правил политик, а также возможных сочетаний пар альтернатив в одном правиле).
Примечание - В случае сложных средств защиты информации (например, операционных систем или систем управления базами данных) возможно проведение частичной верификации конфигурируемого модуля, при которой покрытие языка описания конфигураций не достигается, но обеспечивается достаточный анализ ситуаций, возникающих при изменении лишь небольшой части атрибутов конфигурации. В этом случае корректное применение средства защиты информации будет верифицировано только для тех случаев, когда изменения конфигурации/политик безопасности остаются в рамках покрытого тестами множества наборов значений ее атрибутов (в пределе, только при использовании ровно той же конфигурации, для которой была проведена верификация).
7.6 В описании результатов верификации модуля безопасности должны быть представлены:
- описание формальной спецификации модуля безопасности, обоснование того, что она соответствует формальной модели управления доступом и формальной спецификации средства защиты информации;
- описание тестового (модельного) окружения и процесса верификации и обоснование выбора этого окружения;
- оценка полноты верификации на основе структуры формальной модели управления доступом, формальной спецификации средства защиты информации и структуры реализации модуля безопасности.
(справочное)
ПО ОЦЕНКЕ ПОКРЫТИЯ ФОРМАЛЬНЫХ МОДЕЛЕЙ
Критерии покрытия формальных моделей, используемые при тестировании на соответствие им, должны использовать структурные элементы спецификации операций/событий модели в качестве основы.
Обычно операция/событие имеет некоторый набор условий ее успешного выполнения, называемый предусловием или набором охранных условий. При этом некоторые условия из этого набора обеспечивают саму возможность исполнения операции, а другие - обеспечивают успешность ее исполнения при соблюдении правил и условий безопасности. При нарушении условий первого типа операция не может быть исполнена вообще. Операция может быть исполнена при нарушении условий второго типа, но ее исполнение приводит к возвращению специализированного кода ошибки или созданию ситуации, в которой фиксируется нарушение правил.
Для исполнения операции условия первого типа всегда должны быть выполнены, поэтому они не учитываются при определении полноты тестирования. Условия второго типа могут быть нарушены, при этом нарушение каждого из них должно приводить к неуспешному завершению операции. Поэтому для полноты тестирования необходимо обеспечить в тестах ситуацию успешного исполнения, в которой все условия второго типа выполнены, а также ситуации, в которых эти условия нарушены. Рекомендуется создавать, как минимум, набор ситуаций, в которых только одно из этих условий нарушено, а остальные - выполнены. Это обеспечит при тестировании верификацию того, что рассматриваемые условия влияют на успешность выполнения операции независимо.
Иногда ситуация, в которой одно из условий второго типа нарушено, а остальные выполнены, невозможна. В этих случаях рекомендуется создавать возможные ситуации, в которых нарушено минимальное множество условий второго типа, включающее рассматриваемое условие.
Отдельный подход необходим, если условие представляет собой дизъюнкцию из нескольких выражений-дизъюнктов. То же верно для импликации, при этом импликация может быть преобразована в дизъюнкцию по правилу
. В этом случае для создания ситуации, в которой условие принимает значение FALSE, необходимо, чтобы все входящие в дизъюнкцию выражения приняли значение FALSE. Для покрытия ситуаций, в которых полное условие принимает значение TRUE, рекомендуется создать, как минимум, набор ситуаций, в которых каждое отдельное входящее в дизъюнкцию выражение принимает значение TRUE, а остальные - FALSE. Если ситуация, в которой только одно из выражений выполнено, невозможна, рекомендуется создавать возможные ситуации, в которых выполнено минимальное множество выражений-дизъюнктов, включающее рассматриваемое. Эта рекомендация применяется, когда необходимо выполнение условия-дизъюнкции при выполнении остальных охранных условий. Если одно из других охранных условий нарушается, обеспечение значения TRUE для дизъюнкции не имеет особого значения.Пример
Допустим, мы пытаемся покрыть различные ситуации, связанные с работой операции получения доступа субъекта к объекту GetAccess(subj, obj, akind). Пусть условие успешного выполнения этого события имеет следующий вид (числа в квадратных скобках нумеруют отдельные условия и дизъюнкты).
Получение минимального покрывающего набора тестовых ситуаций в соответствии с представленными выше рекомендациями выполняется следующим образом.
Условия 1, 2, 3, по сути, представляют собой типовые ограничения на параметры и не могут быть нарушены при любой попытке исполнения данной операции. Они являются условиями первого типа для данного примера и во всех ситуациях должны иметь значение TRUE.
Условия 4 и 5 являются в этом примере условиями второго типа и могут быть нарушены. При этом условие 5 состоит из дизъюнктов 5.1 и 5.2, и его выполнение может быть обеспечено обращением в TRUE любого из этих дизъюнктов.
Рекомендуемый для создания в тестах минимальный набор ситуаций для данного примера такой.
1. Условия успешного исполнения операции выполнены, дизъюнкция 5 выполнена за счет дизъюнкта 5.1
subj
2. Условия успешного исполнения операции выполнены, дизъюнкция 5 выполнена за счет дизъюнкта 5.2
subj
3. Условия успешного исполнения нарушены за счет нарушения условия 4
subj
4. Условия успешного исполнения нарушены за счет нарушения условия 5
subj
(справочное)
РЕАЛИЗУЮЩЕГО ПОЛИТИКИ УПРАВЛЕНИЯ ДОСТУПОМ, НА ОСНОВЕ
ФОРМАЛИЗОВАННЫХ ОПИСАНИЙ
МОДЕЛИ УПРАВЛЕНИЯ ДОСТУПОМ
Рассматривается пример верификации средства защиты информации файловой системы в рамках типовой операционной системы. В ней есть операция open. В реальных файловых системах open выполняет две функции: открывает файл, если он уже создан; создает и открывает файл, если в момент вызова open файла с указанным именем нет.
При верификации средства защиты информации файловой системы в рамках типовой операционной системы с операцией open, которая открывает файл, если он уже создан, в качестве нотации моделирования используется Event-B. В формальной модели управления доступом операция open представляется как GetAccessForObjOperation, ее вид следующий:
![]() ![]() В формальной спецификации системного вызова соответствующая операция open выглядит так:
![]() ![]() ![]() Для организации динамической верификации необходимо построить отображение реализационных сущностей (типов данных, переменных, областей памяти и других элементов программы) и вызовов операций в модельные. Реализационными вызовами здесь является подмножество системных вызовов open при условии открытия существующих в системе файлов.
Пример
int open(const char *pathname, int flags);
Где:
Существуют и другие системные вызовы, например openat, описываемые данной моделью, но их рассмотрение выходит за рамки примера.
В качестве отдельного теста может служить простая программа, выполняющая один системный вызов.
Пример
int
main(int argc, char *argv[])
{
syscall(SYS_open, argv[1], argv[2]);
return 0;
}
Тестирование сводится к выполнению этой программы от лица разных пользователей, на файлах с разными разрешениями доступа и разными режимами открытия файла.
Отчет о результатах тестирования может выглядеть как таблица с информацией о покрытых условиях, входящих в охранные условия (см. приложение А) модельной операции (см. таблицу Б.1). К примеру, 141 тест на открытие существующего файла покрыл модельные условия следующим образом: T - количество раз, когда условие получило истинное значение, F - когда условие получило ложное значение, U - когда оно не могло быть вычислено, I - протестировано ли условие независимо от остальных.
Таблица Б.1
модельной операции
Условия grd1 - grd4, grd6 - grd8, grd11 и grd16 опущены, так как они представляют собой типовые ограничения на параметры и всегда должны выполняться.
Условие grd5 в данном примере означает вызов операции с согласованными значениями флагов, что также всегда должно выполняться.
Условие grd9 также означает согласованность флагов при вызове операции для существующего файла и тоже не может быть нарушено.
Условие grd10 представляет собой ограничение на возможные флаги, позволяющие открыть файл только на чтение, только на запись и на чтение и запись одновременно. В рамках тестов реализовывались только первые две ситуации, открытие на чтение и запись одновременно не выполнялось.
Условия grd12 и grd15 означают ограничения на согласованность флагов при открытии каталога. Сами ограничения не нарушались, но в ходе тестов открывались как каталоги, так и обычные файлы.
Условия grd13 и grd 14 означают ограничения на количество файлов, открытых в рамках одного процесса и в системе в целом. Они в рамках тестов всегда были выполнены, попыток открыть слишком большое число файлов не предпринималось.
Условие grd17 означает ограничение на доступность всех директорий на пути до открываемого файла. Это условие в тестах принимало значение как TRUE, так и FALSE.
Условия grd18, grd19 и grd20 описывают специфические ограничения, которые должны выполняться в системе при корректном доступе к файлу только на чтение (grd18), только на запись (grd19) и на чтение и запись (grd20). Эти условия были разбиты на элементарные логические формулы, которые в большинстве случаев (кроме формулы grd20_c00) в тестах принимали значения как TRUE, так и FALSE. При этом сами условия grd18 и grd19 также принимали оба значения, а условие grd20 всегда было выполнено.
Соответственно, рекомендации по покрытию ситуаций, где остальные изменяемые охранные условия принимают оба возможных значения, выполнены, за исключением ситуаций открытия файлов на чтение и запись одновременно.
Проверка набора тестовых ситуаций по независимому выполнению отдельных условий в этом примере не полностью выполнена. На практике полный перебор бывает сложен и анализ зависимостей весьма трудоемок. Известно, что полный перебор тестовых ситуаций с анализом независимого выполнения отдельных условий позволяет повысить степень уверенности в корректности тестируемой системы, такой перебор предписывается, например, в Квалификационных требованиях [1].
Вернуться в "Каталог нормативных документов"
Источник информации: https://internet-law.ru/documents/prod/gost-r_gosudarstvennyj-standart/16/gost_90948.html
На правах рекламы:
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||