Разработчик Haskell (группа подсистемы безопасности, команда разработки KasperskyOS)

компания "лаборатория касперского" о проекте kasperskyos – защищенная микроядерная операционная система. это не очередной дистрибутив linux, а собственная разработка, способная успешно конкурировать на международных рынках. заложенный в kasperskyos принцип кибериммунности позволяет разрабатывать безопасные решения из потенциально небезопасных компонентов. об отделе разработкой kasperskyos занимается отдел secure platform development (spd), состоящий из нескольких групп, которые отвечают за микроядро ос, драйверы, системные компоненты, подсистему безопасности, средства виртуализации, а также обеспечивают непрерывный контроль качества разработки. сейчас у команды много новых, интересных и сложных задач, так что она продолжает расти. о группе группа разработки подсистемы безопасности занимается разработкой принципов обеспечения безопасности kasperskyos, имплементацией моделей безопасности, развитием языка описания политик и компилятора для этого языка. группа также отвечает за создание конфигураций безопасности для проектов на базе kasperskyos. задачи разработка ядра подсистемы безопасности; разработка языков описания систем и инструментариев для них (анализаторы, компиляторы); исследование существующих и разработка новых моделей безопасности; прототипирование/имплементация моделей безопасности; разработка конфигураций безопасности. что требуется от кандидата отличное знание языка программирования haskell; отличное знание языка программирования c; отличное знание функциональных алгоритмов и структур данных; отличное знание классических алгоритмов и структур данных; умение писать надёжный и безопасный correct by construction код; знание подходов к тестированию написанного кода и опыт их практического применения; умение работать в команде; навыки работы с системами контроля версий, управления задачами, code review; знание английского языка на уровне чтения технической документации. желательно знание теории языков программирования; знание теоретических основ информационной безопасности; знание моделей контроля доступа (bell-lapadula, biba, te, rbac, ocap); знание теоретических основ операционных систем; знакомство с основными критериями безопасных систем (common criteria, orange book, гост); опыт использования инструментов model checking (tla+, mcrl2, alloy) опыт использования инструментов theorem proving (agda, coq, event-b); опыт разработки кроссплатформенных приложений.