Содержание

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

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

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

Декларации могут располагаться в файле в любом порядке.
Одна декларация может быть записана в одну или несколько строк. Вторая и последующие строки декларации должны быть записаны с отступами относительно первой строки. Закрывающая фигурная скобка, которая завершает декларацию, может быть записана на уровне первой строки.
В многострочной декларации используются отступы разных размеров, чтобы отразить вложенность конструкций, составляющих эту декларацию. Вторая и последующие строки многострочной конструкции, заключенные в фигурные скобки, должны быть записаны с отступом относительно первой строки этой конструкции. Закрывающая фигурная скобка многострочной конструкции может быть записана с отступом или на уровне первой строки конструкции.
Язык PSL чувствителен к регистру символов.
Поддерживаются однострочные и многострочные комментарии:
/* Это комментарий

* И это тоже */

// Ещё один комментарий

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

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

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

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

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

Включение PSL-файлов

Включение EDL-файлов

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

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

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

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

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

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

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

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

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

В начало

Описание глобальных параметров политики безопасности решения на базе 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.

В начало

Включение PSL-файлов

Для включения 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. */

В начало

Включение EDL-файлов

Чтобы включить 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-файлы, а CDL-файлы содержат ссылки на соответствующие CDL-, IDL-файлы.

В начало

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

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

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

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

[параметры объекта модели безопасности]

}

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

В начало

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

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

<вид события безопасности> [селекторы события безопасности] {

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

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

}

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

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

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 <имя профиля аудита безопасности>. Если профиль аудита безопасности не задан, используется глобальный профиль аудита безопасности.

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

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

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

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

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

Также в качестве входных данных для методов моделей безопасности (правил и выражений) могут использоваться параметры интерфейсных методов. (О получении доступа к параметрам интерфейсных методов см. "Модель безопасности 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".

В начало

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

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

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

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

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

{ <уровень аудита безопасности> :

// Описание конфигурации аудита безопасности

{ <имя объекта модели безопасности> :

{ kss : <условия выполнения аудита безопасности, связанные с результатами

вызовов правил модели безопасности>

[, условия выполнения аудита безопасности, специфичные для модели безопасности]

}

[,]...

...

}

[,]...

...

}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

В начало

Описание и выполнение тестов политики безопасности решения на базе 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=<имя метода>.

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

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

Имена и типы параметров должны соответствовать 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 совместно с маской прав дескриптора нет. Поэтому нельзя тестировать политику безопасности решения в тех случаях, когда маски прав дескрипторов влияют на решения модуля безопасности.

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

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

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

Описания тестов помещаются в PSL-файлы, включая те, которые содержат описание политики безопасности решения (например, в файл security.psl).

Чтобы выполнить тесты, нужно использовать параметр --tests run при запуске компилятора nk-psl-gen-c:

$ nk-psl-gen-c --tests run <остальные параметры> security.psl

Также компилятору nk-psl-gen-c нужно указать следующие сведения:

Директории, которые содержат вспомогательные файлы из состава KasperskyOS SDK (common, sysroot-*-kos/include, toolchain/include). Этот набор директорий задается параметрами -I, -include-dir <путь к файлам>.
Директории, которые содержат PSL-, IDL-, CDL-, EDL-файлы, относящиеся к решению. Этот набор директорий задается параметрами -I, --include-dir <путь к файлам>.
Путь к файлу, в который будет сохранен исходный код модуля безопасности Kaspersky Security Module и тестов. Этот путь задается параметром -o, --output <путь к файлу>.

Компилятор nk-psl-gen-c генерирует исходный код модуля безопасности и тестов на языке C, сохраняет его в файл, а затем запускает компиляцию этого кода с использованием gcc и выполнение полученной тестовой программы. Тестовая программа запускается в среде, где установлен KasperskyOS SDK, то есть на компьютере под управлением ОС Linux. Ядро KasperskyOS, а также системное и прикладное ПО решения не используются.

Чтобы сгенерировать исходный код модуля безопасности и тестов, но не компилировать его, нужно использовать параметр --tests generate при запуске компилятора nk-psl-gen-c.

По умолчанию результаты тестирования выводятся в консоль. Чтобы вывести результаты тестирования в файл, нужно использовать параметр --test-output <путь к файлу> при запуске компилятора nk-psl-gen-c.

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

# PAL test run

## Execute (1/2)

* Happy path: FAIL

Step 2/2: ExpectGrant Execute "This should not fail"

component/secure_platform/kss/nk/psl/nk-psl-gen-c/tests/examples/include/router.psl:38:5-40:3

* No rule: PASS

## IPC (2/2)

* Happy path: PASS

* No rule: PASS

## Security (2/2)

* Happy path: PASS

* No rule: PASS

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

В начало

Типы данных в языке 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. Соответственно, данные, содержащиеся в байтовых буферах, не могут использоваться как входы для методов моделей безопасности.

В начало

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

Перед тем как рассматривать примеры, нужно ознакомиться со сведениями о модели безопасности 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 ()

}

В начало

Примеры описаний простейших политик безопасности решений на базе 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"}

}

В начало

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

Перед тем как рассматривать примеры, нужно ознакомиться со сведениями о моделях безопасности 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 : []

, emit : ["match", "select"]

}

/* Если уровень аудита равен 2, правила объекта base

* и выражения объекта re покрываются аудитом. Правила

* объекта base покрываются аудитом независимо от

* результата, который они возвращают.*/

, 2 :

{ base :

{ kss : ["granted", "denied"]

}

, re :

{ kss : []

, emit : ["match", "select"]

}

В начало

Примеры описаний тестов политик безопасности решений на базе 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 cannot respond" response src=s dst=c endpoint=pingComp.pingImpl

method=Ping {}

}

Пример 2

/* Описание набора тестов, который включает два теста. */

assert "ping tests"{

/* Начальная часть каждого из двух тестов */

setup {

s <- execute dst=Server

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 }

}

В начало