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

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