What's new

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 determines 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:

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

Page top

Bool security model

The Bool security model performs 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:

bool.all (<List<Boolean>>)

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:

bool.any (<List<Boolean>>)

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

bool.cond
  { if   : <Boolean> // Condition
  , then : <ScalarLiteral> // Value returned when the condition is true
  , else : <ScalarLiteral> // Value returned when the condition is false
  }

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.

Page top

Math security model

The Math security model performs 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>>) – "multiple 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:

math.<expression name> (<parameter>)

Page top

Struct security model

The Struct security model obtains 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:

<dictionary>.<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:

message.<interface method parameter name>

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.

To use expressions of the Struct security model, the security event description must be sufficiently precise so that it corresponds to IPC messages of the same type (for more details, see "Binding methods of security models to security events"). IPC messages of this type must contain the defined parameters of the interface method, and the interface method parameters must contain the defined structural elements.

Page top

Base security model

The Base security model implements 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) }

Page top

Regex security model

The Regex security model implements 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.

When writing a regular expression as a text literal, all backslash instances must be doubled.

For example, the following two regular expressions are identical:

// Regular expression within the multi-line regex block
{ pattern:
    ```regex
    Hello\ world\!
    ```
, text: "Hello world!"
}
// Regular expression as a text literal (doubled backslash)
{ pattern: "Hello\\ world\\!"
, text: "Hello world!"
}

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.

Operators are applied to more than one character in a regular expression only if they are immediately before or after the definition of a set or group of characters. If this is the case, the operator is applied to the entire group or set of characters.

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.

Page top

HashSet security model

The HashSet security model associates resources with one-dimensional tables of unique values of the same type, adds or deletes these values, and checks 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

In this section

HashSet security model object

HashSet security model init rule

HashSet security model fini rule

HashSet security model add rule

HashSet security model remove rule

HashSet security model contains expression

Page top

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:

policy object s : HashSet {
    type Entry = UInt32
 
    config =
      { set_size : 5
      , pool_size : 2
      }
}

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.

Page top

HashSet security model init rule

init {sid : <Sid>}

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:

/* A process of the Server class will be allowed to start if,
 * at startup initiation, an association will be created
 * between this process and the table. Otherwise the startup of a process of the
 * Server class will be denied. */
execute dst=Server {
    s.init {sid : dst_sid}
}

Page top

HashSet security model fini rule

fini {sid : <Sid>}

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.

Page top

HashSet security model add rule

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

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:

/* A process of the Server class will receive the "allowed" decision from
 * the Kaspersky Security Module by calling the
 * Add security interface method if, when this method is called, the value
 * 5 will be added to the table associated with this
 * process, or is already in the table. Otherwise
 * a process of the Server class will receive the "denied" decision from the
 * security module by calling the
 * Add security interface method. */
security src=Server, method=Add {
    s.add {sid : src_sid, entry : 5}
}

Page top

HashSet security model remove rule

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

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.

Page top

HashSet security model contains expression

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

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:

/* A process of the Server class will receive the "allowed" decision from
 * the Kaspersky Security Module by calling the
 * Check security interface method if the value 42 is in the table
 * associated with this process. Otherwise a process of the
 * Server class will receive the "denied" decision from the security module
 /* by calling the Check security interface method. */
security src=Server, method=Check {
    assert(s.contains {sid : src_sid, entry : 42})
}

Page top

StaticMap security model

The StaticMap security model associates resources with two-dimensional "key–value" tables, reads and modifies 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 base 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

In this section

StaticMap security model object

StaticMap security model init rule

StaticMap security model fini rule

StaticMap security model set rule

StaticMap security model commit rule

StaticMap security model rollback rule

StaticMap security model get expression

StaticMap security model get_uncommitted expression

Page top

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:

policy object m : StaticMap {
    type Value = UInt16
 
    config =
      { keys:
        { "k1" : 0
        , "k2" : 1
        }
      , pool_size : 2
      }
}

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.

Page top

StaticMap security model init rule

init {sid : <Sid>}

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:

/* A process of the Server class will be allowed to start if,
 * at startup initiation, an association will be created
 * between this process and the table. Otherwise the startup of a process of the
 * Server class will be denied. */
execute dst=Server {
    m.init {sid : dst_sid}
}

Page top

StaticMap security model fini rule

fini {sid : <Sid>}

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.

Page top

StaticMap security model set rule

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

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:

/* A process of the Server class will receive the "allowed" decision from
 * the Kaspersky Security Module by calling the
 * Set security interface method if, when this method is called, the value 2
 * will be assigned to key k1 in the working instance of the table
 * associated with this process. Otherwise a process of the
 * Server class will receive the "denied" decision from the security module
 /* by calling the Set security interface method. */
security src=Server, method=Set {
    m.set {sid : src_sid, key : "k1", value : 2}
}

Page top

StaticMap security model commit rule

commit {sid : <Sid>}

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.

Page top

StaticMap security model rollback rule

rollback {sid : <Sid>}

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.

Page top

StaticMap security model get expression

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

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:

/* A process of the Server class will receive the "allowed" decision from
 * the Kaspersky Security Module by calling the
 * Get security interface method if the value of key k1 in the base
 * instance of the table associated with this process
 * is not zero. Otherwise a process of the Server class will receive
 * the "denied" decision from the security module
 * by calling the Get security interface method. */
security src=Server, method=Get {
    assert(m.get {sid : src_sid, key : "k1"} != 0)
}

Page top

StaticMap security model get_uncommitted expression

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

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.

Page top

Flow security model

The Flow security model associates resources with finite-state machines, receives and modifies the states of finite-state machines, and checks 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

In this section

Flow security model object

Flow security model init rule

Flow security model fini rule

Flow security model enter rule

Flow security model allow rule

Flow security model query expression

Page top

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 associates 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:

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

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.

Page top

Flow security model init rule

init {sid : <Sid>}

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:

/* A process of the Server class will be allowed to start
 * if, at startup initiation, an association will be created
 * between this process and the finite-state machine.
 * Otherwise the startup of the Server-class process will be denied. */
execute dst=Server {
    service_flow.init {sid : dst_sid}
}

Page top

Flow security model fini rule

fini {sid : <Sid>}

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.

Page top

Flow security model enter rule

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

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:

/* Any client in the solution will be allowed to query
 * a server of the Server class if the finite-state machine
 * associated with this server will be switched to
 * the "started" state when initiating the query. Otherwise
 * any client in the solution will be denied to query
 * a server of the Server class. */
request dst=Server {
    service_flow.enter {sid : dst_sid, state : "started"}
}

Page top

Flow security model allow rule

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

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:

/* Any client in the solution is allowed to query a server
 * of the Server class if the finite-state machine associated with this server
 * is in the started or stopped state. Otherwise any client
 * in the solution will be prohibited from querying a server of the Server class. */
request dst=Server {
    service_flow.allow {sid : dst_sid, states : ["started", "stopped"]}
}

Page top

Flow security model query expression

query {sid : <Sid>}

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:

/* Any client in the solution is allowed to query
 * a server of the ResourceDriver class if the finite-state machine
 * associated with this server is in the
 * "started" or "stopped" state. Otherwise any client in the solution
 * is prohibited from querying a server of the ResourceDriver class. */
request dst=ResourceDriver { 
    choice (service_flow.query {sid : dst_sid}) {
        "started"   : grant ()
        "stopped"   : grant ()
        _           : deny ()
    }
}

Page top

Mic security model

The Mic security model implements 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.

In Mic security model terminology, processes and the kernel are called subjects while resources are called objects. However, the information provided in this section slightly deviates from the terminology of the Mic security model. In this section, the term "object" is not used to refer to a "resource".

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 a Mic security model let you perform the following operations:

Assign integrity levels to subjects and resources.
Unassign the integrity level from resources.
Verify the permissibility of data streams based on a comparison of integrity levels.
Increase 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:

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.
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.
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.

In this section

Mic security model object

Mic security model create rule

Mic security model delete rule

Mic security model execute rule

Mic security model upgrade rule

Mic security model call rule

Mic security model invoke rule

Mic security model read rule

Mic security model write rule

Mic security model query_level expression

Page top

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 – set of integrity levels or configuration of a set of integrity levels:
- degrees – set of gradations for generating a set of integrity levels.
- categories – set of categories for generating a set of integrity levels.

Examples:

policy object mic : Mic {
    config = ["LOW", "MEDIUM", "HIGH"]
}
 
policy object mic_po : Mic {
    config =
      { degrees    : ["low", "high"]
      , categories : ["net", "log"]
      }
}

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:

set_of_integrity_levels

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:

order_of_integrity_levels

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}.

For subjects and resources that have incomparable integrity levels, the Mic security model provides conditions that are analogous to the conditions that the security model provides for subjects and resources that have comparable integrity levels.

By default, data streams between subjects that have incomparable integrity levels are prohibited. However, you have the option to allow such data streams if you can guarantee that the subjects receiving data will not be compromised. A resource consumer is prohibited from writing data to a resource and read data from a resource if the integrity level of the resource is incomparable to the integrity level of the resource consumer. You have the option to allow the resource consumer to read data from a resource if you can guarantee that the resource consumer will not be compromised.

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.

Page top

Mic security model create rule

create { source    : <Sid>
       , target    : <Sid>
       , container : <Sid | ()>
       , driver    : <Sid>
       , level     : <Level | ... | ()>
       }

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 field has the value (), 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:

type Level = LevelFull | LevelNoCategory
 
type LevelFull =
  { degree     : Text | ()
  , categories : List<Text> | ()
  }
 
type LevelNoCategory = Text

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:

/* A server of the updater.Realmserv class will be allowed to respond to
 * queries of any client in the solution calling the resolve method
 * of the realm.Reader endpoint if the resource whose creation is requested
 * by the client will be assigned the LOW integrity level during response initiation.
 * Otherwise a server of the updater.Realmserv class will be prohibited from responding to
 * queries of any client calling the resolve method of the realm.Reader endpoint. */
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"
                            }
             }
}

Page top

Mic security model delete rule

delete { source    : <Sid>
       , target    : <Sid>
       , container : <Sid | ()>
       , driver    : <Sid>
       }

Unassigns the integrity level from the target resource in the following situation:

The source process initiates deletion 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 field has the value (), the target resource is considered to be the root resource, which means that it has no container.

The rule returns the "granted" result if it unassigned the integrity level from the target resource.

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

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

Example:

/* Any client in the solution will be allowed to query a server of the foo class
 * updater.Realmserv class by calling the del method of the realm.Reader endpoint if the
 * integrity level will be unassigned from the resource whose deletion is requested by the client.
 * Otherwise, any client in the solution will be prohibited from querying a server of the
 * updater.Realmserv class by calling the del method of the realm.Reader endpoint. */
request dst=updater.Realmserv,
        endpoint=realm.Reader {
            match method=del {
                mic.delete { source : src_sid
                           , target : message.handle.handle
                           , container : ()
                           , driver : dst_sid
                           }
               }
}

Page top

Mic security model execute rule

execute <ExecuteImage | ExecuteLevel>
 
type ExecuteImage =
  { image  : Sid
  , target : Sid
  , level  : Level | ... | ()
  , levelR : Level | ... | ()
  }
 
type ExecuteLevel =
  { image  : Sid | ()
  , target : Sid
  , level  : Level | ...
  , levelR : Level | ... | ()
  }

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 field has the value (), the integrity level of the image executable file is assigned to the target subject. If the image field has the value (), the level field must have a value other than ().

If the levelR field has the value (), the levelR integrity level is assumed to be equal to the integrity level of the target subject.

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:

/* A process of the updater.Manager class will be allowed to start
 * if, at startup initiation, this process will be assigned
 * the integrity level LOW, and the minimum
 * integrity level will be defined for the processes and resources from which this
 * process can received data (LOW). Otherwise the startup of a process
 * of the updater.Manager class will be denied. */
execute src=Einit, dst=updater.Manager, method=main {
    mic.execute { target : dst_sid
                , image : ()
                , level : "LOW"
                , levelR : "LOW"
                }
}

Page top

Mic security model upgrade rule

upgrade { source    : <Sid>
        , target    : <Sid>
        , container : <Sid | ()>
        , driver    : <Sid>
        , level     : <Level | ...>
        }

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 field has the value (), 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.

Page top

Mic security model call rule

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

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:

/* Any client in the solution is allowed to query
 * any server (kernel) if data streams from
 * the server (kernel) to the client are permitted by the
 * Mic security model. Otherwise any client in the solution
 * is prohibited from querying any server (kernel). */
request {
    mic.call { source : src_sid
             , target : dst_sid
             }
}

Page top

Mic security model invoke rule

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

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.

Page top

Mic security model read rule

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

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:

/* Any client in the solution is allowed to query a server of
 * the updater.Realmserv class by calling the read method of the
 * realm.Reader service if the Mic security model permits
 * this client to read data from the resource needed by
 * this client. Otherwise any client in the solution is prohibited from
 * querying a server of the updater.Realmserv class by calling
 * the read method of the realm.Reader endpoint. */
request dst=updater.Realmserv,
        endpoint=realm.Reader {
            match method=read {
                mic.read { source : src_sid
                         , target : message.handle.handle
                         }
               }
}

Page top

Mic security model write rule

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

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.

Page top

Mic security model query_level expression

query_level {source : <Sid>}

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.

Page top

Contents

KasperskyOS Security models

Pred security model

Bool security model

Math security model

Struct security model

Base security model

Regex security model

HashSet security model

HashSet security model object

HashSet security model init rule

HashSet security model fini rule

HashSet security model add rule

HashSet security model remove rule

HashSet security model contains expression

StaticMap security model

StaticMap security model object

StaticMap security model init rule

StaticMap security model fini rule

StaticMap security model set rule

StaticMap security model commit rule

StaticMap security model rollback rule

StaticMap security model get expression

StaticMap security model get_uncommitted expression

Flow security model

Flow security model object

Flow security model init rule

Flow security model fini rule

Flow security model enter rule

Flow security model allow rule

Flow security model query expression

Mic security model

Mic security model object

Mic security model create rule

Mic security model delete rule

Mic security model execute rule

Mic security model upgrade rule

Mic security model call rule

Mic security model invoke rule

Mic security model read rule

Mic security model write rule

Mic security model query_level expression