KasperskyOS Security models

Pred security model

The Pred security model lets you perform comparison operations.

A PSL file containing a description of the Pred security model is located in the KasperskyOS SDK at the following path:

toolchain/include/nk/basic.psl

Pred security model object

The basic.psl file contains a declaration that creates a Pred security model object named pred. Consequently, inclusion of the basic.psl file into the solution security policy description will create a Pred security model object by default.

A Pred security model object does not have any parameters and cannot be covered by a security audit.

It is not necessary to create additional Pred security model objects.

Pred security model methods

A Pred security model contains expressions that perform comparison operations and return values of the Boolean type. To call these expressions, use the following comparison operators:

• <ScalarLiteral> == <ScalarLiteral> – "equals".
• <ScalarLiteral> != <ScalarLiteral> – "does not equal".
• <Number> < <Number> – "is less than".
• <Number> <= <Number> – "is less than or equal to".
• <Number> > <Number> – "is greater than".
• <Number> >= <Number> – "is greater than or equal to".

The Pred security model also contains the empty expression that lets you determine whether data contains its own structural elements. This expression returns values of the Boolean type. If data does not contain its own structural elements (for example, a set is empty), the expression returns true, otherwise it returns false. To call the expression, use the following construct:

Bool security model

The Bool security model lets you perform logical operations.

A PSL file containing a description of the Bool security model is located in the KasperskyOS SDK at the following path:

toolchain/include/nk/basic.psl

Bool security model object

The basic.psl file contains a declaration that creates a Bool security model object named bool. Consequently, inclusion of the basic.psl file into the solution security policy description will create a Bool security model object by default.

A Bool security model object does not have any parameters and cannot be covered by a security audit.

It is not necessary to create additional Bool security model objects.

Bool security model methods

The Bool security model contains expressions that perform logical operations and return values of the Boolean type. To call these expressions, use the following logical operators:

• ! <Boolean> – "logical NOT".
• <Boolean> && <Boolean> – "logical AND".
• <Boolean> || <Boolean> – "logical OR".
• <Boolean> ==> <Boolean> – "implication" (! <Boolean> || <Boolean>).

The Bool security model also contains the all, any and cond expressions.

The expression all performs a "logical AND" for an arbitrary number of values of Boolean type. It returns values of the Boolean type. It returns true if an empty list of values ([]) is passed via the parameter. To call the expression, use the following construct:

The expression any performs a "logical OR" for an arbitrary number of values of Boolean type. It returns values of the Boolean type. It returns false if an empty list of values ([]) is passed via the parameter. To call the expression, use the following construct:

cond expression performs a ternary conditional operation. Returns values of the ScalarLiteral type. To call the expression, use the following construct:

In addition to expressions, the Bool security model includes the assert rule that works the same as the rule of the same name included in the Base security model.

Math security model

The Math security model lets you perform integer arithmetic operations.

A PSL file containing a description of the Math security model is located in the KasperskyOS SDK at the following path:

toolchain/include/nk/basic.psl

Math security model object

The basic.psl file contains a declaration that creates a Math security model object named math. Consequently, inclusion of the basic.psl file into the solution security policy description will create a Math security model object by default.

A Math security model object does not have any parameters and cannot be covered by a security audit.

It is not necessary to create additional Math security model objects.

Math security model methods

The Math security model contains expressions that perform integer arithmetic operations. To call a part of these expressions, use the following arithmetic operators:

• <Number> + <Number> – "addition". Returns values of the Number type.
• <Number> - <Number> – "subtraction". Returns values of the Number type.
• <Number> * <Number> – "multiplication". Returns values of the Number type.

The other expressions are as follows:

• neg <Signed> – "change number sign". Returns values of the Signed type.
• abs <Signed> – "get module of number". Returns values of the Signed type.
• sum <List<Number>> – "add numbers from list". Returns values of the Number type. It returns 0 if an empty list of values ([]) is passed via the parameter.
• product <List<Number>> – "multiply numbers from list". Returns values of the Number type. It returns 1 if an empty list of values ([]) is passed via the parameter.

To call these expressions, use the following construct:

Struct security model

The Struct security model lets you obtain access to structural data elements.

A PSL file containing a description of the Struct security model is located in the KasperskyOS SDK at the following path:

toolchain/include/nk/basic.psl

Struct security model object

The basic.psl file contains a declaration that creates a Struct security model object named struct. Consequently, inclusion of the basic.psl file into the solution security policy description will create a Struct security model object by default.

A Struct security model object does not have any parameters and cannot be covered by a security audit.

It is not necessary to create additional Struct security model objects.

Struct security model methods

The Struct security model contains expressions that provide access to structural data elements. To call these expressions, use the following constructs:

• <{...}>.<field name> – "get access to dictionary field". the type of returned data corresponds to the type of dictionary field.
• <List | Set | Sequence | Array>.[<element number>] – "get access to data element". The type of returned data corresponds to the type of elements. The numbering of elements starts with zero. When out of bounds of dataset, the expression terminates with an error and the Kaspersky Security Module returns the "denied" decision.
• <HandleDesc>.handle – "get SID". Returns values of the Handle type. (For details on the correlation between handles and SID values, see "Resource Access Control").
• <HandleDesc>.rights – "get handle permissions mask". Returns values of the UInt32 type.

Parameters of interface methods are saved in a special dictionary named message. To obtain access to an interface method parameter, use the following construct:

The parameter name is specified in accordance with the IDL description.

To obtain access to structural elements of parameters, use the constructs corresponding to expressions of the Struct security model.

Base security model

The Base security model lets you implement basic logic.

A PSL file containing a description of the Base security model is located in the KasperskyOS SDK at the following path:

toolchain/include/nk/base.psl

Base security model object

The base.psl file contains a declaration that creates a Base security model object named base. Consequently, inclusion of the base.psl file into the solution security policy description will create a Base security model object by default. Methods of this object can be called without indicating the object name.

A Base security model object does not have any parameters.

A Base security model object can be covered by a security audit. There are no audit conditions specific to the Base security model.

It is necessary to create additional objects of the Base security model in the following cases:

• You need to configure a security audit differently for different objects of the Base security model (for example, you can apply different audit profiles or different audit configurations of the same profile for different objects).
• You need to distinguish between calls of methods provided by different objects of the Base security model (audit data includes the name of the security model method and the name of the object that provides this method, so you can verify that the method of a specific object was called).

Base security model methods

The Base security model contains the following rules:

• grant ()

  It has a parameter of the () type. It returns the "granted" result.

  Example:

  /* A client of the foo class is allowed

  * to query a server of the bar class. */

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

• assert <Boolean>

  It returns the "granted" result if the true value is passed via the parameter. Otherwise it returns the "denied" result.

  Example:

  /* Any client in the solution will be allowed to query a server of the foo class

  * by calling the Send method of the net.Net endpoint if the port parameter

  * of the Send method will be used to pass a value greater than 80. Otherwise any

  * client in the solution will be prohibited from querying a server of the

  * foo class by calling the Send method of the net.Net endpoint. */

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

• deny <Boolean | ()>

  It returns the "denied" result if the true or () value is passed via the parameter. Otherwise it returns the "granted" result.

  Example:

  /* A server of the foo class is not allowed to

  * respond to a client of the bar class. */

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

• set_level <UInt8>

  It sets the security audit runtime-level equal to the value passed via this parameter. It returns the "granted" result. (For more details about the security audit runtime-level, see "Describing security audit profiles".)

  Example:

  /* A process of the foo class will receive the "allowed" decision from the

  * Kaspersky Security Module if it calls the

  * SetAuditLevel security interface method to change the security audit runtime-level. */

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

Regex security model

The Regex security model lets you implement text data validation based on statically defined regular expressions.

A PSL file containing a description of the Regex security model is located in the KasperskyOS SDK at the following path:

toolchain/include/nk/regex.psl

Regex security model object

The regex.psl file contains a declaration that creates a Regex security model object named re. Consequently, inclusion of the regex.psl file into the solution security policy description will create a Regex security model object by default.

A Regex security model object does not have any parameters.

A Regex security model object can be covered by a security audit. In this case, you also need to define the audit conditions specific to the Regex security model. To do so, use the following constructs in the audit configuration description:

• emit : ["match"] – the audit is performed if the match method is called.
• emit : ["select"] – the audit is performed if the select method is called.
• emit : ["match", "select"] – the audit is performed if the match or select method is called.
• emit : [] – the audit is not performed.

It is necessary to create additional objects of the Regex security model in the following cases:

• You need to configure a security audit differently for different objects of the Regex security model (for example, you can apply different audit profiles or different audit configurations of the same profile for different objects).
• You need to distinguish between calls of methods provided by different objects of the Regex security model (audit data includes the name of the security model method and the name of the object that provides this method, so you can verify that the method of a specific object was called).

Regex security model methods

The Regex security model contains the following expressions:

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

  Returns a value of the Boolean type. If the specified text matches the pattern regular expression, it returns true. Otherwise it returns false.

  Example:

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

• select {text : <Text>}

  It is intended to be used as an expression that verifies fulfillment of the conditions in the choice construct (for details on the choice construct, see "Binding methods of security models to security events"). It checks whether the specified text matches regular expressions. Depending on the results of this check, various options for security event handling can be performed.

  Example:

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

  "hello\ .*": grant ()

  ".*world" : grant ()

  _ : deny ()

  }

Syntax of regular expressions of the Regex security model

A regular expression for the match method of the Regex security model can be written in two ways: within the multi-line regex block or as a text literal.

For example, the following two regular expressions are identical:

Regular expressions for the select method of the Regex security model are written as text literals with a double backslash.

A regular expression is defined as a template string and may contain the following:

• Literals (ordinary characters)
• Metacharacters (characters with special meanings)
• White-space characters
• Character sets
• Character groups
• Operators for working with characters

Regular expressions are case sensitive.

Literals and metacharacters in regular expressions

• A literal can be any ASCII character except the metacharacters .()*&|!?+[]\ and a white-space character. (Unicode characters are not supported.)

  For example, the regular expression KasperskyOS corresponds to the text KasperskyOS.

• Metacharacters have special meanings that are presented in the table below.

  Special meanings of metacharacters

  Metacharacter	Special meaning
  []	Square brackets (braces) denote the beginning and end of a set of characters.
  ()	Round brackets (parentheses) denote the beginning and end of a group of characters.
  *	An asterisk denotes an operator indicating that the character preceding it can repeat zero or more times.
  +	A plus sign denotes an operator indicating that the character preceding it can repeat one or more times.
  ?	A question mark denotes an operator indicating that the character preceding it can repeat zero or one time.
  !	An exclamation mark denotes an operator excluding the subsequent character from the list of valid characters.
  |	A vertical line denotes an operator for selection between characters (logically close to the "OR" conjunction).
  &	An ampersand denotes an operator for overlapping of multiple conditions (logically close to the "AND" conjunction).
  .	A dot denotes any character. For example, the regular expression K.S corresponds to the sequences of characters KOS, KoS, KES and a multitude of other sequences consisting of three characters that begin with K and end with S, and in which the second character can be any character: literal, metacharacter, or dot.
  \	\<metaSymbol> A backslash indicates that the metacharacter that follows it will lose its special meaning and instead be interpreted as a literal. A backslash placed before a metacharacter is known as an escape character. For example, a regular expression that consists of a dot metacharacter (.) corresponds to any character. However, a regular expression that consists of a backslash with a dot (\.) corresponds to only a dot character. Accordingly, a backslash also escapes another subsequent backslash. For example, the regular expression C:\\Users corresponds to the sequence of characters C:\Users.

• The ^ and $ characters are not used to designate the start and end of a line.

White-space characters in regular expressions

• A space character has an ASCII code of 20 in a hexadecimal number system and has an ASCII code of 40 in an octal number system. Although a space character does not infer any special meaning, it must be escaped to avoid any ambiguous interpretation by the regular expression interpreter.

  For example, the regular expression Hello\ world corresponds to the sequence of characters Hello world.

• \r

  Carriage return character.

• \n

  Line break character.

• \t

  Horizontal tab character.

Definition of a character based on its octal or hexadecimal code in regular expressions

• \x{<hex>}

  Definition of a character using its hex code from the ASCII character table. The character code must be less than 0x100.

  For example, the regular expression Hello\x{20}world corresponds to the sequence of characters Hello world.

• \o{<octal>}

  Definition of a character using its octal code from the ASCII character table. The character code must be less than 0o400.

  For example, the regular expression \o{75} corresponds to the = character.

Sets of characters in regular expressions

A character set is defined within square brackets [] as a list or range of characters. A character set tells the regular expression interpreter that only one of the characters listed in the set or range of characters can be at this specific location in a sequence of characters. A character set cannot be left blank.

• [<BracketSpec>] – character set.

  One character corresponds to any character from the BracketSpec character set.

  For example, the regular expression K[OE]S corresponds to the sequences of characters KOS and KES.

• [^<BracketSpec>] – inverted character set.

  One character corresponds to any character that is not in the BracketSpec character set.

  For example, the regular expression K[^OE]S corresponds to the sequences of characters KAS, K8S and any other sequences consisting of three characters that begin with K and end with S, excluding KOS and KES.

The BracketSpec character set can be listed explicitly or can be defined as a range of characters. When defining a range of characters, the first and last character in the set must be separated with a hyphen.

• [<Digit1>-<DigitN>]

  Any number from the range Digit1, Digit2, ... ,DigitN.

  For example, the regular expression [0-9] corresponds to any numerical digit. The regular expressions [0-9] and [0123456789] are identical.

  Please note that a range is defined by one character before a hyphen and one character after the hyphen. The regular expression [1-35] corresponds only to the characters 1, 2, 3 and 5, and does not represent the range of numbers from 1 to 35.

• [<Letter1>-<LetterN>]

  Any English letter from the range Letter1, Letter2, ... , LetterN (these letters must be in the same case).

  For example, the regular expression [a-zA-Z] corresponds to all letters in uppercase and lowercase from the ASCII character table.

The ASCII code for the upper boundary character of a range must be higher than the ASCII code for the lower boundary character of the range.

For example, the regular expressions [5-2] or [z-a] are invalid.

The hyphen (minus) - character is interpreted as a special character only within a set of characters. Outside of a character set, a hyphen is a literal. For this reason, the \ metacharacter does not have to precede a hyphen. To use a hyphen as a literal within a character set, it must be indicated first or last in the set.

Examples:

The regular expressions [-az] and [az-] correspond to the characters a, z and -.

The regular expression [a-z] corresponds to any of the 26 English letters from a to z in lowercase.

The regular expression [-a-z] corresponds to any of the 26 English letters from a to z in lowercase and -.

The circumflex (caret character) ^ is interpreted as a special character only within a character set when it is located directly after an opening square bracket. Outside of a character set, a circumflex is a literal. For this reason, the \ metacharacter does not have to precede a circumflex. To use a circumflex as a literal within a character set, it must be indicated in a location other than first in the set.

Examples:

The regular expression [0^9] correspond to the characters 0, 9 and ^.

The regular expression [^09] corresponds to any character except 0 and 9.

Within a character set, the metacharacters *.&|!?+ lose their special meaning and are instead interpreted as literals. Therefore, they do not have to be preceded by the \ metacharacter. The backslash \ retains its special meaning within a character set.

For example, the regular expressions [a.] and [a\.] are identical and correspond to the character a and a dot interpreted as a literal.

Groups of characters and operators in regular expressions

A character group uses parentheses () to distinguish its portion (subexpression) within a regular expression. Groups are normally used to allocate subexpressions as operands. Groups can be embedded into each other.

The syntax contains definitions of the following operators (listed in descending order of their priority):

• !<Expression>, where Expression can be a character, set or group of characters.

  This operator excludes the Expression from the list of valid expressions.

  Examples:

  The regular expression K!OS corresponds to the sequences of characters KoS, KES, and a multitude of other sequences that consist of three characters and begin with K and end with S, excluding KOS.

  The regular expression K!(OS) corresponds to the sequences of characters Kos, KES, KOT, and a multitude of other sequences that consist of three characters and begin with K, excluding KOS.

  The regular expression K![OE]S corresponds to the sequences of characters KoS, KeS, K;S, and a multitude of other sequences that consist of three characters and begin with K and end with S, excluding KOS and KES.

• <Expression>*, where Expression can be a character, set or group of characters.

  This operator means that the Expression may occur in the specific position zero or more times.

  Examples:

  The regular expression 0-9* corresponds to the sequences of characters 0-, 0-9, 0-99, ... .

  The regular expression (0-9)* corresponds to the empty sequence "" and the sequences of characters 0-9, 0-90-9, ... .

  The regular expression [0-9]* corresponds to the empty sequence "" and any non-empty sequence of numbers.

• <Expression>+, where Expression can be a character, set or group of characters.

  This operator means that the Expression may occur in the specific position one or more times.

  Examples:

  The regular expression 0-9+ corresponds to the sequences of characters 0-9, 0-99, 0-999, ... .

  The regular expression (0-9)+ corresponds to the sequences of characters 0-9, 0-90-9, ... .

  The regular expression [0-9]+ corresponds to any non-empty sequence of numbers.

• <Expression>?, where Expression can be a character, set or group of characters.

  This operator means that the Expression may occur in the specific position zero or one time.

  Examples:

  The regular expression https?:// corresponds to the sequences of characters http:// and https://.

  The regular expression K(aspersky)?OS corresponds to the sequences of characters KOS and KasperskyOS.

• <Expression1><Expression2> – concatenation. Expression1 and Expression2 can be characters, sets or groups of characters.

  This operator does not have a specific designation. In the resulting expression, Expression2 follows Expression1.

  For example, concatenation of the sequences of characters micro and kernel will result in the sequence of characters microkernel.

• <Expression1>|<Expression2> – disjunction. Expression1 and Expression2 can be characters, sets or groups of characters.

  This operator selects either Expression1 or Expression2.

  Examples:

  The regular expression KO|ES corresponds to the sequences of characters KO and ES, but not KOS or KES because the concatenation operator has a higher priority than the disjunction operator.

  The regular expression Press (OK|Cancel) corresponds to the sequences of characters Press OK or Press Cancel.

  The regular expression [0-9]|() corresponds to numbers from 0 to 9 or an empty string.

• <Expression1>&<Expression2> – conjunction. Expression1 and Expression2 can be characters, sets or groups of characters.

  This operator intersects the result of Expression1 with the result of Expression2.

  Examples:

  The regular expression [0-9]&[^3] corresponds to numbers from 0 to 9, excluding 3.

  The regular expression [a-zA-Z]&() corresponds to all English letters and an empty string.

HashSet security model

The HashSet security model lets you associate resources with one-dimensional tables of unique values of the same type, add or delete these values, and check whether a defined value is in the table. For example, a process of the network server can be associated with the set of ports that this server is allowed to open. This association can be used to check whether the server is allowed to initiate the opening of a port.

A PSL file containing a description of the HashSet security model is located in the KasperskyOS SDK at the following path:

toolchain/include/nk/hashmap.psl

HashSet security model object

To use the HashSet security model, you need to create an object or objects of this model.

A HashSet security model object contains a pool of one-dimensional tables of the same size intended for storing the values of one type. A resource can be associated with only one table from the tables pool of each HashSet security model object.

A HashSet security model object has the following parameters:

• type Entry – type of values in tables (these can be integer types, Boolean type, and dictionaries and tuples based on integer types and the Boolean type).
• config – configuration of the pool of tables:
  • set_size – size of the table.
  • pool_size – number of tables in the pool.

All parameters of a HashSet security model object are required.

Example:

A HashSet security model object can be covered by a security audit. There are no audit conditions specific to the HashSet security model.

It is necessary to create multiple objects of the HashSet security model in the following cases:

• You need to configure a security audit differently for different objects of the HashSet security model (for example, you can apply different audit profiles or different audit configurations of the same profile for different objects).
• You need to distinguish between calls of methods provided by different objects of the HashSet security model (audit data includes the name of the security model method and the name of the object that provides this method, so you can verify that the method of a specific object was called).
• You need to use tables of different sizes and/or with different types of values.

HashSet security model init rule

It associates a free table from the tables pool with the sid resource. If the free table contains values after its previous use, these values are deleted.

It returns the "allowed" result if an association was created between the table and the sid resource.

It returns the "denied" result in the following cases:

• There are no free tables in the pool.
• The sid resource is already associated with a table from the tables pool of the HashSet security model object being used.
• The sid value is outside of the permissible range.

Example:

HashSet security model fini rule

It deletes the association between the table and the sid resource (the table becomes free).

It returns the "allowed" result if the association between the table and the sid resource was deleted.

It returns the "denied" result in the following cases:

• The sid resource is not associated with a table from the tables pool of the HashSet security model object being used.
• The sid value is outside of the permissible range.

HashSet security model add rule

It adds the entry value to the table associated with the sid resource.

It returns the "allowed" result in the following cases:

• The rule added the entry value to the table associated with the sid resource.
• The table associated with the sid resource already contains the entry value.

It returns the "denied" result in the following cases:

• The table associated with the sid resource is completely full.
• The sid resource is not associated with a table from the tables pool of the HashSet security model object being used.
• The sid value is outside of the permissible range.

Example:

HashSet security model remove rule

It deletes the entry value from the table associated with the sid resource.

It returns the "allowed" result in the following cases:

• The rule deleted the entry value from the table associated with the sid resource.
• The table associated with the sid resource does not contain the entry value.

It returns the "denied" result in the following cases:

• The sid resource is not associated with a table from the tables pool of the HashSet security model object being used.
• The sid value is outside of the permissible range.

HashSet security model contains expression

It checks whether the entry value is in the table associated with the sid resource.

It returns a value of the Boolean type. If the entry value is in the table associated with the sid resource, it returns true. Otherwise it returns false.

It runs incorrectly in the following cases:

• The sid resource is not associated with a table from the tables pool of the HashSet security model object being used.
• The sid value is outside of the permissible range.

When the expression runs incorrectly, the Kaspersky Security Module returns the "denied" decision.

Example:

StaticMap security model

The StaticMap security model lets you associate resources with two-dimensional "key–value" tables, read and modify the values of keys. For example, a process of the driver can be associated with the MMIO memory region that this driver is allowed to use. This will require two keys whose values define the starting address and the size of the MMIO memory region. This association can be used to check whether the driver can query the MMIO memory region that it is attempting to access.

Keys in the table have the same type but are unique and immutable. The values of keys in the table have the same type.

There are two simultaneous instances of the table: base instance and working instance. Both instances are initialized by the same data. Changes are made first to the working instance and then can be added to the base instance, or vice versa: the working instance can be changed by using previous values from the base instance. The values of keys can be read from the base instance or working instance of the table.

A PSL file containing a description of the StaticMap security model is located in the KasperskyOS SDK at the following path:

toolchain/include/nk/staticmap.psl

StaticMap security model object

To use the StaticMap security model, you need to create an object or objects of this model.

A StaticMap security model object contains a pool of two-dimensional "key–value" tables that have the same size. A resource can be associated with only one table from the tables pool of each StaticMap security model object.

A StaticMap security model object has the following parameters:

• type Value – type of values of keys in tables (integer types are supported).
• config – configuration of the pool of tables:
  • keys – table containing keys and their default values (keys have the Key = Text | List<UInt8> type).
  • pool_size – number of tables in the pool.

All parameters of a StaticMap security model object are required.

Example:

A StaticMap security model object can be covered by a security audit. There are no audit conditions specific to the StaticMap security model.

It is necessary to create multiple objects of the StaticMap security model in the following cases:

• You need to configure a security audit differently for different objects of the StaticMap security model (for example, you can apply different audit profiles or different audit configurations of the same profile for different objects).
• You need to distinguish between calls of methods provided by different objects of the StaticMap security model (audit data includes the name of the security model method and the name of the object that provides this method, so you can verify that the method of a specific object was called).
• You need to use tables with different sets of keys and/or different types of key values.

StaticMap security model init rule

It associates a free table from the tables pool with the sid resource. Keys are initialized by the default values.

It returns the "allowed" result if an association was created between the table and the sid resource.

It returns the "denied" result in the following cases:

• There are no free tables in the pool.
• The sid resource is already associated with a table from the tables pool of the StaticMap security model object being used.
• The sid value is outside of the permissible range.

Example:

StaticMap security model fini rule

It deletes the association between the table and the sid resource (the table becomes free).

It returns the "allowed" result if the association between the table and the sid resource was deleted.

It returns the "denied" result in the following cases:

• The sid resource is not associated with a table from the tables pool of the StaticMap security model object being used.
• The sid value is outside of the permissible range.

StaticMap security model set rule

It assigns the specified value to the specified key in the working instance of the table associated with the sid resource.

It returns the "allowed" result if the specified value was assigned to the specified key in the working instance of the table associated with the sid resource. (The current value of the key will be overwritten even if it is equal to the new value.)

It returns the "denied" result in the following cases:

• The specified key is not in the table associated with the sid resource.
• The sid resource is not associated with a table from the tables pool of the StaticMap security model object being used.
• The sid value is outside of the permissible range.

Example:

StaticMap security model commit rule

It copies the values of keys from the working instance to the base instance of the table associated with the sid resource.

It returns the "allowed" result if the values of keys were copied from the working instance to the base instance of the table associated with the sid resource.

It returns the "denied" result in the following cases:

• The sid resource is not associated with a table from the tables pool of the StaticMap security model object being used.
• The sid value is outside of the permissible range.

StaticMap security model rollback rule

It copies the values of keys from the base instance to the working instance of the table associated with the sid resource.

It returns the "allowed" result if the values of keys were copied from the base instance to the working instance of the table associated with the sid resource.

It returns the "denied" result in the following cases:

• The sid resource is not associated with a table from the tables pool of the StaticMap security model object being used.
• The sid value is outside of the permissible range.

StaticMap security model get expression

It returns the value of the specified key from the base instance of the table associated with the sid resource.

It returns a value of the Value type.

It runs incorrectly in the following cases:

• The specified key is not in the table associated with the sid resource.
• The sid resource is not associated with a table from the tables pool of the StaticMap security model object being used.
• The sid value is outside of the permissible range.

When the expression runs incorrectly, the Kaspersky Security Module returns the "denied" decision.

Example:

StaticMap security model get_uncommited expression

It returns the value of the specified key from the working instance of the table associated with the sid resource.

It returns a value of the Value type.

It runs incorrectly in the following cases:

• The specified key is not in the table associated with the sid resource.
• The sid resource is not associated with a table from the tables pool of the StaticMap security model object being used.
• The sid value is outside of the permissible range.

When the expression runs incorrectly, the Kaspersky Security Module returns the "denied" decision.

Flow security model

The Flow security model lets you associate resources with finite-state machines, receive and modify the states of finite-state machines, and check whether the state of the finite-state machine is within the defined set of states. For example, a process can be associated with a finite-state machine to allow or prohibit this process from using storage and/or the network depending on the state of the finite-state machine.

A PSL file containing a description of the Flow security model is located in the KasperskyOS SDK at the following path:

toolchain/include/nk/flow.psl

Flow security model object

To use the Flow security model, you need to create an object or objects of this model.

One Flow security model object lets you associate a set of resources with a set of finite-state machines that have the same configuration. A resource can be associated with only one finite-state machine of each Flow security model object.

A Flow security model object has the following parameters:

• type State – type that determines the set of states of the finite-state machine (variant type that combines text literals).
• config – configuration of the finite-state machine:
  • states – set of states of the finite-state machine (must match the set of states defined by the State type).
  • initial – initial state of the finite-state machine.
  • transitions – description of the permissible transitions between states of the finite-state machine.

All parameters of a Flow security model object are required.

Example:

Diagram of finite-state machine states in the example

A Flow security model object can be covered by a security audit. You can also define the audit conditions specific to the Flow security model. To do so, use the following construct in the audit configuration description:

omit : [<"state 1">[,] ...] – the audit is not performed if the finite-state machine is in one of the listed states.

It is necessary to create multiple objects of the Flow security model in the following cases:

• You need to configure a security audit differently for different objects of the Flow security model (for example, you can apply different audit profiles or different audit configurations of the same profile for different objects).
• You need to distinguish between calls of methods provided by different objects of the Flow security model (audit data includes the name of the security model method and the name of the object that provides this method, so you can verify that the method of a specific object was called).
• You need to use finite-state machines with different configurations.

Flow security model init rule

It creates a finite-state machine and associates it with the sid resource. The created finite-state machine has the configuration defined in the settings of the Flow security model object being used.

It returns the "granted" result if an association was created between the finite-state machine and the sid resource.

It returns the "denied" result in the following cases:

• The sid resource is already associated with a finite-state machine of the Flow security model object being used.
• The sid value is outside of the permissible range.

Example:

Flow security model fini rule

It deletes the association between the finite-state machine and the sid resource. The finite-state machine that is no longer associated with the resource is destroyed.

It returns the "granted" result if the association between the finite-state machine and the sid resource was deleted.

It returns the "denied" result in the following cases:

• The sid resource is not associated with a finite-state machine of the Flow security model object being used.
• The sid value is outside of the permissible range.

Flow security model enter rule

It switches the finite-state machine associated with the sid resource to the specified state.

It returns the "granted" result if the finite-state machine associated with the sid resource was switched to the specified state.

It returns the "denied" result in the following cases:

• The transition to the specified state from the current state is not permitted by the configuration of the finite-state machine associated with the sid resource.
• The sid resource is not associated with a finite-state machine of the Flow security model object being used.
• The sid value is outside of the permissible range.

Example:

Flow security model allow rule

It verifies that the state of the finite-state machine associated with the sid is in the set of defined states.

It returns the "granted" result if the state of the finite-state machine associated with the sid resource is in the set of defined states.

It returns the "denied" result in the following cases:

• The state of the finite-state machine associated with the sid resource is not in the set of defined states.
• The sid resource is not associated with a finite-state machine of the Flow security model object being used.
• The sid value is outside of the permissible range.

Example:

Flow security model query expression

It is intended to be used as an expression that verifies fulfillment of the conditions in the choice construct (for details on the choice construct, see "Binding methods of security models to security events"). It checks the state of the finite-state machine associated with the sid resource. Depending on the results of this check, various options for security event handling can be performed.

It runs incorrectly in the following cases:

• The sid resource is not associated with a finite-state machine of the Flow security model object being used.
• The sid value is outside of the permissible range.

When the expression runs incorrectly, the Kaspersky Security Module returns the "denied" decision.

Example:

Mic security model

The Mic security model lets you implement mandatory integrity control. In other words, this security model provides the capability to manage data streams between different processes and between processes and the KasperskyOS kernel by controlling the integrity levels of processes, the kernel, and resources that are used via IPC.

Data streams are generated between subjects when the subjects interact via IPC.

The integrity level of a subject/resource is the level of trust afforded to the subject/resource. The degree of trust in a subject depends on whether the subject interacts with untrusted external software/hardware systems or whether the subject has a proven quality level, for example. (The kernel has a high level of integrity.) The degree of trust in a resource depends on whether this resource was created by a trusted subject within a software/hardware system running KasperskyOS or if it was received from an untrusted external software/hardware system, for example.

The Mic security model is characterized by the following provisions:

• By default, data streams from subjects with less integrity to subjects with higher integrity are prohibited. You have the option of permitting such data streams if you can guarantee that the subjects with higher integrity will not be compromised.
• A resource consumer is prohibited from writing data to a resource if the integrity level of the resource is higher than the integrity level of the resource consumer.
• By default, a resource consumer is prohibited from reading data from a resource if the integrity level of the resource is lower than the integrity level of the resource consumer. You have the option to allow the resource consumer to perform such an operation if you can guarantee that the resource consumer will not be compromised.

Methods of the Mic security model let you assign integrity levels to subjects and resources, check the permissibility of data streams based on a comparison of integrity levels, and elevate the integrity levels of resources.

A PSL file containing a description of the Mic security model is located in the KasperskyOS SDK at the following path:

toolchain/include/nk/mic.psl

For an example of using the Mic security model, we can examine a secure software update for a software/hardware system running KasperskyOS. Four processes are involved in the update:

• Downloader is a low-integrity process that downloads a low-integrity update image from a remote server on the Internet.
• Verifier is a high-integrity process that verifies the digital signature of the low-integrity update image (high-integrity process that can read data from a low-integrity resource).
• FileSystem is a high-integrity process that manages the file system.
• Updater is a high-integrity process that applies an update.

A software update is performed according to the following scenario:

1. The Downloader downloads an update image and saves it to a file by transferring the contents of the image to the FileSystem. A low integrity level is assigned to this file.
2. The Verifier receives the update image from the FileSystem by reading the high-integrity file, and verifies its digital signature. If the signature is correct, the Verifier queries the FileSystem so that the FileSystem creates a copy of the file containing the update image. A high integrity level is assigned to the new file.
3. The Updater receives the update image from the FileSystem by reading the high-integrity file, and applies the update.

In this example, the Mic security model ensures that the high-integrity Updater process can read data only from a high-integrity update image. As a result, the update can be applied only after the digital signature of the update image is verified.

Mic security model object

To use the Mic security model, you need to create an object or objects of this model. You also need to assign a set of integrity levels for subjects and resources.

A Mic security model object has the following parameters:

• config refers to a set of integrity levels or configuration of a set of integrity levels:
  • degrees refers to a set of gradations for generating a set of integrity levels.
  • categories refers to a set of categories for generating a set of integrity levels.

Examples:

A set of integrity levels is a partially ordered set that is linearly ordered or contains incomparable elements. The set {LOW, MEDIUM, HIGH} is linearly ordered because all of its elements are comparable to each other. Incomparable elements arise when a set of integrity levels is defined through a set of gradations and a set of categories. In this case, the set of integrity levels L is a Cartesian product of the Boolean set of categories C multiplied by the set of gradations D:

The degrees and categories parameters in this example define the following set:

{

{}/low, {}/high,

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

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

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

}

In this set, {} means an empty set.

The order relation between elements of the set of integrity levels L is defined as follows:

According to this order relation, the jth element exceeds the ith element if the subset of categories E includes the subset of categories A, and gradation F is greater than or equal to gradation A. Examples of comparing elements of the set of integrity levels L:

• The {net,log}/high element exceeds the {log}/low element because the "high" gradation is greater than the "low" gradation, and the subset of categories {net,log} includes the subset of categories {log}.
• The {net,log}/low element exceeds the {log}/low element because the levels of gradations for these elements are equal, and the subset of categories {net,log} includes the subset of categories {log}.
• The {net,log}/high element is the highest because it exceeds all other elements.
• The {}/low element is the lowest because all other elements exceed this element.
• The {net}/low and {log}/high elements are incomparable because the "high" gradation is greater than the "low" gradation but the subset of categories {log} does not include the subset of categories {net}.
• The {net,log}/low and {log}/high elements are incomparable because the "high" gradation is greater than the "low" gradation but the subset of categories {log} does not include the subset of categories {net,log}.

A Mic security model object can be covered by a security audit. There are no audit conditions specific to the Mic security model.

It is necessary to create multiple objects of the Mic security model in the following cases:

• You need to configure a security audit differently for different objects of the Mic security model (for example, you can apply different audit profiles or different audit configurations of the same profile for different objects).
• You need to distinguish between calls of methods provided by different objects of the Mic security model (audit data includes the name of the security model method and the name of the object that provides this method, so you can verify that the method of a specific object was called).
• You need to use multiple variants of mandatory integrity control that may have different sets of integrity levels for subjects and resources, for example.

Mic security model create rule

Assign the specified integrity level to the target resource in the following situation:

• The source process initiates creation of the target resource.
• The target resource is managed by the driver subject, which is the resource provider or the KasperskyOS kernel.
• The container resource is a container for the target resource (for example, a directory is a container for files and/or other directories).

If the container value is not defined (container : ()), the target resource is considered to be the root resource, which means that it has no container.

To define the integrity level, values of the Level type are used:

The rule returns the "granted" result if a specific integrity level was assigned to the target resource.

The rule returns the "denied" result in the following cases:

• The level value exceeds the integrity level of the source process, driver subject or container resource.
• The level value is incomparable to the integrity level of the source process, driver subject or container resource.
• An integrity level was not assigned to the source process, driver subject, or container resource.
• The value of source, target, container or driver is outside of the permissible range.

Example:

Mic security model execute rule

This assigns the specified integrity level to the target subject and defines the minimum integrity level of subjects and resources from which this subject can receive data (levelR). The code of the target subject is in the image executable file.

If the level value is not defined (level : ()), the integrity level of the image executable file is assigned to the target subject. If the image value is not defined (image : ()), the level value must be defined.

If the levelR value is not defined (levelR : ()), the value of levelR is equal to level.

To define the integrity level and levelR, values of the Level type are used. For the definition of the Level type, see "Mic security model create rule".

The rule returns the "granted" result if it assigned the specified integrity level to the target subject and defined the minimum integrity level of subjects and resources from which this subject can receive data (levelR).

The rule returns the "denied" result in the following cases:

• The level value exceeds the integrity level of the image executable file.
• The level value is incomparable to the integrity level of the image executable file.
• The value of levelR exceeds the value of level.
• The level and levelR values are incomparable.
• An integrity level was not assigned to the image executable file.
• The image or target value is outside of the permissible range.

Example:

Mic security model upgrade rule

This elevates the previously assigned integrity level of the target resource to the specified level in the following situation:

• The source process initiates elevation of the integrity level of the target resource.
• The target resource is managed by the driver subject, which is the resource provider or the KasperskyOS kernel.
• The container resource is a container for the target resource (for example, a directory is a container for files and/or other directories).

If the container value is not defined (container : ()), the target resource is considered to be the root resource, which means that it has no container.

To define the integrity level, values of the Level type are used. For the definition of the Level type, see "Mic security model create rule".

The rule returns the "granted" result if it elevated the previously assigned integrity level of the target resource to the level value.

The rule returns the "denied" result in the following cases:

• The level value does not exceed the integrity level of the target resource.
• The level value exceeds the integrity level of the source process, driver subject or container resource.
• The integrity level of the target resource exceeds the integrity level of the source process.
• An integrity level was not assigned to the source process, driver subject, or container resource.
• The value of source, target, container or driver is outside of the permissible range.

Mic security model call rule

This verifies the permissibility of data streams from the target subject to the source subject.

It returns the "allowed" result in the following cases:

• The integrity level of the source subject does not exceed the integrity level of the target subject.
• The integrity level of the source subject exceeds the integrity level of the target subject, but the minimum integrity level of subjects and resources from which the source subject can receive data does not exceed the integrity level of the target subject.
• The integrity level of the source subject is incomparable to the integrity level of the target subject, but the minimum integrity level of subjects and resources from which the source subject can receive data does not exceed the integrity level of the target subject.

It returns the "denied" result in the following cases:

• The integrity level of the source subject exceeds the integrity level of the target subject, and the minimum integrity level of subjects and resources from which the source subject can receive data exceeds the integrity level of the target subject.
• The integrity level of the source subject exceeds the integrity level of the target subject, and the minimum integrity level of subjects and resources from which the source subject can read data is incomparable to the integrity level of the target subject.
• The integrity level of the source subject is incomparable to the integrity level of the target subject, and the minimum integrity level of subjects and resources from which the source subject can receive data exceeds the integrity level of the target subject.
• The integrity level of the source subject is incomparable to the integrity level of the target subject, and the minimum integrity level of subjects and resources from which the source subject can receive data is incomparable to the integrity level of the target subject.
• An integrity level was not assigned to the source subject or to the target subject.
• The source or target value is outside of the permissible range.

Example:

Mic security model invoke rule

This verifies the permissibility of data streams from the source subject to the target subject.

It returns the "granted" result if the integrity level of the target subject does not exceed the integrity level of the source subject.

It returns the "denied" result in the following cases:

• The integrity level of the target subject exceeds the integrity level of the source subject.
• The integrity level of the target subject is incomparable to the integrity level of the source subject.
• An integrity level was not assigned to the source subject or to the target subject.
• The source or target value is outside of the permissible range.

Mic security model read rule

This verifies that the source resource consumer is allowed to read data from the target resource.

It returns the "allowed" result in the following cases:

• The integrity level of the source resource consumer does not exceed the integrity level of the target resource.
• The integrity level of the source resource consumer exceeds the integrity level of the target resource, but the minimum integrity level of subjects and resources from which the source resource consumer can receive data does not exceed the integrity level of the target resource.
• The integrity level of the source resource consumer is incomparable to the integrity level of the target resource, but the minimum integrity level of subjects and resources from which the source resource consumer can receive data does not exceed the integrity level of the target resource.

It returns the "denied" result in the following cases:

• The integrity level of the source resource consumer exceeds the integrity level of the target resource, and the minimum integrity level of subjects and resources from which the source resource consumer can receive data exceeds the integrity level of the target resource.
• The integrity level of the source resource consumer exceeds the integrity level of the target resource, and the minimum integrity level of subjects and resources from which the source resource consumer can receive data is incomparable to the integrity level of the target resource.
• The integrity level of the source resource consumer is incomparable to the integrity level of the target resource, and the minimum integrity level of subjects and resources from which the source resource consumer can receive data exceeds the integrity level of the target resource.
• The integrity level of the source resource consumer is incomparable to the integrity level of the target resource, and the minimum integrity level of subjects and resources from which the source resource consumer can receive data is incomparable to the integrity level of the target resource.
• An integrity level was not assigned to the source resource consumer or to the target resource.
• The source or target value is outside of the permissible range.

Example:

Mic security model write rule

This verifies that the source resource consumer is allowed to write data to the target resource.

It returns the "granted" result if the integrity level of the target resource does not exceed the integrity level of the source resource consumer.

It returns the "denied" result in the following cases:

• The integrity level of the target resource exceeds the integrity level of the source resource consumer.
• The integrity level of the target resource is incomparable to the integrity level of the source resource consumer.
• An integrity level was not assigned to the source resource consumer or to the target resource.
• The source or target value is outside of the permissible range.

Mic security model query_level expression

It is intended to be used as an expression that verifies fulfillment of the conditions in the choice construct (for details on the choice construct, see "Binding methods of security models to security events"). It checks the integrity level of the source resource or subject. Depending on the results of this check, various options for security event handling can be performed.

It runs incorrectly in the following cases:

• An integrity level was not assigned to the subject or source resource.
• The source value is outside of the permissible range.

When the expression runs incorrectly, the Kaspersky Security Module returns the "denied" decision.