Специалист по защите информации и верификации программного кода
Требования
Местоположение и тип занятости
Компания
Описание вакансии
Условия работы
Мы группа компаний «Астра» – один из лидеров российской 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 минутах ходьбы от станции метро Нагатинская
- Конкурентная заработная плата