Research Developer (Formal Methods Group, KasperskyOS)

Группа формальных методов занимается выполнением проектов по формализации и верификации компонентов KasperskyOS — безопасной микроядерной операционной системы общего назначения. Большой фокус нашей работы направлен на использование легковесных формальных методов, которые позволяют получать полезные результаты за ограниченное количество времени. Группа отвечает за проверку корректности архитектурных решений и участвует в разработке модели безопасности ОС. Мы подбираем методы и инструменты под конкретные задачи, при необходимости используем в работе инструменты интерактивного доказательства теорем, занимаемся верификацией кода, разрабатываем собственные решения. Наша команда работает рамках отдела развития архитектуры KasperskyOS.

Кого ищем:

Мы ищем исследователей, которые могут усилить собственной экспертизой текущие проекты команды, способны выходить за рамки привычного инструментария, а также готовы предлагать и продвигать новые проекты по верификации внутри KasperskyOS.

Задачи:

• Разработка и верификация формальных спецификаций;
• Продвижение использования формальных методов внутри компании;
• Развитие модели безопасности KasperskyOS;
• Предложение и продвижение решений, направленных на повышение надежности и безопасности KasperskyOS;
• Разработка собственных методов и инструментов.

Что требуется от кандидата:

• Опыт разработки и верификации формальных спецификаций;
• Опыт промышленной разработки;
• Навыки работы с системами контроля версий, управления задачами, code review;
• Умение работать в команде;
• Желание развиваться в области разработки надёжного ПО и систем.

Желательно:

• Высшее образование по направлению, связанному с ПО/математикой;
• Опыт использования TLA+, Alloy, Event-B или B;
• Опыт использования инструментов интерактивного доказательства теорем (Isabelle/HOL, Lean, Rocq);
• Опыт дедуктивной верификации программ (Frama-C, Ada/SPARK);
• Опыт работы с требованиями;
• Опыт написания научных статей, выступлений на конференциях;
• Знакомство с методами model-checking/model-finding;
• Знания матлогики, темпоральных логик;
• Знание теоретических основ операционных систем;
• Знание теорий языков программирования;
• Знакомство со стандартами, регламентирующими использование формальных методов (Common Criteria - ISO/IEC 15408, ISO 26262, DO-178C).