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

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

Москва, Санкт-Петербург, ИннополисПолный рабочий день

Компания

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

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

О компании и команде

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

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

Ожидания от кандидата

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

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

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

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

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

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

Что мы предлагаем:

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