Баг borrow checker в Rust: что на самом деле значит soundness

Система типов Rust должна давать твёрдое обещание: если безопасный код компилируется, в нём не может быть висящих указателей, гонок данных или use-after-free. Поэтому, когда в issue на GitHub показали фрагмент совершенно безопасного на вид Rust, который печатает мусор из уже умершего кадра стека, и выяснилось, что дыра одиннадцать лет пряталась в borrow checker, многим стало не по себе. Баг позволяет требованиям ко времени жизни структуры проскочить через ковариантное присваивание поля, а с вредоносной реализацией Drop можно спрятать ссылку на локальную переменную в глобальной области и прочитать её уже после того, как переменная исчезла. AddressSanitizer называет это stack-use-after-scope. Компилятор же считал, что всё в порядке.

Реакции были предсказуемыми. Одни объявили, что безопасность Rust мертва. Другие пожали плечами: баги случаются. Оба подхода упускают главное. Эта история — чистый естественный эксперимент: сколько на самом деле стоят статические гарантии, где неформальные рассуждения ломаются и почему именно в зазоре между «система типов корректна» и «компилятор реально обеспечивает корректную систему типов» живут самые интересные баги. Поэтому давайте возьмём распространённые представления, которые поднял этот случай, и проверим каждое.

Миф 1: баг с unsoundness означает, что модель безопасности Rust провалилась

Первый порыв — считать это трещиной в теории. Это не так. Никто не переписывал правила времён жизни. Никто не обнаружил, что владение и заимствование принципиально сломаны. Система типов Rust, как её задумывали на доске и в RFC, требует отклонить эту программу. Компилятор просто не смог её отклонить.

Разница между спецификацией и реализацией — один из самых старых разломов в нашей области. Тони Хоар подарил нам красивую теорию взаимодействующих последовательных процессов; а десятилетиями C-компиляторы неправильно компилировали код, который по стандарту был полностью корректным. Теория держится, а артефакт протекает. Мы уже писали о том, что разрыв между спецификацией и реализацией — место, где живут баги, и этот случай — хрестоматийный пример. Правила времён жизни не были ошибочными. В коде вывода вариантности в rustc — части, которая решает, когда законно подставить &'a T туда, где ожидается &'static T, — была дыра: присваивание шло через ковариантное поле.

Вот упрощённая схема эксплойта. Вы создаёте обёртку, реализация Drop которой копирует полезную нагрузку в глобальное хранилище 'static. Обычно компилятор требует, чтобы полезная нагрузка была 'static, поэтому ссылки на локальные переменные туда не попадают. Баг позволяет «отмыть» ссылку с коротким временем жизни через ковариантное присваивание, и в итоге обёртка хранит &l, где l — локальная String:

struct Q<T: 'static + Send>(Option<T>);
impl<T: 'static + Send> Drop for Q<T> {
fn drop(&mut self) {
if let Some(t) = self.0.take() {
KEPT.lock().unwrap().push(Box::new(t)); // escapes to 'static!
}
}
}
fn main() {
{
let l = String::from("hello world, this is long enough");
let mut q = Q(None);
q.0 = Some(&l); // should be rejected; 'static required
} // <- drop runs here, stashing &l in KEPT
// l is gone; KEPT now holds a dangling &'static String
}

Каждая отдельная строка выглядит безобидно. Unsoundness существует только в композиции: ковариантное поле, присваивание, которое ослабляет границу времени жизни, и Drop, который переносит полезную нагрузку туда, где она переживёт свой референт. Это типичная сигнатура багов реализации в проверяющих системах: инвариант глобальный, а применяется он локально, и один путь выполнения забыли проверить.

Так что нет, модель безопасности не провалилась. Провалилось её применение. Это меньшая неудача, но, как мы увидим, далеко не тривиальная.

Миф 2: если одиннадцать лет баг никто не замечал, значит он безвреден

Собственная логика команды Rust по приоритетам была примерно такой: это было бы P-critical, если бы на него наступали люди, но одиннадцать лет без единого случая означают, что вызвать его непросто, так что это P-high. В этом есть доля правды. Чтобы реально нарушить безопасность памяти, нужна намеренно гадкая реализация Drop, которая переносит данные в место 'static. Почти никто такого не пишет. Поверхность случайной утечки крошечная.

Но «редко срабатывает случайно» тут делает много работы. Гарантии безопасности нужны не только для случайностей — они нужны, чтобы на что-то опираться, когда окружающий код недружелюбен. Вся суть корректной системы типов в том, что можно рассуждать модульно: мне не нужно проверять вашу реализацию Drop, потому что компилятор уже доказал, что определённые плохие композиции невыразимы. Как только появляется дыра, эта модульность пропадает. Вредоносная зависимость — или тонко ошибочная, но написанная с добрыми намерениями — теперь может сделать то, что язык обещал невозможным.

История полна багов, которые считались «неэксплуатируемыми», пока не появился нужный гаджет. Практический вопрос, как написал один из комментаторов, — сломает ли исправление какой-нибудь реальный крейт в экосистеме; и ответ, вероятно, «очень мало или ничего», а это хорошая новость. Но правильный вывод из одиннадцати тихих лет — не «баг был безвредным». Вывод в том, что отсутствие доказательств — не доказательство отсутствия, особенно для сбоев, которые требуют намерения, а не случайности.

Миф 3: достаточно много глаз — и все баги окажутся поверхностными

Это миф, которому нам должно быть стыдно больше всего. rustc — один из самых тщательно проверяемых компиляторов из когда-либо написанных. Он открыт, у него есть выделенная команда по типам, активное академическое сообщество (RustBelt несколько лет назад дал нам формальную модель ядра Rust) и миллионы пользователей, которые ежедневно его тестируют. И всё же дыра в unsoundness просидела в выводе времён жизни больше десяти лет, сквозь полную переработку окружающего механизма.

Закон Линуса предполагает, что глаза смотрят в нужное место и с нужной моделью в голове. Unsoundness в системе типов подрывает оба предположения. Они живут на пересечении нескольких фич — вариантности, порядка уничтожения, приведения, ограничений трейтов, — и каждая фича локально корректна. Рецензенты читают код и видят задуманный инвариант, потому что код писали люди, которые тоже видели именно этот инвариант. Предвзятость подтверждения встроена в сам процесс. Контрпример требует мышления противника, а адверсарное мышление о собственных абстракциях по-настоящему трудно.

Есть целый сайт, counterexamples.org, где собраны способы, которыми правдоподобно выглядящие правила типов ломаются, и общая нить — изменяемость в сочетании с чем-то ещё хитрым, как раз такая форма, как у этого бага. Это не новые уроки. В системе типов ML была известная unsoundness вокруг изменяемых ссылок и полиморфизма, которую исправили ограничением значений (value restriction). Массивы в Java ковариантны и могут бросить ArrayStoreException во время выполнения, потому что разработчики языка выбрали удобство вместо корректности. Сколько бы всё ни менялось, одни и те же три фичи — подтипизация, мутация и обобщения — снова и снова сходятся, чтобы кого-нибудь укусить. Если вам нравится такая археология, шестидесятилетняя история Лиспа показывает, как долго эти идеи развиваются, а старые правила Роба Пайка о простоте читаются иначе, когда понимаешь, что именно сложность порождает дыры в корректности.

Глаза помогают. Но этого недостаточно. Честная позиция — та, что я слышал от человека, который создаёт собственный язык, — примерно такая: никакой объём ревью не решит все проблемы, поэтому нужны механические методы, которые не устают и не разделяют ваших допущений.

Миф 4: неформальные рассуждения — это по сути доказательство

Когда правила времён жизни в Rust проектировали, их тщательно обсуждали умные люди, с кучей примеров. Это и есть неформальные рассуждения, именно так строятся практически все продакшен-компиляторы. Результат — система, которая корректна насколько кому-либо известно, а это, как мы теперь уже дважды убедились, не то же самое, что корректна.

Разрыв между ними — там, где работают RustBelt и текущая работа над трейт-солвером нового поколения. RustBelt, написанный на Coq (ныне Rocq) поверх фреймворка разделяющей логики Iris, машинно проверил модель основных правил типизации Rust, включая страшные вещи вроде границ абстракций unsafe. Это было знаковым событием. Но обратите внимание, что именно он доказал: модель Rust, а не rustc. Доказательство охватывает исчисление λRust, а продакшен-компилятор тем временем дрейфовал, обрастал фичами и накапливал решения по реализации, которые никто не перепроверял. Эта проблема — счёт за такой дрейф.

Формализовать целиком продакшен-компилятор чудовищно дорого. CompCert, формально верифицированный компилятор C, потребовал многих лет работы экспертов для языка, несравнимо меньшего Rust, и он верифицирует проходы компиляции, а не доказывает, что исходная система типов ловит все плохие программы. Никто не станет писать доказательство в Coq для двух миллионов строк rustc. Реалистичный путь больше похож на эшелонированную защиту:

• Машинно проверенные модели базовых правил (в духе RustBelt), чтобы у самой теории не было дыр.
• Систематический фаззинг и инструменты перебора случаев, которые генерируют враждебные программы — углы взаимодействия фич, которые люди не догадываются проверить.
• Мутационное и property-based тестирование самого проверяющего кода: если переворот границы должен ломать программу, проверьте, что она действительно ломается. Культура тестирования SQLite здесь — образец.
• Поддерживаемый список известных проблем с unsoundness — у Rust их больше сотни с меткой — который ведётся как бэклог с инженерным приоритетом, а не как народное предание.

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

Миф 5: если корректность не абсолютна, статическая безопасность — развод

Циничное прочтение такое: Rust обещал безопасность, в обещании нашлась лазейка, значит, обещание было маркетингом и можно вернуться к тому, чтобы свободно писать указатели на C. Это ровно наоборот, и стоит объяснить почему, с некоторой точностью.

Корректность системы типов — теорема о математическом объекте. То, что даёт продакшен-язык, — это статистическая и экономическая гарантия: целые классы багов — use-after-free, гонки данных, инвалидация итераторов — переходят из категории «постоянного фонового шума кодовой базы» в категорию «событий, достаточно редких, чтобы попасть на главную, когда их находят спустя одиннадцать лет». Сравните базовые показатели. Баги безопасности памяти в больших кодовых базах на C и C++ год за годом составляют большинство серьёзных CVE, и никого уже не удивляет любой отдельный случай. Баги unsoundness в Rust настолько редки, что каждый получает собственный issue на GitHub, собственную ветку обсуждения и собственную культуру постмортемов. Редкость, которую можно перечислить, — это совсем другой мир, чем редкость, которую перечислить нельзя.

Есть и разница в том, как сбои накапливаются. В C каждая строка — потенциальная опасность для безопасности памяти, поэтому стоимость бдительности растёт вместе с размером кода навсегда. В Rust бдительность сосредоточена на границах: блоки unsafe, FFI и (как мы теперь знаем) собственный проверяющий компилятора. Эта концентрация и делает аудит, инструменты вроде Miri и формальные методы вообще посильными. Гарантия не бинарна; это радикальное перераспределение того, где живёт ваш риск.

Система типов с известным багом, который одиннадцать лет продакшен-нагрузки так и не задела, всё равно бесконечно сильнее языка, в котором этот баг — часть дизайна.

Что стоит вынести из этой истории

Если вы пишете на Rust, менять ничего не нужно. Ваш код не был тихо небезопасным до того, как завели этот issue; практический путь эксплуатации требовал намерения. Если вы поддерживаете библиотеки, честный ход остаётся прежним: держите поверхность unsafe маленькой, гоняйте Miri на сложных местах и не считайте borrow checker оракулом для чужого вредоносного кода — относитесь к нему как к крайне надёжному инструменту для поимки собственных ошибок.

Если вы создаёте языки или компиляторы, этот баг — подарок: редкий, хорошо задокументированный образец того, как корректность на самом деле ломается в продакшене. Не в теории, а в применении; не в одной фиче, а на пересечении фич; не на ревью, а в результате адверсарной конструкции. Команды, которые относятся к этому всерьёз и финансируют переписывание трейт-солверов, переработку региональных ограничений и инструменты, близкие к верификации, — именно те, чьи гарантии что-то будут значить через десять лет.

И для всех: пересмотрите, что такое гарантия. Десятилетиями мы путали «доказано» с «убедительно аргументировано и пока что ни разу не опровергнуто» — в системах типов, криптографических протоколах и распределённом консенсусе. Взрослое понимание доверия — это не предположение, что мост идеален. Это знание, что у моста есть инспекторы, которые публикуют свои находки, исправляют найденное и ведут публичный список трещин, которые ещё не починили. С этой точки зрения одиннадцать лет на поиск дыры — не обвинение. Это свидетельство того, что система — человеческая система вокруг компилятора — работает примерно так, как и должна.