ГОСТ Р 59453.2-2021

НАЦИОНАЛЬНЫЙ СТАНДАРТ РОССИЙСКОЙ ФЕДЕРАЦИИ

Защита информации

ФОРМАЛЬНАЯ МОДЕЛЬ УПРАВЛЕНИЯ ДОСТУПОМ

Часть 2

Рекомендации по верификации формальной модели управления доступом

Information protection. Formal access control model. Part 2. Recommendations on verification of formal access control model

ОКС 35.030

Дата введения 2021-06-01

Предисловие

1 РАЗРАБОТАН Федеральной службой по техническому и экспортному контролю (ФСТЭК России), Обществом с ограниченной ответственностью "РусБИТех-Астра" (ООО "РусБИТех-Астра"), Институтом системного программирования им.В.П.Иванникова Российской академии наук (ИСП РАН)

2 ВНЕСЕН Техническим комитетом по стандартизации ТК 362 "Защита информации"

3 УТВЕРЖДЕН И ВВЕДЕН В ДЕЙСТВИЕ Приказом Федерального агентства по техническому регулированию и метрологии от 22 апреля 2021 г. N 271-ст

4 ВВЕДЕН ВПЕРВЫЕ

Правила применения настоящего стандарта установлены в статье 26 Федерального закона от 29 июня 2015 г. N 162-ФЗ "О стандартизации в Российской Федерации". Информация об изменениях к настоящему стандарту публикуется в ежегодном (по состоянию на 1 января текущего года) информационном указателе "Национальные стандарты", а официальный текст изменений и поправок - в ежемесячном информационном указателе "Национальные стандарты". В случае пересмотра (замены) или отмены настоящего стандарта соответствующее уведомление будет опубликовано в ближайшем выпуске ежемесячного информационного указателя "Национальные стандарты". Соответствующая информация, уведомление и тексты размещаются также в информационной системе общего пользования - на официальном сайте Федерального агентства по техническому регулированию и метрологии в сети Интернет (www.gost.ru)

Введение

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

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

В связи с этим настоящий стандарт устанавливает рекомендации по верификации формальных моделей управления доступом с применением инструментальных средств.

Настоящий стандарт применяется совместно с ГОСТ Р 59453.1-2021 "Защита информации. Формальная модель управления доступом. Часть 1. Общие положения".

     1 Область применения

Настоящий стандарт представляет собой рекомендации по верификации с применением инструментальных средств формальных моделей управления доступом, на основе которых разрабатываются средства защиты информации, реализующие политики управления доступом.

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

     2 Нормативные ссылки

В настоящем стандарте применена нормативная ссылка на следующий стандарт:

ГОСТ Р 59453.1 Защита информации. Формальная модель управления доступом. Часть 1. Общие положения

Примечание - При пользовании настоящим стандартом целесообразно проверить действие ссылочных стандартов в информационной системе общего пользования - на официальном сайте Федерального агентства по техническому регулированию и метрологии в сети Интернет или по ежегодному информационному указателю "Национальные стандарты", который опубликован по состоянию на 1 января текущего года, и по выпускам ежемесячного информационного указателя "Национальные стандарты" за текущий год. Если заменен ссылочный стандарт, на который дана недатированная ссылка, то рекомендуется использовать действующую версию этого стандарта с учетом всех внесенных в данную версию изменений. Если заменен ссылочный стандарт, на который дана датированная ссылка, то рекомендуется использовать версию этого стандарта с указанным выше годом утверждения (принятия). Если после утверждения настоящего стандарта в ссылочный стандарт, на который дана датированная ссылка, внесено изменение, затрагивающее положение, на которое дана ссылка, то это положение рекомендуется применять без учета данного изменения. Если ссылочный стандарт отменен без замены, то положение, в котором дана ссылка на него, рекомендуется применять в части, не затрагивающей эту ссылку.

     3 Термины и определения

В настоящем стандарте применены термины по ГОСТ Р 59453.1, а также следующие термины с соответствующими определениями:

3.1 верификация формальной модели управления доступом: Подтверждение посредством представления объективных свидетельств непротиворечивости формальной модели управления доступом и выполнения заданных в ее рамках условий безопасности.

3.2 инструментальное средство верификации: Инструментальное средство, реализующее формальные методы верификации формальных моделей.

Примечание - Инструментальное средство верификации, как правило, поддерживает и формальные методы разработки формальных моделей.

3.3 формализованное (машиночитаемое) описание: Описание формальной модели на формальном языке со строгой и однозначно определенной семантикой, позволяющее использовать инструментальные средства верификации.

3.4 формальный метод: Основанный на математике и логике метод, а также поддерживаемые им языки, для верификации или разработки формальных моделей.

     4 Общие положения

4.1 Для верификации формальной модели управления доступом, описание которой соответствует критериям, установленным ГОСТ Р 59453.1, должен быть осуществлен выбор соответствующих инструментальных средств, для которых должны быть представлены свидетельства, что реализуемые ими формальные методы позволяют осуществить верификацию формальной модели. При этом выбранные инструментальные средства должны допускать полную, независимую от их разработчиков проверку корректности результатов их работы.

4.2 Для верификации с использованием инструментальных средств формальная модель должна иметь формализованное (машиночитаемое) описание на языке, поддерживаемом реализуемыми этими инструментальными средствами формальными методами. Если формальная модель имеет математическое описание, то оно должно быть переведено в формализованное (машиночитаемое) описание на этом языке. При этом должны быть представлены свидетельства согласованности математического и формализованного (машиночитаемого) описаний формальной модели.

Примечание - Для формализованного (машиночитаемого) описания формальной модели управления доступом, как правило, используются формальные методы (Alloy, ASM, B, Event-B, TLA+, VDM-SL, Z), языки которых позволяют строить абстрактные автоматные модели. Примерами инструментальных средств, реализующих эти формальные методы, являются Rodin, TLA Toolbox. Кроме моделирования на основе абстрактных автоматных моделей, для верификации формальных моделей управления доступом могут использоваться темпоральные логики, сети Петри и другие формальные методы.

4.3 Верификация формальной модели управления доступом должна быть осуществлена путем применения к ее формализованному (машиночитаемому) описанию инструментальных средств верификации.

4.4 Верификация формальной модели управления доступом является успешной, если результаты применения инструментальных средств верификации к ее формализованному (машиночитаемому) описанию позволяют сделать вывод о непротиворечивости формальной модели и о выполнении заданных в ее рамках условий безопасности.

     5 Выбор инструментальных средств верификации формальной модели управления доступом

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

5.2 Критерии выбора языка формализованного (машиночитаемого) описания формальной модели управления доступом должны быть основаны на оценке его возможностей (наличие теоретико-множественных примитивов и средств описания сложных структур данных) для представления описываемых в рамках формальной модели состояний и правил перехода из состояний в состояния абстрактного автомата.

5.3 Критерии выбора инструментальных средств верификации, реализующих формальные методы, поддерживающие соответствующий сформированным согласно 5.2 критериям язык формализованного (машиночитаемого) описания формальной модели управления доступом, должны быть основаны на оценке характеристик этих инструментальных средств, включая:

- функциональные характеристики: возможность полной, независимой от разработчиков инструментальных средств верификации проверки корректности результатов их работы; возможность автоматического и интерактивного доказательства, автоматической или полуавтоматической генерации условий верификации (инвариантов), повторного использования ранее полученных доказательств выполнения условий верификации (переиспользования артефактов), создаваемых в ходе верификации; ограничения на размер абстрактного автомата; скорость верификации;

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

5.4 Должны быть представлены свидетельства соответствия выбранных согласно 5.3 инструментальных средств верификации критериям, сформулированным согласно 5.1.

     6 Формализованное (машиночитаемое) описание формальной модели управления доступом

6.1 Для верификации формальная модель управления доступом должна иметь соответствующее ГОСТ Р 59453.1 формализованное (машиночитаемое) описание. Язык описания должен позволять выполнить требования к описанию формальной модели управления доступом и быть обеспечен инструментальными средствами для ее верификации, отвечающими критериям в соответствии с 5.3.

6.2 Если формальная модель управления доступом описана на математическом языке, то должен быть осуществлен перевод ее математического описания в формализованное (машиночитаемое) описание на языке, поддерживаемом формальными методами, реализуемыми выбранными в соответствии с 5.3 инструментальными средствами верификации.

6.3 При переводе математического описания в формализованное (машиночитаемое) описание формальной модели управления доступом должны быть последовательно описаны:

- элементы состояний абстрактного автомата в математическом описании формальной модели;

- правила перехода абстрактного автомата из состояний в состояния, при этом допустимо объединение нескольких правил в одно или разбиение некоторого правила на несколько с сохранением его свойств;

- условия выполнения политик управления доступом в состояниях абстрактного автомата и при переходах из состояний в состояния абстрактного автомата (условия безопасности), при этом могут быть добавлены недостающие для осуществления верификации условия, в целом составляющие условия верификации.

Примеры перевода элементов математического описания формальной модели управления доступом в формализованное (машиночитаемое) описание приведены в приложении А.

6.4 Если при переводе математического описания в формализованное (машиночитаемое) описание формальной модели управления доступом проводилась корректировка математического описания, то скорректированное математическое описание должно соответствовать ГОСТ Р 59453.1.

6.5 Если полученное в соответствии с 6.2 формализованное (машиночитаемое) описание формальной модели управления доступом имеет несоответствия ее математическому описанию, то должны быть представлены свидетельства согласованности и непротиворечивости этих описаний.

     7 Верификация формализованного (машиночитаемого) описания формальной модели управления доступом

7.1 При верификации формальной модели управления доступом выбранные в соответствии с 5.3 инструментальные средства верификации должны быть применены к ее формализованному (машиночитаемому) описанию, полученному в соответствии с 6.1.

7.2 Верификация формализованного (машиночитаемого) описания формальной модели управления доступом с применением инструментальных средств должна состоять в выполнении следующих действий:

- должно быть осуществлено автоматическое доказательство непротиворечивости формальной модели и выполнения заданных в ее рамках условий безопасности (условий верификации) при наличии у инструментальных средств соответствующей функциональности, в противном случае должно быть выполнено интерактивное доказательство этих условий верификации;