Разработчик-исследователь (группа формальных методов) KasperskyOS

О проекте

KasperskyOS – защищенная микроядерная операционная система. Это не очередной дистрибутив Linux, а собственная разработка, способная успешно конкурировать на международных рынках. Заложенный в KasperskyOS принцип кибериммунности позволяет разрабатывать безопасные решения из потенциально небезопасных компонентов.
 

Об отделе

Разработкой KasperskyOS занимается отдел Secure Platform Development (SPD), состоящий из нескольких групп, которые отвечают за микроядро ОС, драйверы, системные компоненты, подсистему безопасности, средства виртуализации, а также обеспечивают непрерывный контроль качества разработки. Сейчас у команды много новых, интересных и сложных задач, так что она продолжает расти.
 

О группе

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

Задачи

• Анализ требований к KasperskyOS и её компонентам;
• Разработка моделей, формализация требований, проверка совместимости требований (непротиворечивость);
• Разработка и валидация спецификаций;
• Разработка методов и инструментов обеспечения выполнения спецификаций в коде.
   

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

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

Желательно

• Знакомство с методами model-checking/model-finding;
• Знакомство с функциональными алгоритмами и структурами данных;
• Знание теорий языков программирования;
• Знания матлогики, темпоральных логик;
• Знание теоретических основ операционных систем;
• Знакомство с основными критериями безопасных систем (Common Criteria, Orange Book, ГОСТ);
• Опыт использования инструментов model checking/model-finding;
• Опыт работы с требованиями и спецификациями;
• Опыт разработки формальных моделей;
• Опыт использования инструментов theorem proving (agda, coq, event-b, Isabelle/HOL, и др);
• Опыт дедуктивной верификации программ (Frama-C, Ada/SPARK).