А.3 Анализ непротиворечивости

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

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

В ИСО/МЭК 15408 различаются несколько типов анализа непротиворечивости.

a) Оценщику необходимо проанализировать внутреннюю непротиворечивость поставки для оценки. Примеры:

- ADV_FSP.1.2C: «Функциональная спецификация должна быть внутренне непротиворечивой»;

- ADV_HLD.1.2C: «Проект верхнего уровня должен быть внутренне непротиворечивым»;

- ADV_IMP.1.2C: «Представление реализации должно быть внутренне непротиворечивым»;

- ADV_LLD.1.2C: «Проект нижнего уровня должен быть внутренне непротиворечивым».

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

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

b) Оценщику необходимо проанализировать, согласована ли поставка для оценки с одной или несколькими другими поставками. Примеры:

- AGD_ADM.1.7C: «Руководство администратора должно быть согласовано со всей другой документацией, представленной для оценки»;

- AGD_USR.1.5C: «Руководство пользователя должно быть согласовано со всей другой документацией, представленной для оценки».

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

- противоречия с другими руководствами по использованию функций безопасности;

- противоречия с ЗБ (например, в части угроз, предположений безопасного использования. не-ИТ-целей безопасности или функций безопасности ИТ);

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

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

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

c) Оценщику необходимо проанализировать и то, что поставка для оценки внутренне непротиворечива, и то, что поставка для оценки согласована с другими поставками. Пример:

- AVA_MSU.1.2C: «Руководства должны быть полны, понятны, непротиворечивы и обоснованны».

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

d) Оценщику необходимо проверить результаты анализа, представленные разработчиком и требуемые для демонстрации непротиворечивости. Примеры:

- ADV_SPM.1.3С: «Модель ПБО должна включать в себя обоснование, которое демонстрирует, что она согласована и полна относительно всех политик ПБО, которые могут быть смоделированы»;

- ADV_SPM.1.4C: «Демонстрация соответствия между моделью ПБО и функциональной спецификацией должна показать, что все функции безопасности в функциональной спецификации являются непротиворечивыми и полными относительно модели ПБО».

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

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

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

Проверка непротиворечивости поставок для оценки может выявить упущения, из-за которых может потребоваться повторное выполнение завершенных ранее шагов оценивания. Например, проверка непротиворечивости целей безопасности может выявить пропуск одного или нескольких требований безопасности. В этом случае оценщику следует проверить соответствие между целями безопасности и ФБО.

Далее >>>