USENIX Security '25 — комплексный формальный анализ безопасности OPC UA

Описание: Комплексный формальный анализ безопасности OPC UA

Винсент Дьемунш, ANSSI и Университет Лотарингии, CNRS, Инрия, ЛОРИЯ, Франция; Лукка Хирши и Стив Кремер, Университет Лотарингии, CNRS, Инрия, ЛОРИЯ, Франция

OPC UA — это стандартизированный протокол промышленной системы управления (ICS), применяемый в критически важных инфраструктурах и направленный на обеспечение безопасности. Предстоящая версия 1.05 включает в себя существенные изменения в базовой криптографической архитектуре, включая обмен ключами на основе протокола Диффи-Хеллмана, в отличие от предыдущей версии на основе RSA. Предполагается, что версия 1.05 обеспечит более высокий уровень безопасности, включая совершенную прямую секретность (PFS). Мы проводим формальный анализ безопасности протоколов безопасности, описанных в OPC UA v1.05 и v1.04, для режимов на основе RSA и нового режима на основе DH, используя современный символьный верификатор протоколов ProVerif. По сравнению с предыдущими исследованиями, наша модель гораздо более полная, включая новую версию протокола, комбинацию различных подпротоколов для установления защищенных каналов, сеансов и управления ими, охватывая широкий спектр возможных конфигураций. В результате получается одна из самых больших моделей, когда-либо исследованных в ProVerif, что вызывает множество проблем, связанных с ее верификацией, главным образом из-за сложности конечного автомата. Мы обсуждаем, как нам удалось снизить эту сложность для получения значимых результатов анализа. Наш анализ выявил несколько новых уязвимостей, о которых OPC Foundation сообщила и которые были признаны. Мы разработали и предложили доказуемо безопасные исправления, большинство из которых включены в следующую версию стандарта.

Полную программу конференции USENIX Security '25 можно посмотреть по адресу https://www.usenix.org/conference/use...