KasperskyOS Community Edition 1.1

Содержание

[Topic ssp_descr_security_models_intro]

Модель безопасности Pred

Модель безопасности Pred позволяет выполнять операции сравнения.

PSL-файл с описанием модели безопасности Pred находится в KasperskyOS SDK по пути:

toolchain/include/nk/basic.psl

Объект модели безопасности Pred

В файле basic.psl содержится декларация, которая создает объект модели безопасности Pred с именем pred. Соответственно, включение файла basic.psl в описание политики безопасности решения обеспечивает создание объекта модели безопасности Pred по умолчанию.

Объект модели безопасности Pred не имеет параметров и не может быть покрыт аудитом безопасности.

Создавать дополнительные объекты модели безопасности Pred не требуется.

Методы модели безопасности Pred

Модель безопасности Pred содержит выражения, которые выполняют операции сравнения и возвращают значения типа Boolean. Для вызова этих выражений нужно использовать операторы сравнения:

  • <ScalarLiteral> == <ScalarLiteral> – "равно";
  • <ScalarLiteral> != <ScalarLiteral> – "не равно";
  • <Number> < <Number> – "меньше";
  • <Number> <= <Number> – "меньше или равно";
  • <Number> > <Number> – "больше";
  • <Number> >= <Number> – "больше или равно".

Также модель безопасности Pred содержит выражение empty, которое позволяет определить, содержат ли данные свои структурные элементы. Выражение возвращает значения типа Boolean. Если данные не содержат своих структурных элементов (например, множество является пустым), выражение возвращает true, иначе возвращает false. Чтобы вызвать выражение, нужно использовать конструкцию:

pred.empty <Text | Set | List | Map | ()>

В начало
[Topic ssp_descr_security_models_pred]

Модель безопасности Bool

Модель безопасности Bool позволяет выполнять логические операции.

PSL-файл с описанием модели безопасности Bool находится в KasperskyOS SDK по пути:

toolchain/include/nk/basic.psl

Объект модели безопасности Bool

В файле basic.psl содержится декларация, которая создает объект модели безопасности Bool с именем bool. Соответственно, включение файла basic.psl в описание политики безопасности решения обеспечивает создание объекта модели безопасности Bool по умолчанию.

Объект модели безопасности Bool не имеет параметров и не может быть покрыт аудитом безопасности.

Создавать дополнительные объекты модели безопасности Bool не требуется.

Методы модели безопасности Bool

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

  • ! <Boolean> – "логическое НЕ";
  • <Boolean> && <Boolean> – "логическое И";
  • <Boolean> || <Boolean> – "логическое ИЛИ";
  • <Boolean> ==> <Boolean> – "импликация" (! <Boolean> || <Boolean>).

Также модель безопасности Bool содержит выражения all, any и cond.

Выражение all выполняет "логическое И" для произвольного числа значений типа Boolean. Возвращает значения типа Boolean. Если передать через параметр пустой список значений ([]), возвращает true. Чтобы вызвать выражение, нужно использовать конструкцию:

bool.all <List<Boolean>>

Выражение any выполняет "логическое ИЛИ" для произвольного числа значений типа Boolean. Возвращает значения типа Boolean. Если передать через параметр пустой список значений ([]), возвращает false. Чтобы вызвать выражение, нужно использовать конструкцию:

bool.any <List<Boolean>>

Выражение cond выполняет тернарную условную операцию. Возвращает значения типа ScalarLiteral. Чтобы вызвать выражение, нужно использовать конструкцию:

bool.cond

{ if : <Boolean> // Условие

, then : <ScalarLiteral> // Значение, возвращаемое при истинности условия

, else : <ScalarLiteral> // Значение, возвращаемое при ложности условия

}

Помимо выражений модель безопасности Bool включает правило assert, которое работает так же, как одноименное правило модели безопасности Base.

В начало
[Topic ssp_descr_security_models_bool]

Модель безопасности Math

Модель безопасности Math позволяет выполнять операции целочисленной арифметики.

PSL-файл с описанием модели безопасности Math находится в KasperskyOS SDK по пути:

toolchain/include/nk/basic.psl

Объект модели безопасности Math

В файле basic.psl содержится декларация, которая создает объект модели безопасности Math с именем math. Соответственно, включение файла basic.psl в описание политики безопасности решения обеспечивает создание объекта модели безопасности Math по умолчанию.

Объект модели безопасности Math не имеет параметров и не может быть покрыт аудитом безопасности.

Создавать дополнительные объекты модели безопасности Math не требуется.

Методы модели безопасности Math

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

  • <Number> + <Number> – "сложение". Возвращает значения типа Number.
  • <Number> - <Number> – "вычитание". Возвращает значения типа Number.
  • <Number> * <Number> – "умножение". Возвращает значения типа Number.

Другая часть включает следующие выражения:

  • neg <Signed> – "изменение знака числа". Возвращает значения типа Signed.
  • abs <Signed> – "получение модуля числа". Возвращает значения типа Signed.
  • sum <List<Number>> – "сложение чисел из списка". Возвращает значения типа Number. Если передать через параметр пустой список значений ([]), возвращает 0.
  • product <List<Number>> – "перемножение чисел из списка". Возвращает значения типа Number. Если передать через параметр пустой список значений ([]), возвращает 1.

Для вызова этих выражений нужно использовать конструкцию:

math.<имя выражения> <параметр>

В начало
[Topic ssp_descr_security_models_math]

Модель безопасности Struct

Модель безопасности Struct позволяет получать доступ к структурным элементам данных.

PSL-файл с описанием модели безопасности Struct находится в KasperskyOS SDK по пути:

toolchain/include/nk/basic.psl

Объект модели безопасности Struct

В файле basic.psl содержится декларация, которая создает объект модели безопасности Struct с именем struct. Соответственно, включение файла basic.psl в описание политики безопасности решения обеспечивает создание объекта модели безопасности Struct по умолчанию.

Объект модели безопасности Struct не имеет параметров и не может быть покрыт аудитом безопасности.

Создавать дополнительные объекты модели безопасности Struct не требуется.

Методы модели безопасности Struct

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

  • <{...}>.<имя поля> – "получение доступа к полю словаря". Тип возвращаемых данных соответствует типу поля словаря.
  • <List | Set | Sequence | Array>.[<номер элемента>] – "получение доступа к элементу данных". Тип возвращаемых данных соответствует типу элементов. Нумерация элементов начинается с нуля. При выходе за границы набора данных выражение завершается некорректно, и модуль безопасности Kaspersky Security Module возвращает решение "запрещено".
  • <HandleDesc>.handle – "получение SID". Возвращает значения типа Handle. (О взаимосвязи между дескрипторами и значениями SID см. "Управление доступом к ресурсам").
  • <HandleDesc>.rights – "получение маски прав дескриптора". Возвращает значения типа UInt32.

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

message.<имя параметра интерфейсного метода>

Имя параметра нужно указать в соответствии с IDL-описанием.

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

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

В начало
[Topic ssp_descr_security_models_struct]

Модель безопасности Base

Модель безопасности Base позволяет реализовать простейшую логику.

PSL-файл с описанием модели безопасности Base находится в KasperskyOS SDK по пути:

toolchain/include/nk/base.psl

Объект модели безопасности Base

В файле base.psl содержится декларация, которая создает объект модели безопасности Base с именем base. Соответственно, включение файла base.psl в описание политики безопасности решения обеспечивает создание объекта модели безопасности Base по умолчанию. Методы этого объекта можно вызывать без указания имени объекта.

Объект модели безопасности Base не имеет параметров.

Объект модели безопасности Base может быть покрыт аудитом безопасности. Условия выполнения аудита, специфичные для модели безопасности Base, отсутствуют.

Необходимость создавать дополнительные объекты модели безопасности Base возникает в следующих случаях:

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

Методы модели безопасности Base

Модель безопасности Base содержит следующие правила:

  • grant ()

    Имеет параметр типа (). Возвращает результат "разрешено".

    Пример:

    /* Клиенту класса foo разрешено

    * обращаться к серверу класса bar. */

    request src=foo dst=bar { grant () }

  • assert <Boolean>

    Возвращает результат "разрешено", если через параметр передать значение true. Иначе возвращает результат "запрещено".

    Пример:

    /* Любому клиенту в решении будет разрешено обращаться к серверу класса

    * foo, вызывая метод Send службы net.Net, если через параметр port

    * метода Send будет передаваться значение больше 80. Иначе любому

    * клиенту в решении будет запрещено обращаться к серверу класса

    * foo, вызывая метод Send службы net.Net. */

    request dst=foo endpoint=net.Net method=Send { assert (message.port > 80) }

  • deny <Boolean | ()>

    Возвращает результат "запрещено", если через параметр передать значение true или (). Иначе возвращает результат "разрешено".

    Пример:

    /* Серверу класса foo запрещено

    * отвечать клиенту класса bar. */

    response src=foo dst=bar { deny () }

  • set_level <UInt8>

    Устанавливает уровень аудита безопасности равным значению, переданному через параметр. Возвращает результат "разрешено". (Подробнее об уровне аудита безопасности см. "Описание профилей аудита безопасности".)

    Пример:

    /* Процесс класса foo получит решение "разрешено" от модуля

    * безопасности Kaspersky Security Module, если вызовет метод интерфейса безопасности

    * SetAuditLevel, чтобы изменить уровень аудита безопасности. */

    security src=foo method=SetAuditLevel { set_level (message.audit_level) }

В начало
[Topic ssp_descr_security_models_base]

Модель безопасности Regex

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

PSL-файл с описанием модели безопасности Regex находится в KasperskyOS SDK по пути:

toolchain/include/nk/regex.psl

Объект модели безопасности Regex

В файле regex.psl содержится декларация, которая создает объект модели безопасности Regex с именем re. Соответственно, включение файла regex.psl в описание политики безопасности решения обеспечивает создание объекта модели безопасности Regex по умолчанию.

Объект модели безопасности Regex не имеет параметров.

Объект модели безопасности Regex может быть покрыт аудитом безопасности. При этом нужно задать условия выполнения аудита, специфичные для модели безопасности Regex. Для этого в описании конфигурации аудита нужно использовать следующие конструкции:

  • emit : ["match"] – аудит выполняется, если вызван метод match;
  • emit : ["select"] – аудит выполняется, если вызван метод select;
  • emit : ["match", "select"] – аудит выполняется, если вызван метод match или select;
  • emit : [] – аудит не выполняется.

Необходимость создавать дополнительные объекты модели безопасности Regex возникает в следующих случаях:

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

Методы модели безопасности Regex

Модель безопасности Regex содержит следующие выражения:

  • match {text : <Text>, pattern : <Text>}

    Возвращает значение типа Boolen. Если текст text соответствует регулярному выражению pattern, возвращает true. Иначе возвращает false.

    Пример:

    assert (re.match {text : message.text, pattern : "[0-9]*"})

  • select {text : <Text>}

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

    Пример:

    choice (re.select {text : "hello world"}) {

    "hello\ .*": grant ()

    ".*world" : grant ()

    _ : deny ()

    }

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

Регулярное выражение для метода match модели безопасности Regex можно записать двумя способами: внутри многострочного блока regex или как текстовый литерал.

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

Например, два регулярных выражения идентичны:

// Регулярное выражение внутри многострочного блока regex

{ pattern:

```regex

Hello\ world\!

```

, text: "Hello world!"

}

// Регулярное выражение как текстовый литерал (обратный слеш удвоен)

{ pattern: "Hello\\ world\\!"

, text: "Hello world!"

}

Регулярные выражения для метода select модели безопасности Regex записываются как текстовые литералы с удвоением обратного слеша.

Регулярное выражение задается в виде строки-шаблона и может содержать:

  • литералы (обычные символы);
  • метасимволы (символы со специальными значениями);
  • пробельные символы;
  • наборы символов;
  • группы символов;
  • операторы для работы с символами.

Регулярные выражения чувствительны к регистру.

Литералы и метасимволы в регулярных выражениях

  • Литералом является любой ASCII-символ, за исключением метасимволов .()*&|!?+[]\ и знака пробела. (Символы Unicode не поддерживаются.)

    Например, регулярному выражению KasperskyOS соответствует текст KasperskyOS.

  • Метасимволы имеют специальные значения, которые приведены в таблице ниже.

    Специальные значения метасимволов

    Метасимвол

    Специальное значение

    []

    Квадратные скобки обозначают начало и конец набора символов.

    ()

    Круглые скобки обозначают начало и конец группы символов.

    *

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

    +

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

    ?

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

    !

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

    |

    Вертикальная черта обозначает оператор выбора между символами (близок по смыслу к союзу "ИЛИ").

    &

    Амперсанд обозначает оператор пересечения нескольких условий (близок по смыслу к союзу "И").

    .

    Точка обозначает соответствие любому символу.

    Например, регулярному выражению K.S соответствуют последовательности символов: KОS, KoS, KES и множество других последовательностей из трех символов, которые начинаются на K и заканчиваются на S, и где второй символ может быть любым: литералом, метасимволом или самой точкой.

    \

    \<metaSymbol>

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

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

    Аналогично обратный слеш действует и на самого себя. Регулярному выражению С:\\Users соответствует последовательность символов C:\Users.

  • Символы ^ и $ как обозначения начала и конца строки не используются.

Пробельные символы в регулярных выражениях

  • Знак пробела имеет ASCII-код, равный 20, в шестнадцатеричной системе счисления и ASCII-код, равный 40, в восьмеричной системе счисления. Знак пробела не имеет специального значения, но во избежание неоднозначной трактовки данного символа интерпретатором регулярных выражений, пробел необходимо экранировать.

    Например, регулярному выражению Hello\ world соответствует последовательность символов Hello world.

  • \r

    Символ возврата каретки.

  • \n

    Символ переноса строки.

  • \t

    Символ горизонтальной табуляции.

Определение символа по его восьмеричному или шестнадцатеричному коду в регулярных выражениях

  • \x{<hex>}

    Определение символа его шестнадцатеричным кодом hex из таблицы ASCII-символов. Код символа должен быть меньше, чем 0x100.

    Например, регулярному выражению Hello\x{20}world соответствует последовательность символов Hello world.

  • \o{<octal>}

    Определение символа его восьмеричным кодом octal из таблицы ASCII-символов. Код символа должен быть меньше, чем 0o400.

    Например, регулярному выражению \o{75} соответствует символ =.

Наборы символов в регулярных выражениях

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

  • [<BracketSpec>] – набор символов.

    Один символ соответствует любому символу из набора символов BracketSpec.

    Например, регулярному выражению K[OE]S соответствуют последовательности символов KOS и KES.

  • [^<BracketSpec>] – набор символов с инверсией.

    Один символ соответствует любому символу, не входящему в набор символов BracketSpec.

    Например, регулярному выражению K[^OE]S соответствуют последовательности символов KAS, K8S и любые другие последовательности из трех символов, которые начинаются на K и заканчиваются на S, кроме KОS и KES.

Набор символов BracketSpec может быть перечислен явно или определен как диапазон символов. Чтобы определить диапазон символов, первый и последний символ в наборе разделяют дефисом.

  • [<Digit1>-<DigitN>]

    Любая цифра из диапазона Digit1, Digit2, ... ,DigitN.

    Например, регулярному выражению [0-9] соответствует любая цифра. Записи регулярных выражений [0-9] и [0123456789] идентичны.

    Обратите внимание, что диапазон определяется одним символом до и одним символом после дефиса. Регулярному выражению [1-35] соответствуют символы 1, 2, 3 и 5, а не диапазон чисел от 1 до 35.

  • [<Letter1>-<LetterN>]

    Любая латинская буква из диапазона Letter1, Letter2, ... , LetterN (буквы должны быть в одинаковых регистрах).

    Например, регулярному выражению [a-zA-Z] соответствуют все буквы в нижнем и верхнем регистре из таблицы ASCII-символов.

ASCII-код символа верхней границы диапазона должен быть больше ASCII-кода символа нижней границы диапазона.

Например, регулярные выражения типа [5-2] или [z-a] недопустимы.

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

Примеры:

Регулярным выражениям [-az] и [az-] соответствуют символы a, z и -.

Регулярному выражению [a-z] соответствует любая из 26 латинских букв от a до z в нижнем регистре.

Регулярному выражению [-a-z] соответствует любая из 26 латинских букв от a до z в нижнем регистре и -.

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

Примеры:

Регулярному выражению [0^9] соответствуют символы 0, 9 и ^.

Регулярному выражению [^09] соответствует любой символ, кроме 0 и 9.

Внутри набора символов метасимволы *.&|!?+ теряют свое специальное значение и интерпретируются как литералы, поэтому предварять их метасимволом \ не обязательно. Обратный слеш \ сохраняет свое специальное значение внутри набора символов.

Например, регулярные выражения [a.] и [a\.] идентичны, и им соответствуют символ a и точка как литерал.

Группы символов и операторы в регулярных выражениях

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

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

В синтаксисе определены следующие операторы (перечислены в порядке убывания приоритета):

  • !<Expression>, где Expression может быть символом, набором или группой символов.

    Оператор означает исключение выражения Expression из списка допустимых выражений.

    Примеры:

    Регулярному выражению K!OS соответствуют последовательности символов KoS, KES и множество других последовательностей, которые состоят из трех символов, начинаются на K и заканчиваются на S, кроме KОS.

    Регулярному выражению K!(OS) соответствуют последовательности символов Kos, KES, KOT и множество других последовательностей, которые состоят из трех символов и начинаются на K, кроме KОS.

    Регулярному выражению K![OE]S соответствуют последовательности символов KoS, KeS, K;S и множество других последовательностей, которые состоят из трех символов, начинаются на K и заканчиваются на S, кроме KОS и KES.

  • <Expression>*, где Expression может быть символом, набором или группой символов.

    Оператор означает, что выражение Expression может встретиться в этой позиции ноль или больше раз.

    Примеры:

    Регулярному выражению 0-9* соответствуют последовательности символов 0-, 0-9, 0-99, ... .

    Регулярному выражению (0-9)* соответствуют пустая последовательность "" и последовательности символов 0-9, 0-90-9, ... .

    Регулярному выражению [0-9]* соответствуют пустая последовательность "" и любая непустая последовательность цифр.

  • <Expression>+, где Expression может быть символом, набором или группой символов.

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

    Примеры:

    Регулярному выражению 0-9+ соответствуют последовательности символов 0-9, 0-99, 0-999, ... .

    Регулярному выражению (0-9)+ соответствуют последовательности символов 0-9, 0-90-9, ... .

    Регулярному выражению [0-9]+ соответствует любая непустая последовательность цифр.

  • <Expression>?, где Expression может быть символом, набором или группой символов.

    Оператор означает, что выражение Expression может встретиться в данной позиции ноль или один раз.

    Примеры:

    Регулярному выражению https?:// соответствуют последовательности символов http:// и https://.

    Регулярному выражению K(aspersky)?OS соответствуют последовательности символов KOS и KasperskyOS.

  • <Expression1><Expression2> – конкатенация. Expression1 и Expression2 могут быть символами, наборами или группами символов.

    Оператор не имеет обозначения. В результирующем выражении за выражением Expression1 следует выражение Expression2.

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

  • <Expression1>|<Expression2> – дизъюнкция. Expression1 и Expression2 могут быть символами, наборами или группами символов.

    Оператор означает выбор выражения Expression1 или выражения Expression2.

    Примеры:

    Регулярному выражению KO|ES соответствуют последовательности символов KO и ES, но не KОS и не KES, так как оператор конкатенации имеет приоритет выше, чем оператор дизъюнкции.

    Регулярному выражению Press (OK|Cancel) соответствуют последовательности символов Press OK или Press Cancel.

    Регулярному выражению [0-9]|() соответствуют цифры от 0 до 9 или пустая строка.

  • <Expression1>&<Expression2> – конъюнкция. Expression1 и Expression2 могут быть символами, наборами или группами символов.

    Оператор означает пересечение результата выражения Expression1 с результатом выражения Expression2.

    Примеры:

    Регулярному выражению [0-9]&[^3] соответствуют цифры от 0 до 9, кроме 3.

    Регулярному выражению [a-zA-Z]&() соответствуют все латинские буквы и пустая строка.

В начало
[Topic ssp_descr_security_models_regex]

Модель безопасности HashSet

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

PSL-файл с описанием модели безопасности HashSet находится в KasperskyOS SDK по пути:

toolchain/include/nk/hashmap.psl

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

Объект модели безопасности HashSet

Правило init модели безопасности HashSet

Правило fini модели безопасности HashSet

Правило add модели безопасности HashSet

Правило remove модели безопасности HashSet

Выражение contains модели безопасности HashSet

В начало
[Topic ssp_descr_security_models_hashset]

Объект модели безопасности HashSet

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

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

Объект модели безопасности HashSet имеет следующие параметры:

  • type Entry – тип значений в таблицах (поддерживаются целочисленные типы, тип Boolean, а также словари и кортежи на базе целочисленных типов и типа Boolean);
  • config – конфигурация пула таблиц:
    • set_size – размер таблицы;
    • pool_size – число таблиц в пуле.

Все параметры объекта модели безопасности HashSet являются обязательными.

Пример:

policy object S : HashSet {

type Entry = UInt32

config =

{ set_size : 5

, pool_size : 2

}

}

Объект модели безопасности HashSet может быть покрыт аудитом безопасности. Условия выполнения аудита, специфичные для модели безопасности HashSet, отсутствуют.

Необходимость создавать несколько объектов модели безопасности HashSet возникает в следующих случаях:

  • Если нужно по-разному настроить аудит безопасности для разных объектов модели безопасности HashSet (например, для разных объектов можно применять разные профили аудита или разные конфигурации аудита одного профиля).
  • Если нужно различать вызовы методов, предоставляемых разными объектами модели безопасности HashSet (поскольку в данные аудита включается как имя метода модели безопасности, так и имя объекта, предоставляющего этот метод, можно понять, что был вызван метод конкретного объекта).
  • Если нужно использовать таблицы разных размеров и/или с разными типами значений.
В начало
[Topic ssp_descr_security_models_hashset_object]

Правило init модели безопасности HashSet

init {sid : <Sid>}

Ассоциирует свободную таблицу из пула таблиц с ресурсом sid. Если свободная таблица содержит значения после предыдущего использования, то эти значения удаляются.

Возвращает результат "разрешено", если создало ассоциацию таблицы с ресурсом sid.

Возвращает результат "запрещено" в следующих случаях:

  • В пуле нет свободных таблиц.
  • Ресурс sid уже ассоциирован с таблицей из пула таблиц используемого объекта модели безопасности HashSet.
  • Значение sid вне допустимого диапазона.

Пример:

/* Запуск процесса класса Server будет разрешен, если

* при инициации запуска будет создана ассоциация этого

* процесса с таблицей. Иначе запуск процесса класса

* Server будет запрещен. */

execute dst=Server {

S.init {sid : dst_sid}

}

В начало
[Topic ssp_descr_security_models_hashset_init]

Правило fini модели безопасности HashSet

fini {sid : <Sid>}

Удаляет ассоциацию таблицы с ресурсом sid (таблица становится свободной).

Возвращает результат "разрешено", если удалило ассоциацию таблицы с ресурсом sid.

Возвращает результат "запрещено" в следующих случаях:

  • Ресурс sid не ассоциирован с таблицей из пула таблиц используемого объекта модели безопасности HashSet.
  • Значение sid вне допустимого диапазона.
В начало
[Topic ssp_descr_security_models_hashset_fini]

Правило add модели безопасности HashSet

add {sid : <Sid>, entry : <Entry>}

Добавляет значение entry в таблицу, ассоциированную с ресурсом sid.

Возвращает результат "разрешено" в следующих случаях:

  • Правило добавило значение entry в таблицу, ассоциированную с ресурсом sid.
  • В таблице, ассоциированной с ресурсом sid, уже содержится значение entry.

Возвращает результат "запрещено" в следующих случаях:

  • Таблица, ассоциированная с ресурсом sid, полностью заполнена.
  • Ресурс sid не ассоциирован с таблицей из пула таблиц используемого объекта модели безопасности HashSet.
  • Значение sid вне допустимого диапазона.

Пример:

/* Процесс класса Server получит решение "разрешено" от

* модуля безопасности Kaspersky Security Module, вызывая метод интерфейса

* безопасности Add, если при вызове этого метода значение

* 5 будет добавлено в таблицу, ассоциированную с этим

* процессом, или уже содержится в этой таблице. Иначе

* процесс класса Server получит решение "запрещено" от

* модуля безопасности, вызывая метод интерфейса

* безопасности Add. */

security src=Server, method=Add {

S.add {sid : src_sid, entry : 5}

}

В начало
[Topic ssp_descr_security_models_hashset_add]

Правило remove модели безопасности HashSet

remove {sid : <Sid>, entry : <Entry>}

Удаляет значение entry из таблицы, ассоциированной с ресурсом sid.

Возвращает результат "разрешено" в следующих случаях:

  • Правило удалило значение entry из таблицы, ассоциированной с ресурсом sid.
  • В таблице, ассоциированной с ресурсом sid, нет значения entry.

Возвращает результат "запрещено" в следующих случаях:

  • Ресурс sid не ассоциирован с таблицей из пула таблиц используемого объекта модели безопасности HashSet.
  • Значение sid вне допустимого диапазона.
В начало
[Topic ssp_descr_security_models_hashset_remove]

Выражение contains модели безопасности HashSet

contains {sid : <Sid>, entry : <Entry>}

Проверяет, содержится ли значение entry в таблице, ассоциированной с ресурсом sid.

Возвращает значение типа Boolean. Если значение entry содержится в таблице, ассоциированной с ресурсом sid, возвращает true. Иначе возвращает false.

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

  • Ресурс sid не ассоциирован с таблицей из пула таблиц используемого объекта модели безопасности HashSet.
  • Значение sid вне допустимого диапазона.

Когда выражение выполняется некорректно, модуль безопасности Kaspersky Security Module возвращает решение "запрещено".

Пример:

/* Процесс класса Server получит решение "разрешено" от

* модуля безопасности Kaspersky Security Module, вызывая метод интерфейса

* безопасности Check, если значение 42 содержится в таблице,

* ассоциированной с этим процессом. Иначе процесс класса

* Server получит решение "запрещено" от модуля безопасности,

* вызывая метод интерфейса безопасности Check. */

security src=Server, method=Check {

assert(S.contains {sid : src_sid, entry : 42})

}

В начало
[Topic ssp_descr_security_models_hashset_contains]

Модель безопасности StaticMap

Модель безопасности StaticMap позволяет ассоциировать с ресурсами двумерные таблицы типа "ключ–значение", читать и изменять значения ключей. Например, можно ассоциировать процесс, в контексте которого выполняется драйвер, с регионом памяти MMIO, который разрешено использовать этому драйверу. Для этого потребуется два ключа, значения которых задают начальный адрес и размер региона памяти MMIO. Эту ассоциацию можно использовать, чтобы проверить, может ли драйвер обращаться к региону памяти MMIO, к которому он пытается получить доступ.

Ключи в таблице имеют одинаковый тип и является уникальными и неизменяемыми. Значения ключей в таблице имеют одинаковый тип.

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

PSL-файл с описанием модели безопасности StaticMap находится в KasperskyOS SDK по пути:

toolchain/include/nk/staticmap.psl

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

Объект модели безопасности StaticMap

Правило init модели безопасности StaticMap

Правило fini модели безопасности StaticMap

Правило set модели безопасности StaticMap

Правило commit модели безопасности StaticMap

Правило rollback модели безопасности StaticMap

Выражение get модели безопасности StaticMap

Выражение get_uncommited модели безопасности StaticMap

В начало
[Topic ssp_descr_security_models_staticmap]

Объект модели безопасности StaticMap

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

Объект модели безопасности StaticMap содержит пул двумерных таблиц типа "ключ–значение", которые имеют одинаковый размер. Ресурс может быть ассоциирован только с одной таблицей из пула таблиц каждого объекта модели безопасности StaticMap.

Объект модели безопасности StaticMap имеет следующие параметры:

  • type Value – тип значений ключей в таблицах (поддерживаются целочисленные типы);
  • config – конфигурация пула таблиц:
    • keys – таблица, содержащая ключи и их значения по умолчанию (ключи имеют тип Key = Text | List<UInt8>);
    • pool_size – число таблиц в пуле.

Все параметры объекта модели безопасности StaticMap являются обязательными.

Пример:

policy object M : StaticMap {

type Value = UInt16

config =

{ keys:

{ "k1" : 0

, "k2" : 1

}

, pool_size : 2

}

}

Объект модели безопасности StaticMap может быть покрыт аудитом безопасности. Условия выполнения аудита, специфичные для модели безопасности StaticMap, отсутствуют.

Необходимость создавать несколько объектов модели безопасности StaticMap возникает в следующих случаях:

  • Если нужно по-разному настроить аудит безопасности для разных объектов модели безопасности StaticMap (например, для разных объектов можно применять разные профили аудита или разные конфигурации аудита одного профиля).
  • Если нужно различать вызовы методов, предоставляемых разными объектами модели безопасности StaticMap (поскольку в данные аудита включается как имя метода модели безопасности, так и имя объекта, предоставляющего этот метод, можно понять, что был вызван метод конкретного объекта).
  • Если нужно использовать таблицы с разными наборами ключей и/или разными типами значений ключей.
В начало
[Topic ssp_descr_security_models_staticmap_object]

Правило init модели безопасности StaticMap

init {sid : <Sid>}

Ассоциирует свободную таблицу из пула таблиц с ресурсом sid. Ключи инициализируются значениями по умолчанию.

Возвращает результат "разрешено", если создало ассоциацию таблицы с ресурсом sid.

Возвращает результат "запрещено" в следующих случаях:

  • В пуле нет свободных таблиц.
  • Ресурс sid уже ассоциирован с таблицей из пула таблиц используемого объекта модели безопасности StaticMap.
  • Значение sid вне допустимого диапазона.

Пример:

/* Запуск процесса класса Server будет разрешен, если

* при инициации запуска будет создана ассоциация этого

* процесса с таблицей. Иначе запуск процесса класса

* Server будет запрещен. */

execute dst=Server {

M.init {sid : dst_sid}

}

В начало
[Topic ssp_descr_security_models_staticmap_init]

Правило fini модели безопасности StaticMap

fini {sid : <Sid>}

Удаляет ассоциацию таблицы с ресурсом sid (таблица становится свободной).

Возвращает результат "разрешено", если удалило ассоциацию таблицы с ресурсом sid.

Возвращает результат "запрещено" в следующих случаях:

  • Ресурс sid не ассоциирован с таблицей из пула таблиц используемого объекта модели безопасности StaticMap.
  • Значение sid вне допустимого диапазона.
В начало
[Topic ssp_descr_security_models_staticmap_fini]

Правило set модели безопасности StaticMap

set {sid : <Sid>, key : <Key>, value : <Value>}

Задает значение value ключу key в рабочем экземпляре таблицы, ассоциированной с ресурсом sid.

Возвращает результат "разрешено", если задало значение value ключу key в рабочем экземпляре таблицы, ассоциированной с ресурсом sid. (Текущее значение ключа будет перезаписано, даже если оно равно новому.)

Возвращает результат "запрещено" в следующих случаях:

  • Ключ key не содержится в таблице, ассоциированной с ресурсом sid.
  • Ресурс sid не ассоциирован с таблицей из пула таблиц используемого объекта модели безопасности StaticMap.
  • Значение sid вне допустимого диапазона.

Пример:

/* Процесс класса Server получит решение "разрешено" от

* модуля безопасности Kaspersky Security Module, вызывая метод интерфейса

* безопасности Set, если при вызове этого метода значение 2

* будет задано ключу k1 в рабочем экземпляре таблицы,

* ассоциированной с этим процессом. Иначе процесс класса

* Server получит решение "запрещено" от модуля безопасности,

* вызывая метод интерфейса безопасности Set. */

security src=Server, method=Set {

M.set {sid : src_sid, key : "k1", value : 2}

}

В начало
[Topic ssp_descr_security_models_staticmap_set]

Правило commit модели безопасности StaticMap

commit {sid : <Sid>}

Копирует значения ключей из рабочего в базовый экземпляр таблицы, ассоциированной с ресурсом sid.

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

Возвращает результат "запрещено" в следующих случаях:

  • Ресурс sid не ассоциирован с таблицей из пула таблиц используемого объекта модели безопасности StaticMap.
  • Значение sid вне допустимого диапазона.
В начало
[Topic ssp_descr_security_models_staticmap_commit]

Правило rollback модели безопасности StaticMap

rollback {sid : <Sid>}

Копирует значения ключей из базового в рабочий экземпляр таблицы, ассоциированной с ресурсом sid.

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

Возвращает результат "запрещено" в следующих случаях:

  • Ресурс sid не ассоциирован с таблицей из пула таблиц используемого объекта модели безопасности StaticMap.
  • Значение sid вне допустимого диапазона.
В начало
[Topic ssp_descr_security_models_staticmap_rollback]

Выражение get модели безопасности StaticMap

get {sid : <Sid>, key : <Key>}

Возвращает значение ключа key из базового экземпляра таблицы, ассоциированной с ресурсом sid.

Возвращает значение типа Value.

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

  • Ключ key не содержится в таблице, ассоциированной с ресурсом sid.
  • Ресурс sid не ассоциирован с таблицей из пула таблиц используемого объекта модели безопасности StaticMap.
  • Значение sid вне допустимого диапазона.

Когда выражение выполняется некорректно, модуль безопасности Kaspersky Security Module возвращает решение "запрещено".

Пример:

/* Процесс класса Server получит решение "разрешено" от

* модуля безопасности Kaspersky Security Module, вызывая метод интерфейса

* безопасности Get, если значение ключа k1 в базовом

* экземпляре таблицы, ассоциированной с этим процессом,

* отлично от нуля. Иначе процесс класса Server получит

* решение "запрещено" от модуля безопасности, вызывая

* метод интерфейса безопасности Get. */

security src=Server, method=Get {

assert(M.get {sid : src_sid, key : "k1"} != 0)

}

В начало
[Topic ssp_descr_security_models_staticmap_get]

Выражение get_uncommited модели безопасности StaticMap

get_uncommited {sid: <Sid>, key: <Key>}

Возвращает значение ключа key из рабочего экземпляра таблицы, ассоциированной с ресурсом sid.

Возвращает значение типа Value.

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

  • Ключ key не содержится в таблице, ассоциированной с ресурсом sid.
  • Ресурс sid не ассоциирован с таблицей из пула таблиц используемого объекта модели безопасности StaticMap.
  • Значение sid вне допустимого диапазона.

Когда выражение выполняется некорректно, модуль безопасности Kaspersky Security Module возвращает решение "запрещено".

В начало
[Topic ssp_descr_security_models_staticmap_get_u]

Модель безопасности Flow

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

PSL-файл с описанием модели безопасности Flow находится в KasperskyOS SDK по пути:

toolchain/include/nk/flow.psl

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

Объект модели безопасности Flow

Правило init модели безопасности Flow

Правило fini модели безопасности Flow

Правило enter модели безопасности Flow

Правило allow модели безопасности Flow

Выражение query модели безопасности Flow

В начало
[Topic ssp_descr_security_models_flow]

Объект модели безопасности Flow

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

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

Объект модели безопасности Flow имеет следующие параметры:

  • type State – тип, определяющий множество состояний конечного автомата (вариантный тип, объединяющий текстовые литералы);
  • config – конфигурация конечного автомата:
    • states – множество состояний конечного автомата (должно совпадать со множеством состояний, заданных типом State);
    • initial – начальное состояние конечного автомата;
    • transitions – описание допустимых переходов между состояниями конечного автомата.

Все параметры объекта модели безопасности Flow являются обязательными.

Пример:

policy object service_flow : Flow {

type State = "sleep" | "started" | "stopped" | "finished"

config = { states : ["sleep", "started", "stopped", "finished"]

, initial : "sleep"

, transitions : { "sleep" : ["started"]

, "started" : ["stopped", "finished"]

, "stopped" : ["started", "finished"]

}

}

}

finite_state_machine_example

Диаграмма состояний конечного автомата в примере

Объект модели безопасности Flow может быть покрыт аудитом безопасности. При этом можно задать условия выполнения аудита, специфичные для модели безопасности Flow. Для этого в описании конфигурации аудита нужно использовать следующую конструкцию:

omit : [<"состояние 1">[,] ...] – аудит не выполняется, если конечный автомат находится в одном из перечисленных состояний.

Необходимость создавать несколько объектов модели безопасности Flow возникает в следующих случаях:

  • Если нужно по-разному настроить аудит безопасности для разных объектов модели безопасности Flow (например, для разных объектов можно применять разные профили аудита или разные конфигурации аудита одного профиля).
  • Если нужно различать вызовы методов, предоставляемых разными объектами модели безопасности Flow (поскольку в данные аудита включается как имя метода модели безопасности, так и имя объекта, предоставляющего этот метод, можно понять, что был вызван метод конкретного объекта).
  • Если нужно использовать конечные автоматы с разными конфигурациями.
В начало
[Topic ssp_descr_security_models_flow_object]

Правило init модели безопасности Flow

init {sid : <Sid>}

Создает конечный автомат и ассоциирует его с ресурсом sid. Созданный конечный автомат имеет конфигурацию, заданную в параметрах используемого объекта модели безопасности Flow.

Возвращает результат "разрешено", если создало ассоциацию конечного автомата с ресурсом sid.

Возвращает результат "запрещено" в следующих случаях:

  • Ресурс sid уже ассоциирован с конечным автоматом используемого объекта модели безопасности Flow.
  • Значение sid вне допустимого диапазона.

Пример:

/* Запуск процесса класса Server будет разрешен,

* если при инициации запуска будет создана

* ассоциация этого процесса с конечным автоматом.

* Иначе запуск процесса класса Server будет запрещен. */

execute dst=Server {

service_flow.init {sid : dst_sid}

}

В начало
[Topic ssp_descr_security_models_flow_init]

Правило fini модели безопасности Flow

fini {sid : <Sid>}

Удаляет ассоциацию конечного автомата ресурсом sid. Конечный автомат, который более не ассоциирован с ресурсом, уничтожается.

Возвращает результат "разрешено", если удалило ассоциацию конечного автомата с ресурсом sid.

Возвращает результат "запрещено" в следующих случаях:

  • Ресурс sid не ассоциирован с конечным автоматом используемого объекта модели безопасности Flow.
  • Значение sid вне допустимого диапазона.
В начало
[Topic ssp_descr_security_models_flow_fini]

Правило enter модели безопасности Flow

enter {sid : <Sid>, state : <State>}

Переводит конечный автомат, ассоциированный с ресурсом sid, в состояние state.

Возвращает результат "разрешено", если перевело конечный автомат, ассоциированный с ресурсом sid, в состояние state.

Возвращает результат "запрещено" в следующих случаях:

  • Переход в состояние state из текущего состояния не допускается конфигурацией конечного автомата, ассоциированного с ресурсом sid.
  • Ресурс sid не ассоциирован с конечным автоматом используемого объекта модели безопасности Flow.
  • Значение sid вне допустимого диапазона.

Пример:

/* Любому клиенту в решении будет разрешено обращаться

* к серверу класса Server, если конечный автомат,

* ассоциированный с этим сервером, будет переведен в

* состояние started при инициации обращения. Иначе

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

* к серверу класса Server. */

request dst=Server {

service_flow.enter {sid : dst_sid, state : "started"}

}

В начало
[Topic ssp_descr_security_models_flow_enter]

Правило allow модели безопасности Flow

allow {sid : <Sid>, states : <Set<State>>}

Проверяет, что состояние конечного автомата, ассоциированного с ресурсом sid, входит в набор состояний states.

Возвращает результат "разрешено", если состояние конечного автомата, ассоциированного с ресурсом sid, входит в набор состояний states.

Возвращает результат "запрещено" в следующих случаях:

  • Состояние конечного автомата, ассоциированного с ресурсом sid, не входит в набор состояний states.
  • Ресурс sid не ассоциирован с конечным автоматом используемого объекта модели безопасности Flow.
  • Значение sid вне допустимого диапазона.

Пример:

/* Любому клиенту в решении разрешено обращаться к серверу класса

* Server, если конечный автомат, ассоциированный с этим сервером,

* находится в состоянии started или stopped. Иначе любому клиенту

* в решении запрещено обращаться к серверу класса Server. */

request dst=Server {

service_flow.allow {sid : dst_sid, states : ["started", "stopped"]}

}

В начало
[Topic ssp_descr_security_models_flow_allow]

Выражение query модели безопасности Flow

query {sid : <Sid>}

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

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

  • Ресурс sid не ассоциирован с конечным автоматом используемого объекта модели безопасности Flow.
  • Значение sid вне допустимого диапазона.

Когда выражение выполняется некорректно, модуль безопасности Kaspersky Security Module возвращает решение "запрещено".

Пример:

/* Любому клиенту в решении разрешено обращаться к

* серверу класса ResourceDriver, если конечный автомат,

* ассоциированный с этим сервером, находится в состоянии

* started или stopped. Иначе любому клиенту в решении

* запрещено обращаться к серверу класса ResourceDriver. */

request dst=ResourceDriver {

choice (service_flow.query {sid : dst_sid}) {

"started" : grant ()

"stopped" : grant ()

_ : deny ()

}

}

В начало
[Topic ssp_descr_security_models_flow_query]

Модель безопасности Mic

Модель безопасности Mic позволяет реализовать мандатный контроль целостности. То есть эта модель безопасности дает возможность управлять информационными потоками между процессами, а также между процессами и ядром KasperskyOS, контролируя уровни целостности процессов, ядра и ресурсов, используемых через IPC.

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

Информационные потоки между субъектами возникают, когда субъекты взаимодействуют через IPC.

Уровень целостности субъекта/ресурса – это степень доверия к субъекту/ресурсу. Степень доверия к субъекту определяется, например, исходя из того, взаимодействует ли субъект с недоверенными внешними программно-аппаратными системами, или имеет ли субъект доказанный уровень качества. (Ядро имеет высокий уровень целостности.) Степень доверия к ресурсу определяется, например, с учетом того, был ли этот ресурс создан доверенным субъектом внутри программно-аппаратной системы под управлением KasperskyOS или получен из недоверенной внешней программно-аппаратной системы.

Модель безопасности Mic характеризуют следующие положения:

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

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

PSL-файл с описанием модели безопасности Mic находится в KasperskyOS SDK по пути:

toolchain/include/nk/mic.psl

В качестве примера использования модели безопасности Mic можно рассмотреть безопасное обновление ПО программно-аппаратной системы под управлением KasperskyOS. В обновлении участвуют четыре процесса:

  • Downloader – низкоцелостный процесс, который загружает низкоцелостный образ обновления с удаленного сервера в интернете.
  • Verifier – высокоцелостный процесс, который проверяет цифровую подпись низкоцелостного образа обновления (высокоцелостный процесс, который может читать данные из низкоцелостного ресурса).
  • FileSystem – высокоцелостный процесс, который управляет файловой системой.
  • Updater – высокоцелостный процесс, который применяет обновление.

Обновление ПО выполняется по следующему сценарию:

  1. Downloader загружает образ обновления и сохраняет его в файл, передав содержимое образа в FileSystem. Этому файлу назначается низкий уровень целостности.
  2. Verifier получает образ обновления у FileSystem, прочитав низкоцелостный файл, и проверяет его цифровую подпись. Если подпись корректна, Verifier обращается к FileSystem, чтобы FileSystem создал копию файла с образом обновления. Новому файлу назначается высокий уровень целостности.
  3. Updater получает образ обновления у FileSystem, прочитав высокоцелостный файл, и применяет обновление.

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

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

Объект модели безопасности Mic

Правило create модели безопасности Mic

Правило execute модели безопасности Mic

Правило upgrade модели безопасности Mic

Правило call модели безопасности Mic

Правило invoke модели безопасности Mic

Правило read модели безопасности Mic

Правило write модели безопасности Mic

Выражение query_level модели безопасности Mic

В начало
[Topic ssp_descr_security_models_mic]

Объект модели безопасности Mic

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

Объект модели безопасности Mic имеет следующие параметры:

  • config – множество уровней целостности или конфигурация множества уровней целостности:
    • degrees – множество градаций для формирования множества уровней целостности;
    • categories – множество категорий для формирования множества уровней целостности.

Примеры:

policy object mic : Mic {

config = ["LOW", "MEDIUM", "HIGH"]

}

policy object mic_po : Mic {

config =

{ degrees : ["low", "high"]

, categories : ["net", "log"]

}

}

Множество уровней целостности представляет собой частично упорядоченное множество, которое является линейно упорядоченным или содержит несравнимые элементы. Множество {LOW, MEDIUM, HIGH} является линейно упорядоченным, так как все его элементы сравнимы между собой. Несравнимые элементы появляются, когда множество уровней целостности задается через множество градаций и множество категорий. В этом случае множество уровней целостности L представляет собой декартово произведение булеана множества категорий C на множество градаций D:

set_of_integrity_levels

Параметры degrees и categories в примере задают следующее множество:

{

{}/low, {}/high,

{net}/low, {net}/high,

{log}/low, {log}/high,

{net,log}/low, {net,log}/high

}

В этом множестве {} означает пустое множество.

Отношение порядка между элементами множества уровней целостности L задается следующим образом:

order_of_integrity_levels

Согласно этому отношению порядка j-й элемент превышает i-й элемент, если подмножество категорий E включает подмножество категорий A, и градация F больше градации A либо равна ей. Примеры сравнения элементов множества уровней целостности L:

  • Элемент {net,log}/high превышает элемент {log}/low, так как градация high больше градации low, и подмножество категорий {net,log} включает подмножество категорий {log}.
  • Элемент {net,log}/low превышает элемент {log}/low, так как уровни градаций для этих элементов равны между собой, и подмножество категорий {net,log} включает подмножество категорий {log}.
  • Элемент {net,log}/high является наибольшим, так как превышает все остальные элементы.
  • Элемент {}/low является наименьшим, так как все остальные элементы превышают этот элемент.
  • Элементы {net}/low и {log}/high являются несравнимыми, так как градация high больше градации low, но подмножество категорий {log} не включает подмножество категорий {net}.
  • Элементы {net,log}/low и {log}/high являются несравнимыми, так как градация high больше градации low, но подмножество категорий {log} не включает подмножество категорий {net,log}.

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

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

Объект модели безопасности Mic может быть покрыт аудитом безопасности. Условия выполнения аудита, специфичные для модели безопасности Mic, отсутствуют.

Необходимость создавать несколько объектов модели безопасности Mic возникает в следующих случаях:

  • Если нужно по-разному настроить аудит безопасности для разных объектов модели безопасности Mic (например, для разных объектов можно применять разные профили аудита или разные конфигурации аудита одного профиля).
  • Если нужно различать вызовы методов, предоставляемых разными объектами модели безопасности Mic (поскольку в данные аудита включается как имя метода модели безопасности, так и имя объекта, предоставляющего этот метод, можно понять, что был вызван метод конкретного объекта).
  • Если нужно использовать несколько вариантов мандатного контроля целостности, например, с разными множествами уровней целостности субъектов/ресурсов.
В начало
[Topic ssp_descr_security_models_mic_object]

Правило create модели безопасности Mic

create { source : <Sid>

, target : <Sid>

, container : <Sid | ()>

, driver : <Sid>

, level : <Level | ... | ()>

}

Назначает ресурсу target уровень целостности level в следующей ситуации:

  • Процесс source инициирует создание ресурса target.
  • Ресурсом target управляет субъект driver, который является поставщиком ресурсов или ядром KasperskyOS.
  • Ресурс container является контейнером для ресурса target (например, директория является контейнером для файлов и/или других директорий).

Если значение container не задано (container : ()), ресурс target рассматривается как корневой, то есть не имеющий контейнера.

Чтобы задать уровень целостности level, используются значения типа Level:

type Level = LevelFull | LevelNoCategory

type LevelFull =

{ degree : Text | ()

, categories : List<Text> | ()

}

type LevelNoCategory = Text

Правило возвращает результат "разрешено", если назначило ресурсу target уровень целостности level.

Правило возвращает результат "запрещено" в следующих случаях:

  • Значение level превышает уровень целостности процесса source, субъекта driver или ресурса container.
  • Значение level несравнимо с уровнем целостности процесса source, субъекта driver или ресурса container.
  • Процессу source, субъекту driver или ресурсу container не назначен уровень целостности.
  • Значение source, target, container или driver вне допустимого диапазона.

Пример:

/* Серверу класса updater.Realmserv будет разрешено отвечать на

* обращения любого клиента в решении, вызывающего метод resolve

* службы realm.Reader, если ресурсу, создание которого запрашивает

* клиент, при инициации ответа будет назначен уровень целостности LOW.

* Иначе серверу класса updater.Realmserv будет запрещено отвечать на

* обращения любого клиента, вызывающего метод resolve службы realm.Reader. */

response src=updater.Realmserv,

endpoint=realm.Reader {

match method=resolve {

mic.create { source : dst_sid

, target : message.handle.handle

, container : ()

, driver : src_sid

, level : "LOW"

}

}

}

В начало
[Topic ssp_descr_security_models_mic_create]

Правило execute модели безопасности Mic

execute <ExecuteImage | ExecuteLevel>

type ExecuteImage =

{ image : Sid

, target : Sid

, level : Level | ... | ()

, levelR : Level | ... | ()

}

type ExecuteLevel =

{ image : Sid | ()

, target : Sid

, level : Level | ...

, levelR : Level | ... | ()

}

Назначает субъекту target уровень целостности level и задает минимальный уровень целостности субъектов и ресурсов, из которых этот субъект может принимать данные (levelR). Код субъекта target содержится в исполняемом файле image.

Если значение level не задано (level : ()), субъекту target назначается уровень целостности исполняемого файла image. Если значение image не задано (image : ()), должно быть задано значение level.

Если значение levelR не задано (levelR : ()), то значение levelR равно level.

Чтобы задать уровни целостности level и levelR, используются значения типа Level. Определение типа Level см. в "Правило create модели безопасности Mic".

Правило возвращает результат "разрешено", если назначило субъекту target уровень целостности level и задало минимальный уровень целостности субъектов и ресурсов, из которых этот субъект может принимать данные (levelR).

Правило возвращает результат "запрещено" в следующих случаях:

  • Значение level превышает уровень целостности исполняемого файла image.
  • Значение level несравнимо с уровнем целостности исполняемого файла image.
  • Значение levelR превышает значение level.
  • Значения level и levelR несравнимы.
  • Исполняемому файлу image не назначен уровень целостности.
  • Значение image или target вне допустимого диапазона.

Пример:

/* Запуск процесса класса updater.Manager будет разрешен,

* если при инициации запуска этому процессу будет назначен

* уровень целостности LOW, а также будет задан минимальный

* уровень целостности процессов и ресурсов, из которых этот

* процесс может принимать данные (LOW). Иначе запуск процесса

* класса updater.Manager будет запрещен. */

execute src=Einit, dst=updater.Manager, method=main {

mic.execute { target : dst_sid

, image : ()

, level : "LOW"

, levelR : "LOW"

}

}

В начало
[Topic ssp_descr_security_models_mic_execute]

Правило upgrade модели безопасности Mic

upgrade { source : <Sid>

, target : <Sid>

, container : <Sid | ()>

, driver : <Sid>

, level : <Level | ...>

}

Повышает назначенный ранее уровень целостности ресурса target до значения level в следующей ситуации:

  • Процесс source инициирует повышение уровня целостности ресурса target.
  • Ресурсом target управляет субъект driver, который является поставщиком ресурсов или ядром KasperskyOS.
  • Ресурс container является контейнером для ресурса target (например, директория является контейнером для файлов и/или других директорий).

Если значение container не задано (container : ()), ресурс target рассматривается как корневой, то есть не имеющий контейнера.

Чтобы задать уровень целостности level, используются значения типа Level. Определение типа Level см. в "Правило create модели безопасности Mic".

Правило возвращает результат "разрешено", если повысило назначенный ранее уровень целостности ресурса target до значения level.

Правило возвращает результат "запрещено" в следующих случаях:

  • Значение level не превышает уровень целостности ресурса target.
  • Значение level превышает уровень целостности процесса source, субъекта driver или ресурса container.
  • Уровень целостности ресурса target превышает уровень целостности процесса source.
  • Процессу source, субъекту driver или ресурсу container не назначен уровень целостности.
  • Значение source, target, container или driver вне допустимого диапазона.
В начало
[Topic ssp_descr_security_models_mic_upgrade]

Правило call модели безопасности Mic

call {source : <Sid>, target : <Sid>}

Проверяет допустимость информационных потоков от субъекта target к субъекту source.

Возвращает результат "разрешено" в следующих случаях:

  • Уровень целостности субъекта source не превышает уровень целостности субъекта target.
  • Уровень целостности субъекта source превышает уровень целостности субъекта target, но минимальный уровень целостности субъектов и ресурсов, из которых субъект source может принимать данные, не превышает уровень целостности субъекта target.
  • Уровень целостности субъекта source несравним с уровнем целостности субъекта target, но минимальный уровень целостности субъектов и ресурсов, из которых субъект source может принимать данные, не превышает уровень целостности субъекта target.

Возвращает результат "запрещено" в следующих случаях:

  • Уровень целостности субъекта source превышает уровень целостности субъекта target, и минимальный уровень целостности субъектов и ресурсов, из которых субъект source может принимать данные, превышает уровень целостности субъекта target.
  • Уровень целостности субъекта source превышает уровень целостности субъекта target, и минимальный уровень целостности субъектов и ресурсов, из которых субъект source может читать данные, несравним с уровнем целостности субъекта target.
  • Уровень целостности субъекта source несравним с уровнем целостности субъекта target, и минимальный уровень целостности субъектов и ресурсов, из которых субъект source может принимать данные, превышает уровень целостности субъекта target.
  • Уровень целостности субъекта source несравним с уровнем целостности субъекта target, и минимальный уровень целостности субъектов и ресурсов, из которых субъект source может принимать данные, несравним с уровнем целостности субъекта target.
  • Субъекту source или субъекту target не назначен уровень целостности.
  • Значение source или target вне допустимого диапазона.

Пример:

/* Любому клиенту в решении разрешено обращаться к

* любому серверу (ядру), если информационные потоки от

* сервера (ядра) к клиенту допускаются моделью

* безопасности Mic. Иначе любому клиенту в решении

* запрещено обращаться к любому серверу (ядру). */

request {

mic.call { source : src_sid

, target : dst_sid

}

}

В начало
[Topic ssp_descr_security_models_mic_call]

Правило invoke модели безопасности Mic

invoke {source : <Sid>, target : <Sid>}

Проверяет допустимость информационных потоков от субъекта source к субъекту target.

Возвращает результат "разрешено", если уровень целостности субъекта target не превышает уровень целостности субъекта source.

Возвращает результат "запрещено" в следующих случаях:

  • Уровень целостности субъекта target превышает уровень целостности субъекта source.
  • Уровень целостности субъекта target несравним с уровнем целостности субъекта source.
  • Субъекту source или субъекту target не назначен уровень целостности.
  • Значение source или target вне допустимого диапазона.
В начало
[Topic ssp_descr_security_models_mic_invoke]

Правило read модели безопасности Mic

read {source : <Sid>, target : <Sid>}

Проверяет допустимость чтения данных из ресурса target потребителем ресурсов source.

Возвращает результат "разрешено" в следующих случаях:

  • Уровень целостности потребителя ресурсов source не превышает уровень целостности ресурса target.
  • Уровень целостности потребителя ресурсов source превышает уровень целостности ресурса target, но минимальный уровень целостности субъектов и ресурсов, из которых потребитель ресурсов source может принимать данные, не превышает уровень целостности ресурса target.
  • Уровень целостности потребителя ресурсов source несравним с уровнем целостности ресурса target, но минимальный уровень целостности субъектов и ресурсов, из которых потребитель ресурсов source может принимать данные, не превышает уровень целостности ресурса target.

Возвращает результат "запрещено" в следующих случаях:

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

Пример:

/* Любому клиенту в решении разрешено обращаться к серверу

* класса updater.Realmserv, вызывая метод read службы

* realm.Reader, если модель безопасности Mic допускает

* чтение данных этим клиентом из ресурса, который требуется

* этому клиенту. Иначе любому клиенту в решении запрещено

* обращаться к серверу класса updater.Realmserv, вызывая

* метод read службы realm.Reader. */

request dst=updater.Realmserv,

endpoint=realm.Reader {

match method=read {

mic.read { source : src_sid,

, target : message.handle.handle

}

}

}

В начало
[Topic ssp_descr_security_models_mic_read]

Правило write модели безопасности Mic

write {source : <Sid>, target : <Sid>}

Проверяет допустимость записи данных в ресурс target потребителем ресурсов source.

Возвращает результат "разрешено", если уровень целостности ресурса target не превышает уровень целостности потребителя ресурсов source.

Возвращает результат "запрещено" в следующих случаях:

  • Уровень целостности ресурса target превышает уровень целостности потребителя ресурсов source.
  • Уровень целостности ресурса target несравним с уровнем целостности потребителя ресурсов source.
  • Потребителю ресурсов source или ресурсу target не назначен уровень целостности.
  • Значение source или target вне допустимого диапазона.
В начало
[Topic ssp_descr_security_models_mic_write]

Выражение query_level модели безопасности Mic

query_level {source : <Sid>}

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

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

  • Субъекту или ресурсу source не назначен уровень целостности.
  • Значение source вне допустимого диапазона.

Когда выражение выполняется некорректно, модуль безопасности Kaspersky Security Module возвращает решение "запрещено".

В начало
[Topic ssp_descr_security_models_mic_query_level]