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.
Just like solution components, the KasperskyOS kernel also has a formal specification (for details, see "Methods of KasperskyOS core endpoints").
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.
The formal specification of a solution component does not define how this component will be implemented. In other words, the presence of components in a formal specification of a solution component does not mean that these components will be present in the architecture of this solution component.
