Тестирование политики безопасности решения на языке Policy Assertion Language (PAL)
Базовый сценарий использования Policy Assertion Language (PAL) – это создание тестовых сценариев для проверки политик безопасности решения, написанных с использованием PSL.
Язык PAL позволяет формировать и отправлять запросы в модуль безопасности, проверяя полученные решения на соответствие ожидаемым решениям. При этом для запуска тестовых сценариев, написанных на PAL, нет необходимости генерировать код клиент-серверных взаимодействий, так как PAL работает на уровне абстракции модуля безопасности.
Общий синтаксис
Тестовый сценарий является последовательностью запросов к модулю безопасности, для каждого из которых указано ожидаемое решение.
Тестовые сценарии можно объединять в группы. Группа сценариев может также содержать секции setup и finally, которые будут выполняться соответственно перед и после выполнения каждого сценария в этой группе. Это можно использовать для задания общих стартовых условий или для проверки общих инвариантов.
Для объявления группы тестовых сценариев используется блочная декларация assert:
assert "имя группы сценариев" {
setup {}
sequence "имя сценария 1" {}
sequence "имя сценария 2" {}
...
finally {}
}
Синтаксис запросов
Для конфигурирования запросов внутри тестовых сценариев используются декларации следующего вида:
<ожидание> <заголовок> <операция> <селекторы события> {сообщение}
Здесь:
<ожидание>– ожидаемое решение:grant,denyилиany.При ожидании
anyрешение модуля безопасности игнорируется, но ошибка при выполнении запроса пометит тестовый сценарий как неудачный.Если ожидаемое решение не указано явно, ожидается решение
grant.<заголовок>– опциональный параметр, содержащий текстовый заголовок описываемого запроса.<операция>– один из видов обращения к модулю безопасности:execute,security,requestилиresponse.<селекторы события>– допустимые селекторы события совпадают с селекторами, использующимися при привязке методов моделей безопасности к событиям безопасности. Например можно указать сущность-получатель сообщения или вызываемый метод.{сообщение}– параметр, содержащий значение аргументов вызываемого метода. Значение этого параметра должно соответствовать операции и селекторам запроса. По умолчанию передается пустое количество аргументов{}.
Пример:
assert "some tests" {
sequence "first sequence" {
// При вызове сущностью Client метода Ping реализации интерфейса pingComp.pingImpl сущности Server ожидается решение grant
// При этом в аргументе value метода Ping передается значение 100
grant "Client calls Ping" request src=Client dst=Server endpoint=pingComp.pingImpl method=Ping {value: 100}
// Ожидается, что сущности Server запрещено отвечать на запросы сущности Client
deny "Server cannot respond" response src=Server dst=Client
}
}
Сокращенная форма запросов
Для удобства можно также применять следующие сокращенные формы запросов:
- При выполнении операции
execute, можно сохранить дескриптор запускаемой сущности в переменную с помощью оператора<-. - Сокращенная форма для операции
security:<сущность> ! <путь.к.методу> {сообщение}При выполнении разворачивается в полную форму:
security src=<сущность> method=<путь.к.методу> {сообщение} - Сокращенная форма для операции
request:<клиент> ~> <сервер> : <путь.к.имплементации.метода> {сообщение}При выполнении разворачивается в полную форму:
request src=<клиент> dst=<сервер> endpoint=<путь.к.имплементации> method=<метод> {сообщение} - Сокращенная форма для операции
response:<клиент> <~ <сервер> : <путь.к.имплементации.метода> {сообщение}При выполнении разворачивается в полную форму:
response src=<сервер> dst=<клиент> endpoint=<путь.к.имплементации> method=<метод> {сообщение}
Пример:
assert "ping test"{
setup {
// переменная s содержит указатель на запущенный экземпляр сущности Server
s <- execute dst=ping.Server
// переменная c содержит указатель на запущенный экземпляр сущности Client
c <- execute dst=ping.Client
}
sequence "ping ping is denied" {
// При вызове сущностью Client метода Ping реализации интерфейса pingComp.pingImpl сущности Server ожидается решение grant
// При этом в аргументе value метода Ping передается значение 100
c ~> s : pingComp.pingImpl.Ping {value: 100 }
// При повторном вызове ожидается решение deny
deny c ~> s : pingComp.pingImpl.Ping {value: 100 }
}
sequence "normal" {
// При последовательном вызове методов Ping и Pong ожидаются решения grant
c ~> s : pingComp.pingImpl.Ping { value: 100 }
c ~> s : pingComp.pingImpl.Pong { value: 100 }
}
}
Запуск тестов
Чтобы запустить написанные на PAL тестовые сценарии, необходимо использовать флаг --tests run при запуске компилятора nk-psl-gen-c:
$ nk-psl-gen-c --tests run <другие параметры> ./security.psl
Компилятор nk-psl-gen-c сгенерирует код модуля безопасности и код тестовых сценариев, а затем скомпилирует их с помощью gcc и запустит.
Чтобы сгенерировать код тестовых сценариев, но не компилировать и запускать их, необходимо использовать флаг --tests generate.