Автоперевод C в Rust испытают на AppArmor и snap-confine

Canonical финансирует исследователей Университета Бристоля, которые проверят автоматический перевод C в Rust на двух компонентах, отвечающих за изоляцию приложений в Linux: AppArmor и snap-confine. Цель эксперимента: выяснить, какие доказательства нужны сопровождающим, прежде чем доверить автоматическому переводу код, работающий в продакшене, сообщает The New Stack.

Коротко

• Языковые модели генерируют Rust, после чего система верификации сравнивает его с исходным C: фаззинг работает вместе с формальным анализом программ и ищет расхождения, которые обычные тесты пропускают.
• Если поведение двух реализаций расходится, symbolic repair, символьное восстановление, диагностирует конкретную причину сбоя и правит сгенерированный код напрямую, без ручного разбора со стороны сопровождающих проекта.
• Перевод, опирающийся на блоки unsafe, переносит в Rust те же риски работы с памятью, поэтому цель эксперимента: код, который остаётся безопасным и совпадает с оригиналом по поведению.

Узкое место автоматического перевода давно не в генерации кода. Написать Rust по мотивам C модель способна в любом объёме, и главный вопрос выглядит иначе: чем сопровождающий подтвердит, что новый код делает ровно то же, что и старый. Выбор AppArmor и snap-confine в качестве полигона читается как попытка сразу взять худший случай, где ошибка интерпретации политики превращается в дыру в защите, а не в падение процесса.

Сгенерированный Rust компилируется чисто и всё равно расходится с C по поведению

Canonical предлагает схему, в которой языковые модели пишут Rust, а затем результат проходит через процесс верификации, рассчитанный на поиск и устранение расхождений в поведении. Код, сгенерированный таким образом, собирается без ошибок и при этом ведёт себя иначе, чем исходный код на C.

Для сравнения двух реализаций исследователи Университета Бристоля соединяют фаззинг с формальным анализом программ: связка рассчитана на различия, которые обычные тесты не показывают. Когда система фиксирует несовпадение, включается symbolic repair: механизм определяет точную причину сбоя и вносит правку в сгенерированный код напрямую.

Canonical формулирует задачу как выяснение того, какие доказательства понадобятся сопровождающим, прежде чем они согласятся принять автоматический перевод боевого кода. Переписывать AppArmor или snap-confine на Rust в компании пока не планируют, эксперимент нужен для проверки самого подхода к переводу, а замена существующих реализаций в планы не входит.

Обвязка AppArmor написана на смеси C, Python и C++

AppArmor и snap-confine решают критичные для безопасности задачи. AppArmor это модуль безопасности Linux, который ограничивает доступ приложений к ресурсам по заданным политикам. Окружающая его пользовательская обвязка написана на смеси C, Python и C++ и должна корректно разбирать, компилировать и загружать эти политики.

Порт на Rust, который интерпретирует политику иначе, чем существующая реализация, скомпилируется без единого замечания и всё равно окажется неверным. В проекте выбор AppArmor объясняют именно этим: ошибки перевода здесь дают последствия для безопасности. Код, проходящий все тесты, способен сломать работу системы способом, которого никто не предусмотрел.

snap-confine отвечает за подготовку среды исполнения и изоляции, в которой запускаются snap-пакеты. Перевод C в Rust снимает целые классы уязвимостей, включая use-after-free и переполнение буфера, но автоматический переводчик способен внести логическую ошибку, и команде из Бристоля предстоит показать, что результат ведёт себя как исходный C.

Опора на unsafe возвращает в Rust прежние ошибки работы с памятью

Блоки unsafe в Rust разрешают операции, недоступные в безопасном подмножестве языка, в том числе часть манипуляций с сырыми указателями. Автоматический переводчик может использовать их, чтобы перенести сложные конструкции C в Rust, но слишком частое обращение к unsafe тянет за собой исходные риски работы с памятью.

Полная отдача от Rust обычно требует большего, чем построчный перевод синтаксиса C. Идиоматичный код предполагает изменение структур данных и времён жизни сразу в нескольких функциях или целых модулях, и обратная связь от системы верификации нужна для того, чтобы удержать перевод в безопасном подмножестве. Целевой результат сформулирован как Rust, который достаточно безопасен, чтобы дать преимущества языка, и достаточно близок к исходному C по поведению, чтобы сопровождающие могли на него положиться.

Операционные системы, библиотеки и инфраструктурный софт, собранные за десятилетия, по-прежнему написаны на C, и значительная часть этого кода активно сопровождается и работает в продакшене. Ручное переписывание потребовало бы огромного объёма инженерной работы и могло бы привести к регрессиям в работающем коде.

Проверка на сотнях тысяч строк

Canonical финансирует работу бристольской группы, чтобы выяснить, масштабируется ли подход на целые репозитории в сотни тысяч строк C. Сроков эксперимента, критериев приёмки и даты, к которой результаты могли бы повлиять на разработку AppArmor или snap-confine, в описании проекта не приводится. Решение о переписывании обоих компонентов на Rust не принято.