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