Стажер Отдела анализа СЗИ и формальной верификации

Обязанности:

• Разработка формальных спецификаций для подсистемы безопасности ОС Astra Linux.
• Формальная верификация подсистемы безопасности на соответствие модели управления доступом.
• Доказательство свойств формальной модели управления доступом.

Требования:

• Базовая математическая культура.
• Знакомство с логикой Флойда-Хоара.
• Знакомство с Coq (или другим инструментом интерактивного доказательства теорем).
• Знание языка С (для понимания кода системного ПО).
• Опыт работы с ОС семейства Linux.

Будет плюсом:

• Опыт формальной верификации императивного кода, особенно опыт с VST, Iris или Frama-C.
• Знакомство с формальными моделями управления доступом (например, Харрисона-Руззо-Ульмана, Белла-ЛаПадулы, Take-Grant, RBAC, ДП-моделями).

Условия:

• Работа в ведущей IT-компании страны;
• Стажировка оплачивается и длится 6 месяцев;
• В случае успешного прохождения стажировки перспективы дальнейшего трудоустройства.