28 августа в Новосибирском государственном университете состоялась финальная конференция Летнего Системного Буткемпа, организованного при поддержке компании-партнёра YADRO. В течение двух недель студенты работали над проектами в области системной разработки и низкоуровневого программирования, а на заключительной встрече представили результаты своей работы.
Участники объединились в команды по исследовательским интересам и под руководством кураторов решали практические задачи. Среди проектов были разработка операционной системы на языке Rust, работа над воспроизводимой цепочкой сборки компилятора на “чистом железе” , дедуктивная верификация программы и исследование производительности нового процессора на архитектуре RISC-V со специализированными ядрами для работы с нейронными сетями.
Один из проектов был посвящён проблеме доверия к цепочке сборки компилятора (атаке класса Reflecting Trust / Trusting Trust). Участники разрабатывали доверенную минималистичную цепочку (bootstrap toolchain), начинающуюся с обозримого исходного бинарного файла минимального размера. Все последующие стадии сборки развёртывались на основе верифицируемых форматов данных и фиксированных артефактов. Конечная цель команды заключалась в сборке компилятора TCC (Tiny C Compiler), обеспечении полной детерминированности (повторяемости) процесса сборки и его успешном запуске на целевой архитектуре RISC-V.
Ещё одна команда занималась дедуктивной верификацией программы реализации умножения матриц. Участники использовали платформу Frama-C и работали с условиями корректности кода, в том числе с учётом особенностей работы с памятью.
– Необходимость дедуктивной верификации понятна уже десятилетиями. Однако на практике она очень сложна. Поэтому дедуктивная верификация долго не выходила из научных лабораторий и с трудом проникала в практику. И лишь в последнее время появились методы автоматизации, которые позволяют применять ее к практическим задачам.
В этом проекте было очень важно понять, смогут ли студенты за довольно короткий промежуток времени освоить эффективную верификацию и применить ее к реальной программе реализации умножения матрицы. Я считаю очень положительным результатом проекта то, что участники, имея небольшую подготовку, изучили такую сложную область за две недели и при этом полностью успешно завершили верификацию реальной программы умножения матриц, – рассказал куратор проекта Дмитрий Кондратьев.
Участница проекта Алиса рассказала, что в начале буткемпа её команда столкнулась с необходимостью постоянно пересматривать первоначальный подход:
– Я пришла с задачей комплексной верификации умножения матриц с помощью одной из платформ, которой мы пользовались, – Frama-C. Мы смогли доказать эффективность этого подхода. Использовали ассемблерные вставки, создали условия корректности для кода, доказали их с помощью Frama-C и получили результат.
Самым сложным было то, что на протяжении двух недель мы постоянно пересматривали идею: возникали проблемы с Frama-C и с тем, что есть некоторые ограничения в памяти. Поэтому были разные варианты того, как мы можем представить память в коде и как с ней работать. Некоторые идеи не проходили, они были неправильными с точки зрения теории, и в итоге мы пришли к достаточно хорошему решению.
Завершился буткемп вручением участникам памятных подарков от компании YADRO. Для команд интенсив стал возможностью попробовать силы в новой для себя области, поработать над реальными практическими задачами и получить опыт совместной разработки под руководством экспертов.
