Формальный анализ CAN XL нашёл семь новых уязвимостей поверх известных проблем классического CAN

Исследователи из Технологического института Джорджии, Университета Пердью и Катарского исследовательского института вычислительной техники провели формальный анализ безопасности MAC-подуровня CAN XL — нового стандарта автомобильных сетей, принятого в мае 2024 года. Работа представлена на 35-м симпозиуме USENIX Security (страницы 2227–2246), о ней сообщил и пресс-релиз института.

Авторы построили бит-точную модель MAC-подуровня CAN XL в проверщике моделей nuXmv и добавили в неё злонамеренный узел, который управляет канальным уровнем в пределах физических ограничений: в SIC-режиме он может менять состояние шины только с 1 на 0, а не выдавать произвольные биты. Проверка свойств P1–P9 показала: CAN XL сохраняет все известные уязвимости MAC-подуровня классического CAN и добавляет семь новых. Найденные дефекты подтвердили на коммерческих контроллерах CAN XL и воспроизвели в двух многоэтапных атаках на стенде, имитирующем трафик автомобиля. Об уязвимостях сообщили Bosch как разработчику стандарта; одна компания уже выпустила исправление.

Что именно позволяет атакующему

Атаки требуют, чтобы злоумышленник уже контролировал один электронный блок управления, подключённый к внутренней сети. Сама работа не показывает, что CAN XL даёт способ проникнуть в автомобиль, — она описывает, что можно сделать после получения доступа.

При отключённой сигнализации ошибок передатчик по спецификации не обнаруживает и не сигнализирует об ошибках от начала кадра до поля AH2 и считает передачу успешной, получив корректное подтверждение. Из этого вырастают две уязвимости. Первая (V1.1) позволяет вбросить ошибку в сообщение и всё равно отправить подтверждение: передатчик считает кадр доставленным, а приёмники его не получают. Вторая (V1.2) даёт перезаписать содержимое кадра, меняя единицы на нули в данных и контрольной сумме так, что CRC остаётся верной, — тогда испорченное сообщение принимают и передатчик, и приёмники.

Рассогласование состояний (V2) возникает из-за того, что при ошибке до подтверждения приёмники уходят в состояние повторного подключения к шине, а передатчик остаётся в обычном режиме. Короткие нулевые импульсы между кадрами, ноль в поле AH2 или в третьем бите паузы удерживают приёмники в этом состоянии, пока передатчик продолжает работу. На этом строятся четыре сценария: картирование идентификаторов узлов, отключение выбранного блока, подмена сообщения и расхождение данных между узлами.

В смешанных сетях, где сосуществуют узлы разных поколений CAN, добавляются V3 и V4: разные типы узлов входят в повторное подключение и выходят из него в разные моменты, поэтому часть узлов может получить поддельный кадр, а часть — настоящий. Уязвимость V5 работает при обеих настройках сигнализации ошибок: поток нулей не даёт узлам набрать 11 подряд идущих единиц, нужных для выхода, и останавливает обмен по шине целиком. Уязвимости V6 и V7 проявляются при включённой сигнализации ошибок и используют новые форматы кадров CAN XL.

Часть атак оказалась быстрее и незаметнее аналогов на классическом CAN: отключение узла занимает примерно длительность одного сообщения плюс 16 бит вместо 255 номинальных битовых интервалов, а картирование идентификаторов зависит только от самого длинного периода сообщения узла, а не от числа передаваемых им идентификаторов.

Авторы предлагают изменить правила CAN XL, чтобы закрыть несколько атак, и дополнить их аутентификацией сообщений и системами обнаружения аномалий. Ограничения работы тоже названы прямо: абстракция CRC и поведения приёмников может давать ложные контрпримеры, сравнение эффективности атак опирается на модель и стенд, а не на парк реальных машин, и CAN XL пока не развёрнут широко в серийных автомобилях.

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