Специалист по защите информации и верификации программного кода

Мы группа компаний «Астра» – один из лидеров российской IT-индустрии, ведущий производитель программного обеспечения, в том числе защищенных операционных систем и платформ виртуализации. Разработка флагманского продукта, ОС семейства Astra Linux, ведется с 2008 года. На сегодня в штате компании более 300 высококвалифицированных разработчиков и специалистов технической поддержки.

Наша миссия – обеспечить технологический суверенитет России и ее лидерство в мировой IT-индустрии путем создания базовых технологий, специального и пользовательского ПО. Стратегическая цель – к 2030 году стать национальным производителем программных продуктов №1

Что нужно будет делать:

• Верифицировать с применением соответствующих инструментов исходного кода подсистем безопасности, включая модули ядра, ОС;
• Разрабатывать формальные спецификации для исходного кода анализируемых программных модулей;
• Проверять (доказательство) соответствие реализации подсистем (модулей) безопасности формальной модели управления доступом (политики безопасности).

Что мы ждем от кандидата:

• Высшее математическое или техническое образование (по направлениям математика, информационные технологии, информационная безопасность);
• Знание архитектуры и уверенные навыки работы в ОС семейства Linux;
• Знание C/C++ для понимания кода прикладного и системного ПО;
• Знание формальных моделей управления доступом (например, Харрисона-Руззо-Ульмана, Белла-ЛаПадулы, Take-Grant, RBAC, ДП-моделей);
• Знание методов верификации (дедуктивной, проверки моделей или др.), опыт применения инструментов верификации.

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

• Знание или опыт применения стандартов и иных нормативных документов по разработке безопасного ПО
• Опыт анализа реализации/написания модулей ядра ОС;
• Знание скриптовых языков программирования (например, bash, python и др.);
• Опыт работы с Git;
• Опыт внедрения, развития и оптимизации процессов CI/CD в GitLab;
• Опыт разработки формальных моделей управления доступом в компьютерных системах;
• Знание языка спецификации ACSL, опыт работы с платформой FRAMA-C;
• Опыт разработки плагинов для расширения функциональных возможностей платформы FRAMA-C;
• Знания языка формального метода Event-B, опыт применения инструментов Rodin или ProB;
• Наличие научных статей по направлению верификации формальный моделей и программного кода.

Мы предлагаем:

• Уверенность в будущем. Мы чтим ТК РФ: у нас стабильный и прозрачный «белый» доход и полноценный соцпакет
• Забота о здоровье. Оформим полис ДМС со стоматологией
• Добираться легко. Офис в 2 минутах ходьбы от станции метро Нагатинская
• Конкурентная заработная плата