Part 3. Solution security policy

Preceding parts of the Guide show how to implement interaction between entities. For simplicity, all solutions were built without a security module (ksm.module), which is provided by Kaspersky Security System.

Kaspersky Security System is the subsystem that monitors queries sent between entities and other events. This means that you can divide a solution into entities, manage their interactions, and thereby enhance the security of the solution.

This part of the Guide illustrates the following:

• PSL language syntax
• Security models supported in Kaspersky Security System
• Example of a solution security policy

General information about a solution security policy description

In simplified terms, a solution security policy description consists of bindings that associate descriptions of security events with calls of methods provided by objects of security models. A security model object is an instance of a class whose definition is a formal representation of the security model (in a PSL file). Formal representations of security models contain signatures of methods of security models that determine the permissibility of interactions between different entities and between entities and the KasperskyOS kernel. These methods are divided into two types:

• Rules of security models are methods of security models that return a "granted" or "denied" result. Security model rules can change security contexts (for information about a security context, see "Managing access to resources").
• Expressions of security models are methods of security models that return values that can be used as input data for other methods of security models.

A security model object provides methods that are specific to one security model and stores the parameters used by these methods (for example, the initial state of a finite-state machine or the size of a container for specific data). The same object can be applied for multiple resources. However, this object will independently use the security contexts of these resources. Likewise, multiple objects of one or more security models can be applied for the same resource. In this case, different objects will use the security context of the same resource without any reciprocal influence.

Security events serve as signals indicating the initiation of interaction between different entities and between entities and the KasperskyOS kernel. Security events include the following events:

• Clients send IPC requests.
• Servers or the kernel send IPC responses.
• The kernel or entities initialize the startup of entities.
• The kernel starts.
• Entities query the Kaspersky Security Module via the security interface.

Security events are processed by the security module.

Security models

The KasperskyOS SDK provides PSL files that describe the following security models:

• Base – methods that implement basic logic.
• Pred – methods that implement comparison operations.
• Bool – methods that implement logical operations.
• Math – methods that implement integer arithmetic operations.
• Struct – methods that provide access to structural data elements (for example, access to parameters of interface methods transmitted in IPC messages).
• Regex – methods for text data validation based on regular expressions.
• HashSet – methods for working with one-dimensional tables associated with resources.
• StaticMap – methods for working with two-dimensional "key–value" tables associated with resources.
• Flow – methods for working with finite-state machines associated with resources.

Security event processing by the Kaspersky Security Module

The Kaspersky Security Module calls all methods (rules and expressions) of security models related to an occurring security event. If all rules returned the "granted" result, the security module returns the "granted" decision. If even one rule returned the "denied" result, the security module returns the "denied" decision.

If even one method related to an occurring security event cannot be correctly performed, the security module returns the "denied" decision.

If no rule is related to an occurring security event, the security module returns the "denied" decision. In other words, all interactions between solution components and between those components and the KasperskyOS kernel are denied by default (Default Deny principle) unless those interactions are explicitly allowed by the solution security policy.

Security audit

A security audit (hereinafter also referred to as an audit) is the following sequence of actions. The Kaspersky Security Module notifies the KasperskyOS kernel about decisions made by this module. Then the kernel forwards this data to the system program Klog, which decodes this information and forwards it to the system program KlogStorage (data is transmitted via IPC). The latter prints the received data via standard output or saves it to a file.

Security audit data (hereinafter referred to as audit data) refers to information about decisions made by the Kaspersky Security Module, which includes the actual decisions ("granted" or "denied"), descriptions of security events, results from calling methods of security models, and data on incorrect IPC messages.

PSL language syntax

Basic rules

1. Declarations can be listed in any sequence in a file.
2. One declaration can be written to one or multiple lines. The second and subsequent lines of the declaration must be written with indentations relative to the first line. The closing brace that completes the declaration can be written on the top line.
3. A multi-line declaration utilizes different-sized indentations to reflect the nesting of constructs comprising this declaration. Lines of a multi-line construct enclosed in braces and the opening brace must be written with an indentation relative to the first line of this construct. The closing brace of a multi-line construct can be written with an indentation or on the first line of the construct.
4. Single-line comments and multi-line comments are supported:

   /* This is a comment

   And this, too */

   // Another comment

Types of declarations

The PSL language has the following types of declarations:

• Describing the global parameters of a solution security policy
• Including PSL files
• Including EDL files
• Creating objects of security models
• Binding methods of security models to security events
• Describing security audit profiles

Describing the global parameters of a solution security policy

Global parameters include the following parameters of a solution security policy:

• Execute interface used by the KasperskyOS kernel when querying the Kaspersky Security Module to notify it about kernel startup or about initiating the startup of entities by the kernel or other entities. To assign this interface, use the following declaration:

  execute: kl.core.Execute

  KasperskyOS currently supports only one Execute interface defined in the file named kl/core/Execute.idl. (This interface consists of one main method, which has no parameters and does not perform any actions. The main method is reserved for potential future use.)

• [Optional] Global security audit profile and initial security audit level. To define these parameters, use the following declaration:

  audit default = <security audit profile name> <security audit level>

  Example:

  audit default = global 0

  The default global profile is the empty security audit profile described in the file named toolchain/include/nk/base.psl from the KasperskyOS SDK, and the default security audit level is 0.

Including PSL files

To include a PSL file, use the following declaration:

The link to the PSL file is the file path (without the extension and dot before it) relative to the directory that is included in the set of directories where the nk-psl-gen-c compiler searches for PSL-, IDL-, CDL-, and EDL files. (This set of directories is defined by parameters of the makekss script in the format "-I <path to files>".) A dot is used as a separator in a path description. A declaration is ended by the ._ character sequence.

Example:

This declaration includes the flow_part.psl file, which is located in the policy_parts directory. The policy_parts directory must reside in one of the directories where the nk-psl-gen-c compiler searches for PSL-, IDL-, CDL-, and EDL files. For example, the policy_parts directory may reside in the same directory as the PSL file containing this declaration.

Including a PSL file containing a formal representation of a security model

To use the methods of a required security model, include a PSL file containing a formal representation of this model. PSL files containing formal representations of security models are located in the <KOS_KASPERSKY> SDK at the following path:

toolchain/include/nk

Example:

Including EDL files

To include an EDL file for the KasperskyOS kernel, use the following declaration:

To include an EDL file for an application or system program (or for a driver), use the following declaration:

The link to the EDL file is the file path (without the extension and dot before it) relative to the directory that is included in the set of directories where the nk-psl-gen-c compiler searches for PSL-, IDL-, CDL-, and EDL files. (This set of directories is defined by parameters of the makekss script in the format "-I <path to files>".) A dot is used as a separator in a path description.

Example:

The nk-psl-gen-c compiler finds IDL- and CDL files via EDL files because EDL files contain links to the corresponding CDL files, and the CDL files contain links to the corresponding CDL- and IDL files.

Creating objects of security models

To call the methods of a required security model, create an object for this security model.

To create a security model object, use the following declaration:

The parameters of a security model object are specific to the security model. A description of parameters and examples of creating objects of various security models are provided in the "Security models" section.

Binding methods of security models to security events

To bind methods of security models to a security event, use the following declaration:

Security event type

The following specifiers are used to define the security event type:

• request – sending IPC requests.
• response –sending IPC responses.
• error – sending IPC responses containing information about errors.
• security – entities attempting to query the Kaspersky Security Module via the security interface.
• execute – initializing the startups of entities or the startup of the KasperskyOS kernel.

Security event selectors

Security event selectors let you clarify the description of the defined type of security event. The following selectors are used:

• src=<kernel/entity class name> – entities of the defined class or the KasperskyOS kernel are the sources of IPC messages.
• dst=<kernel/entity class name> – entities of the defined class or the kernel are the recipients of IPC messages.
• interface=<interface name> – describes the following security events:
  • Clients attempt to query servers or the kernel via the interface with the defined name.
  • Entities query the Kaspersky Security Module via the security interface with the defined name.
  • The kernel or servers send clients the results from processing queries via the interface with the defined name.
• endpoint=<qualified service name> – describes the following security events:
  • Clients attempt to use the service of servers or the kernel with the defined name.
  • The kernel or servers send clients the results from using the service with the defined name.
• method=<method name> – describes the following security events:
  • Clients attempt to query servers or the kernel by calling the method of the service with the defined name.
  • Entities query the security module by calling the method of the security interface with the defined name.
  • The kernel or servers send clients the results from calling the method of the service with the defined name.
  • The kernel notifies the security module about its startup by calling the method of the execute interface with the defined name.
  • The kernel initiates the startup of entities by calling the method of the execute interface with the defined name.
  • Entities initiate the startup of other entities, which results in the kernel calling the method of the execute interface with the defined name.

Entity classes, interfaces, services, and methods must be named the same as they are in the IDL, CDL, and EDL descriptions. The kernel must be named kl.core.Core.

If selectors are not specified, the participants of a security event are considered to be all events and the kernel (except security events in which the kernel is not involved).

You can use combinations of selectors. Selectors can be separated by commas.

There are restrictions on the use of selectors. The interface and endpoint selectors cannot be used for security events of the execute type. The dst and endpoint selectors cannot be used for security events of the security type.

There are also restrictions on combinations of selectors. For security events of the request, response and error types, the method selector can only be used together with one or both of the endpoint and interface selectors. (The method, endpoint and interface selectors must be consistent, which means that the method must correspond to the service or interface, and the service must correspond to the interface.) For security events of the request type, the endpoint selector can be used only together with the dst selector. For security events of the response and error types, the endpoint selector can be used only together with the src selector.

Security audit profile

A security audit profile is defined by the construct audit <security audit profile name>. If a security audit profile is not defined, the global security audit profile is used.

Called rules of security models

Called rules of security models are defined by a list from the following type of constructs:

Input data for security model rules may be values returned by expressions of security models. The following construct is used to call a security model expression:

Parameters of interface methods can also be used as input data for methods of security models (rules and expressions). (For details about obtaining access to parameters of interface methods, see "Struct security model"). In addition, input data for methods of security models can also be the SID values of entities and the KasperskyOS kernel that are defined by the src_sid and dst_sid reserved words. The first reserved word refers to the SID of the entity (or kernel) that is the source of the IPC message. The second reserved word refers to the SID of the entity (or kernel) that is the recipient of the IPC message (dst_sid cannot be used for queries to the Kaspersky Security Module).

Embedded constructs for binding methods of security models to security events

In one declaration, you can bind methods of security models to different security events of the same type. To do so, use the match sections that consist of the following types of constructs:

Match sections can be embedded into another match section. A match section simultaneously uses its own security event selectors and the security event selectors at the level of the declaration and all match sections in which this match section is "wrapped". By default, a match section applies the security audit profile of its own container (match section of the preceding level or the declaration level), but you can define a separate security audit profile for the match section.

In one declaration, you can define different variants for processing a security event depending on the conditions in which this event occurred (for example, depending on the state of the finite-state machine associated with the resource). To do so, use the conditional sections that are elements of the following construct:

The choice construct can be used within a match section. A conditional section uses the security event selectors and security audit profile of its own container, but you can define a separate security audit profile for a conditional section.

If multiple conditions described in the choice construct are simultaneously fulfilled when a security event is processed, only the one conditional section corresponding to the first matching condition on the list is triggered.

Page top

Describing security audit profiles

To perform a security audit, you need to associate objects of security models with a security audit profile(s). A security audit profile (hereinafter also referred to as an audit profile) combines security audit configurations (hereinafter also referred to as audit configurations), each of which defines the objects of security models covered by the audit, and the audit completion conditions. You can define a global audit profile (for more details, see "Describing the global parameters of a solution security policy") and/or assign an audit profile(s) at the level of declarations for binding security model methods to security events, and/or assign an audit profile(s) at the level of match sections or choice sections (for more details, see "Binding methods of security models to security events").

To describe a security audit profile, use the following declaration:

Security audit level

The security audit level (hereinafter referred to as the audit level) is a global parameter of a solution security policy and consists of an unsigned integer that defines the active security audit configuration. (The word "level" here refers to the configuration variant and does not necessarily involve a hierarchy.) The audit level can be changed during operation of the Kaspersky Security Module. This is done by using a specialized method of the Base security model that is called when entities query the security module via the security interface (for more details, see "Base security model"). The initial audit level is assigned together with the global audit profile (for more details, see "Describing the global parameters of a solution security policy"). An empty audit profile can be explicitly assigned as the global audit profile.

You can define multiple audit configurations in an audit profile. In different configurations, different security model objects can be covered by the audit and different audit completion conditions can be applied. Audit configurations in a profile correspond to different audit levels. If a profile does not have an audit configuration corresponding to the current audit level, the security module will activate the configuration that corresponds to the next-lowest audit level. If a profile does not have an audit configuration for an audit level equal to or less than the current level, the security module will not use this profile (in other words, an audit will not be performed for this profile).

Audit levels can be used to regulate the level of detail of an audit, for example. The higher the audit level, the higher the level of detail. The higher the level of detail, the more security model objects are covered by the audit and/or the less restrictions are applied in the audit completion conditions.

Another example of applying audit levels is the capability to shift the audit from one subsystem to another subsystem (for example, shift an audit related to drivers to an audit related to applications, or shift an audit related to the network subsystem to an audit related to the graphic subsystem).

Name of the security model object

The security model object name is indicated so that the methods provided by this object can be covered by the audit. These methods will be covered by the audit whenever they are called, provided that the audit completion conditions are observed.

Security audit completion conditions

Security audit completion conditions are defined separately for each object of a security model.

To define audit completion conditions related to the results from calling rules of security models, use the following constructs:

• ["granted"] – the audit is performed if the called rule returned the "granted" result.
• ["denied"] – the audit is performed if the called rule returned the "denied" result.
• ["granted", "denied"] – the audit is performed if the called rule returned the "granted" or "denied" result.
• [] – the audit is not performed, regardless of the result returned by the called rule.

Audit completion conditions related to results from calling rules are not applied to expressions. These conditions must be defined (with any possible construct) even if the security model contains only expressions because this is required by the PSL language syntax.

Audit completion conditions specific to security models are defined by constructs specific to these models. These conditions are applied to rules and to expressions. For example, one of these conditions can be the state of a finite-state machine.

Security audit profile for a security audit route

A security audit route includes the kernel and the Klog and KlogStorage entities, which are connected by IPC channels based on the "kernel – Klog – KlogStorage" scenario. Security model methods that are associated with transmission of audit data via this route must not be covered by the audit. Otherwise, this will lead to an avalanche of audit data because any data transmission will give rise to new data.

To "suppress" an audit that was defined by a profile with a wider scope (for example, by a global profile or a profile at the level of a declaration for binding security model methods to security events), assign an empty audit profile at the level of the declaration for binding security model methods to security events or at the level of the match section or choice section.

Page top

PSL data types

The data types supported in the PSL language are presented in the table below.

PSL data types

Aliases of certain PSL types

The nk/base.psl file from the KasperskyOS SDK defines the data types that are used as the types of parameters (or structural elements of parameters) and returned values for methods of various security models. Aliases and definitions of these types are presented in the table below.

Aliases and definitions of certain data types in PSL

Mapping IDL types to PSL types

Data types of the IDL language are used to describe the parameters of interface methods. The input data for security model methods have types from the PSL language. The set of data types in the IDL language differs from the set of data types in the PSL language. Parameters of interface methods transmitted in IPC messages can be used as input data for methods of security models, so the author of a solution security policy needs to understand which IDL types are mapped to PSL types.

Integer types of IDL are mapped to integer types of PSL and to variant types of PSL that combine these integer types (including with other types). For example, signed integer types of IDL are mapped to the Signed type in PSL, and integer types of IDL are mapped to the ScalarLiteral type in PSL.

The Handle type in IDL is mapped to the HandleDesc type in PSL.

Unions and structures of IDL are mapped to PSL dictionaries.

Arrays and sequences of IDL are mapped to arrays and sequences of PSL, respectively.

String buffers in IDL are mapped to the text type in PSL.

Byte buffers in IDL are not currently mapped to PSL types, so the data contained in byte buffers cannot be used as inputs for security model methods.

Example of a basic solution security policy

Below is a basic solution security policy in which "everything is allowed" for a solution consisting of Client and Server user entities, an Einit entity, and the KasperskyOS kernel provided by the kl.core.Core entity.

This policy allows the following:

• All interactions between entities (sending any requests and responses)
• Startup of all entities

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:

ping example

The ping example demonstrates the use of a solution security policy to control interactions between entities.

About the ping example

The ping example includes two entities: Client and Server.

The Server entity provides two identical Ping and Pong methods that receive a number and return a modified number:

The Client entity calls both of these methods in a different sequence. If the method call is denied by the solution security policy, the Failed to call... message is displayed.

The ping example implements a solution security policy (security.psl) based on the Flow security model.

Components of the ping example

The ping example consists of the following files:

• client/src/client.c
• resources/edl/Client.edl
• server/src/server.c
• resources/edl/Server.edl, resources/cdl/Control.cdl, resources/idl/Connection.idl
• init.yaml
• security.psl

Implementation of the Client entity in the ping example

The Client entity calls the Ping and Pong methods in a varying sequence.

Implementation of the Server entity in the ping example

Description files in the ping example

Description of the Client entity

The Client entity does not implement an interface, so all you need to do is declare the entity name in the EDL description.

Server entity description

The Server entity implements a Connection interface, which contains two methods: Ping and Pong. As in the echo example, you must declare a separate component, such as Control, which contains a Connection interface implementation.

In the EDL description of the Server entity, you must indicate that it contains an instance of the Control component:

In the CDL description of the Control component, you must indicate that it contains a Connection interface implementation:

In the Connection package, you must declare the Connection interface, which contains two methods: Ping and Pong:

Init description

To enable the Client entity to call a Server entity method, an IPC channel must be created between them.

Solution security policy in the ping example

The solution security policy in this example allows you to start all entities, and allows any entity to query the Core and Server entities. Calls to the Server entity are managed by methods of the Flow security model.

The finite-state machine described in the configuration of the request_state Flow security model object has two states: ping_next and pong_next. The initial state is ping_next. Only transitions from ping_next to pong_next and the reverse are allowed.

When the Ping and Pong methods are called, the current state of the request_state object is checked. In the ping_next state, only a Ping call is allowed, in which case the state changes to pong_next. Likewise, in the pong_next state, only a Pong call is allowed, in which case the state changes to ping_next.

Therefore, the Ping and Pong methods can be called only in succession.

Building and running the ping example

See the Building and running examples section.

Testing a solution security policy based on the Policy Assertion Language (PAL)

The basic scenario for using the Policy Assertion Language (PAL) is to create test scenarios for checking solution security policies written in PSL.

The PAL language lets you generate and send requests to the security module and verify that the received decisions comply with the expected decisions. To run test scenarios written in PAL, you do not need to generate code of client-server interactions because PAL operates at the level of abstraction of the security module.

General syntax

A test scenario is a sequence of requests to the security module, with an expected decision indicated for each of these requests.

Test scenarios can be combined into groups. A group of scenarios may also contain the setup and finally sections, which will be executed before and after the execution of each scenario in this group, respectively. This can be used to define common start conditions or to check common invariants.

The modular assert declaration is used to declare a group of test scenarios:

Syntax of requests

To configure requests within test scenarios, the following types of declarations are used:

In this case:

• <expectation> – expected decision: grant, deny or any.

  When expecting the any decision, the decision of the security module is ignored, but an error when completing the request will mark the test scenario as unsuccessful.

  When the expected decision is not explicitly indicated, the grant decision is expected.

• <title> – optional parameter containing a text header of the described request.
• <operation> – one of the types of queries to the security module: execute, security, request or response.
• <event selectors> – the permissible selectors of an event coincide with the selectors used when binding methods of security models to security events. For example, you can indicate the message recipient entity or the called method.
• {message} – optional parameter containing the value for arguments of the called method. The value of this parameter must match the operation and selectors of the request. An empty number of arguments {} is used by default.

Example:

Abbreviated format of requests

For convenience, you can also use the following abbreviated formats of requests:

• When performing the execute operation, you can save the handle of the started entity to a variable by using the <- operator.
• Abbreviated format for the security operation: <entity> ! <path.to.method> {message}

  When executed, it is expanded to the full format: security src=<entity> method=<path.to.method> {message}

• Abbreviated format for the request operation: <client> ~> <server> : <path.to.method.implementation> {message}

  When executed, it is expanded to the full format: request src=<client> dst=<server> endpoint=<path.to.implementation> method=<method> {message}

• Abbreviated format for the response operation: <client> <~ <server> : <path.to.method.implementation> {message}

  When executed, it is expanded to the full format: response src=<server> dst=<client> endpoint=<path.to.implementation> method=<method> {message}

Example:

Running tests

To run test scenarios written in PAL, use the --tests run flag when starting the nk-psl-gen-c compiler:

The nk-psl-gen-c compiler generates code of the security module and code of test scenarios, uses gcc to compile them, and then runs them.

To generate code of test scenarios without compiling and running them, use the --tests generate flag.