KasperskyOS Community Edition 1.2

Синтаксис языка PSL

Базовые правила

  1. Декларации могут располагаться в файле в любом порядке.
  2. Одна декларация может быть записана в одну или несколько строк.
  3. Язык PSL чувствителен к регистру символов.
  4. Поддерживаются однострочные и многострочные комментарии:
    /* Это комментарий * И это тоже */ // Ещё один комментарий

Типы деклараций

В языке PSL есть следующие типы деклараций:

  • установка глобальных параметров политики безопасности решения;
  • включение PSL-файлов в описание политики безопасности решения;
  • включение EDL-файлов в описание политики безопасности решения;
  • создание объектов моделей безопасности;
  • привязка методов моделей безопасности к событиям безопасности;
  • создание профилей аудита безопасности;
  • создание тестов политики безопасности решения.

В этом разделе

Установка глобальных параметров политики безопасности решения на базе KasperskyOS

Включение PSL-файлов в описание политики безопасности решения на базе KasperskyOS

Включение EDL-файлов в описание политики безопасности решения на базе KasperskyOS

Создание объектов моделей безопасности

Привязка методов моделей безопасности к событиям безопасности

Создание профилей аудита безопасности

Создание и выполнение тестов политики безопасности решения на базе KasperskyOS

Типы данных в языке PSL

Примеры привязок методов моделей безопасности к событиям безопасности

Примеры описаний простейших политик безопасности решений на базе KasperskyOS

Примеры профилей аудита безопасности

Примеры тестов политик безопасности решений на базе KasperskyOS

В начало
[Topic ssp_descr_psl_syntax_intro]

Установка глобальных параметров политики безопасности решения на базе KasperskyOS

Глобальными являются следующие параметры политики безопасности решения:

  • Execute-интерфейс, через который ядро KasperskyOS обращается к модулю безопасности Kaspersky Security Module, чтобы сообщить о запуске ядра или об инициации запуска процесса ядром или другим процессом. Чтобы задать этот интерфейс, нужно использовать следующую декларацию:
    execute: kl.core.Execute

    В настоящее время в KasperskyOS поддерживается только один execute-интерфейс Execute, определенный в файле kl/core/Execute.idl. (Этот интерфейс состоит из одного метода main, который не имеет параметров и не выполняет никаких действий. Метод main зарезервирован для возможного использования в будущем.)

  • [Опционально] Глобальный профиль аудита безопасности и начальный уровень аудита безопасности. (О профилях и уровне аудита безопасности см. "Создание профилей аудита безопасности".) Чтобы задать эти параметры, нужно использовать следующую декларацию:
    audit default = <имя профиля аудита безопасности> <уровень аудита безопасности>

    Пример:

    audit default = global 0

    По умолчанию в качестве глобального используется пустой профиль аудита безопасности empty, описанный в файле toolchain/include/nk/base.psl из состава KasperskyOS SDK, и уровень аудита безопасности 0. Применение профиля аудита безопасности empty означает, что аудит безопасности не выполняется.

В начало
[Topic ssp_descr_psl_syntax_global_params]

Включение PSL-файлов в описание политики безопасности решения на базе KasperskyOS

Чтобы включить в описание политики PSL-файл, нужно использовать следующую декларацию:

use <ссылка на PSL-файл._>

Ссылка на PSL-файл представляет собой путь к PSL-файлу (без расширения и точки перед ним) относительно директории, которая включена в набор директорий, где компилятор nk-psl-gen-c ищет PSL-, IDL-, CDL-, EDL-файлы. (Этот набор директорий задается параметрами -I <путь к директории> при запуске скрипта makekss или компилятора nk-psl-gen-c.) В качестве разделителя в описании пути используется точка. Декларация завершается последовательностью символов ._.

Пример:

use policy_parts.flow_part._

Эта декларация включает файл flow_part.psl, который находится в директории policy_parts. Директория policy_parts должна находиться в одной из директорий, где компилятор nk-psl-gen-c выполняет поиск PSL-, IDL-, CDL-, EDL-файлов. Например, директория policy_parts может располагаться в одной директории с PSL-файлом, содержащим эту декларацию.

Включение PSL-файла с формальным описанием модели безопасности

Чтобы использовать методы требуемой модели безопасности, нужно включить в описание политики PSL-файл с формальным описанием этой модели. PSL-файлы с формальными описаниями моделей безопасности находятся в KasperskyOS SDK по пути:

toolchain/include/nk

Пример:

/* Включение файла base.psl с формальным описанием модели * безопасности Base */ use nk.base._ /* Включение файла flow.psl с формальным описанием модели * безопасности Flow */ use nk.flow._ /* Компилятор nk-psl-gen-c должен быть настроен на поиск * PSL-, IDL-, CDL-, EDL-файлов в директории toolchain/include. */
В начало
[Topic ssp_descr_psl_syntax_include_psl]

Включение EDL-файлов в описание политики безопасности решения на базе KasperskyOS

Чтобы включить в описание политики EDL-файл для ядра KasperskyOS, нужно использовать следующую декларацию:

use EDL kl.core.Core

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

use EDL <ссылка на EDL-файл>

Ссылка на EDL-файл представляет собой путь к EDL-файлу (без расширения и точки перед ним) относительно директории, которая включена в набор директорий, где компилятор nk-psl-gen-c ищет PSL-IDL-, CDL-, EDL-файлы. (Этот набор директорий задается параметрами -I <путь к директории> при запуске скрипта makekss или компилятора nk-psl-gen-c.) В качестве разделителя в описании пути используется точка.

Пример:

/* Включение файла UART.edl, который находится * в KasperskyOS SDK по пути sysroot-*-kos/include/kl/drivers. */ use EDL kl.drivers.UART /* Компилятор nk-psl-gen-c должен быть настроен на поиск * PSL-, IDL-, CDL-, EDL-файлов в директории sysroot-*-kos/include. */

Компилятор nk-psl-gen-c находит IDL-, CDL-файлы через EDL-файлы, так как EDL-файлы содержат ссылки на соответствующие CDL-, IDL-файлы, а CDL-файлы содержат ссылки на соответствующие CDL-, IDL-файлы.

В начало
[Topic ssp_descr_psl_syntax_include_edl]

Создание объектов моделей безопасности

Чтобы вызывать методы требуемой модели безопасности, нужно создать объект этой модели безопасности.

Чтобы создать объект модели безопасности, нужно использовать следующую декларацию:

policy object <имя объекта модели безопасности : название модели безопасности> { [параметры объекта модели безопасности] }

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

В начало
[Topic ssp_descr_psl_syntax_create_objects]

Привязка методов моделей безопасности к событиям безопасности

Чтобы создать привязку методов моделей безопасности к событию безопасности, нужно использовать следующую декларацию:

<вид события безопасности> [селекторы события безопасности] { [профиль аудита безопасности] <вызываемые методы моделей безопасности> }

Вид события безопасности

Чтобы задать вид события безопасности, нужно использовать следующие спецификаторы:

  • request – отправка IPC-запросов;
  • response – отправка IPC-ответов;
  • error – отправка IPC-ответов, содержащих сведения об ошибках;
  • security – обращения процессов к модулю безопасности Kaspersky Security Module через интерфейс безопасности;
  • execute – инициация запусков процессов или запуск ядра KasperskyOS.

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

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

Селекторы события безопасности

Селекторы события безопасности позволяют уточнить описание события безопасности заданного вида. Можно использовать следующие селекторы:

  • src=<имя класса процессов/ядро> – процессы заданного класса или ядро KasperskyOS являются источниками IPC-сообщений;
  • dst=<имя класса процессов/ядро> – процессы заданного класса или ядро являются приемниками IPC-сообщений;
  • interface=<имя интерфейса> – описывает следующие события безопасности:
    • клиенты пытаются использовать службы серверов или ядра с заданным интерфейсом;
    • процессы обращаются к модулю безопасности Kaspersky Security Module через заданный интерфейс безопасности;
    • серверы или ядро отправляют клиентам результаты использования служб с заданным интерфейсом;
  • component=<имя компонента> – описывает следующие события безопасности:
    • клиенты пытаются использовать службы серверов или ядра, предоставляемые заданным компонентом;
    • серверы или ядро отправляют клиентам результаты использования служб, предоставляемых заданным компонентом;
  • endpoint=<квалифицированное имя службы> – описывает следующие события безопасности:
    • клиенты пытаются использовать заданную службу серверов или ядра;
    • серверы или ядро отправляют клиентам результаты использования заданной службы;
  • method=<имя метода> – описывает следующие события безопасности:
    • клиенты пытаются обратиться к серверам или ядру, вызывая заданный метод службы;
    • процессы обращаются к модулю безопасности, вызывая заданный метод интерфейса безопасности;
    • серверы или ядро отправляют клиентам результаты вызова заданного метода службы;
    • ядро сообщает о своем запуске модулю безопасности, вызывая заданный метод execute-интерфейса;
    • ядро инициирует запуски процессов, вызывая заданный метод execute-интерфейса;
    • процессы инициируют запуски других процессов, в результате чего ядро вызывает заданный метод execute-интерфейса.

Классы процессов, компоненты, экземпляры компонентов, интерфейсы, службы, методы должны называться так, как они называются в IDL-, CDL-, EDL-описаниях. Ядро должно называться kl.core.Core.

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

Для событий вида security нужно указывать квалифицированное имя метода интерфейса безопасности, если требуется использовать интерфейс безопасности, заданный в CDL-описании. (Если требуется использовать интерфейс безопасности, заданный в EDL-описании, указывать квалифицированное имя метода не нужно.) Квалифицированное имя метода интерфейса безопасности является конструкцией вида <путь к интерфейсу безопасности.имя метода>. Путь к интерфейсу безопасности представляет собой последовательность разделенных точкой имен экземпляров компонентов, среди которых каждый последующий экземпляр компонента вложен в предыдущий, а последний поддерживает интерфейс безопасности, который включает метод с заданным именем.

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

Можно использовать комбинации селекторов. При этом селекторы можно разделять запятыми.

На использование селекторов есть ограничения. Для событий безопасности вида execute нельзя использовать селекторы interface, component и endpoint. Для событий безопасности вида security нельзя использовать селекторы dst, component, endpoint.

Также есть ограничения на комбинации селекторов. Для событий безопасности видов request, response и error селектор method можно использовать только совместно с одним из селекторов endpoint, interface, component или их комбинацией. (Селекторы method, endpoint, interface и component должны быть согласованы, то есть метод, служба, интерфейс и компонент должны быть связаны между собой.) Для событий безопасности вида request селектор endpoint можно использовать только совместно с селектором dst. Для событий безопасности видов response и error селектор endpoint можно использовать только совместно с селектором src.

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

Чтобы описанию события безопасности соответствовали IPC-сообщения одного типа, для этого описания должно выполняться одно из следующих условий:

  • Для событий безопасности вида request, response и error однозначно определена цепочка "интерфейсный метод-служба-класс сервера или ядро". Например, описанию события безопасности request dst=Server endpoint=net.Net method=Send соответствуют IPC-сообщения одного типа, а описанию события безопасности request dst=Server соответствуют любые IPC-сообщения, отправляемые серверу Server.
  • Для событий вида security указан метод интерфейса безопасности.
  • Для событий вида execute указан метод execute-интерфейса.

    В настоящее время поддерживается только один фиктивный метод execute-интерфейса main. Этот метод используется по умолчанию, поэтому его можно не задавать через селектор method. Таким образом, любому описанию события безопасности вида execute соответствуют IPC-сообщения одного типа.

Профиль аудита безопасности

Чтобы задать профиль аудита безопасности, нужно использовать следующую конструкцию:

audit <имя профиля аудита безопасности>

Если профиль аудита безопасности не задан, используется глобальный профиль аудита безопасности.

Вызываемые методы моделей безопасности

Чтобы вызвать метод модели безопасности, нужно использовать следующую конструкцию:

[имя объекта модели безопасности.]<имя метода модели безопасности> <параметр>

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

  • Если у метода модели безопасности фактически нет параметра, то формально этот метод имеет параметр типа Unit, обозначаемый как ().
  • Если параметром метода модели безопасности является словарь {имя поля 1 : значение поля 1[, имя поля 2 : значение поля 2...]}, то этот параметр не нужно заключать в круглые скобки.
  • Если параметр метода модели безопасности не является словарем и не имеет тип Unit, то этот параметр нужно заключить в круглые скобки.

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

При обработке события безопасности модулем безопасности Kaspersky Security Module выражения вызываются перед правилами, поэтому выражения не получают изменений, сделанных правилами. Например, если в декларации привязки методов модели безопасности StaticMap к событиям безопасности сначала указано правило set, а затем для того же ресурса указано выражение get_uncommited, то выражение get_uncommited вернет значение ключа, которое было до обработки текущего события безопасности, а не то, которое задано правилом set при обработке текущего события безопасности. Значение ключа, заданное правилом set при обработке текущего события безопасности, может быть возвращено выражением get_uncommited только при обработки последующих событий безопасности, если в результате обработки текущего события безопасности модуль безопасности вернет решение "разрешено". Если в результате обработки текущего события безопасности модуль безопасности вернет решение "запрещено", то все изменения, сделанные правилами и выражениями, вызванными при обработке текущего события безопасности, будут отменены.

Метод модели безопасности (правило или выражение) через параметр может принимать параметры интерфейсных методов. (О получении доступа к параметрам интерфейсных методов см. "Модель безопасности Struct"). Также метод модели безопасности через параметр может принимать значения SID процессов и ядра KasperskyOS, которые задаются ключевыми словами src_sid и dst_sid. Первое означает SID процесса (или ядра), который является источником IPC-сообщения. Второе означает SID процесса (или ядра), который является приемником IPC-сообщения (при обращениях к модулю безопасности Kaspersky Security Module dst_sid использовать нельзя).

Для вызова некоторых методов моделей безопасности можно не указывать имя объекта модели безопасности. Также часть методов моделей безопасности нужно вызывать, используя операторы, а не конструкцию вызова. Подробнее о методах моделей безопасности см. "Модели безопасности KasperskyOS".

Вложенные конструкции для привязки методов моделей безопасности к событиям безопасности

В одной декларации можно создать привязку методов моделей безопасности к разным событиям безопасности одного вида. Для этого нужно использовать match-секции, которые представляют собой конструкции следующего вида:

match <селекторы события безопасности> { [профиль аудита безопасности] <вызываемые методы моделей безопасности> }

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

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

choice <вызов выражения модели безопасности, проверяющего выполнение условий> { "<условие 1>" : [{] // Условная секция 1 <вызываемые методы моделей безопасности> [}] "<условие 2>" : ... // Условная секция 2 ... _ : ... // Условная секция, если ни одно условие не выполняется. }

Конструкцию choice можно использовать внутри match-секции. Условная секция использует селекторы события безопасности и профиль аудита безопасности своего контейнера.

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

В качестве выражения, проверяющего выполнение условий в конструкции choice, можно использовать только те выражения, которые предназначены специально для этого. Некоторые модели безопасности содержат такие выражения (подробнее см. "Модели безопасности KasperskyOS").

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

Примеры привязок методов моделей безопасности к событиям безопасности

См. "Примеры привязок методов моделей безопасности к событиям безопасности", "Примеры описаний простейших политик безопасности решений на базе KasperskyOS", "Модели безопасности KasperskyOS".

В начало
[Topic ssp_descr_psl_syntax_binding]

Создание профилей аудита безопасности

Аудит безопасности (далее также аудит) представляет собой следующую последовательность действий. Модуль безопасности Kaspersky Security Module сообщает ядру KasperskyOS сведения о решениях, принятых этим модулем. Затем ядро передает эти данные системной программе Klog, которая декодирует их и передает системной программе KlogStorage (передача данных осуществляется через IPC). Последняя направляет полученные данные в стандартный вывод (или стандартный вывод ошибок) либо записывает в файл.

Данные аудита безопасности (далее данные аудита) – это сведения о решениях модуля безопасности Kaspersky Security Module, которые включают сами решения ("разрешено" или "запрещено"), описания событий безопасности, результаты вызовов методов моделей безопасности, а также данные о некорректности IPC-сообщений. Данные о вызовах выражений моделей безопасности входят в данные аудита так же, как и данные о вызовах правил моделей безопасности.

Для выполнения аудита безопасности нужно ассоциировать объекты моделей безопасности с профилем (профилями) аудита безопасности. Профиль аудита безопасности (далее также профиль аудита) объединяет в себе конфигурации аудита безопасности (далее также конфигурации аудита), каждая из которых задает объекты моделей безопасности, покрываемые аудитом, а также условия выполнения аудита. Можно задать глобальный профиль аудита (подробнее см. "Установка глобальных параметров политики безопасности решения на базе KasperskyOS") и/или назначить профиль (профили) аудита на уровне привязок методов моделей безопасности к событиям безопасности, и/или назначить профиль (профили) аудита на уровне match-секций (подробнее см. "Привязка методов моделей безопасности к событиям безопасности").

Независимо от того, используются профили аудита или нет, данные аудита содержат сведения о решениях "запрещено", которые приняты модулем безопасности Kaspersky Security Module при некорректности IPC-сообщений и обработке событий безопасности, не связанных ни с одним правилом моделей безопасности.

Чтобы создать профиль аудита безопасности, нужно использовать следующую декларацию:

audit profile <имя профиля аудита безопасности> = { <уровень аудита безопасности> : // Конфигурация аудита безопасности { <имя объекта модели безопасности> : { kss : <условия выполнения аудита безопасности, связанные с результатами вызовов методов модели безопасности> [, условия выполнения аудита безопасности, специфичные для модели безопасности] } [ ,...] } [ ,...] }

Уровень аудита безопасности

Уровень аудита безопасности (далее уровень аудита) является глобальным параметром политики безопасности решения и представляет собой беззнаковое целое число, которое задает активную конфигурацию аудита безопасности. (Слово "уровень" здесь означает вариант конфигурации и не предполагает обязательной иерархии.) Уровень аудита можно изменять в процессе работы модуля безопасности Kaspersky Security Module. Для этого нужно использовать специальный метод модели безопасности Base, вызываемый при обращении процессов к модулю безопасности через интерфейс безопасности (подробнее см. "Модель безопасности Base"). Начальный уровень аудита задается совместно c глобальным профилем аудита (подробнее см. "Установка глобальных параметров политики безопасности решения на базе KasperskyOS"). В качестве глобального можно явно назначить пустой профиль аудита empty.

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

Возможность изменять уровень аудита можно использовать, например, чтобы регулировать детализацию аудита. Чем выше уровень аудита, тем выше детализация. То есть при более высоком уровне аудита задействуются конфигурации аудита, при которых больше объектов моделей безопасности покрывается аудитом и/или меньше ограничений применяется в условиях выполнения аудита. Также, изменяя уровень аудита, можно переключать аудит с одного множества логически связанных объектов моделей безопасности на другое. То есть, например, при низком уровне аудита задействуются конфигурации аудита, при которых покрываются аудитом объекты моделей безопасности, связанные с драйверами; при среднем уровне аудита задействуются конфигурации аудита, при которых покрываются аудитом объекты моделей безопасности, связанные с сетевой подсистемой; при высоком уровне аудита задействуются конфигурации аудита, при которых покрываются аудитом объекты моделей безопасности, связанные с прикладными программами.

Имя объекта модели безопасности

Имя объекта модели безопасности указывается, чтобы методы, которые предоставляются этим объектом, могли быть покрыты аудитом. Эти методы будут покрыты аудитом при их вызовах, если условия выполнения аудита будут соблюдены.

Сведения о решениях модуля безопасности Kaspersky Security Module, содержащиеся в данных аудита, включают как общее решение модуля безопасности, так и результаты вызовов отдельных методов моделей безопасности, покрытых аудитом. Чтобы сведения о решении модуля безопасности попали в данные аудита, нужно, чтобы по крайней мере один метод, вызванный при обработке события безопасности, был покрыт аудитом.

Имена объектов моделей безопасности, как и имена методов, предоставляемых этими объектами, попадают в данные аудита.

Условия выполнения аудита безопасности

Условия выполнения аудита безопасности нужно задать отдельно для каждого объекта модели безопасности.

Чтобы задать условия выполнения аудита, связанные с результатами вызовов методов моделей безопасности, нужно использовать следующие конструкции:

  • ["granted"] – аудит выполняется, если правила возвращают результат "разрешено", выражения выполняются корректно.
  • ["denied"] – аудит выполняется, если правила возвращают результат "запрещено", выражения выполняются некорректно.
  • ["granted", "denied"] – аудит выполняется независимо от того, какой результат возвращают правила, и корректно ли выполняются правила.
  • [] – аудит не выполняется.

Условия выполнения аудита, специфичные для моделей безопасности, задаются конструкциями, специфичными для этих моделей (подробнее см. "Модели безопасности KasperskyOS"). Эти условия применяются как к правилам, так и к выражениям. Например, таким условием может быть состояние конечного автомата.

Профиль аудита безопасности для тракта аудита безопасности

Тракт аудита безопасности включает ядро, а также процессы Klog и KlogStorage, которые соединены IPC-каналами по схеме "ядро – Klog – KlogStorage". Методы моделей безопасности, которые связаны с передачей данных аудита через этот тракт, не должны покрываться аудитом. В противном случае это приведет к лавинообразному росту данных аудита, так как передача данных будет порождать новые данные.

Чтобы "подавить" аудит, заданный профилем более широкой области действия (например, глобальным или профилем на уровне привязки методов моделей безопасности к событиям безопасности), нужно назначить пустой профиль аудита empty на уровне привязки методов моделей безопасности к событиям безопасности или на уровне match-секции.

Примеры профилей аудита безопасности

См. "Примеры профилей аудита безопасности".

См. также

Использование системных программ Klog и KlogStorage для выполнения аудита безопасности

В начало
[Topic ssp_descr_psl_syntax_audit]

Создание и выполнение тестов политики безопасности решения на базе KasperskyOS

Тестирование политики безопасности решения выполняется, чтобы проверить, разрешает ли политика то, что должна разрешать, и запрещает ли она то, что должна запрещать.

Чтобы создать набор тестов политики безопасности решения, нужно использовать декларацию:

assert ["название набора тестов"] { // Конструкции на языке PAL (Policy Assertion Language) [setup {<начальная часть тестов>}] sequence ["название теста"] {<основная часть теста>} [...] [finally {<конечная часть тестов>}] }

Можно создать несколько наборов тестов, используя несколько таких деклараций.

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

После выполнения каждого теста все изменения в модуле безопасности Kaspersky Security Module, связанные с выполнением этого теста, "откатываются".

Каждый тест включает один или несколько тестовых примеров.

Тестовые примеры

Тестовый пример ассоциирует описание события безопасности и значения параметров интерфейсного метода с ожидаемым решением модуля безопасности Kaspersky Security Module. Если фактическое решение модуля безопасности совпадает с ожидаемым, тестовый пример проходит, иначе не проходит.

Когда выполняется тест, тестовые примеры выполняются в той последовательности, в которой они описаны. То есть осуществляется проверка, как модуль безопасности обрабатывает последовательность событий безопасности.

Если все тестовые примеры в тесте проходят, тест проходит. Если хотя бы один тестовый пример в тесте не проходит, тест не проходит. Выполнение теста завершается на первом тестовом примере, который не проходит. Каждый тест из набора выполняется независимо от того, прошел или не прошел предыдущий тест.

Описание тестового примера на языке PAL представляет собой следующую конструкцию:

[<ожидаемое решение модуля безопасности> ["название тестового примера"]] <вид события безопасности> <селекторы события безопасности> [{значения параметров интерфейсного метода}]

В качестве ожидаемого решения модуля безопасности можно указать значение grant ("разрешено"), deny ("запрещено") или any ("любое решение"). Можно не указывать ожидаемое решение модуля безопасности. По умолчанию ожидается решение "разрешено". Если указано значение any, решение модуля безопасности не влияет на то, проходит тестовый пример или нет. В этом случае тестовый пример может не пройти из-за ошибок обработки IPC-сообщения модулем безопасности (например, при некорректной структуре IPC-сообщения).

Название тестового примера можно указать, если только указано ожидаемое решения модуля безопасности.

О видах и селекторах событий безопасности, а также об ограничениях использования селекторов см. "Привязка методов моделей безопасности к событиям безопасности". Селекторы должны обеспечивать, чтобы описанию события безопасности соответствовали IPC-сообщения одного типа. (В привязках методов моделей безопасности к событиям безопасности селекторы могут этого не обеспечивать.)

В описаниях событий безопасности вместо имени класса процессов (и ядра KasperskyOS) нужно указывать SID. Исключение составляют события вида execute, при наступлении которых SID запускаемого процесса (или ядра) неизвестен. Чтобы сохранить SID процесса или ядра в переменную, нужно использовать оператор <- в описании тестового примера вида:

<имя переменной> <- execute dst=<имя класса процессов/ядро> ...

Переменной будет присвоено значение SID, даже если запуск процесса заданного класса (или ядра) запрещен тестируемой политикой, но решение "запрещено" является ожидаемым.

В языке PAL поддерживаются сокращенные формы описаний событий безопасности:

  • security: <SID процесса> ! <квалифицированное имя метода интерфейса безопасности> соответствует security src=<SID процесса> method=<квалифицированное имя метода интерфейса безопасности>.
  • request: <SID клиента> ~> <SID сервера/ядра> : <квалифицированное имя службы.имя метода> соответствует request src=<SID клиента> dst=<SID сервера/ядра> endpoint=<квалифицированное имя службы> method=<имя метода>.
  • response: <SID клиента> <~ <SID сервера/ядра> : <квалифицированное имя службы.имя метода> соответствует response src=<SID сервера/ядра> dst=<SID клиента> endpoint=<квалифицированное имя службы> method=<имя метода>.

Значения параметров интерфейсного метода должны быть заданы для всех видов событий безопасности, кроме execute. Если у интерфейсного метода нет параметров, нужно указать {}. Для событий безопасности вида execute нельзя указывать {}.

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

<имя параметра> : <значение>

Имена и типы параметров должны соответствовать IDL-описанию. Порядок следования параметров не важен.

Пример задания значений параметров:

{ param1 : 23, param2 : "bar", param3 : { collection : [5,7,12], filehandle : 15 }, param4 : { name : ["foo", "baz" } }

В этом примере через параметр param1 передается число. Через параметр param2 передается строковый буфер. Через параметр param3 передается структура, состоящая из двух полей. Поле collection содержит массив или последовательность из трех числовых элементов. Поле filehandle содержит SID. Через параметр param4 передается объединение или структура с одни полем. Поле name содержит массив или последовательность из двух строковых буферов.

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

Значения параметров (элементов параметров) можно не указывать. В этом случае автоматически применяются значения по умолчанию, соответствующие IDL-типам параметров (элементов параметров):

  • для числовых типов и типа Handle – ноль;
  • для байтовых или строковых буферов – байтовый или строковый буфер нулевого размера;
  • для последовательностей – последовательность с нулевым числом элементов;
  • для массивов – массив элементов со значениями по умолчанию;
  • для структур – структура, состоящая из полей со значениями по умолчанию;
  • для объединений – значение по умолчанию, соответствующее первому члену объединения.

Пример применения значения по умолчанию для параметра и элемента параметра:

/* Параметр указан. */ request src=x dst=y endpoint=e method=m { name : { firstname: "a", lastname: "b" } } /* Параметр не указан. В качестве значения параметра name будет применена структура, * состоящая из двух строковых буферов нулевого размера.*/ request src=x dst=y endpoint=e method=m {} /* Элемент параметра не указан. В качестве значения элемента параметра lastname будет * применен строковый буфер нулевого размера.*/ request src=x dst=y endpoint=e method=m { name : { firstname: "a"} }

Примеры тестов

См. "Примеры тестов политик безопасности решений на базе KasperskyOS".

Тестовая процедура

Тестовая процедура включает следующие шаги:

  1. Сохранить тесты в одном или нескольких PSL-файлах (*.psl или *.psl.in).
  2. Добавить CMake-команду add_kss_pal_qemu_tests() в один из файлов CMakeLists.txt проекта.

    Через параметр PSL_FILES нужно задать пути к PSL-файлам с тестами. Через параметр DEPENDS нужно задать CMake-цели, в результате выполнения которых IDL-, CDL-, EDL-файлы, от которых зависят PSL-файлы, будут помещены в те директории, где компилятор nk-psl-gen-c сможет их найти. Если используются файлы *.psl.in, через параметр ENTITIES нужно задать имена классов процессов системных программ. (Эти системные программы входят в состав решения на базе KasperskyOS, для которого нужно выполнить тестирование политики безопасности.)

    Пример использования CMake-команды add_kss_pal_qemu_tests() в файле einit/CMakeLists.txt:

    add_kss_pal_qemu_tests ( PSL_FILES src/security.psl.in DEPENDS kos-qemu-image ENTITIES ${ENTITIES})
  3. Собрать и выполнить тесты.

    Нужно запустить Bash-скрипт сборки cross-build.sh с параметром --target pal-test<N>, где N – индекс PSL-файла в списке PSL-файлов, заданных через параметр PSL_FILES CMake-команды add_kss_pal_qemu_tests() на шаге 2. Например, если указать --target pal-test0, будет создан и запущен на QEMU образ решения на базе KasperskyOS, который соответствует первому PSL-файлу, заданному через параметр PSL_FILES CMake-команды add_kss_pal_qemu_tests(). (Вместо прикладных и системных программ это решение будет содержать программу, выполняющую тесты.)

    Пример:

    ./cross-build.sh --target pal-test0

Пример результатов тестирования:

[==========] Running 4 tests from 1 test suite. [----------] Global test environment set-up. [----------] 4 tests from KSS [ RUN ] KSS.KssUnitTest_flow_normal [ OK ] KSS.KssUnitTest_flow_normal (6 ms) [ RUN ] KSS.KssUnitTest_flow_ping_must_be_first /home/work/build/stat/build/install/examples/ping/build/einit/ pal-test/gen_security.psl.test.c:9742: Failure Expected equality of these values: rc Which is: -1 NK_EOK Which is: 0 gen_security.psl:116: expect grant [ FAILED ] KSS.KssUnitTest_flow_ping_must_be_first (8 ms) [ RUN ] KSS.KssUnitTest_flow_ping_ping_is_deny [ OK ] KSS.KssUnitTest_flow_ping_ping_is_deny (4 ms) [ RUN ] KSS.KssUnitTest_flow_test_deny [ OK ] KSS.KssUnitTest_flow_test_deny (1 ms) [----------] 4 tests from KSS (29 ms total) [----------] Global test environment tear-down [==========] 4 tests from 1 test suite ran. (42 ms total) [ PASSED ] 3 tests. [ FAILED ] KSS.KssUnitTest_flow_ping_must_be_first (8 ms)

Результаты тестирования содержат сведения о том, прошел или не прошел каждый тест. Если тест не прошел, то указываются сведения о размещении описания непрошедшего тестового примера в PSL-файле.

В начало
[Topic ssp_descr_psl_syntax_testing]

Типы данных в языке PSL

Типы данных, поддерживаемые в языке PSL, приведены в таблице ниже.

Типы данных в языке PSL

Обозначения типов

Описание типов

UInt8, UInt16, UInt32, UInt64

Беззнаковое целое число

SInt8, SInt16, SInt32, SInt64

Знаковое целое число

Boolean

Логический тип

Логический тип включает два значения: true и false.

Text

Текстовый тип

()

Тип Unit

Тип Unit включает одно неизменяемое значение. Используется как заглушка в случаях, когда синтаксис языка PSL требует указать какие-либо данные, но фактически эти данные не требуются. Например, тип Unit можно использовать, чтобы объявить метод, который не имеет параметров (аналогично тому, как тип void используется в C/C++).

"[тип]"

Текстовый литерал

Текстовый литерал включает одно неизменяемое текстовое значение.

Примеры определений текстовых литералов:

""

"granted"

<тип>

Целочисленный литерал

Целочисленный литерал включает одно неизменяемое целочисленное значение.

Примеры определений числовых литералов:

12

-5

0xFFFF

<тип 1 | тип 2> [| ...]

Вариантный тип

Вариантный тип объединяет два и более типов и может выступать в роли любого из них.

Примеры определений вариантных типов:

Boolean | ()

UInt8 | UInt16 | UInt32 | UInt64

"granted" | "denied"

{ [имя поля : тип поля]

[, ...]

}

Словарь

Словарь состоит из полей одного или нескольких типов. Словарь может быть пустым.

Примеры определений словарей:

{}

{ handle : Handle

, rights : UInt32

}

[[тип] [, ...]]

Кортеж

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

Примеры определений кортежей:

[]

["granted"]

[Boolean, Boolean]

Set<<тип элементов>>

Множество

Множество включает ноль и более уникальных элементов одного типа.

Примеры определений множеств:

Set<"granted" | "denied">

Set<Text>

List<<тип элементов>>

Список

Список включает ноль и более элементов одного типа.

Примеры определений списков:

List<Boolean>

List<Text | ()>

Map<<тип ключа, тип значения>>

Ассоциативный массив

Ассоциативный массив включает ноль и более записей типа "ключ-значение" с уникальными ключами.

Пример определения ассоциативного массива:

Map<UInt32, UInt32>

Array<<тип элементов, число элементов>>

Массив

Массив включает заданное число элементов одного типа.

Пример определения массива:

Array<UInt8, 42>

Sequence<<тип элементов, число элементов>>

Последовательность

Последовательность включает от ноля до заданного числа элементов одного типа.

Пример определения последовательности:

Sequence<SInt64, 58>

Псевдонимы некоторых типов PSL

В файле nk/base.psl из состава KasperskyOS SDK определены типы данных, которые используются как типы параметров (или структурных элементов параметров) и возвращаемых значений для методов разных моделей безопасности. Псевдонимы и определения этих типов приведены в таблице ниже.

Псевдонимы и определения некоторых типов данных в языке PSL

Псевдоним типа

Определение типа

Unsigned

Беззнаковое целое число

UInt8 | UInt16 | UInt32 | UInt64

Signed

Знаковое целое число

SInt8 | SInt16 | SInt32 | SInt64

Number

Целое число

Unsigned | Signed

ScalarLiteral

Скалярный литерал

() | Boolean | Number

Literal

Литерал

ScalarLiteral | Text

Sid

Тип идентификатора безопасности SID

UInt32

Handle

Тип идентификатора безопасности SID

Sid

HandleDesc

Словарь, содержащий поля для SID и маски прав дескриптора

{ handle : Handle

, rights : UInt32

}

Cases

Тип данных, принимаемых выражениями моделей безопасности, вызываемыми в конструкции choice для проверки выполнения условий

List<Text | ()>

KSSAudit

Тип данных, задающих условия выполнения аудита безопасности

Set<"granted" | "denied">

Отображение типов IDL на типы PSL

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

Целочисленные типы IDL отображаются на целочисленные типы PSL, а также на вариантные типы PSL, объединяющие эти целочисленные типы (в том числе с другими типами). Например, знаковые целочисленные типы IDL отображаются на тип Signed в PSL, целочисленные типы IDL отображаются на тип ScalarLiteral в PSL.

Тип Handle в IDL отображается на тип HandleDesc в PSL.

Объединения и структуры IDL отображаются на словари PSL.

Массивы и последовательности IDL отображаются на массивы и последовательности PSL соответственно.

Строковые буферы в IDL отображаются на текстовый тип PSL.

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

В начало
[Topic ssp_descr_psl_syntax_data_types]

Примеры привязок методов моделей безопасности к событиям безопасности

Перед тем как рассматривать примеры, нужно ознакомиться со сведениями о модели безопасности Base.

Обработка инициации запусков процессов

/* Ядру KasperskyOS и любому процессу * в решении разрешено запускать любой * процесс. */ execute { grant () } /* Ядру разрешено запускать процесс * класса Einit. */ execute src=kl.core.Core, dst=Einit { grant () } /* Процессу класса Einit разрешено * запускать любой процесс в решении. */ execute src=Einit { grant () }

Обработка запуска ядра KasperskyOS

/* Ядру KasperskyOS разрешено запускаться. * (Эта привязка нужна, чтобы сообщить модулю * безопасности SID ядра. Ядро запускается независимо * от того, разрешено ли это политикой безопасности решения * или нет. Если политика безопасности решения запрещает * запуск ядра, после запуска ядро прекратит свое * исполнение.) */ execute src=kl.core.Core, dst=kl.core.Core { grant () }

Обработка отправки IPC-запросов

/* Любому клиенту в решении разрешено обращаться к * любому серверу и ядру KasperskyOS. */ request { grant () } /* Клиенту класса Client разрешено обращаться * к любому серверу в решении и ядру. */ request src=Client { grant () } /* Любому клиенту в решении разрешено обращаться * к серверу класса Server. */ request dst=Server { grant () } /* Клиенту класса Client запрещено * обращаться к серверу класса Server. */ request src=Client dst=Server { deny () } /* Клиенту класса Client разрешено * обращаться к серверу класса Server, * вызывая метод Ping службы net.Net. */ request src=Client dst=Server endpoint=net.Net method=Ping { grant () } /* Любому клиенту в решении разрешено обращаться * к серверу класса Server, вызывая метод Send * службы с интерфейсом MessExch. */ request dst=Server interface=MessExch method=Send { grant () }

Обработка отправки IPC-ответов

/* Серверу класса Server разрешено отвечать на * обращения клиента класса Client, который * вызывает метод Ping службы net.Net. */ response src=Server, dst=Client, endpoint=net.Net, method=Ping { grant () } /* Серверу, который содержит компонент kl.drivers.KIDF, * предоставляющий службы с интерфейсом monitor, разрешено * отвечать на обращения клиента класса DriverManager, * который использует эти службы. */ response dst=DriverManager component=kl.drivers.KIDF interface=monitor { grant () }

Обработка отправки IPC-ответов, содержащих сведения об ошибках

/* Серверу класса Server запрещено сообщать клиенту * класса Client об ошибках, которые возникают, * когда клиент обращается к серверу, вызывая метод * Ping службы net.Net. */ error src=Server, dst=Client, endpoint=net.Net, method=Ping { deny () }

Обработка обращений процессов к модулю безопасности Kaspersky Security Module

/* Процесс класса Sdcard получит решение * "разрешено" от модуля безопасности Kaspersky Security Module, * вызывая метод Register интерфейса безопасности. * (Используется интерфейс безопасности, заданный * в EDL-описании.) */ security src=Sdcard, method=Register { grant () } /* Процесс класса Sdcard получит решение "запрещено" * от модуля безопасности, вызывая метод Comp.Register * интерфейса безопасности. (Используется интерфейс * безопасности, заданный в CDL-описании.) */ security src=Sdcard, method=Comp.Register { deny () }

Использование match-секций

/* Клиенту класса Client разрешено обращаться к * серверу класса Server, вызывая методы Send * и Receive службы net. */ request src=Client, dst=Server, endpoint=net { match method=Send { grant () } match method=Receive { grant () } } /* Клиенту класса Client разрешено обращаться к * серверу класса Server, вызывая методы Send * и Receive службы sn.Net и методы Write и * Read службы sn.Storage. */ request src=Client, dst=Server { match endpoint=sn.Net { match method=Send { grant () } match method=Receive { grant () } } match endpoint=sn.Storage { match method=Write { grant () } match method=Read { grant () } } }

Установка профилей аудита

/* Установка глобального профиля аудита default * и начального уровня аудита 0 */ audit default = global 0 request src=Client, dst=Server { /* Установка профиля аудита parent на уровне * привязки методов моделей безопасности к * событиям безопасности */ audit parent match endpoint=net.Net, method=Send { /* Установка профиля аудита child на * на уровне match-секции */ audit child grant () } /* В этой match-секции применяется профиль * аудита parent. */ match endpoint=net.Net, method=Receive { grant () } } /* В этой привязке метода модели безопасности * к событию безопасности применяется профиль * аудита global. */ response src=Client, dst=Server { grant () }
В начало
[Topic ssp_descr_psl_syntax_binding_examples]

Примеры описаний простейших политик безопасности решений на базе KasperskyOS

Перед тем как рассматривать примеры, нужно ознакомиться со сведениями о моделях безопасности Struct, Base и Flow.

Пример 1

Политика безопасности решения в этом примере разрешает любые взаимодействия процессов классов Client, Server и Einit между собой и с ядром KasperskyOS. При обращении процессов к модулю безопасности Kaspersky Security Module всегда будет получено решение "разрешено". Эту политику можно использовать только в качестве заглушки на ранних стадиях разработки решения на базе KasperskyOS, чтобы модуль безопасности Kaspersky Security Module "не мешал" взаимодействиям. В реальном решении на базе KasperskyOS применять такую политику недопустимо.

security.psl

execute: kl.core.Execute use nk.base._ use EDL Einit use EDL Client use EDL Server use EDL kl.core.Core execute { grant () } request { grant () } response { grant () } error { grant () } security { grant () }

Пример 2

Политика безопасности решения в этом примере накладывает ограничения на обращения клиентов класса FsClient к серверам класса FsDriver. Когда клиент открывает ресурс, управляемый сервером класса FsDriver, с этим ресурсом ассоциируется конечный автомат в состоянии unverified. Клиенту класса FsClient разрешено читать данные из ресурса, управляемого сервером класса FsDriver, только если конечный автомат, ассоциированный с этим ресурсом, находится в состоянии verified. Чтобы перевести конечный автомат, ассоциированный с ресурсом, из состояния unverified в состояние verified, процессу класса FsVerifier нужно обратиться к модулю безопасности Kaspersky Security Module.

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

security.psl

execute: kl.core.Execute use nk.base._ use nk.flow._ use nk.basic._ policy object file_state : Flow { type States = "unverified" | "verified" config = { states : ["unverified" , "verified"], initial : "unverified", transitions : { "unverified" : ["verified"], "verified" : [] } } } execute { grant () } request { grant () } response { grant () } use EDL kl.core.Core use EDL Einit use EDL FsClient use EDL FsDriver use EDL FsVerifier response src=FsDriver, endpoint=operationsComp.operationsImpl, method=Open { file_state.init {sid: message.handle.handle} } request src=FsClient, dst=FsDriver, endpoint=operationsComp.operationsImpl, method=Read { file_state.allow {sid: message.handle.handle, states: ["verified"]} } security src=FsVerifier, method=Approve { file_state.enter {sid: message.handle.handle, state: "verified"} }
В начало
[Topic ssp_descr_psl_syntax_simpssp_examples]

Примеры профилей аудита безопасности

Перед тем как рассматривать примеры, нужно ознакомиться со сведениями о моделях безопасности Base, Regex и Flow.

Пример 1

// Описание профиля аудита безопасности trace // base – объект модели безопасности Base // session – объект модели безопасности Flow audit profile trace = /* Если уровень аудита равен 0, аудитом покрываются * правила объекта base, когда эти правила возвращают * результат "запрещено". */ { 0 : { base : { kss : ["denied"] } } /* Если уровень аудита равен 1, аудитом покрываются методы * объекта session в следующих случаях: * 1. Правила объекта session возвращают любой результат, и * конечный автомат находится в состоянии, отличном от closed. * 2. Выражение query объекта session выполняется, и конечный * автомат находится в состоянии, отличном от closed. */ , 1 : { session : { kss : ["granted", "denied"] , omit : ["closed"] } } /* Если уровень аудита равен 2, аудитом покрываются методы * объекта session в следующих случаях: * 1. Правила объекта session возвращают любой результат. * 2. Выражение query объекта session выполняется. */ , 2 : { session : { kss : ["granted", "denied"] } } }

Пример 2

// Описание профиля аудита безопасности test // base – объект модели безопасности Base // re – объект модели безопасности Regex audit profile test = /* Если уровень аудита равен 0, правила объекта base * и выражения объекта re не покрываются аудитом. */ { 0 : { base : { kss : [] } , re : { kss : [] , emit : [] } } /* Если уровень аудита равен 1, правила объекта * base не покрываются аудитом, выражения объекта * re покрываются аудитом.*/ , 1 : { base : { kss : [] } , re : { kss : ["granted"] , emit : ["match", "select"] } } /* Если уровень аудита равен 2, правила объекта base * и выражения объекта re покрываются аудитом. Правила * объекта base покрываются аудитом независимо от * результата, который они возвращают.*/ , 2 : { base : { kss : ["granted", "denied"] } , re : { kss : ["granted"] , emit : ["match", "select"] } } }
В начало
[Topic ssp_descr_psl_syntax_audit_profile_examples]

Примеры тестов политик безопасности решений на базе KasperskyOS

Пример 1

/* Набор тестов, который включает один тест. */ assert "some tests" { /* Тест, который включает четыре тестовых примера. */ sequence "first sequence" { /* Ожидается, что запуск процесса класса Server разрешен. * Если это так, переменной s будет присвоено значение SID * запущенного процесса класса Server. */ s <- execute dst=Server /* Ожидается, что запуск процесса класса Client разрешен. * Если это так, переменной c будет присвоено значение SID * запущенного процесса класса Client. */ c <- execute dst=Client /* Ожидается, что клиенту класса Client разрешено обращаться к * серверу класса Server, вызывая метод Ping службы pingComp.pingImpl * с параметром value, равным 100. */ grant "Client calls Ping" request src=c dst=s endpoint=pingComp.pingImpl method=Ping { value : 100 } /* Ожидается, что серверу класса Server запрещено отвечать клиенту * класса Client, если клиент вызывает метод Ping службы pingComp.pingImpl. * (IPC-ответ не содержит параметров, так как интерфейсный метод Ping * не имеет выходных параметров.) */ deny "Server can not respond" response src=s dst=c endpoint=pingComp.pingImpl method=Ping {} } }

Пример 2

/* Набор тестов, который включает два теста. */ assert "ping tests"{ /* Начальная часть каждого из двух тестов, * которая включает два тестовых примера. */ setup { /* Ожидается, что запуск процесса класса Server разрешен. * Если это так, переменной s будет присвоено значение SID * запущенного процесса класса Server. */ s <- execute dst=Server /* Ожидается, что запуск процесса класса Client разрешен. * Если это так, переменной c будет присвоено значение SID * запущенного процесса класса Client. */ c <- execute dst=Client } /* Тест, который включает четыре тестовых примера: два тестовых примера * в начальной части и два тестовых примера в основной части.*/ sequence "ping-ping is denied" { /* Ожидается, что клиенту класса Client разрешено обращаться к * серверу класса Server, вызывая метод Ping службы pingComp.pingImpl * с параметром value, равным 100. */ c ~> s : pingComp.pingImpl.Ping { value : 100 } /* Ожидается, что клиенту класса Client запрещено обращаться к * серверу класса Server, повторно вызывая метод Ping службы pingComp.pingImpl * с параметром value, равным 100. */ deny c ~> s : pingComp.pingImpl.Ping { value : 100 } } /* Тест, который включает четыре тестовых примера: два тестовых примера * в начальной части и два тестовых примера в основной части. */ sequence "ping-pong is granted" { /* Ожидается, что клиенту класса Client разрешено обращаться к * серверу класса Server, вызывая метод Ping службы pingComp.pingImpl * с параметром value, равным 100. */ c ~> s : pingComp.pingImpl.Ping { value: 100 } /* Ожидается, что клиенту класса Client разрешено обращаться к * серверу класса Server, вызывая метод Pong службы pingComp.pingImpl * с параметром value, равным 100. */ c ~> s : pingComp.pingImpl.Pong { value: 100 } } }

Пример 3

/* Набор тестов, который включает один тест. */ assert { /* Тест, который включает восемь тестовых примеров. */ sequence { storage <− execute dst=test.kl.UpdateStorage manager <− execute dst=test.kl.UpdateManager deployer <− execute dst=test.kl.UpdateDeployer downloader <− execute dst=test.kl.UpdateDownloader grant manager ~> downloader:UpdateDownloader.Downloader.LoadPackage { url : ”url012345678” } grant response src=downloader dst=manager endpoint=UpdateDownloader.Downloader method=LoadPackage { handle : 29, result : 1 } deny manager ~> deployer:UpdateDeployer.Deployer.Start { handle : 29 } deny request src=manager dst=deployer endpoint=UpdateDeployer.Deployer method=Start { handle : 29 } } }
В начало
[Topic ssp_descr_psl_syntax_testing_examples]