Formal specifications of KasperskyOS-based solution components

Solution development includes the creation of formal specifications for its components that form a global picture for the Kaspersky Security Module. A formal specification of a KasperskyOS-based solution component (hereinafter referred to as the formal specification of the solution component) is comprised of a system of IDL, CDL and EDL descriptions (IDL and CDL descriptions are optional) for this component. These descriptions are used to automatically generate transport code of solution components, and source code of the security module and the initializing program. The formal specifications of solution components are also used as source data for the solution security policy description.

Each solution component corresponds to an EDL description. In terms of a formal specification, a solution component is a container for components that provide endpoints. Multiple instances of one solution component may be used at the same time, which means that multiple processes can be started from the same executable file. Processes that correspond to the same EDL description are processes of the same class. An EDL description defines the name of a process class and the components for which a process of the defined class serves as a container.

Each component that is part of a solution component corresponds to a CDL description. This description defines the component name, provided endpoints, security interface, and embedded components. Components can simultaneously provide endpoints, support a security interface, and serve as containers for other components. Each component can provide multiple endpoints with one or more interfaces.

Each interface is defined in an IDL description. This description defines the interface name, signatures of interface methods, and data types for the parameters of interface methods. The data comprising signatures of interface methods and definitions of data types for parameters of interface methods is referred to as a package.

Processes that do not contain components may only act as clients. Processes that contain components can act as servers and/or clients. If components from a process provide endpoints, the process can act as a server and a client at the same time. If components from a process do not provide endpoints (and only support a security interface), the process can act only as a client.

Names of process classes, components, packages and interfaces

Process classes, components, packages and interfaces are identified by their names in IDL, CDL and EDL descriptions. The names of process classes, components and packages form three sets of names within a KasperskyOS-based solution, in which any name is unique within its own set. A set of package names includes a set of interface names.

The name of a process class, component, package or interface is a link to the IDL, CDL or EDL file in which this name is defined. This link is a path to the IDL, CDL or EDL file (without the extension and dot before it) relative to the directory that is included in the set of directories where the source code generators search for IDL, CDL and EDL files. (This set of directories is defined by parameters -I <path to files>.) A dot is used as a separator in a path description.

For example, the kl.core.NameServer process class name is a link to the EDL file named NameServer.edl, which is located in the KasperskyOS SDK at the following path:

sysroot-*-kos/include/kl/core

However, source code generators must be configured to search for IDL, CDL and EDL files in the following directory:

sysroot-*-kos/include

EDL description

EDL descriptions are put into separate *.edl files, which contain the following data:

1. Process class name. The following declaration is used:

   entity <process class name>

2. [Optional] List of instances of components. The following declaration is used:

   components {

   <component instance name : component name>

   ...

   }

   Each component instance is indicated in a separate line. The component instance name must not contain any underscores _. The list can contain multiple instances of one component. Each component instance in the list has a unique name.

The EDL language is case sensitive.

Single-line comments and multi-line comments can be used in an EDL description.

Examples of EDL files

Hello.edl

Signald.edl

LIGHTCRAFT.edl

CDL description

CDL descriptions are put into separate *.cdl files, which contain the following data:

1. The name of the component. The following declaration is used:

   component <component name>

2. [Optional] Security interface. The following declaration is used:

   security <interface name>

3. [Optional] List of endpoints. The following declaration is used:

   endpoints {

   <endpoint name : interface name>

   ...

   }

   Each endpoint is indicated in a separate line. The endpoint name must not contain any underscores _. The list can contain multiple endpoints with the same interface. Each endpoint in the list has a unique name.

4. [Optional] List of instances of embedded components. The following declaration is used:

   components {

   <component instance name : component name>

   ...

   }

   Each component instance is indicated in a separate line. The component instance name must not contain any underscores _. The list can contain multiple instances of one component. Each component instance in the list has a unique name.

The CDL language is case sensitive.

Single-line comments and multi-line comments can be used in a CDL description.

Examples of CDL files

KscProductEventsProvider.cdl

KscConnectorComponent.cdl

FsVerifier.cdl

IDL description

IDL descriptions are put into separate *.idl files, which contain the following data:

1. Package name. The following declaration is used:

   package <package name>

2. [Optional] Packages from which the data types for interface method parameters are imported. The following declaration is used:

   import <package name>

3. [Optional] Definitions of data types for parameters of interface methods.
4. [Optional] Signatures of interface methods. The following declaration is used:

   interface {

   <interface method name([parameters])>;

   ...

   }

   Each method signature is indicated in a separate line. The method name must not contain any underscores _. Each method in the list has a unique name. The parameters of methods are divided into input parameters (in), output parameters (out), and parameters for transmitting error information (error).

   Input parameters and output parameters are transmitted in IPC requests and IPC responses, respectively. Error parameters are transmitted in IPC responses if the server cannot correctly handle the corresponding IPC requests.

   The server can inform a client about IPC request processing errors via error parameters as well as through output parameters of interface methods. If the server sets the error flag in an IPC response when an error occurs, this IPC response will contain the error parameters without any output parameters. Otherwise this IPC response will contain output parameters just like when requests are correctly processed. (The error flag is set in IPC responses by using the nk_err_reset() macro defined in the nk/types.h header file from the KasperskyOS SDK.)

   An IPC response sent with the error flag set and an IPC response with the error flag not set are considered to be different types of events for the Kaspersky Security Module. When describing a solution security policy, this difference lets you conveniently distinguish between the processing of events associated with the correct execution of IPC requests and the processing of events associated with incorrect execution of IPC requests. If the server does not set the error flag in IPC responses, the security module must check the values of output parameters indicating errors to properly process events related to the incorrect execution of IPC requests. (A client can check the state of the error flag in an IPC response even if the corresponding interface method does not contain error parameters. To do so, the client uses the nk_msg_check_err() macro defined in the nk/types.h header file from the KasperskyOS SDK.)

   Signatures of interface methods cannot be imported from other IDL files.

The IDL language is case sensitive.

Single-line comments and multi-line comments can be used in an IDL description.

Examples of IDL files

Env.idl

Kpm.idl

MessageBusSubs.idl

WaylandTypes.idl

IDL data types

Primitive types

IDL supports the following primitive types:

• SInt8, SInt16, SInt32, SInt64 (signed integer)
• UInt8, UInt16, UInt32, UInt64 (unsigned integer)
• Handle (value whose binary representation consists of multiple fields, including a handle field and a handle permissions mask field)
• bytes<<size in bytes>> (byte buffer)
• string<<size in bytes>> (string buffer)

A byte buffer is a memory area with a size that does not exceed the defined number of bytes. A string buffer is a byte buffer whose last byte is a terminating zero. The maximum size of a string buffer is a unit larger than the defined size due to the additional byte with the terminating zero. To transfer a byte buffer or string buffer via IPC, the amount of memory that is actually occupied by this buffer will be used.

For numeric types, you can declare named constants by using the reserved word const:

Constants are used to avoid problems associated with "magic numbers". For example, if an IDL description defines constants for return codes of an interface method, you can interpret these codes without additional information when describing a policy.

In addition to primitive types, the IDL language supports composite types, such as unions, structures, arrays and sequences. In a definition of composite types, constants of primitive types may be applied as parameters (for example, to assign an array size).

The bytes<<size in bytes>> and string<<size in bytes>> constructs are used in definitions of composite types, signatures of interface methods, and when creating type aliases because they define anonymous types (types without a name).

Unions

A union lets you store different types of data in one memory area. In an IPC message, a union is provided with an additional tag field that lets you define which specific member of the union is used.

The following construct is used to define a union:

Example of a union definition:

Structures

The following construct is used to define a structure:

Example of a structure definition:

Arrays

The following construct is used to define an array:

This construct is used in definitions of other composite types, signatures of interface methods, and when creating type aliases because it defines an anonymous type.

Sequences

A sequence is a variable-sized array. When defining a sequence, its maximum number of elements is specified. However, you can actually transmit less than this number (via IPC). In this case, only an amount of memory necessary for the transmitted elements will be used.

The following construct is used to define a sequence:

This construct is used in definitions of other composite types, signatures of interface methods, and when creating type aliases because it defines an anonymous type.

Types based on composite types

Composite types can be used to define other composite types. The definition of an array or sequence can also be included in the definition of another type:

The definition of a union or structure cannot be included in the definition of another type. However, a previously described definition of a union or structure can be included in a type definition. This is done by indicating the names of the included types in the type definition:

Creating aliases of types

Type aliases make it more convenient to work with types. For example, type aliases can be used to assign mnemonic names to types that have abstract names. Assigned aliases for anonymous types also let you receive named types.

The following construct is used to create a type alias:

Example of creating mnemonic aliases:

Example of creating an alias for an array definition:

Example of creating an alias for a sequence definition:

Example of creating an alias for a union definition:

Defining anonymous types in signatures of interface methods

Anonymous types can be defined in signatures of interface methods.

Example of defining a sequence in an interface method signature: