При разработке решения создаются формальные спецификации его компонентов, которые формируют "картину мира" для модуля безопасности Kaspersky Security Module. Формальная спецификация компонента решения на базе KasperskyOS (далее формальная спецификация компонента решения) представляет собой систему IDL-, CDL-, EDL-описаний (IDL- и CDL-описания опциональны) этого компонента. Эти описания используются для автоматической генерации транспортного кода компонентов решения, а также исходного кода модуля безопасности и инициализирующей программы. Также формальные спецификации компонентов решения используются как исходные данные для описания политики безопасности решения.
У ядра KasperskyOS так же, как и у компонентов решения, есть формальная спецификация (подробнее см. "Методы служб ядра KasperskyOS").
Каждый компонент решения соответствует EDL-описанию. С точки зрения формальной спецификации компонент решения – это контейнер компонентов, предоставляющих службы. Одновременно может использоваться несколько экземпляров одного компонента решения, то есть из одного исполняемого файла может быть запущено несколько процессов. Процессы, которые соответствуют одному и тому же EDL-описанию, являются процессами одного класса. EDL-описание задает имя класса процессов и компоненты, для которых процесс заданного класса является контейнером.
Каждый компонент из состава компонента решения соответствует CDL-описанию. Это описание задает имя компонента, предоставляемые службы, интерфейс безопасности, а также вложенные компоненты. Компоненты могут одновременно предоставлять службы, поддерживать интерфейс безопасности и являться контейнерами для других компонентов. Каждый компонент может предоставлять несколько служб с одним или несколькими интерфейсами.
Каждый интерфейс определяется в IDL-описании. Это описание задает имя интерфейса, сигнатуры интерфейсных методов и типы данных для параметров интерфейсных методов. Данные, которые состоят из сигнатур интерфейсных методов и определений типов данных для параметров интерфейсных методов, называются пакетом.
Процессы, которые не содержат компонентов, могут быть только клиентами. Процессы, содержащие компоненты, могут быть серверами и/или клиентами. Если компоненты из состава процесса предоставляют службы, то процесс может быть сервером, но и одновременно может быть клиентом. Если компоненты из состава процесса не предоставляют службы (только поддерживают интерфейс безопасности), то процесс может быть только клиентом.
Формальная спецификация компонента решения не определяет, как будет реализован этот компонент. То есть наличие компонентов в формальной спецификации компонента решения не означает, что эти компоненты будут присутствовать в архитектуре этого компонента решения.