KasperskyOS Community Edition 1.2

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.
  3. The PSL language is case sensitive.
  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 declarations for the following purposes:

  • Setting the global parameters of a solution security policy
  • Including PSL files in a solution security policy description
  • Including EDL files in a solution security policy description
  • Create security model objects
  • Bind methods of security models to security events
  • Creating security audit profiles
  • Creating solution security policy tests

In this section

Setting the global parameters of a KasperskyOS-based solution security policy

Including PSL files in a KasperskyOS-based solution security policy description

Including EDL files in a KasperskyOS-based solution security policy description

Creating security model objects

Binding methods of security models to security events

Creating security audit profiles

Creating and performing tests for a KasperskyOS-based solution security policy

PSL data types

Examples of binding security model methods to security events

Example descriptions of basic security policies for KasperskyOS-based solutions

Examples of security audit profiles

Examples of tests for KasperskyOS-based solution security policies

Page top
[Topic ssp_descr_psl_syntax_intro]

Setting the global parameters of a KasperskyOS-based 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 a process by the kernel or by other processes. To define this interface, use the following declaration:
    execute: kl.core.Execute

    KasperskyOS currently supports only one execute interface (Execute) 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 run-time level. (For more details about profiles and the security audit run-time level, see "Creating security audit profiles".) To define these parameters, use the following declaration:
    audit default = <security audit profile name> <security audit runtime-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 runtime-level is 0. When the empty security audit profile is applied, a security audit is not conducted.

Page top
[Topic ssp_descr_psl_syntax_global_params]

Including PSL files in a KasperskyOS-based solution security policy description

To include a PSL file in a policy description, use the following declaration:

use <link to PSL file._>

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 the parameters -I <path to the directory> when starting the makekss script or the nk-psl-gen-c compiler.) A dot is used as a separator in a path description. A declaration is ended by the ._ character sequence.

Example:

use policy_parts.flow_part._

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 description of a security model

To use the methods of a required security model, the policy description must include a PSL file containing a formal description of this model. PSL files containing formal descriptions of security models are located in the KasperskyOS SDK at the following path:

toolchain/include/nk

Example:

/* Include the base.psl file containing a formal description of the * Base security model */ use nk.base._ /* Include the flow.psl file containing a formal description of the * Flow security model */ use nk.flow._ /* The nk-psl-gen-c compiler must be configured to search for * PSL, IDL, CDL, and EDL files in the toolchain/include directory. */
Page top
[Topic ssp_descr_psl_syntax_include_psl]

Including EDL files in a KasperskyOS-based solution security policy description

To include an EDL file for the KasperskyOS kernel in a policy description, use the following declaration:

use EDL kl.core.Core

To include an EDL file for a program (such as a driver or application) into a policy description, use the following declaration:

use EDL <link to EDL file>

The link to the EDL file is the EDL 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 the parameters -I <path to the directory> when starting the makekss script or the nk-psl-gen-c compiler.) A dot is used as a separator in a path description.

Example:

/* Include the UART.edl file, which is located * in the KasperskyOS SDK at the path sysroot-*-kos/include/kl/drivers. */ use EDL kl.drivers.UART /* The nk-psl-gen-c compiler must be configured to search for * PSL, IDL, CDL, and EDL files in the sysroot-*-kos/include directory. */

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

Page top
[Topic ssp_descr_psl_syntax_include_edl]

Creating security model objects

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:

policy object <security model object name : security model name> { [security model object parameters] }

The security model object name must begin with a lowercase letter. 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 "KasperskyOS security models" section.

Page top
[Topic ssp_descr_psl_syntax_create_objects]

Binding methods of security models to security events

To create an attachment between methods of security models and a security event, use the following declaration:

<security event type> [security event selectors] { [security audit profile] <called security model methods> }

Security event type

To define the security event type, use the following specifiers:

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

When processes interact with the security module, they use a mechanism that is different from IPC. However, when describing a policy, queries sent by processes to the security module can be viewed as the transfer of IPC messages because processes actually transmit messages to the security module (the recipient is not indicated in these messages).

The IPC mechanism is not used to start processes. However, when the startup of a process is initiated, the kernel queries the security module and provides information about the initiator of the startup and the started process. For this reason, the policy description developer can consider the startup of a process to be analogous to sending an IPC message from the startup initiator to the started process. When the kernel is started, this is analogous to the kernel sending an IPC message to itself.

Security event selectors

Security event selectors let you clarify the description of the defined type of security event. You can use the following selectors:

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

Process classes, components, instances of components, interfaces, endpoints, 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.

The qualified name of the endpoint has the format <path to endpoint.endpoint name>. The path to the endpoint is a sequence of component instance names separated by dots. Among these component instances, each subsequent component instance is embedded into the previous one, and the last one provides the endpoint with the defined name.

For security events, specify the qualified name of the security interface method if you need to use the security interface defined in a CDL description. (If you need to use a security interface defined in an EDL description, it is not necessary to specify the qualified name of the method.) The qualified name of a security interface method is a construct in the format <path to security interface.method name>. The path to the security interface is a sequence of component instance names separated by dots. Among these component instances, each subsequent component instance is embedded into the previous one, and the last one supports the security interface that includes the method with the defined name.

If selectors are not specified, the participants of a security event may be any process and the kernel (except security events in which the kernel cannot participate).

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

There are restrictions on the use of selectors. The interface, component, and endpoint selectors cannot be used for security events of the execute type. The dst, component, 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 of the endpoint, interface, or component selectors or a combination of them. (The method, endpoint, interface and component selectors must be coordinated. In other words, the method, endpoint, interface, and component must be interconnected.) 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.

The type and selectors of a security event form the security event description. It is recommended to describe security events with maximum precision to allow only the required interactions between different processes and between processes and the kernel. If IPC messages of the same type are always verified when processing the defined event, the description of this event is maximally precise.

To ensure that IPC messages of the same type correspond to a security event description, one of the following conditions must be fulfilled for this description:

  • For events of the request, response and error type, the "interface method-endpoint-server class or kernel" chain is unequivocally defined. For example, the security event description request dst=Server endpoint=net.Net method=Send corresponds to IPC messages of the same type, and the security event description request dst=Server corresponds to any IPC message sent to the Server.
  • For security events, the security interface method is specified.
  • The execute-interface method is indicated for execute events.

    There is currently support for only one fictitious method of the main execute-interface. This method is used by default, so it does not have to be defined through the method selector. This way, any description of an execute security event corresponds to IPC messages of the same type.

Security audit profile

To define a security audit profile, use the following construct:

audit <security audit profile name>

If a security audit profile is not defined, the global security audit profile is used.

Called security model methods

To call a security model method, use the following construct:

[security model object name.]<security model method name> <parameter>

Data of PSL-supported types can be used as the parameter. However, the following special considerations should be taken into account:

  • If a security model method does not actually have a parameter, this method formally has a Unit-type parameter designated as ().
  • If a security model method parameter is a dictionary {name of field 1 : value of field 1[, name of field 2 : value of field 2]...}, this parameter does not need to be enclosed in parentheses.
  • If the security model method parameter is not a dictionary and does not have the Unit type, this parameter must be enclosed in parentheses.

You can call one or more methods by using the same or different security model objects. Security model rules can use the parameter to receive values returned by expressions of security models.

When a security event is processed by the Kaspersky Security Module, expressions are called before rules. Therefore, expressions do not receive the changes made by rules. For example, if a declaration of attachment between StaticMap security model methods and security events first specifies the set rule and then specifies the get_uncommited expression for the same resource, the get_uncommited expression will return the key value that was defined before the current security event was processed instead of the key value that is defined by the set rule when processing the current security event. The key value defined by the set rule when processing the current security event can be returned by the get_uncommited expression only when processing subsequent security events if the security module returns the "allowed" decision as a result of processing the current security event. If the security module returns a "denied" decision as a result of processing the current security event, all changes made by rules and expressions invoked during processing of the current security event will be discarded.

A security model method (rule or expression) can use the parameter to receive the parameters of interface methods. (For details about obtaining access to parameters of interface methods, see "Struct security model"). A security model method can also use the parameter to receive the SID values of processes and the KasperskyOS kernel that are defined by the reserved words src_sid and dst_sid. The first reserved word refers to the SID of the process (or kernel) that is the source of the IPC message. The second reserved word refers to the SID of the process (or kernel) that is the recipient of the IPC message (dst_sid cannot be used for queries to the Kaspersky Security Module).

You do not have to indicate the security model object name to call certain security model methods. Also, some of the security model methods must be called using operators instead of the call construct. For details about the methods of security models, see KasperskyOS Security models.

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 <security event selectors> { [security audit profile] <called security model methods> }

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:

choice <call of the security model expression that verifies fulfillment of conditions> { "<condition 1>" : [{] // Conditional section 1 <called security model methods> [}] "<condition 2>" : ... // Conditional section 2 ... _ : ... // Conditional section, if no condition is fulfilled. }

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.

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 true condition on the list is triggered.

You can verify the fulfillment of conditions in the choice construct only by using the expressions that are specially intended for this purpose. Some security models contain these expressions (for more details, see KasperskyOS Security models).

Only text and integer literals, logical values and the _ character designating an always true condition can be used as conditions.

Examples of binding security model methods to security events

See "Examples of binding security model methods to security events", "Example descriptions of basic security policies for KasperskyOS-based solutions", and "KasperskyOS security models".

Page top
[Topic ssp_descr_psl_syntax_binding]

Creating security audit profiles

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 data and forwards it to the system program KlogStorage (data is transmitted via IPC). The latter sends the received audit data to standard output (or standard error) or writes 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. Data on calls of security model expressions is included in the audit data just like data on calls of security model rules.

To perform a security audit, you need to associate security model objects with 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 security model objects covered by the audit, and specifies the conditions for conducting the audit. You can define a global audit profile (for more details, see "Setting the global parameters of a KasperskyOS-based solution security policy") and/or assign an audit profile(s) at the level of binding security model methods to security events, and/or assign an audit profile(s) at the level of match sections (for more details, see "Binding methods of security models to security events").

Regardless of whether or not audit profiles are being used, audit data contains information about "denied" decisions that were made by the Kaspersky Security Module when IPC messages were invalid and when handling security events that are not associated with any security model rule.

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

audit profile <security audit profile name> = { <security audit runtime-level> : // Security audit configuration { <security model object name> : { kss: <security audit conditions linked to the results from calls of security model methods> [, security audit conditions specific to the security model] } [ ,...] } [ ,...] }

Security audit runtime-level

The security audit runtime-level (hereinafter referred to as the audit runtime-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 "runtime-level" here refers to the configuration variant and does not necessarily involve a hierarchy.) The audit runtime-level can be changed during operation of the Kaspersky Security Module. To do so, use a specialized method of the Base security model that is called when processes query the security module through the security interface (for more details, see "Base security model"). The initial audit runtime-level is assigned together with the global audit profile (for more details, see "Setting the global parameters of a KasperskyOS-based 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 conditions for conducting the audit can be applied. Audit configurations in a profile correspond to different audit runtime-levels. If a profile does not have an audit configuration corresponding to the current audit runtime-level, the security module will activate the configuration that corresponds to the next-lowest audit runtime-level. If a profile does not have an audit configuration for an audit runtime-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).

The capability to change the audit runtime-level lets you regulate the level of detail of an audit, for example. The higher the audit runtime-level, the higher the level of detail. In other words, a higher audit runtime-level activates audit configurations in which more security model objects are covered by the audit and/or less restrictions are applied in the audit conditions. In addition, you can change the audit runtime-level to switch the audit from one set of logically connected security model objects to another set. For example, a low audit runtime-level activates audit configurations in which the audit covers security model objects related to drivers, a medium audit runtime-level activates audit configurations in which the audit covers security model objects related to the network subsystem, and a high audit runtime-level activates audit configurations in which the audit covers security model objects related to applications.

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 conditions for conducting the audit are observed.

Information about the decisions of the Kaspersky Security Module contained in audit data includes the overall decision of the security module as well as the results from calling individual methods of security modules covered by the audit. To ensure that information about a security module decision is included in audit data, at least one method called during security event handling must be covered by the audit.

The names of security model objects and the names of methods provided by these objects are included in the audit data.

Security audit conditions

Security audit conditions must be defined separately for each object of a security model.

To define the audit conditions related to the results from calling security model methods, use the following constructs:

  • ["granted"] – the audit is performed if the rules return the "granted" result; the expressions are correctly executed.
  • ["denied"] – the audit is performed if the rules return the "denied" result; the expressions are incorrectly executed.
  • ["granted", "denied"] – the audit is performed regardless of the result returned by rules, and regardless of whether or not rules are correctly fulfilled.
  • [] – the audit is not performed.

Audit conditions specific to security models are defined by constructs specific to these models (for more details, see KasperskyOS Security models). These conditions apply to rules and 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 processes, which are connected by IPC channels based on the "kernel – Klog – KlogStorage" scheme. 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 binding security model methods to a security event), assign an empty audit profile at the level of binding security model methods to security events or at the level of the match section.

Examples of security audit profiles

See "Examples of security audit profiles".

See also:

Using the system programs Klog and KlogStorage to perform a security audit

Page top
[Topic ssp_descr_psl_syntax_audit]

Creating and performing tests for a KasperskyOS-based solution security policy

A solution security policy is tested to verify whether or not the policy actually allows what should be allowed and denies what should be denied.

To create a set of tests for a solution security policy, use the following declaration:

assert ["name of test set"] { // Constructs in PAL (Policy Assertion Language) [setup {<initial part of tests>}] sequence ["test name"] {<main part of test>} [...] [finally {<final part of tests>}] }

You can create multiple sets of tests by using several of these declarations.

A set of tests can optionally include the initial part of the tests and/or the final part of the tests. The execution of each test from the set begins with whatever is described in the initial part of the test and ends with whatever is described in the final part of the test. This lets you describe the repeated initial and/or final parts of tests in each test.

After completing each test, all modifications in the Kaspersky Security Module related to the execution of this test are rolled back.

Each test includes one or more test cases.

Test cases

A test case associates a security event description and values of interface method parameters with an expected decision of the Kaspersky Security Module. If the actual security module decision matches the expected decision, the test case passes. Otherwise it fails.

When a test is run, the test cases are executed in the same sequence in which they are described. In other words, the test demonstrates how the security module handles a sequence of security events.

If all test cases within a test pass, the test passes. If even one test case fails to pass, the test fails. A test is terminated on the first failing test case. Each test from the set is run regardless of whether the previous test passed or failed.

A test case description in the PAL language is comprised of the following construct:

[<expected decision of security module> ["test case name"]] <security event type> <security event selectors> [{interface method parameter values}]

The expected decision of the security module can be indicated as grant ("granted"), deny ("denied") or any ("any decision"). You are not required to indicate the expected decision of the security module. The "granted" decision is expected by default. If the any value is specified, the security module decision does not have any influence on whether or not the test case passes. In this case, the test case may fail due to errors that occur when the security module processes an IPC message (for example, when the IPC message has an invalid structure).

The name of the test case can be specified if only the expected decision of the security module is specified.

For information about the types and selectors of security events, and about the limitations when using selectors, see Binding methods of security models to security events. Selectors must ensure that the security event description corresponds to IPC messages of the same type. (When security model methods are bound to security events, selectors may not ensure this.)

In security event descriptions, you need to specify the SID instead of the process class name (and the KasperskyOS kernel). However, this requirement does not apply to execute events for which the SID of the started process (or kernel) is unknown. To save the SID of the process or kernel to a variable, you need to use the <- operator in the test case description in the following format:

<variable name> <- execute dst=<kernel/process class name> ...

The SID value will be assigned to the variable even if startup of the process of the defined class (or kernel) is denied by the tested policy but the "denied" decision is expected.

The PAL language supports abbreviated forms of security event descriptions:

  • security: <Process SID> ! <qualified name of security interface method> corresponds to security src=<process SID> method=<qualified name of security interface method>.
  • request: <client SID> ~> <kernel/server SID> : <qualified name of endpoint.method name> corresponds to request src=<client SID> dst=<kernel/server SID> endpoint=<qualified name of endpoint> method=<method name>.
  • response: <client SID> <~ <kernel/server SID> : <qualified name of endpoint.method name> corresponds to response src=<kernel/server SID> dst=<client SID> endpoint=<qualified name of endpoint> method=<method name>.

The values of interface method parameters must be defined for all types of security events except execute. If the interface method has no parameters, specify {}. You cannot specify {} for security events of the execute type.

Interface method parameters and their values must be defined by comma-separated constructs that look as follows:

<parameter name> : <value>

The names and types of parameters must comply with the IDL description. The sequence order of parameters is not important.

Example definition of parameter values:

{ param1 : 23, param2 : "bar", param3 : { collection : [5,7,12], filehandle : 15 }, param4 : { name : ["foo", "baz" } }

In this example, the number is passed through the param1 parameter. The string buffer is passed through the param2 parameter. A structure consisting of two fields is passed through the param3 parameter. The collection field contains an array or sequence of three numeric elements. The filehandle field contains the SID. A union or structure containing one field is passed through the param4 parameter. The name field contains an array or sequence of two string buffers.

Currently, only an SID can be indicated as the value of a Handle parameter, and there is no capability to indicate the SID together with a handle permissions mask. For this reason, it is not possible to properly test a solution security policy when the permissions masks of handles influence the security module decisions.

The values of parameters (or elements of parameters) do not have to be specified. If they are not specified, the system automatically applies the default values corresponding to the IDL types of parameters (and elements of parameters):

  • The default values for numerical types and the Handle type are zero.
  • A zero-sized byte- or string buffer is the default value for byte- or string buffers.
  • The default value for sequences is a sequence with zero elements.
  • The default value for arrays is an array of elements with the default values.
  • The default value for structures is a structure consisting of fields with the default values.
  • For unions, the default value of the first member of the union is applied by default.

Example of applying the default value for a parameter and parameter element:

/* Parameter is specified. */ request src=x dst=y endpoint=e method=m { name : { firstname: "a", lastname: "b" } } /* Parameter is not specified. The applied value of the name parameter will be a structure * consisting of two zero-sized string buffers.*/ request src=x dst=y endpoint=e method=m {} /* Parameter element is not specified. The applied value of the lastname parameter element will be * a zero-sized string buffer.*/ request src=x dst=y endpoint=e method=m { name : { firstname: "a"} }

Example tests

See "Examples of tests for KasperskyOS-based solution security policies".

Test procedure

The test procedure includes the following steps:

  1. Save the tests in one or multiple PSL files (*.psl or *.psl.in).
  2. Add the CMake command add_kss_pal_qemu_tests() to one of the CMakeLists.txt files of the project.

    Use the PSL_FILES parameter to define the paths to PSL files containing tests. Use the DEPENDS parameter to define the CMake targets whose execution will cause the PSL file-dependent IDL, CDL, and EDL files to be put into the directories where the nk-psl-gen-c compiler can find them. If *.psl.in files are utilized, use the ENTITIES parameter to define the names of process classes of system programs. (These system programs are included in a KasperskyOS-based solution that requires security policy testing.)

    Example use of the CMake command add_kss_pal_qemu_tests() in the file einit/CMakeLists.txt:

    add_kss_pal_qemu_tests ( PSL_FILES src/security.psl.in DEPENDS kos-qemu-image ENTITIES ${ENTITIES})
  3. Build and run the tests.

    You must run the Bash build script cross-build.sh with the parameter --target pal-test<N> (N is the index of the PSL file in the list of PSL files defined through the PSL_FILES parameter of the CMake command add_kss_pal_qemu_tests() at step 2. For example, --target pal-test0 will create a KasperskyOS-based solution image corresponding to the first PSL file defined through the PSL_FILES parameter of the CMake command add_kss_pal_qemu_tests() and then run that image in QEMU. (Instead of applications and system programs, this solution will contain the program that runs tests.)

    Example:

    ./cross-build.sh --target pal-test0

Example test results:

[==========] Running 4 tests from 1 test suite. [----------] Global test environment set-up. [----------] 4 tests from KSS [ RUN ] KSS.KssUnitTest_flow_normal [ OK ] KSS.KssUnitTest_flow_normal (6 ms) [ RUN ] KSS.KssUnitTest_flow_ping_must_be_first /home/work/build/stat/build/install/examples/ping/build/einit/ pal-test/gen_security.psl.test.c:9742: Failure Expected equality of these values: rc Which is: -1 NK_EOK Which is: 0 gen_security.psl:116: expect grant [ FAILED ] KSS.KssUnitTest_flow_ping_must_be_first (8 ms) [ RUN ] KSS.KssUnitTest_flow_ping_ping_is_deny [ OK ] KSS.KssUnitTest_flow_ping_ping_is_deny (4 ms) [ RUN ] KSS.KssUnitTest_flow_test_deny [ OK ] KSS.KssUnitTest_flow_test_deny (1 ms) [----------] 4 tests from KSS (29 ms total) [----------] Global test environment tear-down [==========] 4 tests from 1 test suite ran. (42 ms total) [ PASSED ] 3 tests. [ FAILED ] KSS.KssUnitTest_flow_ping_must_be_first (8 ms)

The test results contain information about whether or not each test passed or failed. If a test failed, information indicating the location of the description of the failed test example will be displayed in the PSL file.

Page top
[Topic ssp_descr_psl_syntax_testing]

PSL data types

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

PSL data types

Designations of types

Description of types

UInt8, UInt16, UInt32, UInt64

Unsigned integer

SInt8, SInt16, SInt32, SInt64

Signed integer

Boolean

Boolean type

The Boolean type includes two values: true and false.

Text

Text type

()

Unit type

The Unit type includes one immutable value. It is used as a stub value in cases when PSL language syntax requires certain data formulation but this data is not actually required. For example, the Unit type can be used to declare a method that does not have any parameters (similar to how the void type is used in C/C++).

"[type]"

Text literal

A text literal includes one immutable text value.

Example definitions of text literals:

""

"granted"

<type>

Integer literal

An integer literal includes one immutable integer value.

Example definitions of integer literals:

12

-5

0xFFFF

<type 1 | type 2> [| ...]

Variant type

A variant type combines two or more types and may perform the role of either of them.

Examples of definitions of variant types:

Boolean | ()

UInt8 | UInt16 | UInt32 | UInt64

"granted" | "denied"

{ [field name : field type]

[, ...]

}

Dictionary

A dictionary consists of one or more types of fields. A dictionary can be empty.

Examples of dictionary definitions:

{}

{ handle : Handle

, rights : UInt32

}

[[type] [, ...]]

Tuple

A tuple consists of fields of one or more types in the order in which the types are listed. A tuple can be empty.

Examples of tuple definitions:

[]

["granted"]

[Boolean, Boolean]

Set<<type of elements>>

Set

A set includes zero or more unique elements of the same type.

Examples of set definitions:

Set<"granted" | "denied">

Set<Text>

List<<type of elements>>

List

A list includes zero or more elements of the same type.

Examples of list definitions:

List<Boolean>

List<Text | ()>

Map<<key type, value type>>

Associative array

An associative array includes zero or more entries of the "key-value" type with unique keys.

Example of defining an associative array:

Map<UInt32, UInt32>

Array<<type of elements, number of elements>>

Array

An array includes a defined number of elements of the same type.

Example of defining an array:

Array<UInt8, 42>

Sequence<<type of elements, number of elements>>

Sequence

A sequence includes from zero to the defined number of elements of the same type.

Example of defining a sequence:

Sequence<SInt64, 58>

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

Type alias

Type definition

Unsigned

Unsigned integer

UInt8 | UInt16 | UInt32 | UInt64

Signed

Signed integer

SInt8 | SInt16 | SInt32 | SInt64

Number

Integer

Unsigned | Signed

ScalarLiteral

Scalar literal

() | Boolean | Number

Literal

Literal

ScalarLiteral | Text

Sid

Type of security ID (SID)

UInt32

Handle

Type of security ID (SID)

Sid

HandleDesc

Dictionary containing fields for the SID and handle permissions mask

{ handle : Handle

, rights : UInt32

}

Cases

Type of data received by expressions of security models called in the choice construct for verifying fulfillment of conditions

List<Text | ()>

KSSAudit

Type of data defining the conditions for conducting the security audit

Set<"granted" | "denied">

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 policy description developer needs to understand how 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.

Page top
[Topic ssp_descr_psl_syntax_data_types]

Examples of binding security model methods to security events

Before analyzing examples, you need to become familiar with the Base security model.

Processing the initiation of process startups

/* The KasperskyOS kernel and any process * in the solution is allowed to start any * process. */ execute { grant () } /* The kernel is allowed to start a process * of the Einit class. */ execute src=kl.core.Core, dst=Einit { grant () } /* An Einit-class process is allowed * to start any process in the solution. */ execute src=Einit { grant () }

Handling the startup of the KasperskyOS kernel

/* The KasperskyOS kernel is allowed to start. * (This binding is necessary so that the security * module can be notified of the kernel SID. The kernel starts irrespective * of whether this is allowed by the solution security policy * or denied. If the solution security policy denies the * startup of the kernel, after startup the kernel will terminate its * execution.) */ execute src=kl.core.Core, dst=kl.core.Core { grant () }

Handling IPC request forwarding

/* Any client in the solution is allowed to query * any server and the KasperskyOS kernel. */ request { grant () } /* A client of the Client class is allowed to query * any server in the solution and the kernel. */ request src=Client { grant () } /* Any client in the solution is allowed to query * a server of the Server class. */ request dst=Server { grant () } /* A client of the Client class is not allowed to * query a server of the Server class. */ request src=Client dst=Server { deny () } /* A client of the Client class is allowed to * query a server of the Server class * by calling the Ping method of the net.Net endpoint. */ request src=Client dst=Server endpoint=net.Net method=Ping { grant () } /* Any client in the solution is allowed to query * a server of the Server class by calling the Send method * of the endpoint with the MessExch interface. */ request dst=Server interface=MessExch method=Send { grant () }

Handling IPC response forwarding

/* A server of the Server class is allowed to respond to * queries of a Client-class client that * calls the Ping method of the net.Net endpoint. */ response src=Server, dst=Client, endpoint=net.Net, method=Ping { grant () } /* The server containing the kl.drivers.KIDF component * that provide endpoints with the monitor interface is allowed to * respond to queries of a DriverManager-class client * that uses these endpoints. */ response dst=DriverManager component=kl.drivers.KIDF interface=monitor { grant () }

Handling the transmission of IPC responses containing error information

/* A server of the Server class is not allowed to notify a client * of the Client class regarding errors that occur * when the client queries the server by calling the * Ping method of the net.Net endpoint. */ error src=Server, dst=Client, endpoint=net.Net, method=Ping { deny () }

Handling queries sent by processes to the Kaspersky Security Module

/* A process of the Sdcard class will receive the * "granted" decision from the Kaspersky Security Module /* by calling the Register method of the security interface. * (Using the security interface defined * in the EDL description.) */ security src=Sdcard, method=Register { grant () } /* A process of the Sdcard class will receive the "denied" decision * from the security module when calling the Comp.Register method * of the security interface. (Using the security interface * defined in the CDL description.) */ security src=Sdcard, method=Comp.Register { deny () }

Using match sections

/* A client of the Client class is allowed to query * a server of the Server class by calling the Send * and Receive methods of the net endpoint. */ request src=Client, dst=Server, endpoint=net { match method=Send { grant () } match method=Receive { grant () } } /* A client of the Client class is allowed to query * a server of the Server class by calling the Send * and Receive methods of the sn.Net endpoint and the Write and * Read methods of the sn.Storage endpoint. */ request src=Client, dst=Server { match endpoint=sn.Net { match method=Send { grant () } match method=Receive { grant () } } match endpoint=sn.Storage { match method=Write { grant () } match method=Read { grant () } } }

Setting audit profiles

/* Set the default global audit profile * and initial audit runtime-level of 0 */ audit default = global 0 request src=Client, dst=Server { /* Set the parent audit profile at the level of * binding methods of security models to * security events */ audit parent match endpoint=net.Net, method=Send { /* Set a child audit profile at the * match section level */ audit child grant () } /* This match section applies a * parent audit profile. */ match endpoint=net.Net, method=Receive { grant () } } /* This binding of the security model method * to the security event utilizes the * global audit profile. */ response src=Client, dst=Server { grant () }
Page top
[Topic ssp_descr_psl_syntax_binding_examples]

Example descriptions of basic security policies for KasperskyOS-based solutions

Before analyzing examples, you need to become familiar with the Struct, Base and Flow security models.

Example 1

The solution security policy in this example allows any interaction between different processes of the Client, Server and Einit classes, and between these processes and the KasperskyOS kernel. The "granted" decision will always be received when these processes query the Kaspersky Security Module. This policy can be used only as a stub during the early stages of development of a KasperskyOS-based solution so that the Kaspersky Security Module does not interfere with interactions. It would be unacceptable to apply such a policy in a real-world KasperskyOS-based solution.

security.psl

execute: kl.core.Execute use nk.base._ use EDL Einit use EDL Client use EDL Server use EDL kl.core.Core execute { grant () } request { grant () } response { grant () } error { grant () } security { grant () }

Example 2

The solution security policy in this example imposes limitations on queries sent from clients of the FsClient class to servers of the FsDriver class. When a client opens a resource controlled by a server of the FsDriver class, a finite-state machine in the unverified state is associated with this resource. A client of the FsClient class is allowed to read data from a resource controlled by a server of the FsDriver class only if the finite-state machine associated with this resource is in the verified state. To switch a resource-associated finite-state machine from the unverified state to the verified state, a process of the FsVerifier class needs to query the Kaspersky Security Module.

In a real-world KasperskyOS-based solution, this policy cannot be applied because it allows an excessive variety of interactions between different processes and between processes and the KasperskyOS kernel.

security.psl

execute: kl.core.Execute use nk.base._ use nk.flow._ use nk.basic._ policy object file_state : Flow { type States = "unverified" | "verified" config = { states : ["unverified" , "verified"], initial : "unverified", transitions : { "unverified" : ["verified"], "verified" : [] } } } execute { grant () } request { grant () } response { grant () } use EDL kl.core.Core use EDL Einit use EDL FsClient use EDL FsDriver use EDL FsVerifier response src=FsDriver, endpoint=operationsComp.operationsImpl, method=Open { file_state.init {sid: message.handle.handle} } request src=FsClient, dst=FsDriver, endpoint=operationsComp.operationsImpl, method=Read { file_state.allow {sid: message.handle.handle, states: ["verified"]} } security src=FsVerifier, method=Approve { file_state.enter {sid: message.handle.handle, state: "verified"} }
Page top
[Topic ssp_descr_psl_syntax_simpssp_examples]

Examples of security audit profiles

Before analyzing examples, you need to become familiar with the Base, Regex and Flow security models.

Example 1

// Describing a trace security audit profile // base – Base security model object // session – Flow security model object audit profile trace = /* If the audit runtime-level is equal to 0, the audit covers * base object rules when these rules return * the "denied" result. */ { 0 : { base : { kss : ["denied"] } } /* If the audit runtime-level is equal to 1, the audit covers methods * of the session object in the following cases: * 1. Rules of the session object return any result, and * the finite-state machine is in a state other than closed. * 2. A query expression of the session object is executed, and the * finite-state machine is in a state other than closed. */ , 1 : { session : { kss : ["granted", "denied"] , omit : ["closed"] } } /* If the audit runtime-level is equal to 2, the audit covers methods * of the session object in the following cases: * 1. Rules of the session object return any result. * 2. A query expression of the session object is executed. */ , 2 : { session : { kss : ["granted", "denied"] } } }

Example 2

// Describing a test security audit profile // base – Base security model object // re – Regex security model object audit profile test = /* If the audit runtime-level is equal to 0, rules of the base object * and expressions of the re object are not covered by the audit. */ { 0 : { base : { kss : [] } , re : { kss : [] , emit : [] } } /* If the audit runtime-level is equal to 1, rules of the * base object are not covered by the audit, and expressions of the * re object are covered by the audit.*/ , 1 : { base : { kss : [] } , re : { kss : ["granted"] , emit : ["match", "select"] } } /* If the audit runtime-level is equal to 2, rules of the base object * and expressions of the re object are covered by the audit. Rules * of the base object are covered by the audit irrespective of the * result that they return.*/ , 2 : { base : { kss : ["granted", "denied"] } , re : { kss : ["granted"] , emit : ["match", "select"] } } }
Page top
[Topic ssp_descr_psl_syntax_audit_profile_examples]

Examples of tests for KasperskyOS-based solution security policies

Example 1

/* Test set that includes only one test. */ assert "some tests" { /* Test that includes four test cases. */ sequence "first sequence" { /* It is expected that startup of a Server-class process is allowed. * If this is true, the s variable will be assigned the SID value * of the started Server-class process. */ s <- execute dst=Server /* It is expected that startup of a Client-class process is allowed. * If this is true, the c variable will be assigned the SID value * of the started Client-class process. */ c <- execute dst=Client /* It is expected that a client of the Client class is allowed to query * a server of the Server class by calling the Ping method of the pingComp.pingImpl endpoint * with the value parameter equal to 100. */ grant "Client calls Ping" request src=c dst=s endpoint=pingComp.pingImpl method=Ping { value : 100 } /* It is expected that a server of the Server class is not allowed to respond to a client * of the Client class if the client calls the Ping method of the pingComp.pingImpl endpoint. * (The IPC response does not contain any parameters because the Ping interface method * has no output parameters.) */ deny "Server cannot respond" response src=s dst=c endpoint=pingComp.pingImpl method=Ping {} } }

Example 2

/* Test set that includes two tests. */ assert "ping tests"{ /* Initial part of each of the two tests that includes two test cases. */ setup { /* It is expected that startup of a Server-class process is allowed. * If this is true, the s variable will be assigned the SID value * of the started Server-class process. */ s <- execute dst=Server /* It is expected that startup of a Client-class process is allowed. * If this is true, the c variable will be assigned the SID value * of the started Client-class process. */ c <- execute dst=Client } /* Test that includes four test cases: two test cases * in the initial part and two test cases in the main part.*/ sequence "ping-ping is denied" { /* It is expected that a client of the Client class is allowed to query * a server of the Server class by calling the Ping method of the pingComp.pingImpl endpoint * with the value parameter equal to 100. */ c ~> s : pingComp.pingImpl.Ping { value : 100 } /* It is expected that a client of the Client class is not allowed to query * a server of the Server class by once again calling the Ping method of the pingComp.pingImpl endpoint * with the value parameter equal to 100. */ deny c ~> s : pingComp.pingImpl.Ping { value : 100 } } /* Test that includes four test cases: two test cases * in the initial part and two test cases in the main part. */ sequence "ping-pong is granted" { /* It is expected that a client of the Client class is allowed to query * a server of the Server class by calling the Ping method of the pingComp.pingImpl endpoint * with the value parameter equal to 100. */ c ~> s : pingComp.pingImpl.Ping { value: 100 } /* It is expected that a client of the Client class is allowed to query * a server of the Server class by calling the Pong method of the pingComp.pingImpl endpoint * with the value parameter equal to 100. */ c ~> s : pingComp.pingImpl.Pong { value: 100 } } }

Example 3

/* Test set that includes only one test. */ assert { /* Test that includes eight test cases. */ sequence { storage <− execute dst=test.kl.UpdateStorage manager <− execute dst=test.kl.UpdateManager deployer <− execute dst=test.kl.UpdateDeployer downloader <− execute dst=test.kl.UpdateDownloader grant manager ~> downloader:UpdateDownloader.Downloader.LoadPackage { url : ”url012345678” } grant response src=downloader dst=manager endpoint=UpdateDownloader.Downloader method=LoadPackage { handle : 29, result : 1 } deny manager ~> deployer:UpdateDeployer.Deployer.Start { handle : 29 } deny request src=manager dst=deployer endpoint=UpdateDeployer.Deployer method=Start { handle : 29 } } }
Page top
[Topic ssp_descr_psl_syntax_testing_examples]