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 process class name and the top-level component parameters, such as the provided endpoints with one or multiple interfaces, the security interface, and embedded components.

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

Each interface (including the security 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 provide endpoints may only act as clients. Processes that provide endpoints are servers, but they can also act as clients at the same time.

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. Within one KasperskyOS-based solution, the names of process classes and the names of components form one set of names, while the names of packages form a different set of names. These two sets may overlap. 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 the directory>.) 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 placed into separate *.edl files and contain declarations in the Entity Definition Language (EDL):

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.

3. [Optional] Security interface. The following declaration is used:
   security <interface name>
4. [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.

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

Downloader.edl

CDL description

CDL descriptions are placed into individual *.cdl files and contain declarations in the Component Definition Language (CDL):

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 placed into separate *.idl files and contain declarations in the Interface Definition Language (IDL):

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). The order of parameters in the description is important: first input parameters, then output parameters, then error parameters. Methods of the security interface cannot have output parameters and error parameters.

   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

IDL supports primitive data types as well as composite data types. The set of supported composite types includes unions, structures, arrays, and sequences.

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 consisting of a memory area with a size that does not exceed the defined number of bytes.
• string<<size in bytes>> – string buffer consisting of 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.

Integer literals can be specified in decimal format, hexadecimal format (for example, 0x2f, 0X2f, 0x2F, 0X2F) or octal format (for example, 0O123, 0o123).

You can use the reserved word const to define the named integer constants by assigning their values using integer literals or integer expressions.

Example definitions of named integer constants:

Named integer constants can be used to avoid problems associated with so-called "magic numbers". For example, if an IDL description defines named integer constants for return codes of an interface method, you can interpret these codes without additional information when describing a policy. Named integer constants and integer expressions can also be applied in definitions of byte buffers, string buffers, and composite types to define the size of data or the number of data elements.

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 stores different types of data in one memory area. In an IPC message, a union is provided with an additional tag field that defines 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, the maximum number of elements of the sequence is specified.

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.

Variable-size and fixed-size types

The bytes, string and sequence types are variable-size types. In other words, the maximum number of elements is assigned when defining these types, but less elements (or none) may actually be used. Data of the bytes, string and sequence types are stored in the IPC message arena. All other types are fixed-size types. Data of fixed-size types are stored in the constant part of IPC messages.

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.

Example definition of a structure with embedded definitions of an array and sequence:

The definition of a union or structure cannot be included in the definition of another type. However, a type definition may include already defined unions and structures. This is done by indicating the names of the included types in the type definition.

Example definition of a structure that includes a union and structure:

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:

Integer expressions in IDL

Integer expressions in IDL are composed of named integer constants, integer literals, operators (see the table below), and grouping parentheses.

Example use of integer expressions:

If an integer overflow occurs when computing an expression, the source code generator using the IDL file will terminate with an error.

Details on operators of integer expressions in IDL