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