Автоматизированная верификация протоколов безопасного обмена сообщениями и их реализаций: символический и вычислительный подход

Многие популярные веб-приложения включают протоколы безопасного обмена сообщениями «конец‑в‑конец», которые стремятся обеспечить конфиденциальность и аутентичность сообщений между пользователями, даже если серверы веб‑приложения скомпрометированы или вынуждены раскрыть все свои данные. Протоколы, обещающие такие сильные гарантии безопасности, должны подвергаться строгому анализу, поскольку ошибки в протоколе и баги в реализации могут легко привести к реальным атакам. Мы предлагаем новую методологию, которая позволяет разработчикам протоколов, реализацию и аналитикам по безопасности совместно верифицировать протокол с помощью автоматизированных инструментов. Протокол реализован на ProScript, новом предметно‑ориентированном языке, предназначенном для написания кода криптографических протоколов, который может выполняться в программах на JavaScript и автоматически переводиться в читаемую модель в прикладном пии‑исчислении (applied pi calculus). Эта модель затем может быть проанализирована символически с помощью ProVerif для поиска атак в различных моделях угроз. Модель также может служить основой для вычислительного доказательства с использованием CryptoVerif, которое сводит безопасность протокола к стандартным криптографическим предположениям. Если ProVerif обнаруживает атаку или доказательство CryptoVerif выявляет слабость, разработчик протокола изменяет код ProScript и регенерирует модель для новой аналитики. Мы демонстрируем нашу методологию, реализовав и проанализировав вариант популярного протокола Signal с незначительными отличиями. Мы используем ProVerif и CryptoVerif для обнаружения новых и ранее известных слабостей в протоколе и предлагаем практические меры защиты. Наш код протокола на ProScript включён в текущий релиз Cryptocat, настольного защищённого мессенджера, написанного на JavaScript. Наши результаты показывают, что при дисциплинированном программировании и наличии некоторой экспертизы в верификации систематический анализ сложных криптографических веб‑приложений становится практически осуществимым.