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

Местоположение и тип занятости

МоскваПолный рабочий день

Компания

Разработка программного обеспечения

Описание вакансии

Условия работы

Группа компаний 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 минутах ходьбы от станции метро Нагатинская;
  • заработная плата по договорённости.