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

Группа компаний Astra Linux – один из лидеров российской IT-индустрии, ведущий производитель программного обеспечения, в том числе защищенных операционных систем и платформ виртуализации.

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

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

ГК Astra Linux — член ассоциации «Руссофт» и АРПП, обладатель множества дипломов, лауреат национальных и международных премий за уникальные решения в области создания и реализации защищенных информационных систем.

Стратегическая цель — к 2030 году стать национальным производителем программных продуктов No1, обеспечивающим, с одной стороны, потребности рынка IT в специализированных и общих решениях и, с другой стороны, формирующим единые стандарты этого рынка в Российской Федерации.

Мы амбициозны, мы постоянно поднимаем планку для себя и для всего рынка, завышаем планы и перевыполняем их! Если ваша жизненная позиция совпадает с нашей — добро пожаловать в команду Astra Linux!

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

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

Требования:

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

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

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

Условия:

• Полная занятость, возможен гибкий график;
• оформление в соответствии с ТК РФ;
• долгосрочные проекты в области разработки системного ПО;
• офис в 2 минутах ходьбы от станции метро Нагатинская;
• заработная плата по договорённости.