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 Singed type.
• abs <Singed> – "get module of number". Returns values of the Singed 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 "Managing access to resources").
• <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 completion 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 service 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 service. */

  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 level equal to the value passed via this parameter. It returns the "granted" result. (For more details about the security audit level, see "Describing security audit profiles".)

  Example:

  /* An entity 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 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. You can also define the audit completion 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 processing can be performed.

  Example:

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

  "^hello .*": grant ()

  ".*world$" : grant ()

  _ : deny ()

  }

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, an entity whose context includes a running 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 completion 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 resource that has the security ID sid. 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 resource.

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

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

Example:

HashSet security model fini rule

It deletes the association between the table and the resource that has the security ID sid (the table becomes free).

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

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

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

HashSet security model add rule

It adds the entry value to the table associated with the resource that has the security ID sid.

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

• The rule added the entry value to the table.
• The table already contains the entry value.

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

• The table is completely filled.
• The resource with the security ID sid is not associated with a table from the tables pool of the HashSet security model object being used.
• Security ID sid is out of the permissible range.

Example:

HashSet security model remove rule

It deletes the entry value from the table associated with the resource that has the security ID sid.

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

• The rule deleted the entry value from the table.
• The table does not have the entry value.

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

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

HashSet security model contains expression

It checks whether the entry value is in the table associated with the resource that has the security ID sid.

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

It runs incorrectly in the following cases:

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

If 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, an entity whose context includes a running 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 call 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 table and working table. 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 completion 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 resource that has the security ID sid. Keys are initialized by the default values.

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

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

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

Example:

StaticMap security model fini rule

It deletes the association between the table and the resource that has the security ID sid (the table becomes free).

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

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

• The resource with the security ID sid is not associated with a table from the tables pool of the StaticMap security model object being used.
• Security ID sid is out 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 resource that has the security ID sid.

It returns the "allowed" result if the specified value was assigned to the specified key. (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.
• The resource with the security ID sid is not associated with a table from the tables pool of the StaticMap security model object being used.
• Security ID sid is out 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 resource that has the security ID sid.

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

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

• The resource with the security ID sid is not associated with a table from the tables pool of the StaticMap security model object being used.
• Security ID sid is out 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 resource that has the security ID sid.

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

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

• The resource with the security ID sid is not associated with a table from the tables pool of the StaticMap security model object being used.
• Security ID sid is out 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 resource that has the security ID sid.

It returns a value of the Value type.

It runs incorrectly in the following cases:

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

If 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 resource that has the security ID sid.

It returns a value of the Value type.

It runs incorrectly in the following cases:

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

If 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, an entity can be associated with a finite-state machine to allow or prohibit this entity 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 completion 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 resource that has the security ID sid. The created finite-state machine has the configuration defined in the settings of the Flow security model object being used.

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

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

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

Example:

Flow security model fini rule

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

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

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

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

Flow security model enter rule

It switches the finite-state machine associated with the resource that has the security ID sid to the specified state.

It returns the "allowed" result if the finite-state machine 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.
• The resource with the security ID sid is not associated with a finite-state machine of the Flow security model object being used.
• Security ID sid is out of the permissible range.

Example:

Flow security model allow rule

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

It returns the "allowed" result if the state of the finite-state machine is in the set of defined states.

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

• The state of the finite-state machine is not in the set of defined states.
• The resource with the security ID sid is not associated with a finite-state machine of the Flow security model object being used.
• Security ID sid is out 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 resource that has the security ID sid. Depending on the results of this check, various options for security event processing can be performed.

It runs incorrectly in the following cases:

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

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

Example: