Создание специализированных UEFI-прошивок 

  • Добавление Measured Boot с привлечением TPM для запуска операционных систем на базе Linux и других.
  • Исследование и применение Intel Boot Guard и иных методов обеспечения корня доверия к платформе.
  • Добавление защиты от DMA атак на ранних стадиях запуска прошивки UEFI и расширение профилей DMAR для изоляции устройств.
  • Классификация и создание профилей доступа к подключаемым устройствам.
  • Использование WIM-образов для проверки целостности и запуска изолированных базовых образов с Windows.
  • Добавление LLVM Sanitizers (ASan, MSan, UBSan) в UEFI код на базе EDK II.
  • Расширение возможностей статического анализа кода UEFI и написание моделей функций для лучшего выявления ошибок, включая Taint-анализ.
  • Создание минимального образа операционной системы для конфигурирования возможностей UEFI-прошивки.
  • Разработка и исследование безопасности драйверов файловых систем для EDK II: BTRFS, EXT4, ExFAT и др.
  • Добавление поддержки нового формата исполняемых файлов в прошивке UEFI на базе EDK II.

Низкоуровневые компоненты встраиваемых ОС

  • Разработка кода начальной загрузки платформы (bare metal firmware/loader) для встраиваемых систем с построением корня доверия (главным образом для платформ на базе ARM, PowerPC и RISC-V).
  • Разработка модулей поддержки платформы (PSP/ASP/BSP) на базе архитектур RISC-V, SPARC, AArch64 и PowerPC64.
  • Расширение списка поддерживаемых платформ на ARM, таких как одноплатные компьютеры общего назначения, и более глубокая их интеграция.
  • Добавление поддержки BSP на базе CHERI (Capability Hardware Enhanced RISC Instructions).
  • Реализация криптостойкого генератора случайных чисел для встраиваемых систем на различных платформах.
  • Добавление поддержки внешнего контроллера кэшей на ARMv7, а также других механизмов кэширования на различных архитектурах.
  • Написания драйверов для эффективной работы с различными видами флеш-памяти и проектирование интерфейсов к ним.
  • Обеспечение лучшей изоляции процессов при переключении задач посредством гибкой конфигурации механизмов кэширования на процессоре.
  • Реализация гипервизора для аппаратного разделения доступа между параллельно запущенными операционными системами на одном устройстве для различных архитектур.
  • Разработка детерминированной реализации Thread Local Storage для разных архитектур.
  • Реализация стековых канареек и других механизмов контроля потока управления программного кода на различных платформах.

Архитектурно-независимые компоненты встраиваемых ОС

  • Разработка минимальной верифицируемой библиотеки встроенных функций компилятора (compiler builtins) и её оптимизация для разных архитектур.
  • Разработка интегрируемого модуля извлечения данных и конфигурации из работающей программы в пользовательском пространстве на лету с целью последующего её обновления с переиспользованием исходного состояния.
  • Разработка концепции обеспечения встроенного диагностирования корректной работы ОСРВ и оборудования (BITE, BIST) на разных этапах функционирования.
  • Реализация и оптимизация компонентов стандартной библиотеки языка C 2018 года и их последующее тестирование и верификация:
    • печать чисел с плавающей точкой с гарантированной точностью;
    • оптимизация libm по точности и под целевые платформы;
    • интеграция аллокаторов памяти с различными стратегиями и их интеграция с LLVM Sanitizers;
    • расширение поддержки POSIX и BSD расширений.
  • Расширение языковой поддержки ADA/SPARK, С++, Modula 2, Rust и др.
  • Интерактивный монитор для контроля состояния операционной системы и выполнения операций управления в отладочном режиме.
  • Реализация файловой системы как хранилища данных в отладочном режиме с прозрачным обновлением, например, через сетевой стек.
  • Создание конфигурируемого монитора состояний для обработки пользовательских ошибок с большей гранулярностью, чем классический монитор состояний ARINC 653.

Инструментарий для работы со встраиваемыми ОС

  • Расширение возможностей встроенного ассемблера компиляторов clang и gcc для поддержки новых инструкций или вариаций кодирования существующих инструкций.
  • Добавление поддержки PowerPC SPE в компилятор gcc и последующая интеграция с upstream.
  • Добавление поддержки механизмов обхода errata в процессорах MIPS на уровне компилятора и их интеграция в upstream для gcc и clang.
  • Расширение конфигураций gcc для лучшей поддержки bare-metal платформ (targets) на базе AArch64, PowerPC64 и других.
  • Обеспечение детерминизма эмуляции в QEMU.
  • Автоматическое и полуавтоматическое вычисление времени наихудшего выполнения кода.
  • Адаптация инструмента вычисления размера стека в наихудшем случае (WCSU) для работы с бинарными компонентами и при использовании кода с неявной передачей управления.
  • Анализ времени работы в худшем случае (WCET) с учётом кэширования, периферийных устройств и независимо работающих ОС на различных ядрах.
  • Выявление недетерминированного поведения при эмуляции целевой платформы с помощью QEMU и иных инструментов и их устранению с целью обеспечения воспроизводимых результатов, в том числе при использовании многоядерного ПО (AMP и SMP).
  • Разработка сервера преобразования данных с последовательного порта (UART/COM) в TCP/IP.
  • Создание средств автоматического развёртывания окружения разработчика на инструментальной машине по декларативному описанию. Потенциально также создание полноценного образа виртуальной машины с необходимым окружением в автоматическом виде.
  • Создание инструмента для автоматизации проведения инспекций кода для непроверяемых через тестирование сценариев.
  • Улучшение интеграции с gdbserver на JTAG устройствах и в эмуляторах: поддержка inferior, получение класса памяти по его адресу в условиях статической конфигурацией памяти.

Тестирование и верификация встраиваемых ОС

  • Адаптация инструментов автоматической верификации для специализированных операционных систем.
  • Создание инструмента поиска потенциально проблемных мест в конфигурации интеграционного проекта ARINC 653.
  • Добавление поддержки фаззинга различных компонентов операционной системы: системных вызовов, сетевых драйверов и других компонентов, в том числе с привлечением символьного выполнения.
  • Разработка методики тестирования и реализация тестового набора для интерфейса файловых систем ARINC 653 Part II с поиском узких мест производительности.
  • Добавление поддержки инструментов поиска гонок во встраиваемых системах на базе ThreadSanitizer в ядре и пользовательском режиме.
  • Добавление поддержки инструментов поиска обращений к неинициализированной памяти во встраиваемых системах на базе MemorySanitizer в ядре.
  • Формализация требований стандарта на кодирование и проведение статического анализа на их соответствие с помощью различных инструментов, включая libTooling и Clang, а также дальнейший автоматический рефакторинг кодовых баз.
  • Расширение возможностей механизмов сбора покрытия. Оптимизация передачи данных по собранному покрытию. Реализация сбора покрытия по MC/DC и другим техникам.
  • Моделирование поведения кода операционной системы в функциях на ассемблере или на стыке уровней привилегий процессора для улучшения эффективности статического анализа.
  • Кодогенерация встроенных проверок через assert и средства LLVM Sanitizers на основе требований, написанных на полуформальном языке.
  • Сбор трасс выполнения кода по моделям для применения в статических анализаторах.
  • Проектирование архитектуры и тестирование сетевого стека нижнего уровня для AFDX сетей в ARINC-совместимой ОСРВ на примере DPAA/DTSEC и GRETH.
  • Разработка CI для оптимизации процесса тестирования встраиваемых систем через распараллеливание и оркестрацию. Агрегация аналитики и выгрузка артефактов в условиях множества тестовых наборов и ограниченного количества оборудования для проведения тестирования. Организация пула доступных аппаратных платформ для тестирования. Обеспечение идентификации задач на уникальность при запуске на оборудовании.

Обеспечение безопасности ядра Linux

  • Unit-тестирование отдельных подсистем.
  • Тестирование на основе моделей.
  • Фаззинг системных вызовов, протоколов, драйверов, отдельных “библиотечных” компонентов, в том числе с написанием грамматик.
  • Написание полносистемных тестов для проверки конформности реализации стандарта POSIX и других.
  • Статический анализ с написанием моделей.
  • Разработка средств автоматической верификации отдельных компонентов.

К.ф.-м.н. Алексей Хорошилов