Описание

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

• Заработная плата: не указана
• Опыт работы: Нет опыта

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

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

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

• Моделирование политик управления доступом и информационными потоками;

• Верификация формальных моделей управления доступом;

• Разработка формальных спецификаций для исходного кода анализируемых программных модулей;

• Проверка (доказательство) соответствия реализации подсистем (модулей) безопасности формальной модели управления доступом (политики безопасности).

• Высокий уровень математической подготовки;

• Знание формальных моделей управления доступом (например, Харрисона-Руззо-Ульмана, Белла-ЛаПадулы, Take-Grant, RBAC, ДП-моделей);

• Опыт моделирования политик управления доступом в компьютерных системах;
• Знание методов верификации (дедуктивной, проверки моделей или др.);

• Знание архитектуры и уверенные навыки работы с ОС семейства Linux;

• Знание C/C++ для понимания кода прикладного и системного ПО.

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

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

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

Контакты